Vol. 0

No. 0

IPSJ Journal

1959

Regular Paper

A Type System for Dynamic Delimited Continuations
Takuo Yonezawa† and Yukiyoshi Kameyama†
We study the control operators ”control” and ”prompt” which manage part of continuations,that is, delimited continuations. They are similar to the well-known control operators ”shift”
and ”reset”, but diﬀer in that the former is dynamic, while the latter is static. In this paper, we
introduce a static type system for ”control” and ”prompt” which does not use recursive types.
We design our type system based on the dynamic CPS transformation recently proposed by
Biernacki, Danvy and Millikin. We also introduce let-polymorphism into our type system,and show that our type system satisﬁes several important properties such as strong typesoundness.

found a CPS transformation for them, together
with several new applications, and there is stillroom for foundational studies on them.
This paper introduces a type system for control and prompt, and studies its properties. In
the literature, studies on the control operatorsfor delimited continuations were mostly done in
type-free languages or with very restricted typesystems. Recently, Asai and Kameyama7) haveproposed a polymorphic type system for shift
and reset and shown that it satisﬁes several
properties such as type soundness and strong
normalization. However, it is still an interesting open question as to whether we can deﬁne astatic polymorphic type system for control andprompt, since control/prompt is inherently dynamic. One might need recursive types which
would drastically change the static nature of
the source calculus. In this paper, we solve thisquestion by introducing a static type system
which does not need recursive types. Our typesystem is much more expressive than the one
implicitly used by Biernacki, Danvy, Millikin6) .
The contribution of this paper can be summarized as follows:• We propose a type system for control/prompt which does not need recursive
types. We show that our type system displays strong type soundness.
• We introduce ML-like let-polymorphism
into the type system, and show that it alsosatisﬁes properties above.
• We compare the expressibility of control/prompt and shift/reset under thetyped framework.
We also emphasize that this paper is the ﬁrst
one which studies the type theoretic foundationof control/prompt.
This paper is organized as follows: We deﬁne

1. Introduction
We are interested in control operators thatmanage (e.g. capture, discard, or reinstall)delimited continuations, part of an evaluation
context. They allow one to represent various kinds of control structures such as nondeterminism, logging, and a base framework to
represent other eﬀects (be they control eﬀects
or not) in direct style.
In the literature, two sets of delimited continuation operators have attracted researchers’interest. The ﬁrst such operators are “control”
and “prompt” proposed by Felleisen in 19881) .
They are classiﬁed as dynamic operators, since,
when a captured delimited continuation is used,
it is merged with the current continuation withno delimiter (prompt) between them. Therefore we cannot regard each delimited continuation as an independent component: they will
be dynamically merged. The second operators“shift” and “reset” proposed by Danvy and Filinski2) in 1990 are classiﬁed as static operators,
since a delimited continuation, when used, iscomposed with the current continuation, i.e., it
can be regarded as an ordinary function, or astatic object. Due to their static nature, shift
and reset have a simple CPS transformation,
which allows one to study the the representation of all monadic eﬀects3) , abstract machine4)
and equational axiomatization5) , together withseveral interesting programming examples, extensively. On the other hand, control andprompt have not been active research targets
until Biernacki, Danvy and Millikin6) recently† Department of Computer Science, Graduate Schoolof Systems and Information Engineering, Universityof Tsukuba
1

2

IPSJ JournalM ::=x| λx.M|M M| let x = v in M
| #M
| Fc.Mv ::= x | λx.M

(expression)(variable)(λ abstraction)(function application)(let)(prompt)(control)(value)Fig. 1 Syntax of the language

the language with control/prompt in Section 2.
We introduce the dynamic CPS transformationin Section 3. In Section 4, we deﬁne the polymorphic type system for control/prompt. We
discuss the relation of our type system with thatfor shift/reset in Section 5. Then we show several properties of the type system in Section 6.
The conclusion appears in Section 7.
2. Deﬁnition of the Language
In this section, we deﬁne the language with
control/prompt and show some examples.
Fig. 1 deﬁnes the syntax of the language
where x and c are variables. Following the ML
families, we restrict the let expression let x =v in M by the “value restriction”, where thesubstituted expression v must be a value.
We introduce the call-by-value reduction
rules of the language. Fig. 2 deﬁnes evaluation context, pure evaluation context (evaluation context without prompt, “pure e-context”
in short), redex, and Fig. 3 deﬁnes reduction
rules. We deﬁne M1 →∗ M2 as the reﬂexivetransitive closure of →, and the equality M1 =M2 as the least congruence relation which contains →.
2.1 Example
Control/prompt can be used as follows:#(Fc.((c 1) + 2)
+3)+4
For the prompt expression #M , the subexpression M is evaluated ﬁrst. If it contains
no control operator F, the value of M is returned. Otherwise, the control operator F captures the continuation up to the most recent
prompt ([ ]+3 in this example), which is in turnassigned to c as a function (λx. x + 3). Thenthe body of the control expression ((c 1) + 2)
is evaluated under this assignment. When its

1959

E ::=

(evaluation context)

[]
|EM
|vE
| #E
P ::=
[]
|P M
|vP
R ::=
(λx.M ) v
| #v
| let x = v in M
| #(P [Fc.M ])(pure e-context)(redex)Fig. 2 Evaluation contexts and redex(λx.M )v →M [v/x]
let x = v in M →M [v/x]#v →v#(P [Fc.M ]) →#(M [λx.P [x]/c])
where x is fresh.
where M [v/x] represents the capture-avoiding
substitution.
Fig. 3 Reduction rules

