Proof Methods for Corecursive Programs

Hutton, Graham; Gibbons, Jeremy

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.

Citation

Hutton, G., & Gibbons, J. (2005). Proof Methods for Corecursive Programs

• Journal Article Type: Article
• Publication Date: Apr 1, 2005
• Deposit Date: Nov 7, 2005
• Publicly Available Date: Oct 9, 2007
• Journal: Fundamenta Informaticae Special Issue on Program Transformation
• Publisher: IOS Press
• Peer Reviewed: Peer Reviewed
• Volume: 66
• Issue: 4
• Public URL: https://nottingham-repository.worktribe.com/output/1019970