BRICS

Basic Research in Computer Science

A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations

Dariusz Biernacki Olivier Danvy Kevin Millikin BRICS Report Series RS-06-15 ISSN 0909-0878 October 2006 BRICS RS-06-15 Biernacki et al.: A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations Copyright \begin{matrix}c \\ ◯ \end{matrix} 2006, Dariusz Biernacki & Olivier Danvy & Kevin

Millikin. BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus IT-parken, Aabogade 34 DK–8200 Aarhus N Denmark

Telephone: +45 8942 9300
Telefax: +45 8942 5601
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/06/15/

A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations^{∗}

Dariusz Biernacki,^{†} Olivier Danvy, and Kevin Millikin BRICS^{‡} Department of Computer Science University of Aarhus^{§}

October 2006

Abstract

We put a pre-existing definitional abstract machine for dynamic delimited continuations in defunctionalized form, and we present the consequences of this adjustment.

We first prove the correctness of the adjusted abstract machine. Because it is in defunctionalized form, we can refunctionalize it into a higher-order evaluation function. This evaluation function, which is compositional, is in continuation+state passing style and threads a trail of delimited continuations and a meta-continuation. Since this style accounts for dynamic delimited continuations, we refer to it as ‘dynamic continuation-passing style’ and we present the corresponding dynamic CPS transformation. We show that the notion of computation induced by dynamic CPS takes the form of a continuation monad with a recursive answer type and we present a new simulation of dynamic delimited continuations in terms of static ones as well as new applications of dynamic delimited continuations.

The significance of the present work is that the computational artifacts surrounding dynamic CPS (i.e., simple motivating examples as well as more complex applications and simulations, a functional encoding in the form of a continuationpassing evaluator, the corresponding CPS transformation, their first-order counterparts, and the continuation monad) are not independent designs: they are mechanical consequences of having put the definitional abstract machine in defunctionalized form.

Technical Report BRICS RS-06-15

http://www.brics.dk/RS/06/Abs/BRICS-RS-06-Abs/BRICS-RS-06-Abs.html#BRICS-RS-06-15

∗Revised version of BRICS RS-05-16.

†Current affiliation: INRIA Futurs, Orsay, France.

‡ Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

§ IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark.

Email: {dabi,danvy,kmillikin}@brics.dk

Contents

1 Introduction 1 2 The definitional abstract machine 1 3 The adjusted abstract machine 2 4 Equivalence of the definitional machine and of the adjusted machine 5 5 The evaluator corresponding to the adjusted machine 8 6 The CPS transformer corresponding to the evaluator in dynamic CPS 8 7 The direct-style evaluator corresponding to the evaluator in dynamic CPS 10 8 Static and dynamic continuation-passing style 11

8.1 Static continuation-passing style . . . . . . . . . . . . . . . . . . . . . . . . . 12 8.2 Dynamic continuation-passing style . . . . . . . . . . . . . . . . . . . . . . . . 12 8.3 A generalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 8.4 Further examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

9 A monad for dynamic continuation-passing style 15 10 A new implementation of control and prompt 18 11 Related work 20 12 Conclusion and issues 22 Appendices 22

A control0  22
B shift0  22

C An implementation of shift and reset 23

List of Figures

1 The definitional call-by-value abstract machine for the λ-calculus extended

with F and # . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2 The adjusted call-by-value abstract machine for the λ-calculus extended with

F and # . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3 A call-by-value evaluator for the λ-calculus extended with F and # . . . . . 9 4 A direct-style evaluator for the λ-calculus extended with F and # . . . . . . 11 5 A monadic evaluator for the λ-calculus extended with F and # . . . . . . . . 17

1 Introduction

The control operator call/cc [11, 35, 42, 49], by now, is an accepted component in the landscape of eager functional programming, where it provides the expressive power of CPS (continuation-passing style) in direct-style programs. An integral part of its success is its surrounding array of computational artifacts: simple motivating examples as well as more complex applications, a functional encoding in the form of a continuation-passing evaluator, the corresponding continuation-passing style and CPS transformation, their first-order counterparts (e.g., the corresponding abstract machine), and the continuation monad.

