Information Services banner Edinburgh Research Archive The University of Edinburgh crest

Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1842/393

This item has been viewed 13 times in the last year. View Statistics

Files in This Item:

File Description SizeFormat
ECS-LFCS-97-376.dviLaTeX DVI File544.05 kBTeX dviView/Open
ECS-LFCS-97-376.pdfAdobe PDF 1.28 MBAdobe PDFView/Open
ECS-LFCS-97-376.psPostScript file983.15 kBPostscriptView/Open
Title: Categorical Structure of Continuation Passing Style
Authors: Thielecke , Hayo
Supervisor(s): Anderson, Stuart
Power, John
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
URI: http://hdl.handle.net/1842/393
Appears in Collections:Informatics thesis and dissertation collection

Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.

 

Valid XHTML 1.0! Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 2013, and/or the original authors. Privacy and Cookies Policy