Strong Normalization of Polymorphic Calculus for
Delimited Continuations
Yukiyoshi Kameyama1 and Kenichi Asai2
1

Department of Computer Science, University of Tsukuba
kameyama@acm.org
2
Department of Information Science, Ochanomizu University
asai@is.ocha.ac.jp

Abstract. The notion of delimited continuations has been proved useful in various
areas of computer programming such as partial evaluation, mobile computing, andweb transaction. In our previous work, we proposed polymorphic calculi with control
operators for delimited continuations. This paper presents a proof of strong normalization (SN) of these calculi based on a reﬁned (i.e. administrative redex-free) CPS
translation.
Keywords: Type System, Delimited Continuation, Control Operator, CPS Translation, Predicative Polymorphism.

1

Introduction

Control operators in functional languages allow the explicit manipulation of control ﬂow ofprograms, and thus give more ﬂexibility and expressiveness than those programs withoutthem. Scheme has the control operator “call/cc” for continuations, which has been intensively
studied from theory to implementation and practical applications. Type-theoretic studies on“call/cc” have revealed that it corresponds to classical logic [10].
Delimited continuation is a similar notion to (unlimited) continuation, but it represents
part of the rest of the computation rather than whole rest of the computation. Since Danvy
and Filinski have proposed the control operators “shift” and “reset” for delimited continuations [6], they have been proved useful in various applications such as backtracking [6],A-normalization in direct style [2], let-insertion in partial evaluation [17], type-safe “printf”[3], and web transaction [15].
This paper investigates the type structure of “shift” and “reset”, and in particular, proves
strong normalization of a polymorphic calculus for them. In our previous work [4], we haveintroduced a polymorphic type system for “shift” and “reset”, and proved a number of properties such as type soundness (subject reduction and progress). The strong normalization
property, however, was only mentioned as a theorem without a proof, which is the subjectof the present paper.
Strong normalization (SN) is the property that no reduction sequence can be inﬁnite,
and is considered as one of the most fundamental properties of many typed lambda calculi
which correspond to logical systems under the Curry-Howard isomorphism. For instance,strong normalization of Girard’s System F [9] implies its (logical) consistency.
On the other hand, strong normalization of computational calculi with control operators
is a subtle issue as shown by the following list:

v ::= c | x | λx.e

value

e ::= v | e1 e2 | Sk.e | hei | let x = e1 in e2| if e1 then e2 else e3

expression
s/r

Fig. 1. Syntax of λlet .

– A typed calculus with “call/cc” is strongly normalizing, while that with exception inStandard ML is not strongly normalizing (see, for instance, [11]).
– The calculus with “shift” and “reset” under Filinski’s typing3 is not normalizing, while,
under Danvy and Filinski’s type system, it is strongly normalizing [1].
– A typed calculus with “control” and “prompt”, the other control operators for delimited continuations, is not normalizing [13]. Similarly, a typed calculus with the control
operator cupto is not normalizing [14].
Hence, we can say SN for the calculi with control operators is a non-trivial issue. This
paper solves the problem for the case of “shift” and “reset” under the polymorphic typesystem.
The rest of this paper is organized as follows: Section 2 gives the syntax and semanticsof the polymorphic calculus for shift and reset in [4], and Section 3 reviews the deﬁnitional
CPS translation for this calculus. In Section 4 we introduce a reﬁned CPS translation andstudy its properties. In Section 5, we prove strong normalization of our calculus by making
use of the reﬁned CPS translation. Section 6 gives conclusion.

2

A Polymorphic Calculus with Shift/Resets/r

In this section we introduce the polymorphic typed calculi λlet for shift and reset in [4].
Following the literature, we distinguish two versions of polymorphism: predicative polymorphism (or let-polymorphism) found in ML families and impredicative polymorphism which
is based on the second order lambda calculus (Girard’s System F [9]). In this paper, weconcentrate on the predicative version.
2.1

Syntax and Operational Semantics

