Reasoning about programs in continuation-passing style

Plotkin's λv-calculus for call-by-value programs is weaker than the λβη-calculus for the same programs in continuation-passing style (CPS). To identify the call-by-value axioms that correspond to βη on CPS terms, we define a new CPS transformation and an inverse mapping, both of which are interesting in their own right. Using the new CPS transformation, we determine the precise language of CPS terms closed under βη-transformations, as well as …