Loading...
Please wait, while we are loading the content...
Similar Documents
A coinductive monad for prop-bounded recursion
| Content Provider | ACM Digital Library |
|---|---|
| Author | Megacz, Adam |
| Abstract | This paper develops machinery necessary to mechanically import arbitrary functional programs into Coq's type theory, manually strengthen their specifications with additional proofs, and then mechanicaly re-extracting the newly-certified program in a form which is as efficient as the original program. In order to facilitate this goal, the coinductive technique of[Capretta2005] is modified to form a monad whose operators are the constructors of a coinductive type rather than functions defined over the type. The inductive invariant technique of [Krstic2003] is extended to allow optional "after the fact" termination proofs. These proofs inhabit members of Prop, and therefore do not affect extracted code. Compared to [Capretta2005], the new monad makes it possible to directly represent unrestricted recursion without violating productivity requirements [Gimenez1995], and it produces efficient code via Coq's extraction mechanism. The disadvantages of this technique include reliance on the JMeq axiom [McBride2000] and a significantly more complex notion of equality. The resulting technique is packaged as a Coq library, and is suitable for formalizing programs written in any side-effect-free functional language with call-by-value semantics. It can be downloaded from: http://www.cs.berkeley.edu/~megacz/computation. |
| Starting Page | 11 |
| Ending Page | 20 |
| Page Count | 10 |
| File Format | |
| ISBN | 9781595936776 |
| DOI | 10.1145/1292597.1292601 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2007-10-02 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Type theory Coinductive types |
| Content Type | Text |
| Resource Type | Article |
