Show simple item record

dc.contributor.advisorAnderson, Stuart
dc.contributor.advisorPower, John
dc.contributor.authorThielecke , Hayo
dc.date.accessioned2004-03-03T11:46:55Z
dc.date.available2004-03-03T11:46:55Z
dc.date.issued1997-07
dc.identifier.urihttp://hdl.handle.net/1842/393
dc.descriptionLaboratory for Foundations of Computer Science
dc.description.abstractThis 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.en
dc.format.extent557112 bytes
dc.format.extent1312158 bytes
dc.format.extent1006746 bytes
dc.format.mimetypeapplication/x-dvi
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.language.isoen
dc.publisherUniversity of Edinburgh. College of Science and Engineering. School of Informatics.en
dc.titleCategorical Structure of Continuation Passing Styleen
dc.typeThesis or Dissertation
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record