A First-Order One-Pass CPS Transformation

Olivier Danvy and Lasse R. Nielsen

To appear at Foundations of Software Science and Computation Structures (FOSSACS02), Grenoble, France, 6-14 April, 2002


We present a new transformation of call-by-value lambda-terms into continuation-passing style (CPS). This transformation operates in one pass and is both compositional and first-order. Operating in one pass, it directly yields compact CPS programs that are comparable to what one would write by hand. Being compositional, it allows proofs by structural induction. Being first-order, reasoning about it does not require a logical relation. This new CPS transformation connects two separate lines of research and has already been used to develop a new and simpler CPS transformation of control-flow information.

Server START Conference Manager
Update Time 14 Dec 2001 at 14:02:38
Maintainer fossacs02@brics.dk.
Start Conference Manager
Conference Systems