evaluation is ﬁnished, its then-current continuation up to the prompt ([ ] + 3) is discarded,
so that the value of the prompt expression is((λx.x + 3) 1) + 2. Finally, the entire result is(((λx.x + 3) 1) + 2) + 4 = 10.
The captured continuation is called a delimited continuation since it is delimited byprompt.
Note that the captured delimited continuation is a function so that it can be used arbitrarily many times. We can simulate nondeterministic computation by using the delimited continuation many times, or an exceptionlike eﬀect by never using it.
2.2 Web Application
A more practical example is web application8) .
Consider a simple console applicationx = input();y = input();
print(x + y);
If we want the application to be a web application, we must suspend the program after
printing an input-form, wait for the user’s submission, and resume the program when the user
submits some value.
A naive solution to implement such a web

Vol. 0

No. 0

A Type System for Dynamic Delimited Continuations

application is to use threads, however it has aproblem. After submitting a value for x, a user
may come back to the input-form page for x (byusing the browser’s “Back” button), and may
submit another value for x. The second value
for x is, however, stored to y with the thread
implementation.
A better solution is to use continuations. We
re-deﬁne the input procedure as follows:
input() =Fc.(generate a fresh continuation id;
save c to a global associative tablewith the continuation id;
print the input-form withthe continuation id asa hidden parameter;)
and the main routine resumes the saved continuation when the user submits a value. Sincecontinuation can be called arbitrarily manytimes, the program will work correctly even if
the user submits values multiple times.
The captured continuation above is a continuation up to, but excluding, the main routine
or other request-speciﬁc codes. Hence it is adelimited continuation9) rather than an unlimited continuation. We can implement the application with control/prompt: we enclose thesession-speciﬁc code (i.e. two input commands
for x and y and a print command) by prompt,
and use the control operator F to capture delimited continuations.
2.3 List Reversing
The control operator “shift” (denoted by S)
is a similar operator to control but it delimits
the captured continuation with prompt. Its reduction rule is deﬁned as follows:#(P [Sc.M ]) → #(M [λx.#(P [x])/c])
where x is fresh.
Let us compare it to one for control:#(P [Fc.M ]) → #(M [λx.P [x]/c])
Shift and control behave diﬀerently for thefollowing example:3

reverse l =letvisit = λl0case l0 of
Nil ⇒ Nil(x : x0 ) ⇒visit(Fk.(x :: (k x0 )))in#(visit l)
The example is a list reversing function. If wereplace control with shift, the function becomesa list copying function.
Biernacki et al10) have shown that we can express the depth-ﬁrst (and breadth-ﬁrst, respectively) traversal by using shift/reset (and control/prompt, respectively).
3. CPS Transformation
In this section, we introduce a CPS transformation for control and prompt proposed by
Biernacki, Danvy and Millikin6) .
A CPS transformation is a syntax-directed
program transformation from a source calculus
to a target calculus in continuation passing style(CPS), i.e., all functions explicitly pass continuations as their arguments. In a typical case, thesource calculus is a lambda calculus with control operators, and the target calculus is one
without. Then the control operators are given
precise semantics through this CPS transformation (so called CPS semantics).
For control/prompt, only non-functional
style CPS transformations were previously
known until Biernacki, Danvy and Millikin6)
discovered a purely functional one in 2005.
They called it a dynamic CPS transformation,
and we introduce its curried version here.
The dynamic CPS transformation is based on
the 2-CPS transformation. While a standard(1-CPS) transformation maps a term to a function term which takes one continuation as its
argument, a 2-CPS transformation maps a term
to a function which takes two continuation parameters as its arguments, one for the ﬁrst level
continuation and the other for the second level
continuation (or meta-continuation). 1-CPS is
suﬃcient to give semantics for undelimited continuation operators like call/cc, while 2-CPS is
the key to interpret control operators for delimited continuations like shift/reset and control/prompt.
The dynamic CPS transformation is an extension of 2-CPS transformation with the no-

4

IPSJ JournalM ::=x| λx.M|M M| let x = M in M
|L
| case M of
Nil ⇒ M(x :: x) ⇒ M
L ::= Nil | M :: L

(expression)(variable)(λ abstraction)(function application)(let)(list)(case)

Fig. 4 Deﬁnition of the target language

tion of “trail”, a list of continuations, which
will be explained later. The source calculus of
the dynamic CPS transformation is the call-byvalue lambda calculus with control and prompt
given in the previous section, and its target calculus is the lambda calculus with lists (for representing trails). Fig. 4 deﬁnes the syntax ofthe target calculus.
Fig. 5 shows the dynamic CPS transformation as a type-free transformation. Note thatthe results of the transformation (except thosefor control and prompt) is identical to Plotkin’s
call-by-value CPS transformation if we η-reduce
the results.
A transformed expression takes (if uncurried)
three arguments, a continuation, a list of continuations or trail, and a meta-continuation,and returns a result value (answer).
The key feature of this transformation is theintroduction of trails. A trail is part of a continuation (i.e. captured by the F operator), but
is represented as a list of delimited continuations. The reason for representing it as a listof continuations rather than a single, composedcontinuation comes from the dynamic nature of
the F operator.
Let us examine how a trail is changed througha computation. Initially (without invocation ofcontrol operators) a trail is empty. But whencontrol operators are invoked, a delimited continuation is captured and when the captured
delimited continuation is invoked, it is added toa trail to form a non-empty trail, and it dynamically changes the behavior of the initial (identity) continuation so that it passes a value tothe continuations in the trail.
Although we gave the transformation as a
type-free one, an informal typing would help
understand its meaning. Informally, if an expression M has a type τ and its answer type isα, the type of the transformed expression [ M ] is1959

