Verifying CPS transformations in Isabelle/HOL

9 years 11 months ago
Verifying CPS transformations in Isabelle/HOL
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 parameterized 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. Categories and Subject Descriptors D.3.4 [Programming Languages]: Processors--compil
Yasuhiko Minamide, Koji Okuma
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2003
Where ICFP
Authors Yasuhiko Minamide, Koji Okuma
Comments (0)