1 Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University2 Department of Computer Science, Science and Technology, Aarhus University3 BRICS, Department of Computer Science, University of Aarhus4 Department of Computer Science, Science and Technology, Aarhus University
We present a new transformation of λ-terms into continuation-passing style (CPS). This transformation operates in one pass and is both compositional and first-order. Previous CPS transformations only enjoyed two out of the three properties of being first-order, one-pass, and compositional, but the new transformation enjoys all three properties. It is proved correct directly by structural induction over source terms instead of indirectly with a colon translation, as in Plotkin's original proof. Similarly, it makes it possible to reason about CPS-transformed terms by structural induction over source terms, directly.The new CPS transformation connects separately published approaches to the CPS transformation. It has already been used to state a new and simpler correctness proof of a direct-style transformation, and to develop a new and simpler CPS transformation of control-flow information.
Theoretical Computer Science, 2003, Vol 308, Issue 1, p. 239-257