25 June 2015, FireEye Research & Development Dresden, Germany
On an abstract level, servers and operating systems can be seen as
infinite processes that continuously accept a request and send a
response. While such a process should not terminate, but run
potentially infinitely, each request should terminate with a response.
Mathematically, such behavior can be modeled by coinduction.
In this talk, I introduce coinduction via some examples and show how
to program and reason coinductively in the Agda proof assistant. This
includes a presentation of my research on copatterns and sized types.