We assume that the sets of constants (denoted by c), variables (denoted by x, y, k, f ), typevariables (denoted by t), and basic types (denoted by b) are mutually disjoint, and that eachconstant is associated with a basic type. We assume bool is a basic type which has constantstrue and false.
s/r
The syntax of λlet is given in Figure 1. A value is either a constant, a variable or a lambda
abstraction. An expression is either a value, an application, a shift expression (denoted bySk.e), a reset expression (denoted by hei), a let expression, or a conditional. Note that weomit the ﬁxpoint operator from the calculus in [4].
3Filinski did not give a type system explicitly, but his well-known implementation of “shift” and“reset” [8] speciﬁes a certain type system.

2

(λx.e)v Ã e[v/x]hvi Ã vhF [Sk.e]i Ã hlet k = λx.hF [x]i in ei
let x = v in e Ã e[v/x]if true then e1 else e2 Ã e1
if false then e1 else e2 Ã e2
s/r

Fig. 2. Reduction rules for λlet
α, β, γ, δ ::= t | b | (α/γ → β/δ)monomorphic type

A ::= α | ∀t.A

polymorphic types/r

Fig. 3. Types of λlet .

Variables are bound by lambda or shift (k is bound in the expression Sk.e), and are freeotherwise. FV(e) denotes the set of free variables in e.
s/r
We give call-by-value operational semantics for λlet . Contexts, pure evaluation contexts(abbreviated as pure e-contexts), and redexes are deﬁned as follows:
C ::= [ ] | λx.C | eC | Ce | Sk.C | hCi | let x = C in e | let x = e in C
| if C then e else e | if e then C else e | if e then e else C
F ::= [ ] | vF | F e | if F then e else e
R ::= (λx.e)v | hvi | hF [Sk.e]i | let x = v in e
| if true then e1 else e2 | if false then e1 else e2

context
pure e-context
redex

A pure e-context F is an evaluation context such that no reset encloses the hole. Therefore,
in the redex hF [Sk.e]i, the outermost reset is guaranteed to be the one corresponding tothis shift, i.e., no reset exists inbetween.
The notion of one-step reduction Ã is deﬁned by C[R] Ã C[e] where C is an arbitrary
context 4 and R Ã e is an instance of reductions in Figure 2. In this ﬁgure, e[v/x] denotes theordinary capture-avoiding substitution. As usual, Ã∗ (and Ã+ , resp.) denotes the reﬂexivetransitive (transitive, resp.) closure of Ã.
2.2

Type Systems/r

The type system of λlet is an extension of Danvy and Filinski’s monomorphic type system
for shift and reset [5].
Types are deﬁned by Figure 3, which are similar to those in core ML except that thefunction type is annotated with two answer types as (α/γ → β/δ) where γ (and δ, resp.)
4Note that we have slightly extended the notion of one-step reduction from our previous paper [4]where the context enclosing a redex must be an evaluation context, not a general context. Hencethe SN property in this paper is slightly stronger than the one in [4].

3(x : A ∈ Γ and τ ≤ A)
(c is a constant of basic type b)
var
const
Γ `p x : τΓ `p c : b
Γ, x : σ; α ` e : τ ; βfunΓ `p λx.e : (σ/α → τ /β)Γ ; γ ` e1 : (σ/α → τ /β); δ Γ ; β ` e2 : σ; γapp
Γ ; α ` e1 e2 : τ ; δΓ, k : ∀t.(τ /t → α/t); σ ` e : σ; βshift
Γ ; α ` Sk.e : τ ; βΓ `p e : τexp
Γ; α ` e : τ; α

Γ ; σ ` e : σ; τresetΓ `p hei : τΓ `p e1 : σ Γ, x : Gen(σ; Γ ); α ` e2 : τ ; βlet
Γ ; α ` let x = e1 in e2 : τ ; β
Γ ; σ ` e1 : bool; β Γ ; α ` e2 : τ ; σ Γ ; α ` e3 : τ ; σif
Γ ; α ` if e1 then e2 else e3 : τ ; β
s/rFig. 4. Type Inference Rules of λlet .

denotes the answer type before (after, resp.) the execution of the function body. See Asai
and Kameyama [4] for details. A type variable is bound by the universal quantiﬁer ∀ asusual, and FTV(α) denotes the set of free type variables in α.
A type context (denoted by Γ ) is a ﬁnite list of the form x1 : A1 , · · · , xn : An where thevariables x1 , · · · , xn are mutually distinct, and A1 , · · · , An are (polymorphic) types.
Judgments are either one of the following forms:Γ `p e : τjudgment for pure expression

Γ; α ` e : τ; βjudgment for general expression

