Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Abstract
[go: Go Back, main page]

Formalizing a Correctness Property of a Type-Directed Partial Evaluator

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.