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.