The ﬁrst form of the judgment signiﬁes the expression e is a pure expression (free from control
eﬀects), and the second is for an arbitrary expression. We distinguish pure expressions fromother expressions in order to present the restriction of let-polymorphism: polymorphism canbe introduced only for pure expressions, as we can see it from the type inference rule for let
below.
s/r
Figure 4 lists the type inference rules of λlet where τ ≤ A in the rule (var) means
the instantiation of type variables by monomorphic types. Namely, if A ≡ ∀t1 . · · · ∀tn .ρ
for some monomorphic type ρ, then τ ≡ ρ[σ1 , · · · , σn /t1 , · · · , tn ] for some monomorphic
types σ1 , · · · , σn . The type Gen(σ; Γ ) in the rule (let) is deﬁned by ∀t1 . · · · ∀tn .σ where{t1 , · · · , tn } = FTV(σ) − FTV(Γ ).
The type inference rules are a natural extension of the monomorphic type system byDanvy and Filinski [5]. Pure expressions are deﬁned by one of the rules (var), (const), (fun)or (reset). They can be freely turned into general expressions by the rule (exp). Pure expressions can be used polymorphically through the rule (let). It generalizes the standard
let-polymorphism found in ML where the so called value restriction is adopted.5 Finally, therule (shift) is extended to cope with the answer type polymorphism of captured continuations: k is given a polymorphic type ∀t.(τ /t → α/t).
5Note that all values are pure, but pure expressions are not necessarily values.

4

2.3

Properties

