Proof methods for structured corecursive programs
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....
| Main Authors: | , |
|---|---|
| Format: | Conference or Workshop Item |
| Published: |
1999
|
| Online Access: | https://eprints.nottingham.ac.uk/236/ |
| _version_ | 1848790376132902912 |
|---|---|
| author | Gibbons, Jeremy Hutton, Graham |
| author_facet | Gibbons, Jeremy Hutton, Graham |
| author_sort | Gibbons, Jeremy |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T18:11:38Z |
| format | Conference or Workshop Item |
| id | nottingham-236 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T18:11:38Z |
| publishDate | 1999 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-2362020-05-04T20:33:08Z https://eprints.nottingham.ac.uk/236/ Proof methods for structured corecursive programs Gibbons, Jeremy Hutton, Graham 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. 1999 Conference or Workshop Item PeerReviewed Gibbons, Jeremy and Hutton, Graham (1999) Proof methods for structured corecursive programs. In: 1st Scottish Functional Programming Workshop, 29 Aug - 1 Sept 1999, Stirling, Scotland. |
| spellingShingle | Gibbons, Jeremy Hutton, Graham Proof methods for structured corecursive programs |
| title | Proof methods for structured corecursive programs |
| title_full | Proof methods for structured corecursive programs |
| title_fullStr | Proof methods for structured corecursive programs |
| title_full_unstemmed | Proof methods for structured corecursive programs |
| title_short | Proof methods for structured corecursive programs |
| title_sort | proof methods for structured corecursive programs |
| url | https://eprints.nottingham.ac.uk/236/ |