Lambda the Ultimate

Revisiting coroutines

This paper defends the revival of coroutines as a general control abstraction. After proposing a new classification of coroutines, we introduce the concept of full asymmetric coroutines and provide a precise definition for it through an operational semantics. We then demonstrate that full coroutines have an expressive power equivalent to one-shot continuations and one-shot partial continuations. We also show that full asymmetric coroutines and one-shot partial continuations have many similarities, and therefore present comparable benefits. Nevertheless, coroutines are easier implemented and understood, specially in the realm of procedural languages. Finally, we provide a collection of programming examples that illustrate the use of full asymmetric coroutines to support direct and concise implementation of several useful control behaviors, including cooperative multitasking.

Taking into account real or imaginary interest to control operators on LtU, I believe this paper makes nice reading. See also Coroutines in Lua.

A Monadic Framework for Subcontinuations

Functional and delimited continuations are more expressive than traditional
abortive continuations and they apparently seem to require a framework
beyond traditional continuation or monadic semantics. We show that this is not the
case: standard continuation semantics is sufficient to explain directly the common
control operators for delimited continuations. This implies a monadic framework for
typed and encapsulated functional and delimited continuations which we design and
implement as a Haskell library.

(via Michael Rys)

This is a Last Call Working Draft. Comments on this document are due no later than 15 July 2005...

I guess that those interested in this area know about this, and for others it is a bit too late to get involved, but at least it's good to know the status of the formal specification.

Although already mentioned before, I believe this paper (which reconciles two approaches to defining continuations) deserves a separate story.

On Evaluation Contexts, Continuations, and the Rest of Computation

Continuations are variously understood as representations of the current evaluation context and as representations of the rest of the computation, but these understandings contradict each other: plugging an expression in a context yields a new expression whereas sending an intermediate result to a continuation yields the final answer. We show that continuations-as-evaluation-contexts are the defunctionalized representation of the continuation of a single-step reduction function and that continuations-as-the-rest-of-thecomputation are the continuation of an evaluation function. Furthermore, we show that defunctionalizing the continuation of an evaluator gives rise to the same evaluation contexts as in the single-step reducer. The only difference is how these evaluation contexts are interpreted: a ‘plug’ interpretation yields one-step reduction, whereas a ‘refocus’ interpretation yields evaluation.

By now, shift/reset should be as popular as call/cc was ten years ago. Some think these control operators are even more important in practice than call/cc, and should be directly supported by PLs. I believe, this paper by Chung-chieh Shan will be interesting to many who loves logic and Curry-Howard isomorphism.

From shift and reset to polarized linear logic

Abstract:

Griffin pointed out that, just as the pure lambda-calculus corresponds to intuitionistic logic, a lambda-calculus with first-class continuations corresponds to classical logic. We study how first-class delimited continuations, in the form of Danvy and Filinski’s shift and reset operators, can also be logically interpreted. First, we refine Danvy and Filinski’s type system for shift and reset to distinguish between pure and impure functions. This refinement not only paves the way for answer type polymorphism, which makes more terms typable, but also helps us invert the continuation-passing-style (CPS) transform: any pure lambda-term with an appropriate type is beta-eta-equivalent to the CPS transform of some shift-reset expression. We conclude that the lambda-calculus with shift and reset and the pure lambda-calculus have the same logical interpretation, namely good old intuitionistic logic. Second, we mix delimited continuations with undelimited ones. Informed by the preceding conclusion, we translate the lambda-calculus with shift and reset into a polarized variant of linear logic that integrates classical and intuitionistic reasoning. Extending previous work on the lambda-µ-calculus, this unifying intermediate language expresses computations with and without control effects, on delimited and undelimited continuations, in call-by-value and call-byname settings.

The Essence of Data Access in Cw, The power is in the dot! Gavin Bierman, Erik Meijer, and Wolfram Schulte.

In this paper we concentrate on the data dimension. Our aim is to describe the essence of these extentions; by which we mean we identify, exemplify and formalize their essential features. Our tool is a small core language FCw, which is a valid subset of the full Cw language... we are able to formalize the type system and operational semantics of the data access fragments of Cw.

If you have been following the discussions here of Cw, you already know about the language features discussed here, since the paper doesn't introduce new features. If you haven't seen Cw, section 2 is a short and readable introduction.

The rest of the paper is more formal, and unless you need to prove formal results regarding Cw, might not be all that interesting. It won't hurt to keep in mind that it exists, since some of us may need something like FCw at one point or another.

We show how some classical static analyses for imperative programs, and the optimizing transformations which they enable, may be expressed and proved correct using elementary logical and denotational techniques. The key ingredients are an interpretation of program properties as relations, rather than predicates, and a realization that although many program analyses are traditionally formulated in very intensional terms, the associated transformations are actually enabled by more liberal extensional properties. We illustrate our approach with formal systems for analysing and transforming while-programs. The first is a simple type system which tracks constancy and dependency information and can be used to perform dead-code elimination, constant propagation and program slicing as well as capturing a form of secure information flow. The second is a relational version of Hoare logic, which significantly generalizes our first type system and can also justify optimizations including hoisting loop invariants. Finally we show how a simple available expression analysis and redundancy elimination transformation may be justified by translation into relational Hoare logic.

Not really exciting as such, but this technical report version of the POPL 2004 paper includes most of the proofs, which some might find helpful.

What follows will be a very subjective and personal view, as much my own history and development in the field and how things looked through my eyes as about the development of the field itself.

This essay is a longer version of the introductory essay in (Partee 2004). The introductory essay was first written in this long form in February 2003, but had to be cut down to about half the size to fit in the book...

This essay is about natural language semantics, but you'll find old friends here: lambdas, bindings, types, quantifiers etc. If you are lazy, go directly to footnote 25...

No surprise, really, if you follow the links we give here from time to time about TLGs and such.

Oleg's presentation at the workshop in honor of Daniel Friedman is great fun as usual. The topic of repeated applications of call/cc has been mentioned on LtU previously, a few years ago. New this time: the full and correct beta-normalizer written as a direct-style syntax-rule. The normalizer implements calculus of explicit substitutions. The talk presents probably the shortest (and the fastest) normal-order beta-normalizer as a (stand-alone) Scheme macro. Another new feature is the discussion of self-applications of delimited continuation operators. The talk mentions incidentally that shift, control, shift0 and other, less-delimited control operators are the members of the same family: gshift/greset.

Hot stuff.

Page 4 of the lecture notes from Mitch Wand's first Principles of Programming Languages lecture:

When looking at a language, we will always ask four questions. As we proceed through the course, we will ask these questions in more and more sophisticated ways; I’ll show some of these subquestions now, even though we haven’t yet covered enough to understand what they mean:

1. What are the values in the language?
   • What are the values manipulated by the language, and what operations on those values are represented in the language?
   • What are the expressed and denoted values in the language?
   • What are the types in the language?
2. What are the scoping rules of the language?
   • How are variables bound? How are they used?
   • What variables are in scope where?
3. What are the effects in the language?
   • Are there side-effects in the language?
   • Can execution of programs have effects in the world?
   • Can execution of programs have effects on other programs?
   • Can execution of a program fail to terminate?
   • Are there non-local control effects in the language?
4. What are the static properties of the language?
   • What can we predict about the behavior of a program without knowing the run-time values?
   • How can we analyze a program to predict this behavior?

What do you consider the fundamental properties of a programming language?