## List of Talks: Continuation Workshop 2011

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.

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, - 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),
- we outline a lightweight
workflow infrastructure in the spirit of Lu and Gannon (eScience 2008)
and
- 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