Continuation Semantics and Self-adjointness
Hayo Thielecke · Electronic Notes in Theoretical Computer Science · 1997
We give an abstract categorical presentation of continuation semantics by taking the continuation type constructor ¬ (or cont in Standard ML of New Jersey) as primitive. This constructor on types extends to a contravariant functor on terms which is adjoint to itself on the left; restricted to the subcategory of those programs that do not manipulate the current continuation, it is adjoint to itself on the right. The motivating example of such a category is built from (equivalence classes of typing judgements for) continuation passing style (CPS) terms. A call-by-value λ-calculus with the control operator callcc as well as a call-by-name λ-calculus can be interpreted. Arrow types are broken down into continuation types for argument/result-continuations pairs. Specialising the semantics to the CPS term model allows a reconstruction of CPS transforms.