Ans α ::=Trail α → (Cont2 α ∗) → ∗Trail α ::=List (Cont1 α α)Cont1 α β ::=α → Ans β
Cont2 α β ::=α → βNote that Ans is deﬁned recursively.
Fig. 6 Answer type of the dynamic CPS
transformation

Cont1 τ α → Ans α where Ans is informally deﬁned as Fig. 6. We note that all continuations
in a trail must be of the same type, continuations from α to α, since all the elements of a list
(trail) should have the same type. This informal discussion will be reﬂected in the design of
our type system in the next section. We think
this is a natural restriction, but it may delimit
the extent of the applicability of our type system, which will be discussed in Section 4.
4. Type System
Now we introduce the type system for the
language with control/prompt based on the dynamic CPS transformation in Section 3 so thatit satisﬁes the following property: a source expression is typable whenever its CPS transformation is typable in the target calculus.
Since the transformed expressions mention
the type of “answers” (ﬁnal results of computations), our type system for the source language
has to also mention the answer type. Therefore,
we extend the notation of type judgments andfunction types: a type judgmentΓ ` M : τ /α
is read as: under a type environment Γ, the expression M has a type τ and its answer type is
α. A function type σ → τ /α similarly represents the type of a function which takes a valueof σ as the argument, returns a value of τ , andits answer type is α. For pure expressions (i.e.
values and prompt), we use a pure judgmentΓ `p M : τ
to represent that the answer type of pure expressions can be arbitrary.
Fig. 7 deﬁnes the syntax of types. Greek alphabets (α, β, γ, . . . ) denote types in this paper.
Fig. 8 deﬁnes the typing rules. The typing
rules are deﬁned to reﬂect the CPS transformation. For example, the expression [ Fx.M ] inthe target language is typable as follows:Vol. 0

No. 0

A Type System for Dynamic Delimited Continuations

