List of Talks: Continuation Workshop 2011

Continuation Semantics in Linguistics (Invited Talk)
Mats Rooth (Linguistics and CIS, Cornell University)

For decades, typed lambda calculus has been an essential part of the toolkit for work on semantics in theoretical linguistics. While practitioners in linguistics have been aware that the same logical and type-theoretic methods are used in theoretical computer science, the advantages of this in importing ideas into linguistics are only starting to be cashed out. The chief success so far is the "continuation semantics" for linguistic phenomena including scope and coreference. In this talk, I will explain the linguistic intuition about continuation semantics for scope, and look at some of my own research on intonational focus and ellipsis. I will also talk about using lambda calculators in teaching, and anticipated benefits of using CS-derived ideas in linguistic semantics.

Continuations and classical logic (Invited talk)
Koji NAKAZAWA

It is well known as the Curry-Howard isomorphism that there is a neat correspondence between logical systems and typed calculi, in particular, the intuitionistic natural deduction and the simply typed lambda calculus. In his paper in 1989, Griffin showed that the correspondence is extended to classical logic and calculi with control operators, and then some typed calculi based on classical logic have been proposed and studied from viewpoints of both logic and programming languages.

In this talk, I show how continuations relate to classical logic, and that we can use ideas from continuations to prove a fundamental property of logic, that is, normalization theorem for some proof systems of classical logic.

Non-Deterministic Search Library
Kenichi ASAI, Chihiro KANEKO

Non-deterministic programming has been used as a non-trivial application of (delimited) continuations. We report on our experience of using OchaCaml, an extension of Caml Light with (polymorphically typed) shift and reset, to write a search problem using non-deterministic operators. We provide a library for non-deterministic operations implemented using shift and reset and show how it enables us to write a search problem in direct style, using party puzzles as a concrete example.

