@inbook{39b39c5e12c54b349556bc1ac7e29ccc,
title = "A Tutorial on Co-induction and Functional Programming",
abstract = "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{\textquoteright}s Take Lemma, a well-known proof technique for lazy streams.",
author = "Gordon, {Andrew D.}",
year = "1995",
doi = "10.1007/978-1-4471-3573-9_6",
language = "English",
isbn = "978-3-540-19914-4",
series = "Workshops in Computing",
publisher = "Springer",
pages = "78--95",
editor = "Kevin Hammond and Turner, {David N.} and Sansom, {Patrick M.}",
booktitle = "Functional Programming, Glasgow 1994",
address = "United Kingdom",
}