Coinductive Proofs

Coinductive Proofs
 

The goal of this advanced lecture is to give an introduction to the notion of coinductive proofs, an elegant proof technique that finds many applications in Computer Science,
in particular in security and program verification.

Proofs by induction appear everywhere in theoretical computer science; you certainly encountered them on many occasions, starting with the lecture Programming 1.
Another essential proof method, less well-known but equally useful, is coinduction. 
If you're familiar with the notion of simulation proofs (as in the lectures Concurrency and Verification), you have already dealt with a particular instance of proofs by coinduction, maybe without knowing it.

This lecture aims to present a general framework to understand the theory behind both induction and coinduction.
We will see that while induction is a suitable technique for reasoning about finite objects (e.g., data structures), coinduction gives a systematic way to reason about potentially infinite ones (e.g., program executions). This unlocks a lot of potential, in particular, to write proofs about systems and programs that may run indefinitely (e.g., web servers, microprocessors).
We will discuss applications of proofs by coinduction to security and program verification and present several advanced proof techniques that are particularly useful in this context.