Lecture 16: Coinduction.

Proofs by structural induction work well when we reason about finite objects. But they are insufficient when we prove properties about inifinite objects prevalent in lazy languages like Haskell. The solution to this problem lies in talking about the behavior of programs via bisimulations and proofs by coinduction.

Suggested Reading Materials:

Slides by Jan von Eijck.

Previous lecture: Lecture 15
Next lecture: Lecture 17