In our previous paper [4], we claimed that our calculus provides a good foundation forstudying the interaction between polymorphism and delimited continuations. To support
this claim, we have presented the proofs of the following properties: Strong Type Soundness,
Existence of Principal Types, and Preservation of types and equality through CPS translation. We have also stated Conﬂuence and Strong Normalization for the calculus, but did
not present the proofs.
In this subsection, we quickly review the properties which were proved in [4].6
Theorem 1 (Subject Reduction). If Γ ; α ` e1 : τ ; β is derivable and e1 Ã∗ e2 , then
Γ ; α ` e2 : τ ; β is derivable. Similarly, if Γ `p e1 : τ is derivable and e1 Ã∗ e2 , thenΓ `p e2 : τ is derivable.
Theorem 2 (Progress). If `p hei : τ is derivable, then hei can be reduced.
By Theorems 1 and 2, we can conclude that our type system is sound (strong typesoundness in the sense of [18]).
s/r

Theorem 3 (Principal Type and Type Inference). In λlet , principal type exists, andwe can construct a sound and complete type inference algorithm as an extension of HindleyMilner’s algorithm.

3

Deﬁnitional CPS Translation

A CPS translation is a translation from one calculus (typically with control operators) to asimpler calculus (typically without control operators). It allows us to investigate the semantic
structure of the source calculus. The merit of shift and reset over other control operators fordelimited continuations comes from the fact that there exists a simple, compositional CPS
translation. Danvy and Filinski gave the precise semantics of shift and reset in terms of a
CPS translation [6, 7], and based on their translation, various theoretical results as well as
applications using shift and reset have been proposed (see, for instance, [12]).
In this section, we present an extension of Danvy and Filinski’s CPS translation, namely,
s/ra CPS translation from λlet to a pure polymorphic lambda calculus λlet . We call this CPS
s/rtranslation as “deﬁnitional” one, since it deﬁnes the semantics of λlet .
In the following, we ﬁrst deﬁne the target calculus λlet , and then present the deﬁnitional
CPS translation.
3.1

Target Calculus λlet
s/r

The syntax of values and expressions in λlet are the same as those in λlet except that λletdoes not have control operators shift and reset. Types of λlet are standard and given by:

6α, β ::= t | b | α → βmonomorphic type

A ::= α | ∀t.A

polymorphic type

Strictly speaking, these theorems are extended versions of the corresponding theorems in [4],since the notion of reduction in this paper is slightly extended.

5(x : A ∈ Γ and τ ≤ A)var
Γ `x:τ
Γ, x : α ` e : βfunΓ ` λx.e : α → β(c is a constant of basic type b)constΓ `c:bΓ ` e1 : α → β Γ ` e2 : αappΓ ` e1 e2 : βΓ ` e1 : σ Γ, x : Gen(σ; Γ ) ` e2 : βletΓ ` let x = e1 in e2 : βΓ ` e1 : bool Γ ` e2 : β Γ ` e3 : βif
Γ ` if e1 then e2 else e3 : β

Fig. 5. Type Inference Rules of λletb∗ = bfor a basic type b

∗

t =t

for a type variable t((α/γ → β/δ))∗ = α∗ → (β ∗ → γ ∗ ) → δ ∗(∀t.A)∗ = ∀t.A∗(Γ, x : A)∗ = Γ ∗ , x : A∗
Fig. 6. CPS translation for types and type contexts.

Figure 5 deﬁnes the type inference rules of λlet . Note that, in the type inference rulefor (let), there is no side condition on the expression e1 . Hence, for instance, an expression
s/r
let x = yz in x is not typable in λlet , but is typable in λlet .
s/r

The reduction rules for λlet are the same as those for λlet restricted to the expressions
in λlet , and are omitted.

3.2

s/r

Deﬁnitional CPS Translation from λlet to λlet

Figures 6 and 7 deﬁne the deﬁnitional CPS translation for λlet where the variables κ, κ0 , m
and n are fresh. The type (α/γ → β/δ) is translated to the type of a function which, given
a parameter of type α∗ and a continuation of type β ∗ → γ ∗ , returns a value of type δ ∗ .
In [4], we proved that the CPS translation preserves types and equality.
s/r

s/r

Theorem 4 (Preservation of Types). If Γ ; α ` e : τ ; β is derivable in λlet , thenΓ ∗ ` [ e]] : (τ ∗ → α∗ ) → β ∗ is derivable in λlet .
s/r
If Γ `p e : τ is derivable in λlet , then Γ ∗ ` [ e]] : (τ ∗ → γ) → γ is derivable for an
arbitrary type γ in λlet .
Theorem 5 (Preservation of Equality). If Γ ; α ` e1 : τ ; β is derivable and e1 Ã∗ e2
s/r
in λlet , then [ e1 ] = [ e2 ] in λlet where = is the least congruence relation containing Ã inλlet .
Note that Theorem 5 only guarantees that the equality is preserved through the CPS
translation. In fact, we cannot show that e1 Ã e2 implies [ e1 ] Ã∗ [ e2 ] .
6c∗ = cx∗ = x(λx.e)∗ = λx.[[e]][ v]] = λκ.κv ∗[ e1 e2 ] = λκ.[[e1 ] (λm.[[e2 ] (λn.mnκ))[ Sk.e]] = λκ.let k = λnκ0 .κ0 (κn) in [ e]](λm.m)[ hei]] = λκ.κ([[e]](λm.m))[ let x = e1 in e2 ] = λκ.let x = [ e1 ] (λm.m) in [ e2 ] κ[ if e1 then e2 else e3 ] = λκ.[[e1 ] (λm.if m then [ e2 ] κ else [ e3 ] κ)
Fig. 7. CPS translation for values and expressions.
e ::= c | x | λx.e | λx.e | e1 @e2 | e1 @e2| let x = e1 in e2 | if e1 then e2 else e3α, β ::= t | b | α→β | α→βexpression
monomorphic type

A ::= α | ∀t.A

polymorphic typeFig. 8. Syntax of Two-Level Polymorphic Lambda Calculus.

4

Reﬁned CPS Translation

The deﬁnitional CPS translation is useful in the semantic study of shift and reset. However,it does not preserve reductions, and hence cannot be used to prove SN. The failure ofpreservation of reduction is due to the fact that the CPS translation introduces a lot of
administrative redexes through the translation.
To overcome this diﬃculty, we reﬁne the deﬁnitional CPS translation so that it may
produce fewer administrative redexes. There are several ways to deﬁne such optimized CPS
translations since Plotkin proposed Colon Translation [16]. Here we use an extended versionof two-level lambda calculus [7] as the target calculus of the translation, and deﬁne a reﬁned
s/r
CPS translation from λlet to it.
4.1

Two-Level Version of Polymorphic Lambda Calculus

In this subsection we introduce λ2Llet , a two-level version of polymorphic typed lambda calculus (without control operators). In this calculus, function spaces are classiﬁed into two static one and dynamic one. Accordingly, each occurrence of λ and application (explicitly
denoted by “@”) is annotated by overlines (static) as λ and @, or underlines (dynamic) as λand @. In their original article, Danvy and Filinski classiﬁed every construct into two, buthere we only classify lambda’s and applications, and we assume that the other constructs
are implicitly classiﬁed as dynamic ones.
Figure 8 gives the syntax of λ2Llet , which is an annotated variant of λlet .
Figure 9 gives the type system of λ2Llet , where the type inference rules for (var), (const),(let), and (if) are the same as those in λlet , and are omitted.
7

Γ, x : α ` e : βstatic fun, x ∈ FV(e) Γ, x : α ` e : β dynamic funΓ ` λx.e : α→βΓ ` λx.e : α→βΓ ` e1 : α→β Γ ` e2 : αΓ ` e1 : α→β Γ ` e2 : αstatic app
dynamic app
Γ ` e1 @e2 : βΓ ` e1 @e2 : β
Fig. 9. Type Inference Rules of Two Level Polymorphic Calculus.

The crucial diﬀerence of the type system of λ2Llet from that of λlet (besides the annotations)is the side condition x ∈ FV(e) in the static function:
Γ, x : α ` e : βΓ ` λx.e : α→βstatic fun, x ∈ FV(e)The condition imposes that the abstracted variable x must occur freely in e.
We put this side condition by the following reason: we will use the static lambda abstraction to constitute an administrative redex (a redex which does not exist in the source
expression, and is created by the CPS translation). When we prove that the CPS translation
preserves reductions, it is important to guarantee that reducing an administrative redex does
not discard any subexpressions, hence we put the side condition.
Note that the static lambda expression is not necessarily linear, namely, x may appear
more than once in e, since CPS translating conditional expressions (if-then-else) may duplicate the arguments of continuations. Note also that the side condition is not applied to
dynamic lambda abstraction which corresponds to lambda abstraction in the source express/rsion. In other words, the actual continuations in λlet may discard their arguments.
2L
The operational semantics of λlet is given as regarding the only redex as the static βredex. Namely, the following single rule constitutes the notion of reduction in λ2Llet :(λx.e1 )@e2 Ã e1 [e2 /x]
Note that this is full β-reduction, rather than the call-by-value variant.
For this notion of reduction, we have subject reduction, strong normalization and conﬂuence as follows.
0
Theorem 6 (Subject Reduction). If Γ ` e : α is derivable in λ2Llet , and e Ã e by
reducing static β-redexes only, then Γ ` e0 : α is derivable in λ2L.
let

Note that this theorem is not trivial, as we have a side condition in the typing rule forstatic lambda abstractions.
Proof. Since all static lambda abstractions λx.e satisfy the side condition x ∈ FV(e), all freevariables in (λx.e)@e0 occur in e[e0 /x] freely, so the result of static β-reduction also satisﬁes
the side condition, too.
Theorem 7. Static reduction Ã in λ2L
let is conﬂuent and strongly normalizing.
Proof. Since we can embed λ2L
let into the second order lambda calculus (where we only
consider static reductions in λ2Llet ), strong normalization is apparent. We can easily provethat static reduction is Church-Rosser, since dynamic constructs are not reduced throughthe reduction.
8b∗ = bfor a basic type b

∗

t =t

for a type variable t(α/γ → β/δ)∗ = α∗ →(β ∗ →γ ∗ )→δ ∗(∀t.A)∗ = ∀t.A∗(Γ, x : A)∗ = Γ ∗ , x : A∗
Fig. 10. Reﬁned CPS translation for types.

By this theorem, for each expression e in λ2Llet , its normal form uniquely exists (thenormality is deﬁned with respect to the static β-reduction). The normal form of e is denoted
by NF(e).
4.2

Reﬁned CPS Translations/r

The reﬁned CPS translation is a syntax-directed translation from λlet to λ2L
let where we use
static constructs (λ and @) for administrative redexes, and dynamic constructs (λ, @ andall other constructs) for source redexes.
s/r
Given an expression e in λlet and an expression K in λ2Llet , we deﬁne an expression [ e, K]]
2L
in λlet as the CPS translation for e with respect to the continuation K. We ﬁrst deﬁne thetranslation for types in Figure 10.

