Loading...
Please wait, while we are loading the content...
Similar Documents
Formalizing a correctness property of a type-directed partial evaluator
| Content Provider | ACM Digital Library |
|---|---|
| Author | Asai, Kenichi Hirota, Noriko |
| Abstract | This paper presents our experience of formalizing Danvy's type-directed partial evaluator (TDPE) for the call-by-name lambda calculus in the proof assistant Coq. Following the previous approach by Coquand and Ilik, we characterize TDPE as a composition of completeness and soundness theorems of typing rules with respect to the semantics. To show the correctness property of TDPE (i.e., TDPE preserves semantics), we further define a logical relation between residualizing and standard semantics, following Filinski. The use of parametric higher-order abstract syntax (PHOAS) leads to a simple formalization without being disturbed by fresh names created during TDPE. Because of the higher-order nature of PHOAS, it also requires us to prove manually a core property that corresponds to the main lemma of logical relations, which appears to be difficult to prove in Coq. |
| Starting Page | 41 |
| Ending Page | 46 |
| Page Count | 6 |
| File Format | |
| ISBN | 9781450325677 |
| DOI | 10.1145/2541568.2541572 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2014-01-11 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Type-directed partial evaluator Parametric higher-order abstract syntax Proof assistant coq |
| Content Type | Text |
| Resource Type | Article |