5[ x]] =λk1 t1 k2 .k1 x t1 k2[ λx.M ] =λk1 t1 k2 .k1 (λx.[[M ] ) t1 k2[ M0 M1 ] =λk1 t1 k2 .[[M0 ] (λv0 t01 k20 .[[M1 ] (λv1 t001 k200 .v0 v1 k1 t001 k200 )t01 k20 ) t1 k2[ let x = v in M ] =λ k1 t1 k2 .
let x = v ∗in [ M ] k1 t1 k2[ #M ] =λk1 t1 k2 .[[M ] θ1 Nil (λv.k1 v t1 k2 )[ Fx.M ] =λk1 t1 k2 .
let x = λv k10 t01 k20 .k1 v (t1 @(k10 :: t01 )) k20
in [ M ] θ1 Nil k2
θ1 =λv t1 k2 . case t1 ofNil ⇒ k2 v
(k1 :: t01 ) ⇒ k1 v t01 k2x∗ =x(λx. M )∗ =λx. [ M ]where @ is the list concatenation.
Fig. 5 Deﬁnition of dynamic CPS transformationτ ::=t| (τ → τ /τ )A ::=
τ | ∀t.AΓ ::=∅| Γ[x 7→ A](monomorphic type)(type variable)(function type)(polymorphic type)(type environment)(empty type environment)(type env. extension)

Fig. 7 Syntax of type and type environment..
..

∅[x 7→ (τ → Cont1 α α → Ans α)] `M : Cont1 β β → Ans α..
..
∅ ` [ Fx.M ] : Cont1 τ α → Ans α
We can prove that none of the typesof the transformed expressions match with
Cont1 β β → Ans α but only with Cont1 α α →Ans α, so that we can type it as:..
..
∅[x 7→ (τ → Cont1 α α → Ans α)] `M : Cont1 α α → Ans α..
..
∅ ` [ Fx.M ] : Cont1 τ α → Ans α
Mapping Γ ` [ X]] : Cont1 τ α → Ans α to
Γ ` X : τ /α, we obtain a typing ruleΓ[c 7→ (τ → α/α)] ` M : α/αΓ ` Fc.M : τ /α
Other rules can be derived similarly.
Moreover, we introduce ML-like let poly-morphism with value-restriction. In Fig. 8,Gen(σ; Γ) is ∀t1 . . . . ∀tn .σ where {t1 , . . . , tn } =FTV(σ) − FTV(Γ), F T V (α) denotes the set offree type variables in α, and τ ≤ A means that
A is ∀t1 . . . . ∀tn .ρ and τ is ρ[σ1 , . . . σn /t1 , . . . , tn ]for some monomorphic types ρ, σ1 , . . . , σn andtype variables t1 , . . . , tn .
Discussion: Answer Type Modiﬁcation
Answer type modiﬁcation is a control eﬀect
where the (ﬁnal) answer type of an expression diﬀers from the return type of the current continuation. For a term without control operators, these two types always agree asshown by the type of its CPS transformation(α → X) → X. With control operators, however, these two types may diﬀer, for instance,
Asai11) has shown that a direct style implementation of printf in ML needs answer type modiﬁcation.
Our type system does not support answer
type modiﬁcation. This restriction comes fromthe restriction that the types of continuations in
a trail must be the same as the type of continuations from α to α. Eliminating the restrictionis left for future work. ☆
5. Relation to shift/reset
In this section, we discuss the relationship between prompt/control and shift/reset.
In the type-free setting, shift/reset and control/prompt are known to be equally expressive,
namely, each set of control operators can simulate the other13) . To see this, we identify resetwith prompt, and simulate shift by control and☆

See our forthcoming paper12) .

6

IPSJ Journal

1959Γ `p M : τΓ[x 7→ σ] ` M : τ /αΓ(x) = A τ ≤ Afrom pure
λ abstraction
variableΓ `p x : τΓ `p λx.M : (σ → τ /α)Γ ` M : τ /αΓ ` M1 : (σ → τ /α)/α Γ ` M2 : σ/αfunction applicationΓ ` M1 M2 : τ /αΓ `p v : σ Γ[x 7→ Gen(σ; Γ)] ` M : τ /αlet
Γ ` let x = v in M : τ /α
Γ[c 7→ (τ → α/α)] ` M : α/αΓ ` M : τ /τpromptcontrolΓ `p #M : τΓ ` Fc.M : τ /αFig. 8 Typing rules

prompt as follows:
Sc.M = Fc0 . let c = λx.#(c0 x) in M
Then it is easy to see that shift/reset can be
simulated by control/prompt.
The converse direction is also possible, but israther complicated, for instance, the encodingof control in terms of shift/reset needs recursive
types if we type the encoding.
Here we show that the one-way simulation(simulating shift/reset by control/prompt) is
possible even under the polymorphic type system.☆ Namely, the expression Fc0 . let c =λx.#(c0 x) in M can be typed in our type system asΓ[c0 7→ . . . ][c 7→ ∀β.(τ → α/β)] ` M : α/α..
..
Γ ` F c0 . let c = λx.#(c0 x) in M : τ /αThis type is essentially equivalent to the type
for the shift expression in Murthy’s type system
restricted to level 1 (with polymorphism), or
the one in Asai and Kameyama’s type system
without answer type modiﬁcation, which can bedeﬁned as follows:Γ[c 7→ ∀β.(τ → α/β)] ` M : α/αshiftΓ ` Sc.M : τ /αNote that Asai and Kameyama’s type system
uses ∀ both in the rule for let and in the rule
for shift (i.e. ∀β at the type of c), while our system uses it only in the rule for let. In fact, we
can derive polymorphism of the answer type ofcontinuations captured by shift from the typing
rules for let, reset, and control. Hence, we cansay that the let polymorphism and the type ofcontrol eﬀects (control and prompt) are orthog☆

At the time of submitting this paper, we did notknow if the converse simulation was possible or not.
After that, we came up with a counterexample of theconverse simulation, which is detailed in our forthcoming paper12) .

onal in our type system.
6. Properties of the Type System
Here we show three important properties of
the type system:• Strong type soundness.
• Preservation of types with respect to CPS
transformation.
• Preservation of equality with respect to
CPS transformation.
Proofs of theorems in this section can befound in the appendix.
Type soundness is the most important property for static type systems for programming
languages, stated as follows:
Theorem 1 (Type Soundness). If ∅ `p
#M : τ is derivable, then either M is a value(a variable or lambda abstraction), or there exists some term N such that #M → #N and∅ `p #N : τ .
The theorem states strong type soundness inthe sense the type of an expression is preserved
through evaluation, while weak type soundness
means that a well typed program does not gowrong14) .
Theorem 1 is a combination of the following
two properties:
Theorem 2 (Subject Reduction). If Γ `M1 : τ /α is derivable and M1 →∗ M2 , thenΓ ` M2 : τ /α is derivable. If Γ `p M1 : τ isderivable and M1 →∗ M2 , then Γ `p M2 : τ isderivable.
Theorem 3 (Progress). If ∅ `p #M : τ isderivable, then either M is a value, or #M
can be uniquely decomposed into the form E[R]
where E is an evaluation context and R is aredex.
The progress property above takes a slightly
unusual form in that the expression being considered is not an arbitrary one M , but an expression in the form of #M , i.e., we only con-Vol. 0

No. 0

A Type System for Dynamic Delimited Continuations

sider #M with no free variables as a program.
In fact, Felleisen assumes that the operator #is always supplied from the top level, and thus
called this operator prompt.
Next, we show the CPS transformation given
above is well behaved, namely, it preserves
types and equality. Before stating the property, we need to deﬁne the CPS transformation
for types. For this purpose, let us recall the informal deﬁnition of types given in Fig. 6. By
expanding the informal deﬁnition of Trail, weget:Trail α = List (Cont1 α α)
= List (α → Ans α)= List (α → Trail α→ (α → ∗) → ∗)Based on this intuition, we formally deﬁne thetype constructor Trail as:
Trail α ::= µX.List (α → X → (α → ∗) → ∗)where µX. . . . is a recursive type, and ∗ is theanswer type. We also regard the informal definitions for the other type constructors Ans,
Cont1 , and Cont2 as formal. Then it is easy
to see the formal deﬁnition coincides with theinformal one (modulo the folding/unfolding ofrecursive types).
Note on Answer Type Polymorphism:
Since we use so called 2-CPS transformation(it uses two continuation variables k1 and k2 ),the ﬁnal answer type ∗ used to type the target
terms of the CPS transformation can be madepolymorphic. Thus, if we were to work in thesecond order lambda calculus, we could bind all∗’s by universal type quantiﬁer as ∀ ∗ .Trail α.
Alternatively we can locally quantify the typevariable ∗ such as · · · → ∀ ∗ .((α → ∗) → ∗)).
For more details about answer type polymorphism, see Thielecke15) .
Now we deﬁne the CPS transformation fortypes:t∗ = t for type variable(α → β/γ)∗ = α∗ → (Cont1 β ∗ γ ∗ )→ (Ans γ ∗ )∗(∀t.α) = ∀t.α∗
The CPS translation can be naturally extended
to type context Γ.
Then we can state the type preservation property with respect to the CPS transformation.
The formal deﬁnition of the type system of thetarget language is given by Fig. 9 and Fig. 10
in the appendix.
Theorem 4 (Preservation of Types). If Γ `7

