Open AccessA First-Order One-Pass CPS Transformation
Author(s) -
Olivier Danvy,
Lasse R. Nielsen
Publication year - 2001
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v8i49.21709
Subject(s) - transformation (genetics) , correctness , mathematical proof , continuation , computer science , realization (probability) , state (computer science) , order (exchange) , mathematics , calculus (dental) , algebra over a field , programming language , pure mathematics , medicine , biochemistry , chemistry , statistics , geometry , dentistry , gene , finance , economics
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. 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.