A First-Order One-Pass CPS Transformation

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Department of Computer Science
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.
Original languageEnglish
Title of host publicationFoundations of Software Science and Computer Structures : 5th International Conference, FOSSACS 2002 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8–12, 2002 Proceedings
EditorsMogens Nielsen, Uffe Engberg
Number of pages17
Publication year2002
ISBN (print)978-3-540-43366-8
Publication statusPublished - 2002
EventETAPS'02 - Grenoble, France
Duration: 10 Apr 200212 Apr 2002
Conference number: 5


SeriesLecture Notes in Computer Science

    Research areas

  • λ-calculus, Continuations, Continuation-passing style (CPS), Administrative reductions

See relations at Aarhus University Citationformats

ID: 281560