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 the call-by-value axioms that correspond to the so-called administrative βη-reductions on CPS terms. Using the inverse mapping, we map the remaining β and η equalities on CPS terms to axioms on call-by-value terms. On the pure (constant free) set of Λ-terms, the resulting set of axioms is equivalent to Moggi's computational λ-calculus. If the call-by-value language includes the control operatorsabort andcall-with-current-continuation, the axioms are equivalent to an extension of Felleisenet al.'s λv-C-calculus and to the equational subtheory of Talcott's logic IOCC.