Reasoning about programs in continuation-passing style.

Abstract

Plotkin's λ-value calculus is sound but incomplete for reasoning about β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 β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 βη can prove the corresponding equation between CPS programs. The extended calculus is equivalent to an untyped variant of Moggi's computational λ-calculus.