Verifying the CPS Transformation in Isabelle/HOL

We verified two versions of the CPS transformation in Isabelle/HOL: one by Plotkin by Danvy and Filinski. We adopted first order abstract syntax 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 introduce parameterized der abstract syntax implemented as a polymorphic datatype. The verification of Danvy and Filinski's transformation requires us to reformulate the transformation in several respects. We also need to consider -equivalence of terms for the verification. To make automatic theorem proving possible to some extent, we reformulate -equivalence as a syntax-directed deductive system.

• Type: Conference
• Year: 2001
• Where: APLAS
• Authors: Yasuhiko Minamide, Koji Okuma
• Keywords: Abstract Syntax, APLAS 2001, CPS Transformation, Order Abstract Syntax, Programming Languages