Loading...
Date
2012
Abstract
Proofs involving infinite structures can use corecursive functions as inhabitants of a corecursive type. Admissibility of such functions in theorem provers such as Coq or Agda, requires that these functions are productive. Typically this is proved by showing satisfaction of a guardedness condition. The guardedness condition however is extremely restrictive and many programs which are in fact productive and therefore will not compromise soundness are nonetheless rejected. Supercompilation is a family of program transformations which retain program equivalence. Using supercompilation we can take programs whose productivity is suspected and transform them into programs for which guardedness is syntactically apparent.
Supervisor
Description
peer-reviewed
Publisher
META
Citation
Third International Workshop on Metacomputation;
Files
Loading...
Mendelgleson_2012_.pdf
Adobe PDF, 477.98 KB
Keywords
ULRR Identifiers
Funding code
Funding Information
Science Foundation Ireland (SFI)
Sustainable Development Goals
External Link
Type
Meetings and Proceedings
Rights
https://creativecommons.org/licenses/by-nc-sa/1.0/