We present a new transformation of call-by-value lambdaterms into continuation-passing style (CPS). This transformation operates in one pass and is both compositional and first-order. Because it operates in one pass, it directly yields compact CPS programs that are comparable to what one would write by hand. Because it is compositional, it allows proofs by structural induction. Because it is first-order, reasoning about it does not require the use of a logical relation. This new CPS transformation connects two separate lines of research. 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.
CITATION STYLE
Danvy, O., & Nielsen, L. R. (2002). A first-order one-pass CPS transformation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2303, pp. 98–113). Springer Verlag. https://doi.org/10.1007/3-540-45931-6_8
Mendeley helps you to discover research relevant for your work.