Proof Methods for Corecursive Programs
Jeremy Gibbons and Graham Hutton
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 four methods for proving properties of corecursive programs: fixpoint induction, the approximation lemma, coinduction, and fusion.
Details
| Journal |
Fundamenta Informaticae |
| Month |
April/May |
| Number |
4 |
| Pages |
353−366 |
| Volume |
66 |
| Year |
2005 |
Links
Related pages
|
People |
|
|
Activities |