Co-induction is an important tool for reasoning about unbounded structures. This tutorial explains the foundations of co-induction, and shows how it justifies intuitive arguments about lazy streams, of central importance to lazy functional programmers. We explain from first principles a theory based on a new formulation of bisimilarity for functional programs, which coincides exactly with Morris-style contextual equivalence. We show how to prove properties of lazy streams by co-induction and derive Bird and Wadler’s Take Lemma, a well-known proof technique for lazy streams.
|Title of host publication||Functional Programming, Glasgow 1994|
|Subtitle of host publication||Proceedings of the 1994 Glasgow Workshop on Functional Programming, Ayr, Scotland, 12–14 September 1994|
|Editors||Kevin Hammond, David N. Turner, Patrick M. Sansom|
|Place of Publication||London|
|Number of pages||18|
|Publication status||Published - 1995|
|Name||Workshops in Computing|