M : τ /α is derivable, then we can derive Γ∗ `[ M ] : (Cont1 τ ∗ α∗ ) → (Ans α∗ ) in the target
calculus.
Similarly, if Γ `p M : τ is derivable, then we
can derive Γ∗ ` [ M ] : (Cont1 τ ∗ α) → (Ans α)
for any type α in the target calculus.
Note that, the types in the target calculus
implicitly contains the type variable ∗.
We can also show that equality in the source
calculus is preserved with respect to the CPS
transformation.
We deﬁne the equality of expressions of thetarget language as the least congruence relation
which includes β-equality and the following additional equality:[ M ] k1 t1 k2 = [ M ] θ1 (k1 :: t1 ) k2
for a source expression M , a continuation k1 oftype Cont1 α β, a trail t1 of type Trail α, ameta-continuation k2 of type Cont2 α β.
The additional equality can be justiﬁed by
the following argument: since the continuation
k1 is used linearly at the tail position withtrail t1 appended to some trail at the end, or
captured by control with a trail t1 appended
to some trail at the end. In the former case,both sides of the additional equality are clearly
equal. In the later case, since trails are destroyed (used) by θ1 only, and (k1 v t1 k2 ) isequal to (θ1 v (k1 :: t1 ) k2 ), both sides of theequality are equal. In this paper, we regard theequation as an axiom for simplicity.
Theorem 5 (Preservation of Equality). IfΓ ` Mi : τ /α is derivable for i = 1, 2 and M1 =M2 , then we have [ M1 ] = [ M2 ] in the target
calculus.
7. Conclusion
We have proposed a type system for a language with control/prompt based on the dynamic CPS transformation, and showed several
important properties of the type system suchas type soundness, relation to the CPS transformation, and relation to shift/reset under thetyped framework. We emphasize that our typesystem does not need recursive types, but does
have let polymorphism. We have also shownthat answer type polymorphism of shift can bederived from let polymorphism.
Future work includes studies on the following
topics:• Type inference algorithm for our type system.
• Answer type modiﬁcation: the type systemin this paper does not allow modiﬁcation of

8

IPSJ Journal

answer types. We are working on a typesystem which does not have this restriction12) .
• Multi-level control operators.
• More general polymorphism.
Acknowledgments We would like to thankthe anonymous referees and the attendees of
the SIG-Programming meeting for useful comments. This work was partly supported by
JSPS Grant-in-Aid for Scientiﬁc Research (C)16500004.
References
1) Felleisen, M.: The Theory and Practice ofFirst-Class Prompts, POPL ’88: Proceedings ofthe 15th ACM SIGPLAN-SIGACT symposiumon Principles of programming languages, New
York, NY, USA, ACM, pp. 180–190 (1988).
2) Danvy, O. and Filinski, A.: Abstracting Control, LFP ’90: Proceedings of the 1990 ACM
conference on LISP and functional programming, New York, NY, USA, ACM, pp. 151–160(1990).
3) Filinski, A.: Representing Monads, POPL
’94: Proceedings of the 21st ACM SIGPLANSIGACT symposium on Principles of programming languages, New York, NY, USA, ACM,
pp. 446–457 (1994).
4) Biernacka, M., Biernacki, D. and Danvy, O.:
An Operational Foundation for Delimited Continuations, Proceedings of the 4th ACM SIGPLAN Workshop on Continuations, Technical
Report CSR-04-1, School of Computer Science,
University of Birmingham, pp. 25–34 (2004).
5) Kameyama, Y. and Hasegawa, M.: A Soundand Complete Axiomatization of Delimited
Continuations, ICFP ’03: Proceedings of the
8th ACM SIGPLAN international conference
on Functional programming, New York, NY,
USA, ACM, pp. 177–188 (2003).
6) Biernacki, D., Danvy, O. and Millikin, K.: A
Dynamic Continuation-Passing Style for Dynamic Delimited Continuations, Technical Report BRICS-RS-05-16, BRICS, University of
Aarhus, Denmark (2005).
7) Asai, K. and Kameyama, Y.: Polymorphic Delimited Continuations, APLAS ’07: Proceedings of 5th Asian Symposium on Programming
Languages and Systems, LNCS 4807 , pp. 239–
254 (2007).
8) Queinnec, C.: The Inﬂuence of Browsers on
Evaluators or, Continuations to Program Web
Servers, ICFP ’00: Proceedings of the 5th ACM
SIGPLAN international conference on Functional programming, New York, NY, USA,ACM, pp. 23–33 (2000).

