Reasoning about programs in continuation-passing style.

Plotkin's &lgr;-value calculus is sound but incomplete for reasoning about &bgr;eegr;-transformations on programs in continuation-passing style (CPS). To find a complete extension, we define a new, compactifying CPS transformation and an “inverse”mapping, un-CPS, both of which are interesting in their own right. Using the new CPS transformation, we can determine the precise language of CPS terms closed under &bgr;7eegr;-transformations. Using the un-CPS transformation, we can derive a set of axioms such that every equation between source programs is provable if and only if &bgr;&eegr; can prove the corresponding equation between CPS programs. The extended calculus is equivalent to an untyped variant of Moggi's computational &lgr;-calculus.