*Abstract:*

This thesis attempts to make precise the structure inherent in Continuation Passing Style (CPS).

We emphasize that CPS translates lambda-calculus into a very basic calculus that does not have functions as primitive.

We give an abstract categorical presentation of continuation
semantics by taking the continuation type constructor
(`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. The categorical approach suggests a notion of effect-free term as well as some operators for manipulating continuations. We use these for writing programs that illustrate our categorical approach and refute some conjectures about control effects.

A call-by-value lambda-calculus with the control operator
`callcc` can be interpreted. Arrow types are broken down
into continuation types for argument/result-continuations pairs,
reflecting the fact that CPS compiles functions into a special case
of continuations. Variant translations are possible, among them
lazy call-by-name, which can be derived by way of argument
thunking, and a genuinely call-by-name transform. Specialising the
semantics to the CPS term model allows a rational reconstruction of
various CPS transforms.

This is a 171-page PhD thesis.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file