Threads Yield Continuations

Just as a traditional continuation represents the rest of acomputation from a given point in the computation, a subcontinuationrepresents the rest of a subcomputation from agiven point in the subcomputation. Subcontinuationsare more expressive than traditional continuations and have been shown to beuseful for controlling tree-structured concurrency, yet they havepreviously been implemented only on uniprocessors. This article describes aconcurrent implementation of one-shot subcontinuations. Like one-shotcontinuations, one-shot subcontinuations are first-class but may be invokedat most once, a restriction obeyed by nearly all programs that usecontinuations. The techniques used to implement one-shot subcontinuationsmay be applied directly to other one-shot continuation mechanisms and may begeneralized to support multi-shot continuations as well. A novel feature ofthe implementation is that continuations are implemented in terms ofthreads. Because the implementation model does not rely upon any speciallanguage features or compilation techniques, the model is applicable toany language or language implementation that supports a small set of threadprimitives.     

Reflections on Landin''s J-operator: A partly historical note

Landin's J-operator was the first attempt to extend the λ-calculus with a non-functional control facility. We show in this note how the extended language can be embedded in Scheme. This finally clarifies the relationship between the J- and the call/cc-operator. Beyond the historical perspective the note simultaneously provides insight into the programming with continuations and the construction of language embeddings for the clarification of semantic issues.     

An Early Use of Continuations and Partial Evaluation for Compiling Rules Written in First-Order Predicate Calculus

This brief historical note describes research done in the period 1970-1973, and where continuations were introduced in a fairly pragmatic way together with partial evaluation in order to compile rules expressed as statements in first-order predicate calculus. Although the methods used at that time were quite straightforward, this work may shed some light on the early history of the concept of continuations. In particular, unlike other early contributions that addressed issues in mainstream programming languages, the present approach initially addressed implementation techniques for special-purpose languages.     

Implementation Strategies for First-Class Continuations

Scheme and Smalltalk continuations may have unlimited extent. This means that a purely stack-based implementation of continuations, as suffices for most languages, is inadequate. We review several implementation strategies for continuations and compare their performance using instruction counts for the normal case and continuation-intensive synthetic benchmarks for other scenarios, including coroutines and multitasking. All of the strategies constrain a compiler in some way, resulting in indirect costs that are hard to measure directly. We use related measurements on a set of benchmarks to calculate upper bounds for these indirect costs.     

Types as Graphs: Continuations in Type Logical Grammar

Using the programming-language concept of continuations, we propose a new, multimodal analysis of quantification in Type Logical Grammar. Our approach provides a geometric view of in-situ quantification in terms of graphs, and motivates the limited use of empty antecedents in derivations. Just as continuations are the tool of choice for reasoning about evaluation order and side effects in programming languages, our system provides a principled, type-logical way to model evaluation order and side effects in natural language. We illustrate with an improved account of quantificational binding, weak crossover, wh-questions, superiority, and polarity licensing.     

Controlling Control Flow in Web Applications

Control flow is often key problem in current web applications. For example, using the back button gives a POSTDATA error, using multiple windows books the wrong hotel, and sending a link to a friend does not work.Previous solutions used continuations as a model for user interaction. However continuations are insufficient as a model of all web interactions. We believe the protocol and browsers themselves are insufficiently powerful to represent the control flow desired in a web application.Our solution is to extend the protocol and browser sufficiently that these problems can be avoided. We seek to be agnostic about how web applications are written and instead recognise that many of the problems stem from underlying weaknesses in the protocol.As an example, the application ought to be able to inform the browser that pressing back on a payment confirmation page is not allowed. Instead, the cached page can be displayed in a read-only, archive fashion to the user, or a new page can be shown instead which is consistent with the global state.We discuss how some of these ideas may be implemented within the existing HTTP/1.1 protocol; and what modest extensions to the protocol would enable full implementation. We also discuss the interaction with Web 2.0 and the security and privacy implications of our extensions.     

Integrating User-Level Threads with Processes in Scsh

Scsh, the Scheme shell, enables concurrent system programming with portable user-level threads. In scsh, threads behave like processes in many ways: each thread receives its own set of process resources; like Unix processes, new threads can inherit resources from the creating thread. The combination of scsh's interface to the POSIX API with user-level threads creates a number of design and implementation challenges: Scsh's abstractions for managing process resources raise interesting modularity issues, particularly in connection with first-class continuations. Scsh also provides an interface to the fork system call; its implementation must avoid common pitfalls that arise with a user-level thread system. This paper describes the design and implementation of the relevant abstractions and discusses the implications for programming-language and system design.     

Comparing Control Constructs by Double-Barrelled CPS

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 different control operators: first-class continuations; dynamic control; and (depending on a further choice of a variable) either the return statement of C; or Landin's J-operator. In each case there is an associated simple typing. For those constructs that allow upward continuations, the typing is classical, for the others it remains intuitionistic, giving a clean distinction independent of syntactic details. Moreover, those constructs that make the typing classical in the source of the CPS transform break the linearity of continuation use in the target.     

Recursion from iteration