x∗ = xc∗ = c(λx.e)∗ = λx.λκ.[[e, λm. κ@m]][ v, K]] = K@v ∗[ e1 e2 , K]] = [ e1 , λm1 .[[e2 , λm2 .(m1 @m2 )@(λn. K@n)]]][ hei, K]] = K@[[e, λm.m]][ Sk.e, K]] = let m1 = true inlet k = λn.λκ0 .κ0 @(K@n) in [ e, λm.m]][ let x = e1 in e2 , K]] = let x = [ e1 , λm.m]] in [ e2 , K]][ if e1 then e2 else e3 , K]] = [ e1 , λm.if m then [ e2 , K]] else [ e3 , K]]]
Fig. 11. Reﬁned CPS translation for expressions and values.

Figure 11 gives the CPS translation for expressions and values where m, m1 , m2 , n,κ, and κ0 are fresh variables. In the deﬁnition for shift, we have added a redundant redex
let m1 = true in · · · for the purpose of SN proof.
The complete CPS transform of an expression e may be deﬁned by C[[e]] ≡ λκ.[[e, λx.κ@x]],
though we do not need this deﬁnition in the proof of strong normalization.
9

Theorem 8 (Preservation of Types).
1. Suppose Γ ; α ` e : τ ; β is derivable in λlet , ∆ ` K : τ ∗ →α∗ is derivable in λ2Llet , and∗∗2L
Γ ∗ , ∆ is a valid type context in λ2L
.
Then
Γ
,
∆
`
[
e,
K]
]
:
β
is
derivable
in
λ
let
let .
s/r
∗
2. Suppose Γ `p e : τ is derivable in λlet and ∆ ` K : τ →γ is derivable in λ2Llet , and∗2L
Γ ∗ , ∆ is a valid type context in λ2Llet . Then Γ , ∆ ` [ e, K]] : γ is derivable in λlet .
s/r

