Jeremy Gibbons
Proof methods for structured corecursive programs
Gibbons, Jeremy; Hutton, Graham
Abstract
Corecursive programs produce values of greatest fixpoint types, in contrast to recursive programs, which consume values of least fixpoint types. There are a number of widely used methods for proving properties of corecursive programs, including fixpoint induction, the take lemma, and coinduction. However, these methods are all rather low level, in that they do not exploit the common structure that is often present in corecursive definitions. We argue for a more structured approach to proving properties of corecursive programs. In particular, we show that by writing corecursive programs using a simple operator that encapsulates a common pattern of corecursive definition, we can then use high-level algebraic properties of this operator to conduct proofs in a purely calculational style that avoids the use of inductive or coinductive methods.
Citation
Gibbons, J., & Hutton, G. Proof methods for structured corecursive programs. Presented at 1st Scottish Functional Programming Workshop
Conference Name | 1st Scottish Functional Programming Workshop |
---|---|
End Date | Sep 1, 1999 |
Publication Date | Jan 1, 1999 |
Deposit Date | Oct 26, 2005 |
Publicly Available Date | Oct 9, 2007 |
Peer Reviewed | Peer Reviewed |
Public URL | https://nottingham-repository.worktribe.com/output/1023961 |
Additional Information | Papers from the conference were ultimately published in: Trends in functional programming / edited by Greg Michaelson, Phil Trinder and Hans-Wolfgang Loidl. Bristol: Intellect, 2000. |
Files
methods.pdf
(97 Kb)
PDF
You might also like
Calculating Compilers Effectively (Functional Pearl)
(2024)
Presentation / Conference Contribution
Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl)
(2024)
Journal Article
Quotient Haskell: Lightweight Quotient Types for All
(2024)
Journal Article
Programming language semantics: It’s easy as 1,2,3
(2023)
Journal Article
Monadic compiler calculation (functional pearl)
(2022)
Journal Article
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: discovery-access-systems@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2025
Advanced Search