In a simply-typed, call-by-value (CBV) language with first-class continuations, the usual CBV fixpoint operator can be defined in terms of a simple, infinitely-looping iteration primitive. We first consider a natural but flawed definition, based on exceptions and iterative deepening of finite unfoldings, and point out some of its shortcomings. Then we present the proper construction using full first-class continuations, with both an informal derivation and a proof that the behavior of the defined operator faithfully mimics a built-in recursion primitive. In fact, given an additional uniformity assumption, the construction is a two-sided inverse of the usual definition of iteration from recursion. Continuing, we show that the CBV looping primitive is in fact the direct-style equivalent of a continuation-passing-style fixpoint, and that this correspondence extends all the way to traditional definitions of these operators in terms of reflexive types.An earlier version of this work appeared inProceedings of the 1992 ACM SIGPLAN Workshop on Continuations.Supported in part by NSF Grant CCR-8922109 and in part by the Avionics Lab, Wright Research and Development Center, Aeronautical Systems Division (AFSC), U.S. Air Force, Wright-Patterson AFB, OH 45433-6543 under Contract F33615-90-C-1465, ARPA Order No. 7597. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. Government.     

How to Determine the Expressive Power of Constraints

Some constraint languages are more powerful than others because they allow us to express a larger collection of problems. In this paper, we give a precise meaning to this concept of expressive power for constraints over finite sets of values. The central result of the paper is that the expressive power of a given set of constraint types is determined by certain algebraic properties of the underlying relations. These algebraic properties can be calculated by solving a particular constraint satisfaction problem, which we call an 'indicator problem'. We discuss the connection between expressive power and computational complexity, and show that indicator problems provide a simple method to test for tractability.     

Safe-for-Space Threads in Standard ML

Threads can easily be implemented using first-class continuations, but the straightforward approaches for doing so lead to space leaks, especially in a language with exceptions like Standard ML. We show how these space leaks arise and give a new implementation for threads that is safe for space.     

Linear Continuation-Passing

Continuations can be used to explain a wide variety of control behaviours, including calling/returning (procedures), raising/handling (exceptions), labelled jumping (goto statements), process switching (coroutines), and backtracking. However, continuations are often manipulated in a highly stylised way, and we show that all of these, bar backtracking, in fact use their continuations linearly; this is formalised by taking a target language for CPS transforms that has both intuitionistic and linear function types.     

Axioms for Recursion in Call-by-Value

We propose an axiomatization of fixpoint operators in typed call-by-value programming languages, and give its justifications in two ways. First, it is shown to be sound and complete for the notion of uniform T-fixpoint operators of Simpson and Plotkin. Second, the axioms precisely account for Filinski's fixpoint operator derived from an iterator (infinite loop constructor) in the presence of first-class continuations, provided that we define the uniformity principle on such an iterator via a notion of effect-freeness (centrality). We then explain how these two results are related in terms of the underlying categorical structures.     

Threads Yield Continuations

Just as a traditional continuation represents the rest of acomputation from a given point in the computation, a subcontinuationrepresents the rest of a subcomputation from agiven point in the subcomputation. Subcontinuationsare more expressive than traditional continuations and have been shown to beuseful for controlling tree-structured concurrency, yet they havepreviously been implemented only on uniprocessors. This article describes aconcurrent implementation of one-shot subcontinuations. Like one-shotcontinuations, one-shot subcontinuations are first-class but may be invokedat most once, a restriction obeyed by nearly all programs that usecontinuations. The techniques used to implement one-shot subcontinuationsmay be applied directly to other one-shot continuation mechanisms and may begeneralized to support multi-shot continuations as well. A novel feature ofthe implementation is that continuations are implemented in terms ofthreads. Because the implementation model does not rely upon any speciallanguage features or compilation techniques, the model is applicable toany language or language implementation that supports a small set of threadprimitives.     

Secure Information Flow via Linear Continuations

Security-typed languages enforce secrecy or integrity policies by type-checking. This paper investigates continuation-passing style (CPS) as a means of proving that such languages enforce noninterference and as a first step towards understanding their compilation. We present a low-level, secure calculus with higher-order, imperative features and linear continuations.Linear continuations impose a stack discipline on the control flow of programs. This additional structure in the type system lets us establish a strong information-flow security property called noninterference. We prove that our CPS target language enjoys the noninterference property and we show how to translate secure high-level programs to this low-level language. This noninterference proof is the first of its kind for a language with higher-order functions and state.     

Continuations Revisited

To introduce the republication of his joint 1974 paper with Christopher Strachey, Continuations: A Mathematical Semantics for Handling Full Jumps, the author recalls earlier unsuccessful struggles which culminated eventually in the almost instantaneous insight for their discovery of continuations in 1970.     

A type-theoretic foundation of delimited continuations

There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters, the continuations become composable and the calculi become more expressive. We present a fine-grained analysis of control delimiters and formalise that their addition corresponds to the addition of a single dynamically-scoped variable modelling the special top-level continuation. From a type perspective, the dynamically-scoped variable requires effect annotations. In the presence of control, the dynamically-scoped variable can be interpreted in a purely functional way by applying a store-passing style. At the type level, the effect annotations are mapped within standard classical logic extended with the dual of implication, namely subtraction. A continuation-passing-style transformation of lambda-calculus with control and subtraction is defined. Combining the translations provides a decomposition of standard CPS transformations for delimited continuations. Incidentally, we also give a direct normalisation proof of the simply-typed lambda-calculus with control and subtraction.     

On the static and dynamic extents of delimited continuations

We show that breadth-first traversal exploits the difference between the static delimited-control operator shift (alias ) and the dynamic delimited-control operator control (alias ). For the last 15 years, this difference has been repeatedly mentioned in the literature but it has only been illustrated with one-line toy examples. Breadth-first traversal fills this vacuum.

We also point out where static delimited continuations naturally give rise to the notion of control stack whereas dynamic delimited continuations can be made to account for a notion of ‘control queue’.