Online Version - Last Updated - 20 Jan 2012 |
 |
| Home |
| |
| Procedures and Resources for Authors |
|
| Information and Resources for Volume Editors |
| |
| Orders and Subscriptions |
| |
| Published Articles |
|
| Upcoming Volumes |
| |
| Contact Us |
| |
| Useful External Links |
| |
| CRPIT Site Search |
Mechanically Verifying Correctness of CPS Compilation
Tian, Y.H.
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 veri_ed in the logical framework Twelf.
Cite as: Tian, Y.H. (2006). Mechanically Verifying Correctness of CPS Compilation. In Proc. Twelfth Computing: The Australasian Theory Symposium (CATS2006), Hobart, Australia. CRPIT, 51. Gudmundsson, J. and Jay, B., Eds. ACS. 41-51.
(from crpit.com)
(local if available)