Proof. We can prove this theorem by induction on the derivation of Γ ; α ` e : τ ; β andΓ `p e : τ . Here, we give proofs for a few cases.
s/r(Case e = e1 e2 ) We assume that Γ ; α ` e1 e2 : τ ; β is derivable in λlet and ∆ ` K :∗∗2L
τ →α is derivable in λlet .
By inversion, we haves/r

Γ ; γ ` e1 : (σ/α → τ /β); δin λletΓ ; β ` e2 : σ; γin λlets/rThen by induction hypothesis on e2 , we have:Γ ∗ , ∆ ` [ e2 , λm2 .(m1 @m2 )@(λn. K@n)]] : γ ∗in λ2Lletand by induction hypothesis on e1 , we have:Γ ∗ , ∆ ` [ e1 , λm1 .[[e2 , λm2 .(m1 @m2 )@(λn. K@n)]]] : δ ∗in λ2L
let

Hence we are done.
(Case Γ ; α ` Sk.e : τ ; β) By inversion, we haveΓ, k : ∀t.(τ /t → α/t); σ ` e : σ; βs/r

in λletBy induction hypothesis on e, we have:Γ ∗ , k : ∀t.(τ ∗ →(α∗ →t)→t), ∆ ` [ e, λm.m]] : β ∗in λ2Lletand then it is easy to derive:Γ ∗ , ∆ ` let m1 = true in let k = λn.λκ0 .κ0 @(K@n) in [ e, λm.m]] : β ∗in λ2Llethence we are done.
4.3

Summary of this Section

We can summarize the results in this section as the properties on the following translations:s/rλlet =⇒ λ2L
let =⇒ λlets/r

