Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >
Please use this identifier to cite or link to this item:
|Title: ||Categorical Structure of Continuation Passing Style|
|Authors: ||Thielecke , Hayo|
|Supervisor(s): ||Anderson, Stuart|
|Issue Date: ||Jul-1997|
|Publisher: ||University of Edinburgh. College of Science and Engineering. School of Informatics.|
|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.|
|Description: ||Laboratory for Foundations of Computer Science|
|Appears in Collections:||Informatics thesis and dissertation collection|
Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.