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
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.