A Tutorial on Co-induction and Functional Programming

Research output: Chapter in Book/Report/Conference proceedingChapter


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.
Original languageEnglish
Title of host publicationFunctional Programming, Glasgow 1994
Subtitle of host publicationProceedings of the 1994 Glasgow Workshop on Functional Programming, Ayr, Scotland, 12–14 September 1994
EditorsKevin Hammond, David N. Turner, Patrick M. Sansom
Place of PublicationLondon
PublisherSpringer London
Number of pages18
ISBN (Electronic)978-1-4471-3573-9
ISBN (Print)978-3-540-19914-4
Publication statusPublished - 1995

Publication series

NameWorkshops in Computing
PublisherSpringer London
ISSN (Print)1431-1682


Dive into the research topics of 'A Tutorial on Co-induction and Functional Programming'. Together they form a unique fingerprint.

Cite this