Sciweavers

Share
CATS
2006

Mechanically Verifying Correctness of CPS Compilation

11 years 1 months ago
Mechanically Verifying Correctness of CPS Compilation
In this paper, we study the formalization of one-pass call-by-value CPS compilation using higher-order abstract syntax. In particular, we verify mechanically that the source program and the CPS-transformed program have the same observable behavior. A key advantage of this approach is that it avoids any administrative redexes thereby simplifying the proofs about CPS-translations. The CPS translation together with its correctness proof is implemented and mechanically verified in the logical framework Twelf.
Ye Henry Tian
Added 30 Oct 2010
Updated 30 Oct 2010
Type Conference
Year 2006
Where CATS
Authors Ye Henry Tian
Comments (0)
books