Skip to main content

Research Repository

See what's under the surface

Proof methods for structured corecursive programs

Gibbons, Jeremy; Hutton, Graham

Authors

Jeremy Gibbons



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.

Publication Date Jan 1, 1999
Peer Reviewed Peer Reviewed
APA6 Citation Gibbons, J., & Hutton, G. (1999). Proof methods for structured corecursive programs
Copyright Statement Copyright information regarding this work can be found at the following address: http://eprints.nottingh.../end_user_agreement.pdf
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

Copyright Statement
Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf





You might also like



Downloadable Citations