19599) Kiselyov, O., chieh Shan, C. and Sabry, A.:
Delimited Dynamic Binding, ICFP ’06: Proceedings of the 11th ACM SIGPLAN international conference on Functional programming,
New York, NY, USA, ACM, pp. 26–37 (2006).
10) Biernacki, D., Danvy, O. and Shan, C.: On theStatic and Dynamic Extents of Delimited Continuations, Technical Report BRICS-RS-05-36,
BRICS, University of Aarhus, Denmark (2005).
11) Asai, K.: On Typing Delimited Continuations:Three New Solutions to the Printf Problem(2007). Submitted. See
http://pllab.is.ocha.ac.jp/~asai/papers/.
12) Kameyama, Y. and Yonezawa, T.: Typed Dynamic Control Operators for Delimited Continuations (2008). FLOPS ’08: Proceedingsof 9th International Symposium on Functionaland Logic Programming.
13) Biernacki, D. and Danvy, O.: A Simple
Proof of a Folklore Theorem about Delimited
Control, Technical Report BRICS-RS-05-25,
BRICS, University of Aarhus, Denmark (2005).
14) Wright, A. K. and Felleisen, M.: A Syntactic
Approach to Type Soundness, Information andComputation, Vol. 115, No. 1, pp. 38–94 (1994).
15) Thielecke, H.: From Control Eﬀects to Typed
Continuation Passing, POPL ’03: Proceedingsof the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages,
New York, NY, USA, ACM, pp. 139–149(2003).

Appendix
A.1 Proof
We ﬁrst prove several lemmas which are necessary to prove subject reduction.
Lemma 1 (Weakening of Type Environment). If Γ ` M : τ /α is derivable and a variable x does not freely occur in M , Γ[x 7→ σ] `M : τ /α is derivable.
If Γ `p M : τ is derivable and a variable x
does not freely occur in M , Γ[x 7→ σ] `p M : τ
is derivable.
Proof. By structural induction on the derivation.
Lemma 2 (Substitution for Monomorphic
Variable). If Γ1 `p v : β and Γ2 [x 7→ β] `M : τ /α is derivable and Γ1 ⊆ Γ2 , then Γ2 `M [v/x] : τ /α is derivable.
If Γ1 `p v : β and Γ2 [x 7→ β] `p M : τ isderivable and Γ1 ⊆ Γ2 , then Γ2 `p M [v/x] : τ
is derivable.
Proof. By mutual structural induction on theVol. 0

No. 0

A Type System for Dynamic Delimited Continuations