`Focus movement' by delimited continuations
Daisuke BEKKI

In the past 10 years, the application of the notion of continuations to natural language semantics has been pursued in order to capture non-local aspects of semantic composition. The phenomenon of “focus” is an example of such aspects, in which the “focused element” induces a universal quantification which refers to the meaning of the whole sentence. In this talk, we will first introduce a theory of the meta-lambda calculus, a kind of two-level typed lambda calculus, to define a monadic translation by which shift/reset operators are defined via continuation monad. We then introduce Bekki and Asai's analysis of focus in which focus contains a shift operator and the adverbial “only” denotes a reset operator. Such a compositional encoding of focus becomes possible through the clear semantics of the meta-lambda calculus based on category theory.

Swarm: transparent scalability through portable continuations
James DOUGLAS

Transparent scalability is an elusive characteristic sought for successful software projects which inevitably outgrow themselves. A common way to approach the design of such applications is with the MapReduce pattern, which requires considerable foresight into how the application can be broken down into the functional map and reduce operations. A problem with this and similar approaches is the investment required at the beginning of development; the problem domain must be carefully analyzed and a solution crafted to support the predicted scalability needs. It would be preferable if applications could be developed simply and cheaply, then later, when necessary, made scalable without reworking the existing source code. We present an approach to building transparently scalable applications using Swarm, a framework which enables code execution to “follow the data” within Scala's serializable delimited continuations. Swarm abstracts the location of data across a distributed system from the developer, eliminating costly architectural and modeling requirements of popular distributed computing patterns and frameworks. We explain the design of an example implementation of a Twitter-like Web application which uses Swarm's continuation-passing style collections, and show how the developer is unburdened by the complexity of scalability. We demonstrate how this Swarm-based application can be transparently scaled without requiring changes to the code or accommodation by the architecture.

Correctness of Functions with Shift and Reset
Noriko HIROTA, Kenichi ASAI

Although shift and reset have become used to write various interesting functions, the understanding of those functions is not always simple. As an attempt to better understand their behavior, we formalize and prove correct some functions written with shift and reset in Coq. Building on Sozeau and Kiselyov's formalization of shift and reset using Generalized Continuation Monad, we first formalize Kameyama and Hasegawa's axioms for shift and reset in Coq. We then write a few functions in monadic style and prove them correct using Kameyama and Hasegawa's axioms and the standard monad laws. By carefully not unfolding the definition of monadic operators, we can effectively prove correctness of functions in direct style. We report on two case studies of this approach: reverse and times, and mention that non-trivial generalization of hypothesis is required to properly characterize the behavior of continuations.

Yield, the control operator: applications and a conjecture
Roshan P. JAMES, Amr SABRY

In previous work, “Yield: Mainstream delimited continuations” (TPDC 2011), we presented a generalized version of the yield control operator that was distilled from studying yield operators of various programming languages. In this brief abstract,
  1. we extend that presentation to establish the connection of yield with dynamic binding, dynamic scope and generalized stack inspection in the spirit of Kiselyov et al (SIGPLAN Not. 2006),
  2. we outline a lightweight workflow infrastructure in the spirit of Lu and Gannon (eScience 2008) and
  3. we provide a yield monad transformer that allows yield to be composed with other effects.
Finally, we pose a question of considerable theoretical interest: do delimited continuations expressed using yield in combination with session types shed light on answer-type polymorphism?

Demonstration of Continuation based C on GCC
Shinji KONO

We have implemented a C-like Continuation based programming language. Continuation based C, CbC was implemented using micro-C on various architectures, and we have tried several CbC programming experiments. Here we report a new implementation of CbC compiler based on GCC 4.5. Since it contains full C capability, we can use both CbC and C.

Modular rollback through free monads
Conor McBRIDE, Olin SHIVERS, Aaron TURON

Control operators prove to be an excellent tool for decoupling concerns, and in particular for separating error repair or user interaction from the processing of correct input. In a paper to appear in this year's ICFP, Shivers and Turon give one such use case, a programming pattern for “modular rollback through control logging.” Using this pattern, an input processor can be written in a direct way, without any knowledge of a user's ability to back up and alter the input, or a repair module's ability to fix errors.

The original pattern is presented in direct style, assuming first-class control operators. In this presentation, we will contrast it with an approach, due to Conor McBride, that uses free monads to achieve a similar kind of modularity. The focus of the talk will be the tradeoffs between these two designs.

Using delimited continuations for distributed computing with the CIEL engine
Derek G. MURRAY, Malte SCHWARZKOPF, Christopher SMOWTON, Steven SMITH, Anil MADHAVAPEDDY, Steven HAND

CIEL is a universal execution engine for distributed computation, designed to achieve high scalability and reliability when run on a commodity cluster. CIEL supports the full range of MapReduce-style computations, and additionally Turing-powerful data-dependent control-flow that permits efficient, fault-tolerant evaluation of iterative and dynamic programming problems that are difficult to express in a pure MapReduce framework. CIEL also has a clear separation between the execution engine and the programming language interfaces, and so in this talk I will describe the integration of delimited continuations (Scala, OCaml), monadic workflow (Haskell), pure continuations (Stackless Python), and manual callbacks (Java).

The limit of the CPS hierarchy
Josef SVENNINGSSON

We present a language which we refer to as the limit of the CPS hierarchy. It allows for an unbounded number of levels of continuations. We present a semantics in the form of an abstract machine.

Visualizing continuations
Naoki TAKASHIMA, Yukiyoshi KAMEYAMA

Direct manipulation of delimited continuations allows one to write elegant and modular programs. However, it is often hard for beginners to understand their behavior due to their semantical difficulty. To ease such a burden, we have designed a new language Redex for visualizing delimited continuations. It has nested (multi-prompt) delimited-control operators and a serialization mechanism. The latter gives the source-term representation, rather than binary representation, of any represented values in the language so that one can see the delimited continuations at any time of execution of a program. We believe that such a feature is very useful for learning delimited continuations.
Program Co-Chairs: Oleg Kiselyov and Chung-chieh Shan