The delimited-control operators control (alias F) and prompt (alias #) [27, 30, 53] were designed to go ‘beyond continuations’ [29]. This vision was investigated in the early 1990’s [34, 37,38,46,48,54] and today it is receiving renewed attention: Shan and Kiselyov are studying its simulation properties [43, 52], and Dybvig, Peyton Jones, and Sabry are proposing a general framework where multiple control delimiters can coexist [25].

We observe, though, that none of these recent works on control and prompt uses the entire array of artifacts that organically surrounds call/cc. Our goal here is to do so.

This work: We present an abstract machine that accounts for dynamic delimited continuations and that is in defunctionalized form [23, 49], and we prove its equivalence with a definitional abstract machine that is not in defunctionalized form. We also present the corresponding higher-order evaluator from which one can obtain the corresponding CPS transformer. The resulting ‘dynamic continuation-passing style’ (dynamic CPS) threads a list of trailing delimited continuations, i.e., it is a continuation+state-passing style. This style is equivalent to, but simpler than, the one recently proposed by Shan [52]. It is structurally related to the one recently proposed by Dybvig, Peyton Jones, and Sabry [25]. We also show that it corresponds to a computational monad, and we present some new examples.

Overview: We first present the definitional machine for dynamic delimited continuations in Section 2. In Section 3, we put the definitional machine into defunctionalized form and we establish the equivalence of the two machines in Section 4. We present the corresponding higher-order evaluator, which is compositional, in Section 5. This evaluator is expressed in a dynamic continuation-passing style and we present the corresponding dynamic CPS transformer in Section 6 and the corresponding direct-style evaluator in Section 7: transforming this direct-style evaluator into dynamic CPS yields the evaluator of Section 5. We illustrate dynamic continuation-passing style in Section 8 and in Section 9, we show that it can be characterized with a computational monad: macro-expanding the definition of this monad into a monadic evaluator and CPS transforming the result yields a curried version of the evaluator of Section 5. In Section 10, we present a new simulation of control and prompt based on dynamic CPS. We then address related work and conclude. In Appendices A and B we consider the abstract machines corresponding to the control operators control0 and prompt0. Finally, for completeness, we give an ML implementation of shift and reset in Appendix C.

Prerequisites and notation: We assume some basic familiarity with operational semantics, abstract machines, eager functional programming in (Standard) ML, defunctionalization, and continuations.

2 The definitional abstract machine

In our earlier work [4], we obtained an abstract machine for the static delimited-control operators shift and reset by defunctionalizing a definitional evaluator that had two layered continuations [18, 19]. In this abstract machine, the first continuation takes the form of an evaluation context and the second takes the form of a stack of evaluation contexts. By construction, this abstract machine is an extension of Felleisen et al.’s CEK machine [28], which has one evaluation context and is itself a defunctionalized evaluator with one continuation [2, 3, 13, 49].

The abstract machine for static delimited continuations implements the application of a delimited continuation (represented as a captured context) by pushing the current context onto the stack of contexts and installing the captured context as the new current context [4]. In contrast, the abstract machine for dynamic delimited continuations implements the application of a delimited continuation (also represented as a captured context) by concatenating the captured context to the current context [30]. As a result, static and dynamic delimited continuations differ because a subsequent control operation will capture either the remainder of the reinstated context (in the static case) or the remainder of the reinstated context together with the then-current context (in the dynamic case). An abstract machine implementing dynamic delimited continuations therefore a priori requires defining an operation to concatenate contexts.

Figure 1 displays the definitional abstract machine for dynamic delimited continuations, including the operation to concatenate contexts. It only differs from our earlier abstract machine for static delimited continuations [4, Figure 7 and Section 4.5] in the way captured delimited continuations are applied, by concatenating their representation with the representation of the current continuation (the shaded transition in Figure 1).^{1} Biernacka and Danvy present the corresponding calculus elsewhere [5, Section 6.2].

Contexts form a monoid:

Proposition 1. The operation ⋆ defined in Figure 1 satisfies the following properties:

(1) C_{1} ⋆ END = C_{1} = END ⋆ C_{1},

(2) (C_{1} ⋆ C′_{1}) ⋆ C′′_{1} = C_{1} ⋆ (C′_{1} ⋆ C′′_{1}).

Proof. By induction on the structure of C_{1}.

In the definitional machine, the constructors of contexts are not solely consumed in the cont_{1} transitions, but also by ⋆. Therefore, the definitional abstract machine is not in the range of defunctionalization [16, 23, 49]: it does not correspond to a higher-order evaluator. In the next section, we present a new abstract machine that implements dynamic delimited continuations and is in the range of defunctionalization.

3 The adjusted abstract machine

The definitional machine is not in the range of defunctionalization because of the concatenation of contexts. We therefore introduce a new component in the machine to avoid this concatenation. This new component, the trail of contexts, holds the then-current contexts that would have been concatenated to the captured context in the definitional machine. These then-current contexts are then reinstated in turn when the captured context completes. Together, the current context and the trail of contexts represent the current dynamic context. The final component of the machine holds a stack of dynamic contexts (represented as a list: nil denotes the empty list, the infix operator :: denotes list construction, and the infix operator @ denotes list concatenation, as in ML).

⟨FUN (C′_{1}, C_{1}), v, C_{2}⟩_{cont_{1}} ⇒ ⟨C′_{1}, v, C_{1} :: C_{2}⟩_{cont_{1}}

1In contrast, static delimited continuations are applied as follows:

• Terms: e ::= x | λx.e | e_{0} e_{1} | #e | Fx.e

• Values (closures and captured continuations): v ::= [x, e, ρ] | C_{1}

• Environments: ρ ::= ρ_{mt} | ρ{x ↦ v}

• Contexts: C_{1} ::= END | ARG ((e, ρ), C_{1}) | FUN (v, C_{1})

• Concatenation of contexts:

END ⋆ C′_{1} =^{def} C′_{1}
(ARG ((e, ρ), C_{1})) ⋆ C′_{1} =^{def} ARG ((e, ρ), C_{1} ⋆ C′_{1})
(FUN (v, C_{1})) ⋆ C′_{1} =^{def} FUN (v, C_{1} ⋆ C′_{1})

• Meta-contexts: C_{2} ::= nil | C_{1} :: C_{2}

• Initial transition, transition rules, and final transition:

e

⇒_{def}

⟨e, ρ_{mt}, END, nil⟩_{eval}
⟨x, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{def} ⟨C_{1}, ρ(x), C_{2}⟩_{cont_{1}}
⟨λx.e, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{def} ⟨C_{1}, [x, e, ρ], C_{2}⟩_{cont_{1}}
⟨e_{0} e_{1}, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{def} ⟨e_{0}, ρ, ARG ((e_{1}, ρ), C_{1}), C_{2}⟩_{eval}
⟨#e, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{def} ⟨e, ρ, END, C_{1} :: C_{2}⟩_{eval}

⟨Fx.e, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{def} ⟨e, ρ{x ↦ C_{1}}, END, C_{2}⟩_{eval}

⟨END, v, C_{2}⟩_{cont_{1}} ⇒_{def} ⟨C_{2}, v⟩_{cont_{2}}
⟨ARG ((e, ρ), C_{1}), v, C_{2}⟩_{cont_{1}} ⇒_{def} ⟨e, ρ, FUN (v, C_{1}), C_{2}⟩_{eval}

⟨FUN ([x, e, ρ], C_{1}), v, C_{2}⟩^{cont_{1}} ⇒_{def} ⟨e, ρ{x ↦ v}, C_{1}, C_{2}⟩_{eval}

⟨FUN (C′_{1}, C_{1}), v, C_{2}⟩_{cont_{1}} ⇒_{def} ⟨C′_{1} ⋆ C_{1}, v, C_{2}⟩_{cont_{1}}

⟨C_{1} :: C_{2}, v⟩_{cont_{2}} ⇒_{def} ⟨C_{1}, v, C_{2}⟩_{cont_{1}}
⟨nil, v⟩_{cont_{2}} ⇒_{def} v

Figure 1: The definitional call-by-value abstract machine for the λ-calculus extended with F and #

Figure 2 displays the new abstract machine for dynamic delimited continuations. It only differs from the definitional abstract machine in the way dynamic contexts are represented (a context and a trail of contexts (represented as a list) instead of one concatenated context). In Section 4, we establish the equivalence of the two machines.

In the new machine, the constructors of contexts are solely consumed in the cont_{1} transitions. Therefore the new machine, unlike the definitional machine, is in the range of defunctionalization [16]: it can be refunctionalized into a higher-order evaluator, which we present in Section 5.

• Values (closures and captured continuations): v ::= [x, e, ρ] | [C_{1}, T_{1}]

• Environments: ρ ::= ρ_{mt} | ρ{x ↦ v}

• Contexts: C_{1} ::= END | ARG ((e, ρ), C_{1}) | FUN (v, C_{1})

• Trail of contexts: T_{1} ::= nil | C_{1} :: T_{1}

• Meta-contexts: C_{2} ::= nil | (C_{1}, T_{1}) :: C_{2}

• Initial transition, transition rules, and final transition:

e

⇒_{adj}

⟨e, ρ_{mt}, END, nil, nil⟩_{eval}
⟨x, ρ, C_{1}, T_{1}, C_{2}⟩_{eval} ⇒_{adj} ⟨C_{1}, ρ(x), T_{1}, C_{2}⟩_{cont_{1}}
⟨λx.e, ρ, C_{1}, T_{1}, C_{2}⟩_{eval} ⇒_{adj} ⟨C_{1}, [x, e, ρ], T_{1}, C_{2}⟩_{cont_{1}}
⟨e_{0} e_{1}, ρ, C_{1}, T_{1}, C_{2}⟩_{eval} ⇒_{adj} ⟨e_{0}, ρ, ARG ((e_{1}, ρ), C_{1}), T_{1}, C_{2}⟩_{eval}

⟨#e, ρ, C_{1}, T_{1}, C_{2}⟩_{eval} ⇒_{adj} ⟨e, ρ, END, nil, (C_{1}, T_{1}) :: C_{2}⟩_{eval}

⟨Fx.e, ρ, C_{1}, T_{1}, C_{2}⟩_{eval} ⇒_{adj} ⟨e, ρ{x ↦ [C_{1}, T_{1}]}, END, nil, C_{2}⟩_{eval}

⟨END, v, T_{1}, C_{2}⟩_{cont_{1}} ⇒_{adj} ⟨T_{1}, v, C_{2}⟩_{trail_{1}}
⟨ARG ((e, ρ), C_{1}), v, T_{1}, C_{2}⟩_{cont_{1}} ⇒_{adj} ⟨e, ρ, FUN (v, C_{1}), T_{1}, C_{2}⟩_{eval}

⟨FUN ([x, e, ρ], C_{1}), v, T_{1}, C_{2}⟩^{cont_{1}} ⇒_{adj} ⟨e, ρ{x ↦ v}, C_{1}, T_{1}, C_{2}⟩_{eval}

⟨FUN ([C′_{1}, T′_{1}], C_{1}), v, T_{1}, C_{2}⟩_{cont_{1}} ⇒_{adj} ⟨C′_{1}, v, T′_{1} @ (C_{1} :: T_{1}), C_{2}⟩_{cont_{1}}

⟨nil, v, C_{2}⟩^{trail_{1}} ⇒_{adj} ⟨C_{2}, v⟩_{cont_{2}}

⟨C_{1} :: T_{1}, v, C_{2}⟩_{trail_{1}} ⇒_{adj} ⟨C_{1}, v, T_{1}, C_{2}⟩_{cont_{1}}
⟨(C_{1}, T_{1}) :: C_{2}, v⟩_{cont_{2}} ⇒_{adj} ⟨C_{1}, v, T_{1}, C_{2}⟩_{cont_{1}}
⟨nil, v⟩_{cont_{2}} ⇒_{adj} v

Figure 2: The adjusted call-by-value abstract machine for the λ-calculus extended with F and #

N.B.: The trail concatenation, in Figure 2, could be avoided by adding a new component to the machine—a meta-trail of pairs of contexts and trails, managed last-in, first-out—and the corresponding new transitions. A captured continuation would then be a triple of context, trail, and meta-trail, and applying it would require this meta-trail to be concatenated to the current trail. In turn, this concatenation could be avoided by adding a meta-meta-trail, etc. Because each of the meta^{n}-trails (for n ≥ 1) but the last one has one point of consumption, they all are in defunctionalized form except the last one. Adding meta^{n}-trails amounts to trading space for time.

4 Equivalence of the definitional machine and of the adjusted machine

We relate the configurations and transitions of the definitional abstract machine to those of the adjusted abstract machine. As a diacritical convention [44], we annotate the components, configurations, and transitions of the definitional machine with a tilde ( ˜ ·). In order to relate a dynamic context of the adjusted machine (a context and a trail of contexts) to a context of the definitional machine, we convert it into a context of the adjusted machine:

Definition 1. We define an operation ˆ⋆, concatenating a context and a trail of contexts, by induction on its second argument:

C_{1} ˆ⋆ nil =^{def} C_{1}
C_{1} ˆ⋆ (C′_{1} :: T_{1}) =^{def} C_{1} ⋆ (C′_{1} ˆ⋆ T_{1})

Proposition 2. C_{1} ˆ⋆ (C′_{1} :: T_{1}) = (C_{1} ⋆ C′_{1}) ˆ⋆ T_{1},

Proof. Follows from Definition 1 and from the associativity of ⋆ (Proposition 1(2)).

Proposition 3. (C_{1} ˆ⋆ T_{1}) ˆ⋆ T′_{1} = C_{1} ˆ⋆ (T_{1} @ T′_{1}).

Proof. By induction on the structure of T_{1}.

Definition 2. We relate the definitional abstract machine and the adjusted abstract machine with the following family of relations ≃:

Terms: ẽ ≃_{e} e iff ẽ = e

Values: (a) [x̃, ẽ, ρ̃] ≃_{v} [x, e, ρ] iff x̃ = x, ẽ ≃_{e} e and ρ̃ ≃_{env} ρ (b) C̃_{1} ≃_{v} [C_{1}, T_{1}] iff C̃_{1} ≃_{c} C_{1} ˆ⋆ T_{1}

Environments: (a) ρ̃_{mt} ≃_{env} ρ_{mt} (b) ρ̃{x̃ ↦ ṽ} ≃_{env} ρ{x ↦ v} iff x̃ = x, ṽ ≃_{v} v and ρ̃\ {x̃} ≃_{env} ρ \ {x}, where ρ \ {x} denotes the restriction of ρ to its domain excluding x

Contexts: (a) ẼND ≃_{c} END (b) ÃRG ((ẽ, ρ̃), C̃_{1}) ≃_{c} ARG ((e, ρ), C_{1}) iff ẽ ≃_{e} e, ρ̃ ≃_{env} ρ, and C̃_{1} ≃_{c} C_{1} (c) F̃UN (ṽ, C̃_{1}) ≃_{c} FUN (v, C_{1}) iff ṽ ≃_{v} v and C̃_{1} ≃_{c} C_{1}

Meta-contexts: (a) ñil ≃_{mc} nil (b) C̃_{1} :: C̃_{2} ≃_{mc} (C_{1}, T_{1}) :: C_{2} iff C̃_{1} ≃_{c} C_{1} ˆ⋆ T_{1} and C̃_{2} ≃_{mc} C_{2}

Configurations: (a) ⟨ẽ, ρ̃, C̃_{1}, C̃_{2}⟩ẽval ≃ ⟨e, ρ, C_{1}, T_{1}, C_{2}⟩_{eval} iff ẽ ≃_{e} e, ρ̃ ≃_{env} ρ, C̃_{1} ≃_{c} C_{1} ˆ⋆ T_{1}, and C̃_{2} ≃_{mc} C_{2} (b) ⟨C̃_{1}, ṽ, C̃_{2}⟩{ \atop cont_{1}} ≃ ⟨C_{1}, v, T_{1}, C_{2}⟩_{cont_{1}} iff C̃_{1} ≃_{c} C_{1} ˆ⋆ T_{1}, ṽ ≃_{v} v, and C̃_{2} ≃_{mc} C_{2} (c) ⟨C̃_{2}, ṽ⟩{ \atop cont_{2}} ≃ ⟨C_{2}, v⟩_{cont_{2}} iff C̃_{2} ≃_{mc} C_{2} and ṽ ≃_{v} v

By writing δ ⇒^{∗} δ′ and δ ⇒^{+} δ′, we mean that there is respectively zero or more and one or more transitions leading from the configuration δ to the configuration δ′. Definition 3. The partial evaluation functions eval_{def} and eval_{adj} mapping terms to values are defined as follows:

(1) eval_{def} (ẽ) = ṽ if and only if ⟨ẽ, ρ̃_{mt}, ẼND, ñil⟩ẽval ⇒_{def}^{+} ⟨ñil, ṽ⟩{ \atop cont_{2}};

(2) eval_{adj} (e) = v if and only if ⟨e, ρ_{mt}, END, nil, nil⟩_{eval} ⇒_{adj}^{+} ⟨nil, v⟩_{cont_{2}} . We want to prove that eval_{def} and eval_{adj} are defined on the same programs (i.e., closed

terms), and that for any given program, they yield equivalent values. Theorem 1 (Equivalence). For any programs ẽ and e such that ẽ ≃_{e} e (i.e., ẽ = e), eval_{def} (ẽ) = ṽ for some value ṽ if and only if eval_{adj} (e) = v for some value v such that ṽ ≃_{v} v.

Proving Theorem 1 requires proving the following lemmas. Lemma 1. If C̃_{1} ≃_{c} C_{1} and C̃′_{1} ≃_{c} C′_{1} then C̃_{1} ˜⋆ C̃′_{1} ≃_{c} C_{1} ⋆ C′_{1}. Proof. By induction on the structure of C̃_{1}.

The following lemma addresses the configurations of the adjusted abstract machine that break the one-to-one correspondence with the definitional abstract machine. Lemma 2. If δ = ⟨END, v, T_{1}, C_{2}⟩_{cont_{1}} then

(1) if T_{1} = \underbrace{END :: …:: END}_{n} :: nil, where n ≥ 0, then δ ⇒_{adj}^{+} ⟨C_{2}, v⟩_{cont_{2}} ;

(2) if T_{1} = \underbrace{END :: …:: END}_{n} :: C_{1} :: T′_{1}, where n ≥ 0 and C_{1} ≠ END, then δ ⇒_{adj}^{+} ⟨C_{1}, v, T′_{1}, C_{2}⟩_{cont_{1}} .

Proof. By induction on n.

The following key lemma relates single transitions of the two abstract machines. Lemma 3. If δ̃ ≃ δ then

(1) if δ̃ ⇒_{def} δ̃′ then there exists a configuration δ′ such that δ ⇒_{adj}^{+} δ′ and δ̃′ ≃ δ′;

(2) if δ ⇒_{adj} δ′ then there exist configurations δ̃′ and δ′′ such that δ̃ ⇒_{def} δ̃′, δ′ ⇒_{adj}^{∗} δ′′ and δ̃′ ≃ δ′′.

Proof. By case analysis of δ̃ ≃ δ. Most of the cases follow directly from the definition of the relation ≃. We show the proof of one such case: Case: δ̃ = ⟨x̃, ρ̃, C̃_{1}, C̃_{2}⟩ẽval and δ = ⟨x, ρ, C_{1}, T_{1}, C_{2}⟩_{eval} From the definition of the definitional abstract machine, δ̃ ⇒_{def} δ̃′, where δ̃′ = ⟨C̃_{1}, ρ̃(x̃), C̃_{2}⟩{ \atop cont_{1}}. From the definition of the adjusted abstract machine, δ ⇒_{adj} δ′, where δ′ = ⟨C_{1}, ρ(x), T_{1}, C_{2}⟩_{cont_{1}} . By assumption, ρ̃(x̃) ≃_{v} ρ(x), C̃_{1} ≃_{c} C_{1} ˆ⋆ T_{1} and C̃_{2} ≃_{mc} C_{2}. Hence, δ̃′ ≃ δ′ and both directions of Lemma 3 are proved in this case.

There are only three interesting cases. One of them arises when a captured continuation is applied, and the remaining two explain why the two abstract machines do not operate in lockstep:

Case: δ̃ = ⟨F̃UN (C̃′_{1}, C̃_{1}), ṽ, C̃_{2}⟩{ \atop cont_{1}} and δ = ⟨FUN ([C′_{1}, T′_{1}], C_{1}), v, T_{1}, C_{2}⟩_{cont_{1}}

From the definition of the definitional abstract machine, δ̃ ⇒_{def} δ̃′, where δ̃′ = ⟨C̃′_{1} ˜⋆ C̃_{1}, ṽ, C̃_{2}⟩{ \atop cont_{1}}. From the definition of the adjusted abstract machine, δ ⇒_{adj} δ′, where δ′ = ⟨C′_{1}, v, T′_{1} @ (C_{1} :: T_{1}), C_{2}⟩_{cont_{1}} . By assumption, C̃′_{1} ≃_{c} C′_{1} ˆ⋆ T′_{1} and C̃_{1} ≃_{c} C_{1} ˆ⋆ T_{1}. By Lemma 1, we have C̃′_{1} ˜⋆ C̃_{1} ≃_{c} (C′_{1} ˆ⋆ T′_{1}) ⋆ (C_{1} ˆ⋆ T_{1}). By the definition of ˆ⋆, (C′_{1} ˆ⋆ T′_{1}) ⋆ (C_{1} ˆ⋆ T_{1}) = (C′_{1} ˆ⋆ T′_{1}) ˆ⋆ (C_{1} :: T_{1}). By Proposition 3, (C′_{1} ˆ⋆ T′_{1}) ˆ⋆ (C_{1} :: T_{1}) = C′_{1} ˆ⋆ (T′_{1} @ (C_{1} :: T_{1})). Since ṽ ≃_{v} v and C̃_{2} ≃_{mc} C_{2}, we infer that δ̃′ ≃ δ′ and both directions of Lemma 3 are proved in this case.

Case: δ̃ = ⟨ẼND, ṽ, C̃_{2}⟩{ \atop cont_{1}} and δ = ⟨END, v, T_{1}, C_{2}⟩_{cont_{1}}

From the definition of the definitional abstract machine, δ̃ ⇒_{def} δ̃′, where δ̃′ = ⟨C̃_{2}, ṽ⟩{ \atop cont_{2}}.

By the definition of ≃, ṽ ≃_{v} v, C̃_{2} ≃_{mc} C_{2}, and ẼND ≃_{c} END ˆ⋆ T_{1}. Hence, it follows from the definition of ≃_{c} that END ˆ⋆ T_{1} = END, which is possible only when T_{1} = \underbrace{END :: …:: END}_{n} :: nil for some n ≥ 0.

Then by Lemma 2(1), δ ⇒_{adj}^{+} δ′, where δ′ = ⟨C_{2}, v⟩_{cont_{2}} and δ̃′ ≃ δ′, and both directions of the lemma are proved in this case.

Case: δ̃ = ⟨C̃_{1}, ṽ, C̃_{2}⟩{ \atop cont_{1}} and δ = ⟨END, v, T_{1}, C_{2}⟩_{cont_{1}} , where C̃_{1} ≠ ẼND

By the definition of ≃, ṽ ≃_{v} v, C̃_{2} ≃_{mc} C_{2}, and C̃_{1} ≃_{c} END ˆ⋆ T_{1}. Hence, it follows from the definition of ≃_{c} that END ˆ⋆ T_{1} ≠ END, which is possible only when T_{1} = \underbrace{END :: …:: END}_{n} :: C_{1} :: T′_{1} for some n ≥ 0 and C_{1} ≠ END.

Then by Lemma 2(2), δ ⇒_{adj}^{+} δ′, where δ′ = ⟨C_{1}, v, T′_{1}, C_{2}⟩_{cont_{1}} , C_{1} ≠ END, and since END ˆ⋆ T_{1} = C_{1} ˆ⋆ T′_{1}, we have δ̃ ≃ δ′. By one of the trivial cases for δ̃ ≃ δ′ (not shown in the proof), both directions of the lemma are proved in this case.

Given the relation between single-step transitions of the two abstract machines, it is straightforward to generalize it to the relation between their multi-step transitions.

Lemma 4. If δ̃ ≃ δ then

(1) if δ̃ ⇒_{def}^{+} δ̃′ then there exists a configuration δ′ such that δ ⇒_{adj}^{+} δ′ and δ̃′ ≃ δ′;

(2) if δ ⇒_{adj}^{+} δ′ then there exist configurations δ̃′ and δ′′ such that δ̃ ⇒_{def}^{+} δ̃′, δ′ ⇒_{adj}^{∗} δ′′ and δ̃′ ≃ δ′′.

Proof. Both directions follow from Lemma 3 by induction on the number of transitions.

We are now in position to prove the equivalence theorem.

Proof of Theorem 1. The initial configuration of the definitional abstract machine, i.e., ⟨ẽ, ρ̃_{mt}, ẼND, ñil⟩ẽval, and the initial configuration of the adjusted abstract machine, i.e., ⟨e, ρ_{mt}, END, nil, nil⟩_{eval}, are in the relation ≃ when ẽ = e. Therefore, if the definitional abstract machine reaches the final configuration ⟨ñil, ṽ⟩{ \atop cont_{2}}, then by Lemma 4(1), there is

a configuration δ′ such that δ ⇒_{adj}^{+} δ′ and δ̃′ ≃ δ′. By the definition of ≃, δ′ must be ⟨nil, v⟩_{cont_{2}} , with ṽ ≃_{v} v. The proof of the converse direction follows similar steps.

5 The evaluator corresponding to the adjusted machine

The raison d’être of the adjusted abstract machine is that it is in defunctionalized form. Refunctionalizing its contexts and meta-contexts yields the higher-order evaluator of Figure 3. This evaluator is compositional, i.e., the recursive calls on each right-hand side are over a proper sub-term of the corresponding left-hand side. The evaluator is expressed in a continuation+state-passing style where the state consists of a trail of continuations and a meta-continuation. Defunctionalizing it gives the abstract machine of Figure 2. Since this continuation+state-passing style came into being to account for dynamic delimited continuations, we refer to it as a ‘dynamic continuation-passing style’ (dynamic CPS).

6 The CPS transformer corresponding to the evaluator in dynamic CPS

The dynamic CPS transformer corresponding to the evaluator of Figure 3 can be immediately obtained as the associated syntax-directed encoding into the term model of the meta-language (using fresh variables):

⟦x⟧ = λ(k_{1}, t_{1}, k_{2}).k_{1} (x, t_{1}, k_{2})
⟦λx.e⟧ = λ(k_{1}, t_{1}, k_{2}).k_{1} (λ(x, k_{1}, t_{1}, k_{2}). ⟦e⟧ (k_{1}, t_{1}, k_{2}), t_{1}, k_{2})
⟦e_{0} e_{1}⟧ = λ(k_{1}, t_{1}, k_{2}).⟦e_{0}⟧ (λ(v_{0}, t_{1}, k_{2}). ⟦e_{1}⟧ (λ(v_{1}, t_{1}, k_{2}). v_{0} (v_{1}, k_{1}, t_{1}, k_{2}), t_{1}, k_{2}), t_{1}, k_{2})
⟦#e⟧ = λ(k_{1}, t_{1}, k_{2}).⟦e⟧ (θ_{1}, nil, λv. k_{1} (v, t_{1}, k_{2}))
⟦Fx.e⟧ = λ(k_{1}, t_{1}, k_{2}).let x = λ(v, k′_{1}, t′_{1}, k_{2}). k_{1} (v, t_{1} @ (k′_{1} :: t′_{1}), k_{2}) in ⟦e⟧ (θ_{1}, nil, k_{2})

A transformed term is evaluated by supplying an initial continuation, trail, and metacontinuation as follows: ⟦e⟧ (θ_{1}, nil, θ_{2}), where θ_{1} and θ_{2} are defined in Figure 3. As usual, this initialization is equivalent to delimiting control in the translated term.

It is straightforward to write a one-pass version of the dynamic CPS transformer [19].

An example: In our earlier work [8, Section 2.5], we presented a simple example where using control and prompt led to one result and using shift and reset led to another. We displayed the CPS counterpart of the latter and stated that no such simple functional encoding existed for the former. Dynamic CPS, however, provides such a functional encoding. The example reads as follows:

     fun test ()
         = prompt (fn () => control (fn k => 10 + (k 100)) + control (fn k' => 1))

Applying test to () yields 1 since the second occurrence of control wipes out the entire delimited evaluation context. Its shift and reset counterpart yields 11 since the second occurrence of control only wipes out the evaluation context up to the application of k to 100.

• Terms: Exp ∋ e ::= x | λx.e | e_{0} e_{1} | #e | Fx.e

• Values, continuations, meta-continuations, and trails of continuations:

v ∈ Val = Val × Cont_{1} × Trail_{1} × Cont_{2} → Val
θ_{1}, k_{1} ∈ Cont_{1} =  Val × Trail_{1} × Cont_{2} → Val
θ_{2}, k_{2} ∈ Cont_{2} =  Val → Val
t_{1} ∈ Trail_{1} = List(Cont_{1})

• Environments: Env ∋ ρ ::= ρ_{mt} | ρ{x ↦ v}

• Initial continuation: θ_{1} = λ(v, t_{1}, k_{2}). case t_{1} of nil ⇒ k_{2} v | k_{1} :: t′_{1} ⇒ k_{1} (v, t′_{1}, k_{2})

• Initial meta-continuation: θ_{2} = λv. v

• Evaluation function: eval : Exp × Env × Cont_{1} × Trail_{1} × Cont_{2} → Val

eval_{dcps} (x, ρ, k_{1}, t_{1}, k_{2}) = k_{1} (ρ(x), t_{1}, k_{2})
eval_{dcps} (λx.e, ρ, k_{1}, t_{1}, k_{2}) = k_{1} (λ(v, k_{1}, t_{1}, k_{2}). eval_{dcps} (e, ρ{x ↦ v}, k_{1}, t_{1}, k_{2}), t_{1}, k_{2})
eval_{dcps} (e_{0} e_{1}, ρ, k_{1}, t_{1}, k_{2}) = eval_{dcps} (e_{0}, ρ, λ(v_{0}, t_{1}, k_{2}). eval_{dcps} (e_{1}, ρ, λ(v_{1}, t_{1}, k_{2}). v_{0} (v_{1}, k_{1}, t_{1}, k_{2}), t_{1}, k_{2}), t_{1}, k_{2})
eval_{dcps} (#e, ρ, k_{1}, t_{1}, k_{2}) = eval_{dcps} (e, ρ, θ_{1}, nil, λv. k_{1} (v, t_{1}, k_{2}))
eval_{dcps} (Fx.e, ρ, k_{1}, t_{1}, k_{2}) = eval_{dcps} (e, ρ{x ↦ λ(v, k′_{1}, t′_{1}, k_{2}). k_{1} (v, t_{1} @ (k′_{1} :: t′_{1}), k_{2})}, θ_{1}, nil, k_{2})

• Main function: evaluate : Exp → Val

evaluate_{dcps} (e) = eval_{dcps} (e, ρ_{mt}, θ_{1}, nil, θ_{2})

Figure 3: A call-by-value evaluator for the λ-calculus extended with F and # 9

The dynamic CPS transformation yields the following program, which we write in the syntax of ML:

     datatype ('a, 'b) cont1 = CONT1 of 'a * 'b trail1 * 'b cont2 -> 'b
     withtype 'a trail1 = ('a, 'a) cont1 list
          and 'a cont2 = 'a -> 'a
     (*  theta1 : 'a * ('a, 'a) trail1 * 'a cont2 -> 'a  *)
     fun theta1 (v, nil, k2)
         = k2 v
       | theta1 (v, (CONT1 k1) :: t1, k2)
         = k1 (v, t1, k2)
     (*  theta2 : 'a cont2  *)
     fun theta2 v
         = v
     fun test_dcps () (k1, t1, k2)
         = let fun k (v, k1', t1', k2)
                   = let fun k' (v', k1'', t1'', k2)
                             = k1 (v + v', t1' @ (k1'' :: t1''), k2)
                     in theta1 (1, nil, k2)
                     end
           in k (100, CONT1 (fn (v, t1, k2) => theta1 (10 + v, t1, k2)), nil, k2)
           end

or again, unfolding the two let expressions and inlining theta1:

     fun test_dcps () (k1, t1, k2)
         = k2 1

The initial call is test dcps () (theta1, nil, theta2). In our experience, out-of-the-box dynamic CPS programs are rarely enlightening the way normal CPS programs (at least after some practice) tend to be. However, again in our experience, a combination of simplifications (e.g., inlining theta1 in the example just above) and defunctionalization often clarifies the intent and the behavior of the original direct-style program. We illustrate this point in Section 8.

7 The direct-style evaluator corresponding to the evaluator in dynamic CPS

Figure 4 shows a direct-style evaluator for the λ-calculus extended with F and # written in a meta-language enriched with F and #.

The following coherence property holds. Transforming this direct-style evaluator into dynamic continuation-passing style, using the one-pass version of the dynamic CPS transformer of Section 6, yields the evaluator of Figure 3. Earlier on [18, Section 2], Danvy and Filinski have shown that a similar coherence property holds for static delimited continuations: CPS-transforming a direct-style evaluator for the λ-calculus extended with shift and reset written in a meta-language extended with shift and reset yields the definitional interpreter for the λ-calculus extended with shift and reset. (In the same spirit, Danvy and Lawall have transformed into direct style a continuation-passing evaluator for the λ-calculus extended with call/cc, obtaining a traditional direct-style evaluator interpreting call/cc with call/cc [20, Section 1.2.1].)

• Terms: Exp ∋ e ::= x | λx.e | e_{0} e_{1} | #e | Fx.e

• Values: v ∈ Val = Val → Val

• Environments: Env ∋ ρ ::= ρ_{mt} | ρ{x ↦ v}

• Evaluation function: eval : Exp × Env → Ans

eval_{ds} (x, ρ) = ρ(x)
eval_{ds} (λx.e, ρ) = λv. eval_{ds} (e, ρ{x ↦ v})
eval_{ds} (e_{0} e_{1}, ρ) = eval_{ds} (e_{0}, ρ) (eval_{ds} (e_{1}, ρ))
eval_{ds} (#e, ρ) = #(eval_{ds} (e, ρ))
eval_{ds} (Fx.e, ρ) = Fv.eval_{ds} (e, ρ{x ↦ v})

• Main function: evaluate : Exp → Val

evaluate_{ds} (e) = eval_{ds} (e, ρ_{mt})

Figure 4: A direct-style evaluator for the λ-calculus extended with F and #

8 Static and dynamic continuation-passing style

Biernacka, Biernacki, and Danvy have recently presented the following simple example to contrast the effects of shift and of control [4, Section 4.6]. We write it below in ML, using Filinski’s implementation of shift and reset [32] shown in Appendix C, and using the implementation of control and prompt presented in Section 10. In both cases, the type of the intermediate answers is int list:

(*  foo : int list -> int list  *)          (*  bar : int list -> int list  *)
fun foo xs                                  fun bar xs
    = let fun visit nil                         = let fun visit nil
              = nil                                       = nil
            | visit (x :: xs)                           | visit (x :: xs)
              = visit                                     = visit
                 (shift                                      (control
                    (fn k => x :: (k xs)))                     (fn k => x :: (k xs)))
      in reset (fn () => visit xs)                in prompt (fn () => visit xs)
      end                                         end

The two functions traverse their input list recursively, and construct an output list. They only differ in that to abstract the recursive call to visit into a delimited continuation, foo uses shift and reset whereas bar uses control and prompt. This seemingly minor difference has a major effect since it makes foo behave as a list-copying function and bar as a list-reversing function.

To illustrate this difference of behavior, Biernacka, Biernacki, and Danvy have used contexts and meta-contexts [4, Section 4.6], and Biernacki and Danvy have used an intuitive source representation of the successive contexts [7, Section 2.3]: given the list [1,2,3], the captured delimited continuation in foo is always fn v => visit v, whereas for bar, it is suc-

cessively fn v => visit v, fn v => 1 :: (visit v), fn v => 2 :: 1 :: (visit v), and fn v

=> 3 :: 2 :: 1 :: (visit v), making it clear that foo copies its argument whereas bar reverses it. In this section, we use static and dynamic continuation-passing style to illustrate the difference of behavior.

8.1 Static continuation-passing style

Applying the canonical CPS transformation for shift and reset [18] to the definition of foo yields the following purely functional program:

     fun foo_scps xs
         = let fun visit (nil, k1, k2)
                   = k1 (nil, k2)
                 | visit (x :: xs, k1, k2)
                   = let fun k (v, k1', k2')
                             = visit (v, k1, fn v => k1' (v, k2'))
                     in k (xs, fn (v, k2) => k2 (x :: v), k2)
                     end
           in visit (xs, fn (v, k2) => k2 v, fn v => v)
           end

Inlining k and k1' and lambda-dropping k1 [24] and then inlining it yields the following simpler program:

     fun foo_scps_simplified xs
         = let fun visit (nil, k2)
                   = k2 nil
                 | visit (x :: xs, k2)
                   = visit (xs, fn v => k2 (x :: v))
           in visit (xs, fn v => v)
           end

Defunctionalizing k2 into a list yields the following first-order program:

     fun foo_scps_defunct xs
         = let fun visit (nil, k2)
                   = continue (k2, nil)
                 | visit (x :: xs, k2)
                   = visit (xs, x :: k2)
               and continue (nil, v)
                   = v
                 | continue (x :: k2, v)
                   = continue (k2, x :: v)
           in visit (xs, nil)
           end

These successive equivalent views make it increasingly clearer that the program copies its input list by first reversing it using the meta-continuation as an accumulator (in visit), and then by reversing the accumulator (in continue).

8.2 Dynamic continuation-passing style

Applying the dynamic CPS transformation for control and prompt (Section 6) to the definition of bar yields the following purely functional program:

     datatype ('a, 'b) cont1 = CONT1 of 'a * 'b trail1 * 'b cont2 -> 'b
     withtype 'a trail1 = ('a, 'a) cont1 list
          and 'a cont2 = 'a -> 'a

fun theta1 (v, nil, k2)
= k2 v
| theta1 (v, (CONT1 k1) :: t1, k2)
= k1 (v, t1, k2)
fun theta2 v
= v
fun bar_dcps xs
= let fun visit (nil, k1, t1, k2)
= k1 (nil, t1, k2)
| visit (x :: xs, k1, t1, k2)
= let fun k (v, k1', t1', k2)
          = visit (v, k1, t1 @ (k1' :: t1'), k2)
  in k (xs, CONT1 (fn (v, t1, k2) => theta1 (x :: v, t1, k2)),
        nil, k2)
  end
in visit (xs, theta1, nil, theta2)
end

Inlining k, lambda-dropping k1 and k2 and then inlining them, defunctionalizing the continuation into the ML option type, and using an auxiliary function continue aux to interpret the trail, yields the following first-order program:

fun bar_dcps_defunct xs
= let fun visit (nil, t1)
= continue (NONE, nil, t1)
| visit (x :: xs, t1)
= visit (xs, t1 @ ((SOME x) :: nil))
and continue (NONE, v, t1)
= continue_aux (t1, v)
| continue (SOME x, v, t1)
= continue (NONE, x :: v, t1)
and continue_aux (nil, v)
= v
| continue_aux (k1 :: t1, v)
= continue (k1, v, t1)
in visit (xs, nil)
end

Further simplifications (essentially inlining the calls to continue) lead one to the following program:

fun bar_dcps_defunct_simplified xs
= let fun visit (nil, t1)
= continue_aux (t1, nil)
| visit (x :: xs, t1)
= visit (xs, t1 @ (x :: nil))
and continue_aux (nil, v)
= v
| continue_aux (k1 :: t1, v)
= continue_aux (t1, k1 :: v)
in visit (xs, nil)
end

These successive equivalent views make it increasingly clearer that the program reverses its input list by first copying it to the trail through a series of concatenations (with visit), and then by reversing the trail (with continue aux).

8.3 A generalization

Let us briefly generalize the programming pattern above from lists to binary trees:

     datatype tree = EMPTY
                   | NODE of tree * int * tree

In the following two definitions, the type of the intermediate answers is int list:

• Here, the two recursive calls to visit are abstracted into a static delimited continuation

     using shift and reset:
          fun traverse_sr t
              = let fun visit (EMPTY, a)
                        = a
                      | visit (NODE (t1, i, t2), a)
                        = visit (t1, visit (t2, shift (fn k => i :: (k a))))
                in reset (fn () => visit (t, nil))
                end

• Here, the two recursive calls to visit are abstracted into a dynamic delimited continuation using control and prompt:

          fun traverse_cp t
              = let fun visit (EMPTY, a)
                        = a
                      | visit (NODE (t1, i, t2), a)
                        = visit (t1, visit (t2, control (fn k => i :: (k a))))
                in prompt (fn () => visit (t, nil))
                end

The static delimited continuations yield a preorder and right-to-left traversal, whereas the dynamic delimited continuation yield a postorder and left-to-right traversal. The resulting two lists are reverse of each other.

Again, CPS transformation and defunctionalization yield first-order programs whose behavior is more patent.

8.4 Further examples

We now turn to the lazy depth-first and breadth-first traversals recently presented by Biernacki, Danvy, and Shan [8]. To support laziness, they used the following signature of generators:

     signature GENERATOR
     = sig
         type 'a computation
         datatype sequence = END
                           | NEXT of int * sequence computation
         val make_sequence : tree -> sequence
         val compute : sequence computation -> sequence
       end

The following generator is parameterized by a scheduler that is given four commands (i.e., unit-yieldings thunks) to be applied in turn. The functor make Control and Prompt is defined in Section 10.

     signature SCHEDULER
     = sig
         type command = unit -> unit
         val schedule : command * command * command * command -> unit
       end
     functor make_Lazy_Generator (S : SCHEDULER) : GENERATOR
     = struct
         datatype sequence = END
                           | NEXT of int * sequence computation
         withtype 'a computation = unit -> 'a
         structure CP = make_Control_and_Prompt (type answer = sequence)
         (*  visit : tree -> unit *)
         fun visit EMPTY
             = ()
           | visit (NODE (t1, i, t2))
             = CP.control
                 (fn k =>
                    let val () = S.schedule
                                   (fn () => visit t1,
                                    fn () => CP.control (fn k' => NEXT (i, k')),
                                    fn () => visit t2,
                                    fn () => let val _= k () in () end)
                    in END
                    end)
         (*  make_sequence : tree -> sequence  *)
         fun make_sequence t
             = CP.prompt (fn () => let val () = visit t
                                   in END
                                   end)
         (*  compute : sequence computation -> sequence  *)
         fun compute k
             = CP.prompt (fn () => k ())
       end

The relative scheduling of the first and third commands determines whether the traversal of the input tree is from left to right or from right to left. The relative scheduling of the second command with respect to the first and the third determines whether the traversal is preorder, inorder, or postorder. The relative scheduling of the fourth command determines whether the traversal is depth-first, breadth-first, or a mix of both.

In each case, dynamic CPS transformation and defunctionalization yield first-order programs whose behavior is patent in that the depth-first traversal uses a stack, the breadth-first traversal uses a queue, and the mixed traversal uses a queue to hold the right (respectively the left) subtrees while visiting the left (respectively the right) ones.

9 A monad for dynamic continuation-passing style

The evaluator of Figure 3 is compositional, and has the following type:

Exp × Env × Cont_{1} × Trail_{1} × Cont_{2} → Val

Let us curry and map the evaluator to direct style with respect to the meta-continuation [12]. The type signature of the resulting evaluator eval′_{dcps} is as follows:

Exp × Env → Cont_{1} → Trail_{1} → Val

where

Cont_{1} = Val → Trail_{1} → Val
Val = Val → Cont_{1} → Trail_{1} → Val
Trail_{1} = List(Cont_{1})

In all clauses of the evaluator but the one defining prompt, the direct-style transformation consists of eliminating the meta-continuation, whereas the new clause defining prompt is transformed into continuation-composing style [18]:

eval′_{dcps} (#e, ρ) k_{1} t_{1} = k_{1} (eval′_{dcps} (e, ρ) θ nil) t_{1}

The initial continuation also is transformed:

θ_{1} = λv. λt_{1}. case t_{1} of nil ⇒ v | k′_{1} :: t′_{1} ⇒ k′_{1} v t′_{1}

The new evaluator operates on values only of one type Val, so in order to exhibit the general notion of computation dynamic CPS induces, we abstract both the argument type (α) and the final answer type (o) of continuations and we introduce the following type constructor [45,55]:

D(α) = Cont_{1}(α) → Trail_{1} → o

where

Cont_{1}(α) = α → Trail_{1} → o
Trail_{1} = List(Cont_{1}(o))

We observe that for a fixed type o, D can be expressed as follows:

D(α) = (α → Ans) → Ans

where

Ans = List(o → Ans) → o

Therefore, the notion of computation induced by dynamic CPS takes the form of the continuation monad with the recursive answer type Ans (which confirms Shan’s point that a static simulation of dynamic continuations requires a recursive answer type [52]), the type constructor D, and the usual continuation monad operations unit and bind:

unit : α → D(α)
unit v = λk. k v
bind : D(α) → (α → D(β)) → D(β)
bind c f = λk. c (λv. f v k)

Having identified the monad for dynamic continuation-passing style, we are now in position to define control and prompt as operations in this monad:

• Values: v ∈ Val = Val → D(Val)

• Environments: Env ∋ ρ ::= ρ_{mt} | ρ{x ↦ v}

• Evaluation function: eval : Exp × Env → D(Val)

eval_{mon} (x, ρ) = unit (ρ(x))
eval_{mon} (λx.e, ρ) = unit (λv. eval_{mon} (e, ρ{x ↦ v}))
eval_{mon} (e_{0} e_{1}, ρ) = bind (eval_{mon} (e_{0}, ρ)) (λv_{0}. bind (eval_{mon} (e_{1}, ρ)) (λv_{1}. v_{0} v_{1})))
eval_{mon} (#e, ρ) = prompt (eval_{mon} (e, ρ))
eval_{mon} (Fx.e, ρ) = control (λv. eval_{mon} (e, ρ{x ↦ v}))

• Main function: evaluate : Exp → Val

evaluate_{mon} (e) = run (eval_{mon} (e, ρ_{mt}))

Figure 5: A monadic evaluator for the λ-calculus extended with F and #

Definition 4. We define the monad operations control, prompt and run as follows:

control : ((α → D(o)) → D(o)) → D(α)
control f = λk_{1}. λt_{1}. let x = λv. λk′_{1}. λt′_{1}. k_{1} v (t_{1} @ (k′_{1} :: t′_{1})) in f x θ_{1} nil
prompt : D(o) → D(o)
prompt c = λk_{1}. λt_{1}. k_{1} (c θ_{1} nil) t_{1}
run : D(o) → o
run c = c θ_{1} nil

We can now extend the usual call-by-value monadic evaluator for the λ-calculus to F and # by taking α = o = Val (see Figure 5). Inlining the abstraction layer provided by the monad yields the evaluator eval′_{dcps}, and uncurrying and CPS-transforming the evaluator eval′_{dcps} yields the evaluator of Figure 3. Dynamic continuation-passing style therefore fits the functional correspondence between evaluators and abstract machines advocated by the first two authors [1–3,6,14,15]. Furthermore, and as has been observed before for other CPS transformations and for the continuation monad [36, 55], the dynamic CPS transformation itself can be factored through Moggi’s monadic metalanguage and the monad above.

The monad presented in this section determines a simple type system that accounts for dynamic delimited-control operators, where, for a fixed type o, control and prompt have the following type signatures:

control : ((α → o) → o) → α

                        prompt : o → o

This type system is expressive enough to type most of the existing programming examples and makes it possible to implement control and prompt in ML (see Section 10). It requires, however, that the answer type of each delimited continuation be the same as the final answer type of the entire program. In order to obtain more liberal and expressive type systems for dynamic continuations, we could follow Wadler [56] and parameterize the monad by intermediate answer types. Allowing for one additional type parameter would yield a typeand-effect system à la Murthy [47], whereas allowing for two additional type parameters would yield a type-and-effect system à la Danvy and Filinski [17].

10 A new implementation of control and prompt

The operations control and prompt in the continuation monad can be implemented in direct style in terms of shift and reset. In direct style, we use the monadic reflection operators reify and reflect to convert between implicit and explicit representations of computations [32]. They have types:

reify : (unit → α) → D(α)
reflect : D(α) → α

The reify operator takes a computation (represented as a thunk in call by value) that may have implicit effects and coerces it into an effect-free value that represents those effects. The reflect operator takes an effect-free value and coerces it into a computation, performing the effects represented by the value.

We insert occurrences of reify and reflect in the definitions of control and prompt from Section 9 guided by the types: we reify a computation that possibly has control effects in order to explicitly apply it to a continuation, and we reflect pure functional values that expect a continuation. Since our implementation language is a call-by-value functional language, we require the argument to prompt (a computation which may have control effects) to be a thunk:

control : ((α → o) → o) → α
control f = reflect λk_{1}. λt_{1}. let x = λv. reflect λk′_{1}. λt′_{1}. k_{1} v (t_{1} @ (k′_{1} :: t′_{1})) in reify (λ(). f x) θ_{1} nil
prompt : (unit → o) → o
prompt c = reflect λk_{1}. λt_{1}. k_{1} (reify c θ_{1} nil) t_{1}

Since control and prompt are operations in the continuation monad, we use the definitions of reify and reflect for the continuation monad [33]:^{2}

reify c = λk. reset λ(). k (c ())
reflect f = shift f

We obtain definitions of control and prompt in terms of shift and reset by inlining the occurrences of reify and reflect and simplifying:

control f = {definition of control}
reflect λk_{1}. λt_{1}. let x = λv. reflect λk′_{1}. λt′_{1}. k_{1} v (t_{1} @ (k′_{1} :: t′_{1})) in reify (λ(). f x) θ_{1} nil
= {definition of reify and reflect}
shift λk_{1}. λt_{1}. let x = λv. shift λk′_{1}. λt′_{1}. k_{1} v (t_{1} @ (k′_{1} :: t′_{1})) in (λk. reset λ(). k ((λ(). f x) ())) θ_{1} nil
= {two β_{v}-reductions}
shift λk_{1}. λt_{1}. let x = λv. shift λk′_{1}. λt′_{1}. k_{1} v (t_{1} @ (k′_{1} :: t′_{1})) in reset (λ(). θ_{1} (f x)) nil

prompt c = {definition of prompt}
reflect λk_{1}. λt_{1}. k_{1} (reify c θ_{1} nil) t_{1}
= {definition of reify and reflect}
shift λk_{1}. λt_{1}. k_{1} ((λk. reset λ(). k (c ())) θ_{1} nil) t_{1}

2The definitions given here for reify and reflect are simplifications of the ones given in Filinski’s dissertation [33, page 82]. They are obtained by erasing the level tags and then simplifying according to standard call-by-value reasoning.

= {β_{v}-reduction}
shift λk_{1}. λt_{1}. k_{1} (reset (λ(). θ_{1} (c ())) nil) t_{1}
= {η-reduction}
shift λk_{1}. k_{1} (reset (λ(). θ_{1} (c ())) nil)
= {S-elim: Sk.k M = M, if k ∉ FV (M)}
reset (λ(). θ_{1} (c ())) nil

where the final step is justified by Kameyama and Hasegawa’s S-elim axiom [41]. Translating these definitions into an implementation in Standard ML is straightforward:

signature CONTROL_AND_PROMPT
= sig
type answer
val control : (('a -> answer) -> answer) -> 'a
val prompt : (unit -> answer) -> answer
end
functor make_Control_and_Prompt (type answer) : CONTROL_AND_PROMPT
= struct
type answer = answer                                (* final answer type *)
datatype ans = ANS of trail1 -> answer             (* answer type of the *)
withtype 'a cont1 = 'a -> ans                      (* continuation monad *)
     and trail1 = answer cont1 list
exception MISSING_PROMPT
structure SR = make_Shift_and_Reset (type answer = ans)
fun continue (ANS f) t1           (*  continue : ans -> trail1 -> answer *)
    = f t1
fun theta1 v                                       (*  theta1 : 'a cont1 *)
    = ANS (fn nil        => v
            | (k1 :: t1) => continue (k1 v) t1)
fun control f              (* control : (('a -> answer) -> answer) -> 'a *)
    = SR.shift
        (fn k1 => ANS (fn t1 =>
           let val x = fn v =>
                         SR.shift
                           (fn k1' => ANS (fn t1' =>
                              continue (k1 v) (t1 @ (k1' :: t1'))))
           in continue (SR.reset (fn () => theta1 (f x))) nil
           end)) handle MISSING_RESET => raise MISSING_PROMPT
fun prompt c                      (* prompt : (unit -> answer) -> answer *)
    = continue (SR.reset (fn () => theta1 (c ()))) nil
end

This implementation is a direct consequence of the abstract-machine semantics of control and prompt. It is formally connected to the operations in the continuation monad by monadic reflection and the monad is formally connected to the abstract machine by defunctionalization.

As usual with implementations of delimited control operators, a program using control and prompt needs a toplevel control delimiter: not only the capture of the current delimited continuation (like for shift and reset) but also the application of a captured continuation (unlike for shift and reset) must occur within a delimited context.

11 Related work

The concept of meta-continuation and its representation as a function originate in Wand and Friedman’s formalization of reflective towers [58], and its representation as a list in Danvy and Malmkjær’s followup study [21]. Danvy and Filinski then realized that a metacontinuation naturally arises by “one more” CPS transformation, giving rise to success and failure continuations [18], and later Danvy and Nielsen observed that the list representation naturally arises by defunctionalization [23].

As for delimited continuations, the representation of the meta-continuation as a list has a long history. Johnson and Duggan use it in their early work on composable continuations [39]. Danvy and Filinski use it to specify (what is now known as) shift0 [17, Appendix C]. Moreau and Queinnec later used it to specify their control operators call/pc and marker [46]. Dybvig, Peyton Jones, and Sabry have recently used it in their monadic framework for delimited continuations [25].

The original approaches to delimited continuations were split between composing continuations dynamically by concatenating their representations [30] and composing them statically using continuation-passing function composition [18]. Recently, Shan [52], Dybvig, Peyton Jones, and Sabry [25], and Kiselyov [43] have each proposed accounts of dynamic delimited continuations:

• Shan gives a continuation semantics for dynamic delimited continuations. His continuation semantics threads a state equivalent to our trail. This state is a functional representation of a binary tree with continuations at the leaves. He extends Felleisen et al.’s idea of an algebra of contexts [30] and uses the algebraic operators Send and Compose rather than standard list operators to propagate intermediate results and compose delimited continuations.

The abstract machine corresponding to Shan’s continuation semantics is similar to our adjusted abstract machine. Like ours it uses an extra component to delay the concatenation of contexts. Shan’s approach corresponds to viewing the composition operator (⋆) as a context constructor rather than a meta-level operation, thus obtaining a machine in defunctionalized form. He justifies the correctness of his continuation semantics by (1) using defunctionalization to obtain the corresponding abstract machine, and (2) relating it to the definitional machine for control and prompt given here in Section 2.

Shan informally connects his continuation semantics to his direct-style implementation in Scheme via a pair of transformations. He transforms an abstraction over a continuation into a use of shift and transforms an application to a continuation into an application of a continuation guarded by a reset. Here we show that these transformations are formally justified by the monadic reflection operators reflect and reify for the continuation monad.

Shan considers two other dynamic delimited continuation operators. He gives them continuation semantics and implementations that correspond to two other abstract machines. Our adjusted abstract machine and the corresponding dynamic continuation-passing style can be adapted to account for either of these variations as well, by leaving the metacontinuation defunctionalized (see Appendices A and B).

• Dybvig, Peyton Jones, and Sabry provide a general framework for delimited continuations. They give a continuation semantics that threads a state that is a list of continuations annotated with multiple control delimiters. This state is related to our trail and meta-continuation. Defunctionalizing our meta-continuation, inserting explicit delimiters between its segments, flattening it, and appending it to our trail of continuations yields their state specialized to a single delimiter. Their framework, however, was designed independently of defunctionalization. They exhibit an abstract machine that corresponds to their continuation semantics. Our adjusted abstract machine is related to their machine specialized to a single delimiter and restricted to control and prompt. We find this coincidence of result remarkable considering the difference of motivation and methodology:

– Dybvig, Peyton Jones, and Sabry sought “a typed monadic framework in which one can define and experiment with control operators that manipulate delimited continuations” [25, Section 8], based on Moreau and Queinnec’s representation of the metacontinuation as a list of control-delimiter tags and of continuations, and using Gunter, Rémy, and Riecke’s control operators set and cupto [34] as a common basis, whereas

– we wanted an abstract machine for control and prompt that is in the range of Reynolds’s defunctionalization in order to provide a consistent spectrum of tools for programming with and reasoning about delimited continuations, both in direct style and in continuation-passing style.

Dybvig et al. give a direct-style Scheme implementation of their framework in terms of call/cc and state, but do not formally justify the correctness of this implementation. Their framework is more general than the present work: it can account for all the variations on control operators considered by Shan, as well as variations with multiple delimiters. In contrast, we have focused on specifying control and prompt and on illustrating them.

• Kiselyov gives an encoding of dynamic delimited continuations in terms of shift and reset and recursion. His approach is qualitatively different from ours, Shan’s, and Dybvig et al.’s. It does not thread an extra state parameter, but rather tags values sent to the meta-continuation to indicate control effects or their absence. His transformation wraps code around delimiters and the bodies of continuation functions in order to handle control effects. The abstract machine corresponding to Kiselyov’s encoding does not have an extra component to delay the concatenation of contexts. Instead, it uses the meta-continuation for temporary storage of continuations to delay their concatenation to the current continuation. Kiselyov proves his encoding correct by showing that its behavior under reduction agrees with the reduction semantics of control and prompt. His approach allows variations on delimited continuations by choosing how to handle delimiters and continuation application.

As for adjusting an abstract machine to put it in defunctionalized form, there are precedents. For example, as pointed out by the two last authors [22], Felleisen’s version of the SECD machine with the J operator [26] differs from its predecessors in that it is in defunctionalized form. (In effect, it uses a control delimiter.)

Finally, just as repeated CPS transformations give rise to a static CPS hierarchy [4,18,40, 47], repeated dynamic CPS transformations give rise to a dynamic CPS hierarchy—a future work.

12 Conclusion and issues

In our earlier work [8], we argued that dynamic delimited continuations need examples, reasoning tools, and meaning-preserving program transformations, not only new variations, new formalizations, or new implementations. The present work fulfills these wishes for control and prompt by providing, in a concerted way, an abstract machine that is in defunctionalized form, the corresponding evaluator, the corresponding continuation-passing style and CPS transformer, a monadic account of this continuation-passing style, a new simulation of dynamic delimited-control operators in terms of static ones, and several new examples.

Compared to static delimited continuations, and despite recent implementation advances, the topic of dynamic delimited continuations still remains largely unexplored. We believe that the spectrum of compatible computational artifacts presented here—abstract machine, evaluator, computational monad, and dynamic continuation-passing style—puts one in a better position to assess them.

Acknowledgments: We are grateful to Mads Sig Ager, Małgorzata Biernacka, Julia Lawall, Kristian Støvring, and the anonymous reviewers for their comments. This work is supported by the Danish Natural Science Research Council, Grant no. 21-03-0545 and by the ESPRIT

Working Group APPSEM (http://www.appsem.org).

Appendices

A control0

Shan [52] considers a variation of control, control0 (^{−}F^{−} in the parlance of Dybvig, Peyton Jones, and Sabry [25]). Informally, control0 is like control except that capturing a delimited continuation removes a delimiter (and therefore programs using control0 may need more than one toplevel control delimiter or alternatively a “master,” undiscardable control delimiter). Our adjusted abstract machine can be modified to account for this variation.

The adjusted machine is modified to implement the semantics of control0 by replacing the clause for capturing a delimited continuation as follows:

⟨^{−}F^{−}x.e, ρ, C_{1}, T_{1}, (C′_{1}, T′_{1}) :: C_{2}⟩_{eval} ⇒_{adj} ⟨e, ρ{x ↦ [C_{1}, T_{1}]}, C′_{1}, T′_{1}, C_{2}⟩_{eval}

The machine is still in defunctionalized form with respect to its contexts. It can thus be refunctionalized, which yields a compositional continuation-passing evaluator. The rest of the development (CPS transformation, direct-style evaluator, monad, and implementation) follows Sections 6, 7, 9, and 10 mutatis mutandis.^{3}

B shift0

The fourth control operator considered by Shan is shift0 (^{−}F^{+} in the parlance of Dybvig, Peyton Jones, and Sabry [25]). Informally, shift0 is like shift except that capturing a delimited continuation removes a delimiter (and therefore programs using shift0 may need more than one toplevel control delimiter). Our adjusted abstract machine can be modified to account for this variation as well.

3The meta-contexts remain defunctionalized, and therefore cannot be eliminated from the evaluator (and thus the monad and implementation) via direct-style transformation.

The adjusted machine is modified to implement the semantics of shift0 by replacing the clause for applying a captured continuation as follows, in addition to the modification of Appendix A:

⟨^{−}F^{+}x.e, ρ, C_{1}, T_{1}, (C′_{1}, T′_{1}) :: C_{2}⟩_{eval} ⇒_{adj} ⟨e, ρ{x ↦ [C_{1}, T_{1}]}, C′_{1}, T′_{1}, C_{2}⟩_{eval}
⟨FUN ([C′_{1}, T′_{1}], C_{1}), v, T_{1}, C_{2}⟩_{cont_{1}} ⇒_{adj} ⟨C′_{1}, v, T′_{1}, (C_{1}, T_{1}) :: C_{2}⟩_{cont_{1}}

The machine is still in defunctionalized form with respect to its contexts. It can thus be refunctionalized, which yields a compositional continuation-passing evaluator. Just as in Appendix A, the rest of the development follows Sections 6, 7, 9, and 10.

C An implementation of shift and reset

We use Filinski’s implementation of shift and reset in SML [32], renaming some identifiers for uniformity:

signature ESCAPE
= sig
type void
val coerce : void -> 'a
val escape : (('a -> void) -> 'a) -> 'a
end
structure Escape : ESCAPE
= struct
open SMLofNJ.Cont
datatype void = VOID of void
fun coerce (VOID v) = coerce v
fun escape f = callcc (fn k => f (fn x => throw k x))
end
signature SHIFT_AND_RESET
= sig
type answer
val shift : (('a -> answer) -> answer) -> 'a
val reset : (unit -> answer) -> answer
end
functor make_Shift_and_Reset (type answer) : SHIFT_AND_RESET
= struct
open Escape
type answer = answer
exception MISSING_RESET
val mk : (answer -> void) ref = ref (fn _=> raise MISSING_RESET)
fun abort x = coerce (!mk x)
fun reset t
    = escape (fn k => let val m = !mk
                      in mk := (fn r => (mk := m; k r));
                         abort (t ())
                      end)
fun shift h
    = escape (fn k => abort (h (fn v => reset (fn () => coerce (k v)))))
end

References

[1] Mads Sig Ager. Partial Evaluation of String Matchers & Constructions of Abstract Machines. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, January 2006.

[2] Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A functional correspondence between evaluators and abstract machines. In Dale Miller, editor, Proceedings of the Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP’03), pages 8–19, Uppsala, Sweden, August 2003. ACM Press.

[3] Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A functional correspondence between monadic evaluators and abstract machines for languages with computational effects. Theoretical Computer Science, 342(1):149–172, 2005. Extended version available as the technical report BRICS RS-04-28.

[4] Małgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Computer Science, 1(2:5):1–39, November 2005. A preliminary version was presented at the Fourth ACM SIGPLAN Workshop on Continuations (CW’04).

[5] Małgorzata Biernacka and Olivier Danvy. A syntactic correspondence between contextsensitive calculi and abstract machines. Technical Report BRICS RS-05-38, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 2005. Accepted for publication in Theoretical Computer Science (March 2006).

[6] Dariusz Biernacki. The Theory and Practice of Programming Languages with Delimited Continuations. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, December 2005.

[7] Dariusz Biernacki and Olivier Danvy. A simple proof of a folklore theorem about delimited control. Journal of Functional Programming, 16(3):269–280, 2006.

[8] Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan. On the static and dynamic extents of delimited continuations. Science of Computer Programming, 60:274–297, 2006.

[9] Hans-J. Boehm, editor. Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, Portland, Oregon, January 1994. ACM Press.

[10] Robert (Corky) Cartwright, editor. Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, Snowbird, Utah, July 1988. ACM Press.

[11] William Clinger, Daniel P. Friedman, and Mitchell Wand. A scheme for a higher-level semantic algebra. In John Reynolds and Maurice Nivat, editors, Algebraic Methods in Semantics, pages 237–250. Cambridge University Press, 1985.

[12] Olivier Danvy. Back to direct style. Science of Computer Programming, 22(3):183– 195, 1994. A preliminary version was presented at the Fourth European Symposium on Programming (ESOP 1992).

[13] Olivier Danvy. On evaluation contexts, continuations, and the rest of the computation. In Hayo Thielecke, editor, Proceedings of the Fourth ACM SIGPLAN Workshop on Continuations (CW’04), Technical report CSR-04-1, Department of Computer Science, Queen Mary’s College, pages 13–23, Venice, Italy, January 2004. Invited talk.

[14] Olivier Danvy. A rational deconstruction of Landin’s SECD machine. In Clemens Grelck, Frank Huch, Greg J. Michaelson, and Phil Trinder, editors, Implementation and Application of Functional Languages, 16th International Workshop, IFL’04, number 3474 in Lecture Notes in Computer Science, pages 52–71, Lübeck, Germany, September 2004. Springer-Verlag. Recipient of the 2004 Peter Landin prize. Extended version available as the technical report BRICS RS-03-33.

[15] Olivier Danvy. An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, University of Aarhus, Aarhus, Denmark, October 2006.

[16] Olivier Danvy. Refunctionalization at work. In Preliminary proceedings of the 8th International Conference on Mathematics of Program Construction (MPC ’06), Kuressaare, Estonia, July 2006. Invited talk.

[17] Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. DIKU Rapport 89/12, DIKU, Computer Science Department, University of Copenhagen, Copenhagen, Denmark, July 1989.

[18] Olivier Danvy and Andrzej Filinski. Abstracting control. In Wand [57], pages 151–160.

[19] Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, 1992.

[20] Olivier Danvy and Julia L. Lawall. Back to direct style II: First-class continuations. In William Clinger, editor, Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. V, No. 1, pages 299–310, San Francisco, California, June 1992. ACM Press.

[21] Olivier Danvy and Karoline Malmkjær. Intensions and extensions in a reflective tower. In Cartwright [10], pages 327–341.

[22] Olivier Danvy and Kevin Millikin. A rational deconstruction of Landin’s J operator. In Andrew Butterfield, Clemens Grelck, and Frank Huch, editors, Implementation and Application of Functional Languages, 17th International Workshop, IFL’05, number 4015 in Lecture Notes in Computer Science, pages 55–73, Dublin, Ireland, September 2005. Springer-Verlag. Extended version available as the technical report BRICS RS-06-4 (February 2006).

[23] Olivier Danvy and Lasse R. Nielsen. Defunctionalization at work. In Harald Søndergaard, editor, Proceedings of the Third International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP’01), pages 162–174, Firenze, Italy, September 2001. ACM Press. Extended version available as the technical report BRICS RS-01-23.

[24] Olivier Danvy and Ulrik P. Schultz. Lambda-dropping: Transforming recursive equations into programs with block structure. Theoretical Computer Science, 248(1-2):243–287, 2000.

[25] R. Kent Dybvig, Simon Peyton-Jones, and Amr Sabry. A monadic framework for subcontinuations. To appear in the Journal of Functional Programming. Available at

<http://www.cs.indiana.edu/~sabry/research.html>, May 2006.

[26] Matthias Felleisen. Reflections on Landin’s J operator: a partly historical note. Computer Languages, 12(3/4):197–207, 1987.

[27] Matthias Felleisen. The theory and practice of first-class prompts. In Ferrante and Mager [31], pages 180–190.

[28] Matthias Felleisen and Daniel P. Friedman. Control operators, the SECD machine, and the λ-calculus. In Martin Wirsing, editor, Formal Description of Programming Concepts III, pages 193–217. Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 1986.

[29] Matthias Felleisen, Daniel P. Friedman, Bruce Duba, and John Merrill. Beyond continuations. Technical Report 216, Computer Science Department, Indiana University, Bloomington, Indiana, February 1987.

[30] Matthias Felleisen, Mitchell Wand, Daniel P. Friedman, and Bruce F. Duba. Abstract continuations: A mathematical semantics for handling full functional jumps. In Cartwright [10], pages 52–62.

[31] Jeanne Ferrante and Peter Mager, editors. Proceedings of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, January 1988. ACM Press.

[32] Andrzej Filinski. Representing monads. In Boehm [9], pages 446–457.

[33] Andrzej Filinski. Controlling Effects. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, May 1996. Technical Report CMU-CS-96-119.

[34] Carl Gunter, Didier Rémy, and Jon G. Riecke. A generalization of exceptions and control in ML-like languages. In Simon Peyton Jones, editor, Proceedings of the Seventh ACM Conference on Functional Programming and Computer Architecture, pages 12–23, La Jolla, California, June 1995. ACM Press.

[35] Robert Harper, Bruce F. Duba, and David MacQueen. Typing first-class continuations in ML. Journal of Functional Programming, 3(4):465–484, October 1993.

[36] John Hatcliff and Olivier Danvy. A generic account of continuation-passing styles. In Boehm [9], pages 458–471.

[37] Robert Hieb and R. Kent Dybvig. Continuations and concurrency. In Proceedings of the Second ACM SIGPLAN Symposium on Principles & Practice of Parallel Programming, SIGPLAN Notices, Vol. 25, No. 3, pages 128–136, Seattle, Washington, March 1990. ACM Press.

[38] Robert Hieb, R. Kent Dybvig, and Claude W. Anderson, III. Subcontinuations. Lisp and Symbolic Computation, 5(4):295–326, December 1993.

[39] Gregory F. Johnson and Dominic Duggan. Stores and partial continuations as first-class objects in a language and its environment. In Ferrante and Mager [31], pages 158–168.

[40] Yukiyoshi Kameyama. Axioms for delimited continuations in the CPS hierarchy. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 442–457, Karpacz, Poland, September 2004. Springer.

[41] Yukiyoshi Kameyama and Masahito Hasegawa. A sound and complete axiomatization of delimited continuations. In Olin Shivers, editor, Proceedings of the 2003 ACM SIG-PLAN International Conference on Functional Programming (ICFP’03), pages 177–188, Uppsala, Sweden, August 2003. ACM Press.

[42] Richard Kelsey, William Clinger, and Jonathan Rees, editors. Revised^{5} report on the algorithmic language Scheme. Higher-Order and Symbolic Computation, 11(1):7–105, 1998.

[43] Oleg Kiselyov. How to remove a dynamic prompt: Static and dynamic delimited continuation operators are equally expressible. Technical Report 611, Computer Science Department, Indiana University, Bloomington, Indiana, March 2005.

[44] Robert E. Milne and Christopher Strachey. A Theory of Programming Language Semantics. Chapman and Hall, London, and John Wiley, New York, 1976.

[45] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

[46] Luc Moreau and Christian Queinnec. Partial continuations as the difference of continuations, a duumvirate of control operators. In Manuel Hermenegildo and Jaan Penjam, editors, Sixth International Symposium on Programming Language Implementation and Logic Programming, number 844 in Lecture Notes in Computer Science, pages 182–197, Madrid, Spain, September 1994. Springer-Verlag.

[47] Chethan R. Murthy. Control operators, hierarchies, and pseudo-classical type systems: A-translation at work. In Olivier Danvy and Carolyn L. Talcott, editors, Proceedings of the First ACM SIGPLAN Workshop on Continuations (CW’92), Technical report STAN-CS-92-1426, Stanford University, pages 49–72, San Francisco, California, June 1992.

[48] Christian Queinnec and Bernard Serpette. A dynamic extent control operator for partial continuations. In Robert (Corky) Cartwright, editor, Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 174–184, Orlando, Florida, January 1991. ACM Press.

[49] John C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of 25th ACM National Conference, pages 717–740, Boston, Massachusetts, 1972. Reprinted in Higher-Order and Symbolic Computation 11(4):363–397, 1998, with a foreword [50].

[50] John C. Reynolds. Definitional interpreters revisited. Higher-Order and Symbolic Computation, 11(4):355–361, 1998.

[51] Chung-chieh Shan. Shift to control. In Olin Shivers and Oscar Waddell, editors, Proceedings of the 2004 ACM SIGPLAN Workshop on Scheme and Functional Programming, Technical report TR600, Computer Science Department, Indiana University, Snowbird, Utah, September 2004.

[52] Chung-chieh Shan. A static simulation of dynamic delimited control. Higher-Order and Symbolic Computation, 2007. Journal version of [51]. To appear.

[53] Dorai Sitaram and Matthias Felleisen. Control delimiters and their hierarchies. Lisp and Symbolic Computation, 3(1):67–99, January 1990.

[54] Dorai Sitaram and Matthias Felleisen. Reasoning with continuations II: Full abstraction for models of control. In Wand [57], pages 161–175.

[55] Philip Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2(4):461–493, 1992.

[56] Philip Wadler. Monads and composable continuations. LISP and Symbolic Computation, 7(1):39–55, January 1994.

[57] Mitchell Wand, editor. Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, Nice, France, June 1990. ACM Press.

[58] Mitchell Wand and Daniel P. Friedman. The mystery of the tower revealed: A nonreflective description of the reflective tower. Lisp and Symbolic Computation, 1(1):11–38, May 1988. A preliminary version was presented at the 1986 ACM Conference on Lisp and Functional Programming (LFP 1986).

Recent BRICS Report Series Publications

RS-06-15 Dariusz Biernacki, Olivier Danvy, and Kevin Millikin. A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations. October 2006. ii+28 pp. Revised version of BRICS RS-05-16.

RS-06-14 Giorgio Delzanno, Javier Esparza, and Jiří Srba. Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols. July 2006. 31 pp. To appear in ATVA ’06.

RS-06-13 Jiří Srba. Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation. July 2006. 21 pp. To appear in CSL ’06.

RS-06-12 Kristian Støvring. Higher-Order Beta Matching with Solutions in Long Beta-Eta Normal Form. June 2006. 13 pp. To appear in Nordic Journal of Computing, 2006.

RS-06-11 Kim G. Larsen, Ulrik Nyman, and Andrzej Wasowski. An Interface Theory for Input/Output Automata. June 2006. 40 pp. Appears in Misra, Nipkow and Sekerinski, editors, Formal Methods: 14th International Symposium, FM ’06 Proceedings, LNCS 4085, 2006, pages 82–97.

RS-06-10 Christian Kirkegaard and Anders Møller. Static Analysis for Java Servlets and JSP. June 2006. 23 pp. Full version of paper presented at SAS ’06.

RS-06-9 Claus Brabrand, Robert Giegerich, and Anders Møller. Analyzing Ambiguity of Context-Free Grammars. April 2006. 19 pp.

RS-06-8 Christian Kirkegaard and Anders Møller. Static Analysis for Java Servlets and JSP. April 2006. 22 pp.

RS-06-7 Petr Jančar and Jiří Srba. Undecidability Results for Bisimilarity on Prefix Rewrite Systems. April 2006. 20 pp. Presented at FoSSaCS 2006, LNCS 3921:277–291.

RS-06-6 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. A Finite Equational Base for CCS with Left Merge and Communication Merge. March 2006. 22 pp.

RS-06-5 Kristian Støvring. Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative. March 2006. 18 pp. To appear in Logical Methods in Computer Science. Supersedes RS-05-35.