derivation of M and Lemma 1.
We omit the proof since it is almost the sameas (and simpler than) the proof of Lemma 3.
Lemma 3 (Substitution for Polymorphic
Variable). If Γ1 `p v : σ and Γ2 [x 7→Gen(σ; Γ1 )] ` M : τ /α is derivable and Γ1 ⊆
Γ2 , then Γ2 ` M [v/x] : τ /α is derivable.
If Γ1 `p v : σ and Γ2 [x 7→ Gen(σ; Γ1 )] `p
M : τ is derivable and Γ1 ⊆ Γ2 , then Γ2 `p
M [v/x] : τ is derivable.
Proof. From Γ1 `p v : σ, we can derive Γ2 ` v :β/α by Lemma 1. We use structural induction
on the type derivation of M .
Case 1. If the last derivation is a derivation
for a variable and M = x, then we can derive Γ2 `p M [v/x] : τ since τ ≤ Gen(σ; Γ1 )and we can systematically replace type variables FTV(τ ) − FTV(Γ) in the derivation ofΓ2 ` v : β to arbitrary type variables. If M isa variable with M 6= x, it is obvious.
Case 2. The other cases are proved by simple
induction, since in all typing rules, type environment used in the conclusion is smaller thanor equal to one in the premises.
Lemma 4. If Γ ` P [M ] : τ /α is derivable,
then Γ ` M : σ/α is derivable for some σ.
Proof. By structural induction on P .
Lemma 5. If Γ ` P [M ] : τ /α is derivable andΓ ` M : σ/α is derivable, Γ `p λx.P [x] : (σ →τ /α) is derivable for a fresh variable x.
Proof. Case analysis on P .
Case 1. If P = [ ], it is obvious.
Case 2. If P = P 0 M 0 , the last part of thederivation of Γ ` P [M ] : τ /α must be:Γ ` P 0 [M ] : (ρ → τ /α)/α Γ ` M 0 : ρ/αΓ ` P 0 [M ] M 0 : τ /α
By the assumption of induction, we can derive Γ ` λx.P 0 [x] : (σ → (ρ → τ /α)/α andΓ[x 7→ σ] ` P 0 [x] : (ρ → τ /α)/α.
Thereby, we can derive Γ `p λx.P 0 [x] M 0 :(σ → τ /α), that is, Γ `p λx.P [x] : (σ → τ /α)
as follows:Γ[x 7→ σ] ` P 0 [x] : (ρ → τ /α)/αΓ[x 7→ σ] ` M 0 : ρ/α00Γ[x 7→ σ] ` P [x] M : τ /αΓ `p λx.P 0 [x] M 0 : (σ → τ /α)9Case 3. If P = v P 0 , we can prove it similarly
to the case for P = P 0 M .
Theorem 2 (Subject Reduction). If Γ `M1 : τ /α is derivable and M1 →∗ M2 , thenΓ ` M2 : τ /α is derivable.
Proof. We show the case of one-step reduction. The other case can be derived straightforwardly.
Now we will perform case analysis on the reduction rule used in the one-step reduction.
Case 1 (β reduction and elimination of let). If
the reduction is the β reduction ((λx.M )v →M [v/x]), the statement holds by Lemma 2. If
the reduction is the elimination of let (let x =v in M → M [v/x]), the statement holds byLemma 3.
Case 2 (elimination of prompt). If the reduction is the elimination of prompt (#v → v),
then, by assumption, we have the following
derivation:..
..
Γ `p v : τΓ ` v : τ /τΓ `p #v : τ
Therefore, the statement holds in this case.
Case 3 (elimination of control). If the reduction is the elimination of control (#P [Fc.M ] →#M [λx.P [x]/c]), then we have the following
derivation by the assumption and Lemma 4.
Γ[c 7→ (π → τ /τ )] ` M : τ /τΓ ` F c.M : π/τ..
..
Γ ` P [Fc.M ] : τ /τΓ `p #P [Fc.M ] : τApplying Lemma 5, we can deriveΓ `p λx.P [x] : (π → τ /τ )and applying Lemma 2, we can deriveΓ ` M [λx.P [x]/c] : τ /τHence we can derive the following judgment
by applying the typing rule for prompt.
Γ `p #M [λx.P [x]/c] : τConsequently, Subject Reduction holds.
Theorem 3 (Progress). If ∅ `p #M : τ isderivable, then either M is a value, or #M
can be uniquely decomposed into the form E[R]
where E is an evaluation context and R is a

10

IPSJ Journalτ ::=(monomorphic type)t(type variable)| (τ → τ /τ )(function type)| List τ(list)| µt.τ
(recursive type)A ::=(polymorphic type)τ | ∀t.AΓ ::=(type environment)∅(empty type environment)| Γ[x 7→ A](type environment)
Fig. 9 Syntax of type and type environment of thetarget language

redex.
Proof. We can prove that if M is not a value,
we can decompose it to the unique forms P [R],P [Fc.M 0 ], or P [#M 0 ].
If it is decomposed to P [R], the theorem
holds.
If it is decomposed to P [Fc.M 0 ], combining P with the outer #, it becomes a redex#P [Fc.M 0 ] and the theorem holds.
If it is decomposed to P [#M 0 ], if M 0 is avalue, it is trivial. Otherwise, we recursively
decompose M 0 to E 0 [R], and let E[ ] be P [E 0 [ ]],and the theorem holds.

Proof (Theorem 4), Preservation of Types.
We prove that, if Γ ` M : τ /α is derivable in the source calculus, then Γ∗ ` [ M ] :(Cont1 τ ∗ α∗ ) → (Ans α∗ ) is derivable in thetarget calculus. This is proved by induction on
the derivation of Γ ` M : τ /α, and we state
several important cases here.
Case 1 (M = #M 0 ). We have the following
derivation:..
..
Γ ` M 0 : τ /τΓ `p #M 0 : τand by the induction hypothesis, we have:Γ∗ ` [ M 0 ] : (Cont1 τ ∗ τ ∗ ) → (Ans τ ∗ )in the target calculus.
Note that θ1 , deﬁned in Fig. 5 has typeCont1 α α for any type α, and therefore `θ1 : Cont1 τ ∗ τ ∗ is derivable. We also have
` Nil : Trail τ ∗ and∅[k1 7→ Cont1 τ ∗ τ ∗ ][t1 7→ Trail τ ∗ ][k2 7→ τ ∗ → ∗]` λv.k1 vt1 k2 : (τ ∗ → ∗)1959

Then it is easy to see that:Γ∗ `λk1 t1 k2 .[[M 0 ] θ1 Nil (λv.k1 v t1 k2 ): (Cont1 τ ∗ τ ∗ ) → (Ans τ ∗ )Case 2 (M = Fx.M 0 ). We have the following
derivation:..
..
Γ[c 7→ (τ → α/α)] ` M 0 : α/αΓ ` Fc.M 0 : τ /α
By the induction hypothesis, we have:Γ∗ [c 7→ τ ∗ → (Cont1 α∗ α∗ ) → (Ans α∗ )]` [ M 0 ] : (Cont1 α∗ α∗ ) → (Ans α∗ )in the target calculus.
Let ∆ = Γ∗ [k1 7→ Cont1 τ ∗ α∗ , t1 7→
Trail α∗ , k2 7→ α∗ → ∗] and Σ = ∆[c 7→ τ ∗ →(Cont1 α∗ α∗ ) → (Ans α∗ )].
Then, we can derive:∆ `λv k10 t01 k20 .k1 v (t1 @(k10 :: t01 )) k20: τ ∗ → (Cont1 α∗ α∗ ) → (Ans α∗ )Σ `[[M 0 ] θ1 Nil k2 : ∗Then we can derive:Γ∗ ` [ Fx.M ] : (Cont1 τ ∗ α∗ ) → (Ans α∗ )Case 3 (M = let x = v in M ). We have thefollowing derivation:
..
..
..
..
Γ `p v : σ Γ[x 7→ Gen(σ; Γ)] ` M : τ /αΓ ` let x = v in M : τ /α
By induction hypothesis, we have:Γ∗ ` v ∗ : σ ∗andΓ∗ [x 7→ Gen(σ ∗ ; Γ∗ )]` [ M ] : (Cont1 τ ∗ α∗ ) → (Ans α∗ )in the target calculus.
Let ∆ = Γ∗ [k1 7→ Cont1 τ ∗ α∗ , t1 7→
Trail α∗ , k2 7→ α∗ → ∗].
Then we can easily derive ∆ [x 7→Gen(σ ∗ ; Γ∗ )] ` [ M ] k1 t1 k2 : ∗.
Altogether, we can derive:∆ ` v∗ : σ∗∆[x 7→ Gen(σ ∗ ; Γ∗ )] ` [ M ] k1 t1 k2 : ∗∆ ` let x = v ∗in [ M ] k1 t1 k2 : ∗Γ∗ `[[ let x = v in M ]: (Cont1 τ ∗ α∗ ) → (Ans α∗ )Proof (Theorem 5), Preservation of Equality.
We show the interesting case only, that is,
M1 =#P [Fc. M 0 ]M2 =#M 0 [(λx. P [x])/c]
We let[ P [M ]]] = λk1 t1 k2 . [ M ] (f k1 ) t1 k2
We then transform [ M1 ] as follows:Vol. 0

No. 0

A Type System for Dynamic Delimited Continuations

11

Γ[x 7→ σ] ` M : τΓ(x) = A τ ≤ A
λ abstraction
variableΓ`x:τΓ ` λx.M : (σ → τ )Γ ` M1 : (σ → τ ) Γ ` M2 : σΓ ` M1 : σ Γ[x 7→ Gen(σ; Γ)] ` M1 : τfunction applicationletΓ ` M1 M2 : τΓ ` let x = M1 in M2 : τΓ ` Nil : List τ

empty listΓ ` M1 : τ Γ ` M2 : List τlistΓ ` (M1 :: M2 ) : List τΓ ` M0 : List σ Γ ` M1 : τ Γ[x 7→ σ][y 7→ List σ] ` M2 : τcaseΓ ` case M0 of Nil ⇒ M1 (x :: y) ⇒ M2 : τΓ ` M : τ [µt.τ /t]Γ ` M : µt.τ
unrollrollΓ ` M : µt.τΓ ` M : τ [µt.τ /t]
Fig. 10 Typing rules of target language[ M1 ] =λk1 t1 k2 .
(λk10 t01 k20 . [ Fc. M 0 ] (f k10 ) t01 k20 )θ1 Nil (λv. k1 v t1 k2 )=λk1 t1 k2 . [ Fc. M 0 ](f θ1 ) Nil (λv. k1 v t1 k2 )=λk1 t1 k2 .
let c = λv k10 t01 k20 . (f θ1 ) v(k10 :: t01 ) k20
0
in [ M ] θ1 Nil (λv. k1 v t1 k2 )=λk1 t1 k2 .
[ M 0 ] [(λv k10 t01 k20 . (f θ1 ) v(k10 :: t01 ) k20 )/c]
θ1 Nil (λv. k1 v t1 k2 )Moreover, we transform [ M2 ] as follows:[ M2 ] = λk1 t1 k2 .
[ M 0 [(λx. P [x])/c]]]
θ1 Nil (λv. k1 v t1 k2 )= λk1 t1 k2 .
[ M 0 ] [(λv. [ P [v]]])/c]
θ1 Nil (λv. k1 v t1 k2 )= λk1 t1 k2 .
[ M 0 ] [(λv k10 t01 k20 . (f k10 ) v
t01 k20 )/c]
θ1 Nil (λv. k1 v t1 k2 )Hence, we only need show the following equation.
(λv k10 t01 k20 . (f k10 ) v t01 k20 )=(λv k10 t01 k20 . (f θ1 ) v (k10 :: t01 ) k20

We can transform these expressions as follows:(λv k10 t01 k20 . (f k10 ) v t01 k20 )=(λv k10 t01 k20 . [ P [v]]] k10 t01 k20 )(λv k10 t01 k20 . (f θ1 ) v (k10 :: t01 ) k20 )=(λv k10 t01 k20 . [ P [v]]] θ1 (k10 :: t01 ) k20 )By the deﬁnition of the equality of the target
language, we have that these two expressions
are equal.
(Received ??? ??, ????)(Accepted ??? ??, ????)
Takuo Yonezawa is a Graduate Student of the Master’s
Program at the Departmentof Computer Science, Graduate
School of Systems and Information Engineering, University ofTsukuba.
He is interested in type systems and computational eﬀects of programming languages.
e-mail: yone@logic.cs.tsukuba.ac.jp
URL: http://logic.cs.tsukuba.ac.jp/˜yone/
Yukiyoshi Kameyama is
an Associate Professor of Computer Science at the Graduate
School of Systems and Information Engineering, University ofTsukuba. He is interested inprogramming logic and software
veriﬁcation. He is a member of ACM, JSSST,
and IEICE.
e-mail: kameyama@acm.org
URL: http://logic.cs.tsukuba.ac.jp/˜kam/