Sciweavers

APLAS
2001
ACM

Verifying the CPS Transformation in Isabelle/HOL

14 years 3 months ago
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.
Yasuhiko Minamide, Koji Okuma
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2001
Where APLAS
Authors Yasuhiko Minamide, Koji Okuma
Comments (0)