In the ﬁrst step, the reﬁned CPS translation maps an expression in λlet to an expressionin λ2Llet . Theorem 8 guarantees that this step preserves the type.
In the second step, an expression in λ2L
let is normalized to its unique normal form, which
can be viewed as an expression in λlet by removing all the overlines and underlines.7 Theorem
6 guarantees that this step preserves the type.
We know that the calculus λlet is strongly normalizing, since it can be embedded in,for instance, the second order lambda calculus [9]. Hence, in order to prove the strongs/rs/r
normalizability of λlet , it only remains to show that the composed translation from λlet toλlet preserves reductions, which will be proved in the next section.
7

Note that static constructs may remain in the normal forms.

105Strong Normalizations/r

In this section, we prove that reductions in λlet are preserved by the composed translationof the reﬁned CPS translation and the static reduction in λ2Llet .
Theorem 9 (Preservation of Reduction). Suppose Γ ; α ` e1 : τ ; β is derivable ins/r
λlet , and ∆ ` K : τ ∗ →α∗ is derivable in λ2Llet . Then we have:
1. If e1 Ã e2 by a reduction rule other than the reset-value reduction (hvi Ã v), then
NF([[e1 , K]]) Ã+ NF([[e2 , K]]) in λlet .
2. If e1 Ã e2 by the reset-value reduction (hvi Ã v), then NF([[e1 , K]]) ≡ NF([[e2 , K]]) in λlet .
In the theorem above, we regard expressions in λ2L
let as those in λlet by erasing all overlines
and underlines.
Proof. The ﬁrst part of this theorem is proved by the case analysis of reduction rules usedin e1 Ã e2 .
– If the reduction is the call-by-value β reduction (the ﬁrst reduction in Figure 2), or
reductions for let, or conditional, then the theorem can be proved easily.
– For the reduction hF [Sk.e]i Ã hlet k = λx.hF [x]i in ei, we ﬁrst prove that NF([[F [e], K]]) ≡NF([[e, λm.[[F [m], K]]] ). This property can be easily proved by induction on F . Note that
this property holds for typable expressions only.
Then we can prove:
NF([[hF [Sk.e]i, K]])
≡ NF(K@[[F [Sk.e], λm.m]])≡ NF(K@[[Sk.e, λm0 .[[F [m0 ], λm.m]]] )≡ NF(K@(let m1 = true in let k = λn.λκ0 .κ0 @((λm0 .[[F [m0 ], λm.m]])@n) in [ e, λm.m]]))≡ NF(K@(let m1 = true in let k = λn.λκ0 .κ0 @[[F [n], λm.m]] in [ e, λm.m]]))Ã+ NF(K@(let k = λn.λκ0 .κ0 @[[F [n], λm.m]] in [ e, λm.m]]))In the last step above, since K does not discard its argument by the side condition of
the static lambda expression, the reduction let m1 = true in e1 Ã e1 is preserved,
and at least one step reduction occurs during this sequence. (Recall that we have added
a dummy redex in the reﬁned CPS translation of the shift expression.) We also have:
NF([[hlet k = λx.hF [x]i in ei, K]])
≡ NF(K@let k = λx.λκ.κ@[[F [x], λm.m]] in [ e, λm.m]])and therefore the resulting expressions are the same up to α-equivalence, hence we have:
NF([[hF [Sk.e]i, K]]) Ã+ NF([[hlet k = λx.hF [x]i in ei, K]])The second part of this theorem is proved by a simple calculation, hence we are done.
s/r

We now give the strong normalization property for λlet as a theorem.
11

s/r

