Certifying CPS Transformation of Let-polymorphic Calculus Using PHOAS
This paper formalizes the correctness of a one-pass CPS transformation
for the lambda calculus extended with let-polymorphism.
We prove in Agda that equality is preserved through the CPS
Parameterized higher-order abstract syntax is used to represent
binders both at the term level and the type level.
Unlike the previous work based on denotational semantics, we use
small-step operational semantics to formalize the equality.
Thanks to the small-step formalization, we can establish the
correctness without any hypothesis on the well-formedness of input
The resulting formalization is simple enough to serve as a basis for
more complex CPS transformations such as selective one for a calculus
with delimited control operators.