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.

• Type: Conference
• Year: 2006
• Where: CATS
• Authors: Ye Henry Tian
• Keywords: CATS 2006, CATS 2007, Logical Framework Twelf, Observable Behavior, One-pass Call-by-value Cps