Proof Methods for Corecursive Programs

Issue title: Program Transformation: Theoretical Foundations and Basic Techniques. Part 1

Article type: Research Article

Authors: Gibbons, Jeremy | Hutton, Graham

Affiliations: Oxford University Computing Laboratory, UK | School of Computer Science and IT University of Nottingham, UK

Note: [] Address for correspondence: Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford OXI 3QD, UK

Abstract: Recursion is a well-known and powerful programming technique, with a wide variety of applications. The dual technique of corecursion is less well-known, but is increasingly proving to be just as useful. This article is a tutorial on the four main methods for proving properties of corecursive programs: fixpoint induction, the approximation (or take) lemma, coinduction, and fusion.

Journal: Fundamenta Informaticae, vol. 66, no. 4, pp. 353-366, 2005