No-Brainer CPS Conversion

Milo Davis (Northeastern University, USA) gives the fourth talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP. Co-written by William Meehan and Olin Shivers (Northeastern University, USA). Algorithms that convert direct-style lambda-calculus terms to their equivalent terms in continuation-passing style (CPS) typically introduce so-called 'administrative redexes' -- useless artifacts of the conversion that must be cleaned up by a subsequent pass over the result to reduce them away. We present a simple, linear-time algorithm for CPS conversion that introduces no administrative redexes. In fact, the output term is a normal form in a reduction system that generalizes the notion of 'administrative redexes' to what we call 'no-brainer redexes,' that is, redexes whose reduction shrinks the size of the term. We state the theorems which establish the algorithm's desireable properties, along with sketches of the full proofs.