Verifying CPS transformations in Isabelle/HOL
Yasuhiko Minamide, Koji Okuma · 2003
We have verified several versions of the CPS transformation in Isabelle/HOL. In our verification we adopted first-order abstract syntax with variable names so that the formalization is close to that of hand-written proofs and compilers. To simplify treatment of fresh variables introduced by the transformation, we introduced abstract syntax parameter-ized with the type of variables. We also found that the standard formalization of α-equivalence was cumbersome for theorem provers and reformulated α-equivalence as a syntax-directed deductive system. To simplify verification of the CPS transformation on the language extended with let-expressions, it was essential to impose that variables are uniquely used in a program.