Theorem 10 (Strong Normalization). If Γ ; α ` e : τ ; β is derivable in λlet , then there
is no inﬁnite reduction sequence starting from e.
s/rProof. Suppose there is an inﬁnite reduction sequence e1 Ã e2 Ã · · · in λlet . Since thereset-value reduction (hvi Ã v) cannot be applied to an expression inﬁnitely many times,
the reduction sequence must contain inﬁnitely many reductions which are not the reset-value
reduction. Then by Theorem 9, we have an inﬁnite sequence NF(C[[e1 ] ) Ã+ NF(C[[e2 ] ) Ã+ · · · .
But, since the target calculus λlet is a strongly normalizing calculus, we get contradiction.
s/r
Hence, λlet does not have an inﬁnite reduction sequence.
s/r

As a corollary of strong normalization, we obtain conﬂuence of λlet , though it can beproved directly.
s/r

Theorem 11 (Conﬂuence). The notion of reduction in λlet is conﬂuent.
s/rProof. Since the reductions in λlet are not overlapping, they are weakly Church-Rosser(WCR). Church-Rosser property is subsumed by WCR and SN.

6

Conclusion

In this paper, we have presented a proof of strong normalization of the polymorphic calculus
for shift and reset introduced by our previous work. The calculus allows let-polymorphismwith a less restricted condition than the value restriction in ML families.
Let us emphasize that our proof is simple and easy to understand compared with the
SN proofs for the calculi with call/cc and λµ, for which one needs more involved proof. The
simplicity of our proof partly comes from the modularity of the proof, but mainly from thedesign of the control operators shift and reset and the naturality of the type system [4].
For future work, we plan to extend this result to the calculi with impredicative polymorphism given in [4]. Finding a better perspective of strong normalizability of calculi withvarious control operators is also left for future work.
Acknowledgments. We would like to thank Koji Nakazawa, Oleg Kiselyov and Chungchieh Shan for helpful comments. The anonymous referees provided insightful comments.
The ﬁrst author was partly supported by JSPS and FWF under the Japan-Austria
Research Cooperative Program and by JSPS Grant-in-Aid for Scientiﬁc Research 20650003.
The second author was partly supported by JSPS Grant-in-Aid for Scientiﬁc Research (C)18500005.

References
1. Z. M. Ariola, H. Herbelin, and A. Sabry. A type-theoretic foundation of continuations andprompts. In ICFP, pages 40–53, 2004.
2. K. Asai. Logical Relations for Call-by-value Delimited Continuations. In Trends in Functional
Programming, volume 6, pages 63–78, 2007.
3. K. Asai. On Typing Delimited Continuations: Three New Solutions to the Printf Problem. Technical Report OCHA-IS 07-1, Dept. of Information Science, Ochanomizu University, September
2007. 9 pages.
4. K. Asai and Y. Kameyama. Polymorphic Delimited Continuations. In APLAS, pages 239–254,
2007.

12

5. O. Danvy and A. Filinski. A Functional Abstraction of Typed Contexts. Technical Report
89/12, DIKU, University of Copenhagen, July 1989.
6. O. Danvy and A. Filinski. Abstracting Control. In Proc. 1990 ACM Conference on Lisp andFunctional Programming, pages 151–160, 1990.
7. O. Danvy and A. Filinski. Representing Control: a Study of the CPS Transformation. Mathematical Structures in Computer Science, 2(4):361–391, 1992.
8. A. Filinski. Representing Monads. In POPL, pages 446–457, 1994.
9. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts in
Theoretical Computer Science. Cambridge University Press, 1989.
10. T. Griﬃn. A Formulae-as-Types Notion of Control. In POPL, pages 47–58, 1990.
11. R. Harper and M. Lillibridge. Explicit Polymorphism and CPS Conversion. In POPL, pages
206–219, 1993.
12. Y. Kameyama and M. Hasegawa. A Sound and Complete Axiomatization for Delimited Continuations. In ICFP, pages 177–188, 2003.
13. Y. Kameyama and T. Yonezawa. Typed Dynamic Control Operators for Delimited Continuations. In FLOPS, LNCS 4989, pages 239–254, 2008.
14. O. Kiselyov. Simply Typed Lambda-Calculus with a Typed-Prompt Delimited Control is not
Strongly Normalizing. 2006. http://okmij.org/ftp/Computation/Continuations.html.
15. O. Kiselyov. Demo of Persistent Delimited Continuations in OCaml for Nested Web Transactions. In Talk presented at Continuation Fest2008, Tokyo, Japan, 2008.
16. G. D. Plotkin. Call-by-Name, Call-by-Value, and the λ-Calculus. Theoretical Computer Science,
1:125–159, 1975.
17. P. Thiemann. Combinators for Program Generation. J. Funct. Program., 9(5):483–525, 1999.
18. A. K. Wright and M. Felleisen. A Syntactic Approach to Type Soundness. Inf. Comput.,
115(1):38–94, 1994.

13