Extracting the Range of cps from Affine Typing Extended Abstract (2008)
Josh Berdine, Peter W. O’hearn, Hayo Thielecke
Increasing degrees of reasoning about programs are being mechanized, and hence more formality is needed. Here we present an instance of this formalization in the form of a precise characterization of...
An Introduction to Landin's "A Generalization of Jumps and Labels " (2007)
. This note introduces Peter Landin's 1965 technical report "A Generalization of Jumps and Labels", which is reprinted in this volume. Its aim is to make that historic paper more...
Extracting the Range of cps from Ane Typing Extended Abstract (2007)
Josh Berdine, Peter W. O'hearn, Hayo Thielecke
Increasing degrees of reasoning about programs are being mechanized, and hence more formality is needed. Here we present an instance of this formalization in the form of a precise characterization of...
On Ane Typing and Completeness of cps Extended Summary Draft (2007)
Josh Berdine, Peter W. O'hearn, Hayo Thielecke
This paper is a companion to \Linearly Used Continuations " by the authors. There, we show how a variety of control behaviours use continuations anely, including calling/returning...
MFPS XXI, and to Jean-Louis Krivine and Xavier Leroy, to accept our invitation to speak at the workshop.
A Type-theoretic Reconstruction of the Visitor Pattern Abstract (2005)
Peter Buchlovsky, Hayo Thielecke
In object-oriented languages, the Visitor pattern can be used to traverse tree-like data structures: a visitor object contains some operations, and the data structure objects allow themselves to be...
Answer type polymorphism in call-by-name continuation passing (2004)
Abstract. This paper studies continuations by means of a polymorphic type system. The traditional call-by-name continuation passing style transform admits a typing in which some answer types are...
From control effects to typed continuation passing (2003)
First-class continuations are a powerful computational effect, allowing the programmer to express any form of jumping. Types and effect systems can be used to reason about continuations, both in the...
From Control Effects to Typed Continuation Passing (2003)
First-class continuations are a powerful computational effect, allowing the programmer to express any form of jumping. Types and effect systems can be used to reason about continuations, both in the...
On the call-by-value CPS transform and its semantics (2003)
Carsten Führmann, Hayo Thielecke
We investigate continuations in the context of idealized call-by-value programming languages. On the semantic side, we analyze the categorical structures that arise from continuation models of...
Linear continuationpassing (2002)
Josh Berdine, Uday Reddy, Hayo Thielecke
Abstract. Continuations can be used to explain a wide variety of control behaviours, including calling/returning (procedures), raising/handling (exceptions), labelled jumping (goto statements),...
Linear continuationpassing (2002)
Josh Berdine, Uday Reddy, Hayo Thielecke
Abstract. Continuations can be used to explain a wide variety of control behaviours, including calling/returning (procedures), raising/handling (exceptions), labelled jumping (goto statements),...
Linear Continuation-Passing (2002)
Josh Berdine, Peter O'Hearn, Uday Reddy, Hayo Thielecke
Continuations can be used to explain a wide variety of control behaviours, including calling/returning (procedures), raising/handling (exceptions), labelled jumping (goto statements), process...
Linear continuationpassing (2002)
Josh Berdine, Uday Reddy, Hayo Thielecke
Abstract. Continuations can be used to explain a wide variety of control behaviours, including calling/returning (procedures), raising/handling (exceptions), labelled jumping (goto statements),...
Comparing Control Constructs by Double-barrelled CPS (2002)
We investigate call-by-value continuation-passing style transforms that pass two continuations. Altering a single variable in the translation of #-abstraction gives rise to di#erent control...
Modelling Environments in Call-By-Value Programming Languages (2002)
Paul Blain Levy, John Power, Hayo Thielecke
this paper, we investigate environments in call-by-value languages by analysing a fine-grain variant of Moggi's computational #- calculus, giving two equivalent sound and complete classes of...
Contrasting exceptions and continuations (2001)
Exceptions and first-class continuations are the most powerful forms of control in programming languages. While both are a form of non-local jumping, there is a fundamental difference between them....
Linearly used continuations (2001)
Josh Berdine, Peter W. O'hearn, Uday S. Reddy, Hayo Thielecke
Continuations are the raw material of control. They can be used to explain a wide variety of control behaviours, including calling/returning (procedures), raising/handling
Linearly used continuations (2001)
Josh Berdine, Peter W. O'hearn, Uday S. Reddy, Hayo Thielecke
Continuations are the raw material of control. They can be used to explain a wide variety of control behaviours, including calling/returning (procedures), raising/handling
Comparing Control Constructs by Typing Double-barrelled CPS Transforms (2001)
We investigate continuation-passing style transforms that pass two continuations. Altering a single variable in the translation of -abstraction gives rise to different control operators: firstclass...
Comparing control constructs by typing double-barrelled cps transforms (2001)
ABSTRACT We investigate continuation-passing style transforms that pass two continuations. Altering a single variable in the translation of *-abstraction gives rise to different control operators:...
On Exceptions versus Continuations in the Presence of State (2000)
. We compare the expressive power of exceptions and continuations when added to a language with local state in the setting of operational semantics. Continuations are shown to be more expressive than...
Typed Exceptions and Continuations Cannot Macro-Express Each Other (1999)
Jon Riecke And, Jon G. Riecke, Hayo Thielecke
. The most powerful control constructs in modern programming languages are continuations and exceptions. Although they can be used interchangeably in some cases, they are fundamentally different...
Closed Freyd- and k-Categories (1999)
. We give two classes of sound and complete models for the computational -calculus, or c-calculus. For the first, we generalise the notion of cartesian closed category to that of closed...
Typed Exceptions and Continuations Cannot Macro-Express Each Other (1999)
. The most powerful control constructs in modern programming languages are continuations and exceptions. Although they can be used interchangeably in some cases, they are fundamentally different...
Typed Exceptions and Continuations Cannot Macro-Express Each Other (1999)
Jon Riecke And, Jon G. Riecke, Hayo Thielecke
. The most powerful control constructs in modern programming languages are continuations and exceptions. Although they can be used interchangeably in some cases, they are fundamentally different...
Closed Freyd- and k-Categories (1999)
. We give two classes of sound and complete models for the computational -calculus, or c-calculus. For the first, we generalise the notion of cartesian closed category to that of closed...
Continuations, Functions and Jumps (1999)
this article, therefore, is to help the reader uncompress the CPS transform by way of a rational reconstruction from jumps.
Using a Continuation Twice and Its Implications for the Expressive Power of Call/cc (1998)
. We study the implications for the expressive power of call/cc of upward continuations, specifically the idiom of using a continuation twice. Although such control effects were known to Landin and...
Categorical Structure of Continuation Passing Style (1997)
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...
Categorical Structure of Continuation Passing Style (1997)
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...
Continuation Semantics and Self-adjointness (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...
Environments, Continuation Semantics and Indexed Categories (1997)
. There have traditionally been two approaches to modelling environments, one by use of ønite products in Cartesian closed categories, the other by use of the base categories of indexed categories...
Categorical Structure of Continuation Passing Style (1997)
Hayo Thielecke, Alan Paxton, Andy Pitts, Jon Riecke, David N. Turner, Phil Wadler
This thesis attempts to make precise the structure inherent in Continuation Passing Style (CPS). We emphasize that CPS translates λ-calculus into a very basic calculus that does not have functions...
Categorical Structure of Continuation Passing Style (1997)
Hayo Thielecke, Alan Paxton, Andy Pitts, Jon Riecke, David N. Turner, Phil Wadler
This thesis attempts to make precise the structure inherent in Continuation Passing Style (CPS).
Continuation Passing Style and Self-Adjointness (1996)
Hayo Thielecke Lfcs, Hayo Thielecke
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...
Continuation Passing Style and Self-Adjointness (1996)
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...
A proposed categorical semantics for ML modules (1995)
Michael Fourman, Hayo Thielecke
We present a simple categorical semantics for ML signatures, structures and functors. Our approach relies on realizablity semantics in the category of assemblies. Signatures and structures are...