Axioms for Control Operators in the CPS Hierarchy ∗Yukiyoshi Kameyama

kameyama@acm.org

Department of Computer Science, University of Tsukuba
Abstract. A CPS translation is a syntactic translation of programs, which isuseful for describing their operational behavior. By iterating the standard callby-value CPS translation, Danvy and Filinski discovered the CPS hierarchy andproposed a family of control operators, shift and reset, that make it possible tocapture successive delimited continuations in a CPS hierarchy.
Although shift and reset have found their applications in several areas such as
partial evaluation, most studies in the literature have been devoted to the base levelof the hierarchy, namely, to level-1 shift and reset. In this article, we investigate
the whole family of shift and reset. We give a simple calculus with level-n shift andlevel-n reset for an arbitrary n > 0. We then give a set of equational axioms forthem, and prove that these axioms are sound and complete with respect to the CPS
translation. The resulting set of axioms is concise and a natural extension of thosefor level-1 shift and reset.
Keywords: CPS translation, control operator, delimited continuation, axiomatization, type system

1. Introduction
A CPS translation transforms a source term into continuation-passing
style (CPS for short). It can be regarded as a compilation step, since
it makes explicit the evaluation order of the source program and gives
names to intermediate results. Another motivating fact for CPS is thatit makes it possible to represent various control mechanisms, such as
callcc in Scheme and Standard ML of New Jersey, that give programmers first-class continuations in the source language.
Logically, a CPS translation for the simply typed lambda calculus
is a double negation interpretation from classical logic into minimal
logic, or Friedman’s A-translation [17]. The control mechanisms added
to the source language can also be understood logically. For instance,
Griffin [18] has revealed the Curry-Howard correspondence between thecalculus with callcc and classical logic.
Danvy and Filinski [9, 10] have observed that there is room for amore refined control mechanism. By repeatedly CPS translating theanswer type of the standard CPS translation, they obtained what theycall a CPS hierarchy. Furthermore, they have proposed a family of∗This article is a revised version of the paper presented at CSL’04, September,2004.
c 2005 Kluwer Academic Publishers. Printed in the Netherlands.
°

main.tex; 12/07/2005; 23:57; p.1

2
control operators shift and reset to abstract delimited continuationsin this hierarchy. In the literature, many different control operators fordelimited continuations have been proposed [12, 19, 20, 21]. In contrast
to these control operators, shift and reset are defined by the CPS
translation in a purely functional way. In addition, they have foundapplications in partial evaluation [24], one-pass CPS translation [10],and normalization by evaluation [7], as well as to represent layered
monads [15] and mobile computation [30].
In this article, we study a theoretical foundation of the control
operators in the CPS hierarchy. Specifically, we address the problemof finding direct-style axioms for them. While these operators are usedin many applications and their semantics is given by a CPS translation(be it iterated or extended), we often want to reason about source
programs directly, rather than about the image of a translation, since a
CPS translation is a global program transformation which significantly
changes the overall structure of source programs. Also finding a goodset of direct-style axioms could lead one to a better understanding ofthese operators.
We give a simple set of axioms consisting of only three equations
for shift and two equations for reset, and then prove that this set of
equations is sound and complete with respect to the CPS translation.
This work builds on our previous work, in which we gave a soundand complete axiomatization for level-1 shift and reset [23], and forlevel-2 shift and reset [22]. Since completeness proofs of this kind often
require quite a lot of calculations, we make the proof more structured
by reconstructing Sabry’s proof method [28] in a type-theoretic setting.
Overview: The rest of this article is organized as follows. In Section 2, we informally introduce shift and reset and we explain theiroperational aspects. In Section 3 we formally introduce the calculi withthese control operators, and in Section 4, we give a CPS translation
for them as well as a type structure for the target calculus of the CPS
translation. In Section 5 we present the axioms for control operatorsand develop useful equations from them. In Section 6, we give a directstyle translation as an inverse of the CPS translation, and by using it
we prove soundness and completeness. In Section 7, we conclude andmention future work.
Prerequisites: We assume that readers have some familiarity with
CPS translations.

main.tex; 12/07/2005; 23:57; p.2

3
2. Control Operators in the CPS hierarchy

2.1. A Simple Example
The following example uses shift and reset in a simple way:
1 + h2 ∗ Sk. (3 + (k (k 4)))i = let k be λx.h2 ∗ xi
in 1 + h3 + (k (k 4))i
= 1 + h3 + h2 ∗ h2 ∗ 4iii
= 20
where h i is the reset operator and S is the shift operator, which binds
the variable k in the scope 3 + (k (k 4)). Unlike the continuation
captured by callcc, the continuation captured by shift is not the whole
rest of the computation (such as 1 + h2 ∗ [ ]i), but the part which isdelimited by reset, that is, h2 ∗ [ ]i. Also it is not abortive, and thus
we can compose the captured continuation with ordinary functions.
When several occurrences of reset enclose an occurrence of shift, the(dynamically determined) nearest one is chosen as the delimiter.
As more substantial examples, we borrow the ones by Danvy andFilinski [9].

2.2. Nondeterminism
A non-deterministic choice can be represented by backtracking in direct
style using shift and reset as follows:defflip(x) = Sc. begin c(true); c(false); fail( ) end
def

fail(x) = Sc. "no"defchoice(n) = if n < 1 then fail( )else if flip( ) then choice(n − 1)else nwhere is an anonymous variable, true and false are truth values,
and begin· · · end is for sequencing.

main.tex; 12/07/2005; 23:57; p.3

4
To understand the program, we CPS translate1 these three functionsas:def

flip-c(x, k) = begin k(true); k(false); fail-c( , k) end
def

fail-c(x, k) = "no"defchoice-c(n, k) = if n < 1 then fail-c( , k)else flip-c( , λy. if y then choice-c(n − 1, k)else k(n))
Suppose display is a function for displaying values to the screen, andconsider the program hdisplay(choice(3))i. Its CPS translation (asa program) is choice-c(3, display), which displays 1, 2 and 3. Thus,
shift captures the current continuation, which is composable with an
ordinary function. The control operator reset delimits the extent of thecaptured evaluation context. Its role can be made clearer by comparing
the following two programs:
def

p1 = begin hdisplay(choice(3))i; display(10) end
def

p2 = hbegin display(choice(3)); display(10) endi
The program p1 is CPS translated to
begin choice-c(3, display); display(10) end
which, when executed, displays 1, 2, 3 and then 10. On the other hand,the program p2 is CPS translated to
choice-c(3, λx.(begin display(x); display(10) end))
which, when executed, displays 1, 10, 2, 10, 3, and 10.
2.3. Collecting Successive Results
Consider now the function emit defined as follows, which is meant tocollect a series of answers:
defemit(n) = Sc. cons(n, c(nil))where cons and nil are for lists. For instance,
hbegin emit(1); emit(2); emit(3); nil endi
returns a list (1 2 3).
1

The definition of the CPS translation appears in a later section.

main.tex; 12/07/2005; 23:57; p.4

5
It is then natural to expect that the combined program hemit(choice(3))i
generates the list (1 2 3) of all non-deterministic choices. However itdoes not, since the control operators in the two programs interfere. To
see this, let us CPS translate emit as:
def

emit-c(n, k) = cons(n, k(nil))
The term hemit(choice(3))i is CPS translated into
choice-c(3, λx.emit-c(x, λx.x)),
which generates three lists (1), (2) and (3), but never collects theseanswers.
A correct way of combining these programs is to make them layered.
The continuation captured in emit should be in a higher level thanthat captured in choice. To achieve this, the CPS counterpart of emit
should be:defemit-c2(n, k, γ) = cons(n, k(nil)γ)
where γ is a level-2 continuation, or a metacontinuation. Its direct-stylecounterpart is:defemit-c1(n, k) = k(Sc. cons(n, c(nil)))which passes a continuation, even though it is not in CPS since theargument of k is not a trivial term.2 Its direct-style counterpart is:defemit(n) = S2 c. cons(n, c(nil))This is the point where we need a level-2 control operator S2 in the
CPS hierarchy.
Finally, by replacing control operators without indices by those withlevel-1 (for instance S is replaced by S1 ), and enclosing the whole termby a level-2 reset, we get a program:hbegin hemit(choice(3))i1 ; nil endi2
which evaluates to (1 2 3) as expected.
In summary, a direct-style program with level-2 control operators
is CPS translated to a 1-CPS program with level-1 control operators,
which is then CPS translated to a 2-CPS program with no control
operators. CPS translating this program yields a real CPS program2

A trivial term is a synonym for a value.

main.tex; 12/07/2005; 23:57; p.5

6
where all calls are tail calls and all subterms are trivial. The family oflayered control operators thus corresponds to the CPS hierarchy.
3. The Calculi with Control Operators
In this section, we introduce the languages of our source calculi andtheir operational semantics.
3.1. Language of the Calculi
The calculus we choose here is a type-free call-by-value lambda calculus
with control operators for delimited continuations. Later we will briefly
discuss typed calculi.
We define two calculi λSn and λC n for a natural number n. The
former is a calculus with shift and reset, and the latter is a calculus
with C and reset. The control operator C will be explained later.
We assume that there are infinitely many variables (written x, y, z, k
and so on). Terms of λSn are defined by the following grammar (1 ≤i ≤ n):
M, N ::= x | λx.M | M N | hM ii | Si k.M
The index i denotes the level of control operators, which is conceptually the number of the iterations of CPS translations that arenecessary to interpret the control operator. hM ii is a term with a leveli reset operator, and Si k.M is a term with a level-i shift operator. The
defvariable k is bound in Si k.M . We define hM i0 = M .
Terms of λC n are defined in the same way as λSn where Si k.M isreplaced by Ci k.M . The variable k is bound in Ci k.M .
A value (written V ) is either a variable or λ-abstraction. Variables
are bound by λ and Si in λSn and λ and Ci in λC n . Free and boundvariables of terms are defined as usual. FV(M ) denotes the set of freevariables in M . We identify two terms which differ only in renamingof bound variables. M {x := N } is the result of the capture-avoiding
substitution of N for x in M .
Contexts (C), evaluation contexts (E) and level-j evaluation contexts (E j for 0 ≤ j ≤ n) in λSn are defined as follows:
C ::= [ ] | CM | M C | λx.C | Si k.C | hCii
E ::= [ ] | EM | V E | hEii
E j ::= [ ] | E j M | V E j | hE j il for 1 ≤ l ≤ jContexts and evaluation contexts are the standard ones in call by value
with the addition of shift and reset. E j is a level-j evaluation context in

main.tex; 12/07/2005; 23:57; p.6

7
which the levels of reset operators enclosing the hole must be equal to orless than j. For example, hx[ ]i2 and hx[ ]i2 hyzi3 are level-2 evaluation
contexts. As a special case, E 0 is an evaluation context in which noreset may enclose the hole. In our previous work [23], E 0 was calleda pure evaluation context. Contexts, evaluation contexts and level-j
evaluation contexts in λC n are defined similarly.
As we will see in the next section, being aware of the levels of
evaluation contexts is important in defining reduction rules for control
operators, since level-j shift captures the delimited continuation up tolevel-j.
3.2. Operational Semantics
We introduce the operational semantics of λSn in this section. The
formal definitions of shift and reset will be given in terms of the CPS
translation, and the operational semantics in this section should beconsidered as an informal explanation of these control operators. Nevertheless, we present it here to provide intuition about their operational
behavior.
The small-step operational semantics is given a set of reduction rules
for programs, where programs are terms that have no free variables3 .
We have the following three reduction rules (where x 6∈ FV(E j−1 ) and1 ≤ j ≤ n):E[(λx.M )V ] → E[M {x := V }]E[hV ij ] → E[V ]E[hE j−1 [Sj k.M ]ij ] → E[hM {k := λx.hE j−1 [x]ij }ij ]The first rule is the standard call-by-value β-reduction. The second rulesays that delimiting a value does nothing. The third rule shows how
shift and reset work. Shift captures the continuation delimited by thereset which has the same level as shift. If there are multiple occurrencesof reset which enclose the term Sj k.M , the (dynamically determined)
nearest reset is chosen, as the evaluation context E j−1 contains nooccurrences of level-j reset which enclose the hole.
In order to understand the third reduction rule, let us compare itwith the rule for callcc, the control operator for unlimited continuationsin Scheme and Standard ML of New Jersey:
E 0 [callcc(λk.M )] → E 0 [M {k := λx.abort(E 0 [x])}]where abort has the reduction rule: E 0 [abort(V )] → V . In the case ofshift, the continuation delimited by the corresponding reset operator
3

We will refine the definition of programs later in this section.

main.tex; 12/07/2005; 23:57; p.7

8(the evaluation context hE j−1 ij ) is captured and k is bound to a function λx.hE j−1 [x]ij . In the case of callcc, the whole evaluation context
E 0 is captured and k is bound to a function λx.abort(E 0 [x]). Thus,
continuations captured by shift are called delimited continuations. Another difference between these operators is that the former contains
an additional reset, while the latter contains an additional abort. As aconsequence continuations captured by shift are composable with otherfunctions.
To illustrate how the three reduction rules are used, we evaluate thechoice-emit example. The program we want to evaluate is hE[M ]i2
where E is a level-1 evaluation context (begin h[ ]i1 ; nil end) and M
is emit(choice(1)). →∗ denotes the reflexive, transitive closure of →.
hE[M ]i2hE[emit(if (S1 c.begin c(true); c(false); fail( ) end)
then choice(0) else 1)]i2∗→ hE[begin (λx.hemit(if x then choice(0) else 1)i1 )(true);(λx.hemit(if x then choice(0) else 1)i1 )(false);
fail( )
end]i2∗→ hE[begin hS2 c.cons(1, c(nil))i1 ; fail( ) end]i2→∗

Now the continuation captured by S2 is hE[begin h[ ]i1 ; fail( ) end]i2 .
If we had used S1 instead of S2 in the definition of emit, the captured
continuation would have been h[ ]i1 , in which case the function emit
could not collect all the answers of non-deterministic choices.
The whole evaluation proceeds as follows:→∗ hcons(1, c(nil)){c := λx.hE[begin hxi1 ; fail( ) end]i2 }i2→∗ hcons(1, hE[begin hnili1 ; fail( ) end]i2 )i2→∗ cons(1, nil)
Similarly we have:hbegin hemit(choice(3))i1 ; nil endi2 →∗ cons(1, cons(2, cons(3, nil)))which is the desired result.
The reduction rule for shift (the third reduction rule) is applicable
only when the level of shift and that of reset agree, and we must
generalize it to the case when they are different. Shift and reset arelayered control operators in that the evaluation context captured by alevel-j shift is delimited not only by a level-j reset but by any higherlevel reset. Therefore a general reduction rule is (where j ≤ i andmain.tex; 12/07/2005; 23:57; p.8

9f 6∈ FV(E j−1 )):E[hE j−1 [Sj k.M ]ii ] → E[hM {k := λx.hE j−1 [x]ij }ii ]Put differently, a level-i reset delimits not only a level-i evaluation
context, but also any level-j evaluation contexts if j ≤ i.
3.3. Comparison of Control Operators for Delimited
Continuations
We briefly compare several control operators for delimited continuations proposed in the literature.
The first group of control operators consists of shift/reset and theirrelatives, C/reset and D/reset, whose key reduction rules are defined
as follows (for j ≤ i):
E[hE j−1 [Cj k.M ]ii ] → E[hM {k := λx.Aj hE j−1 [x]ij }ii ]E[hE j−1 [Dj k.M ]ii ] → E[hE j−1 [M {k := λx.Aj hE j−1 [x]ij }]ii ]The control operator C was investigated by Murthy [26], and we use
it in the completeness proof in a later section. The control operator D
generalizes callcc, for D1 coincides with callcc in the absence of reset[23]. Filinski studied the relationship among these control operators[14].
Despite the difference of reduction rules, these control operators havethe same expressive power, for they are inter-definable (in the presenceof A). More precisely we have:(Si , reset) ↔ (Ci , reset) ↔ (Di , Ai , reset)
where ↔ means inter-definability. For instance, Si and Ci are definedby each other as:
Si k.M = Ci k 0 .M {k := λx.hk 0 xii }Ci k.M = Si k 0 .M {k := λx.Si .k 0 x}
where is an anonymous variable. These equations can be formallyjustified by the CPS translation in the next section.
In the literature shift and reset are sometimes called control operators for “composable continuations”, as the continuations they capture
are composable, while those captured by callcc (and by Ci and Di ) areabortive. We think that “delimited continuations” is a better name,since as long as we are concerned only with expressivity, it does not matter whether the captured continuations are composable or not, while
it does matter whether the calculus in consideration has a delimiter(reset) or not.

main.tex; 12/07/2005; 23:57; p.9

10
The second group consists of Felleisen’s prompt (denoted by #) andF, the first control operator for delimited continuations [12], and theirrelatives (e.g. Gunter, Rémy and Riecke’s operator “cupto” [19]). The
reduction rule of Felleisen’s operators is defined by:
E[#(E 0 [Fk.M ])] → E[#(M {k := λx.E 0 [x]})]The reduction rule looks similar to that for shift/reset if we put i =j = 1, and identify # with reset and F with shift of level-1. A notabledifference is that the evaluation context captured by F does not contain the enclosing prompt (as indicated by λx.E 0 [x] in the righthandside), and the captured continuation is therefore merged with an outer
continuation, which leads to the dynamic behavior of these control
operators.
Control operators in the first group are static and have simple CPS
translations expressed as pure lambda terms, while those in the second group are dynamic and are not known to have such simple CPS
translations. In this article, we use the CPS translations as an essential
tool and develop a rigid theory by making use of it, hence we confine
ourselves to the static control operators. We will come back to thisissue in Section 7.

4. CPS Translation

In this section we follow Danvy and Filinski [9] and give CPS translations for higher level shift and reset. For simplicity, the version we
present here does not use environments nor it does perform optimization for administrative redexes.

4.1. The First CPS Translation
The first CPS translation is the standard Plotkin-style call-by-value
CPS translation extended to the calculi λS1 and λC 1 . It consists of
two translations [ ] 1 for terms and ∗1 for values in λS1 (or λC 1 ). The
results of these translations are type-free lambda terms without control

main.tex; 12/07/2005; 23:57; p.10

11
operators:
def[ V ] 1 = λk. k(V ∗1 )def

[ M N ] 1 = λk. [ M ] 1 (λm. [ N ] 1 (λn. mnk))def[ S1 c.M ] 1 = λk. [ M ] 1 {c := λxk 0 . k 0 (kx)}(λx.x)
def[ C1 c.M ] 1 = λk. [ M ] 1 {c := λxk 0 . kx}(λx.x)
def[ hM i1 ] 1 = λk. k([[M ] 1 (λx.x))
defx∗1 = xdef

(λx.M )∗1 = λx. [ M ] 1
For shift (the third line), the current continuation k is captured andthe variable c is bound to a function which composes k and k 0 . For
C (the fourth line), the function bound to c discards k 0 , and it isabortive. For reset (the fifth line), the current continuation is reset tothe identity function λx.x (which corresponds to the empty evaluation
context [ ]). The resulting terms are not in the usual CPS form in thatsome subterms are not trivial (kx and [ M ] 1 (λx.x) are in the argument
positions of functional application). Shift and reset represent a new programming pattern where one can compose continuations with functions
and reset continuations, which Danvy and Filinski called Continuation
Composing Style (CCS for short).
We introduce the following type structure for the target terms of
the first CPS translation:
def

Exp0 = Cont1 → Ans
def

Cont1 = Value → Ans
def

Value = Value → Exp0
where Ans is the type of answers. The type Value is defined by arecursive type, reflecting that the source calculi are type-free.
The type structure above works for the source calculi without control
operators. In the presence of control operators in the source calculi, we
need one more constraint Ans = Value which is necessary to type
terms in CCS, for instance, k 0 (kx). The target terms of the first CPS
translation are typable under this constraint, namely, for a term M
and a value V in λS1 (or λC 1 ), [ M ] 1 and V ∗1 have the types Exp0 and
Value, resp.

main.tex; 12/07/2005; 23:57; p.11

12
4.2. The Second CPS Translation
The results of the first CPS translation are not in the ordinary CPS
form, but if we CPS translate them once more, the resulting terms are
ordinary CPS terms, and the call-by-value and call-by-name semantics
coincide (Plotkin’s indifference theorem [27]). Rather than sending asource term M to [ [ M ] 1 ] 1 , Danvy and Filinski defined their second CPS
translation as translating terms of the answer type only. A rationale
for this choice is that, after the first CPS translation, a term of typeAns is not necessarily a trivial term, while a target term of other types
is a trivial term.
We first introduce the type structure for the target terms of thesecond CPS translation:
def

Exp0

=

def

Cont1

=

def

Value

=

Cont1 → Exp1
Value → Exp1

Exp1
Cont2

def

=

Cont2 → Ans

def=

Value → Ans

Value → Exp

where Ans is an arbitrary type.
The second CPS translation [ ] σ2 is parametrized over types σ. It
sends a term of type Ans to a term of type Exp1 (= (Value → Ans) →Ans), and it is homomorphic on a term of other types. We remarkthat after the first CPS translation, a term of type Ans (= Value) iseither one of the forms: M K (for M : Exp0 and K : Cont1 ), KW (forK : Cont1 and W : Value), x (for x : Value), or λx.M (for x : Valueand M : Exp0 ).
def

Ans
Cont1
[ KW ] Ansvγ)
2 = λγ.[[W ] 2 (λv.[[K]]2
def

Exp0

[ M K]]Ans
2 = λγ.[[M ] 2

1[ K]]Contγ
2def= λk.[[A]]Ans
2

Exp0 def[ W1 W2 ] 2

Ans= [ W1 ] Ans
2 [ W2 ] 2

def[ x]]Ans
2 = λγ.γx
defExp0 def[ λk.A]]2

1[ k]]Cont
=k
2

Exp0

[ λx.M ] Ans
2 = λγ.γ(λx.[[M ] 2

)

def

1
[ λx.A]]Cont= λx.[[A]]Ans
2
2

In the first two definitions in the left column, we gave an optimized
version by making use of the fact that terms of type Exp or Cont1 aretrivial terms.
By composing two CPS translations, we obtain a single CPS translation, called 2-CPS translation. After performing the administrativeβη-reductions, the 2-CPS translation can be represented as follows

main.tex; 12/07/2005; 23:57; p.12

13
where two continuation variables k and γ are introduced:
def[ V ] = λkγ. kV ∗ γdef[ M N ] = λkγ. [ M ] (λmγ 0 . [ N ] (λnγ 00 . mnkγ 00 )γ 0 )γdef

[ S1 c.M ] = λkγ. [ M ] {c := λxk 0 γ 0 . kx(λy.k 0 yγ 0 )}(λaγ 00 .γ 00 a)γdef[ C1 c.M ] = λkγ. [ M ] {c := λxk 0 . kx}(λaγ 00 .γ 00 a)γdef[ hM i1 ] = λkγ. [ M ] (λaγ 0 .γ 0 a)(λx.kxγ)
defx∗ = xdef(λx.M )∗ = λx. [ M ]It is easy to check that the results are typable under the type structure
above, namely, for a source term M and a value V , [ M ] and V ∗ are oftypes Exp0 and Value, resp.
4.3. CPS Hierarchy
The 2-CPS translation sends every term with shift and reset to the
CPS form. That all the translated terms are in CPS means that there
is more room yet for continuation composing style in the target language, namely, resetting and composing continuations, which should
correspond to another set of control operators in the source language.
By this observation, Danvy and Filinski proposed to iterate CPS translations, and obtained a hierarchy of higher level shift and reset control
operators. What is interesting here is that we only have to iterate thestandard CPS translations to obtain a series of control operators, andnothing else is needed.
Let us summarize the relation between the levels of source terms(that is, the maximum levels of control operators in source terms) andthe number of iterations of CPS translations. Let M be a term withlevel ≤ n control operators. If we n-times CPS translate M , we get aterm without control operators, but the result is not necessarily in theordinary CPS form (a term in CCS). If we n + 1-times CPS translate
M , we get a term without control operators which is an ordinary CPS
term. To type CCS terms, we need an additional constraint Ans =Value, while to type CPS terms, we do not need this constraint andthe answer type can be an arbitrary type. In the following, we only
consider (n + 1)-times (or more) iteration of CPS translations for leveln control operators so that all the target terms are in the ordinary CPS
forms.

main.tex; 12/07/2005; 23:57; p.13

14
We abbreviate sequences as follows (for 1 ≤ i ≤ n + 1):
def

λk1,i .M = λk1 .λk2 . · · · λki .Mdef

M k1,i = M k1 k2 · · · kidefM θ1,i = M θ1 θ2 · · · θidef

Ck1,i .M = C1 k1 .C2 k2 . · · · Ci ki .M
We define a CPS translation from the source calculi λSn and λC n(n ≥ 0) to pure lambda calculus. The translation is a compositionof n + 1 CPS translations, which takes n + 1 continuation variables
k1 , · · · , kn+1 each introduced by the i-th CPS translation. Given a term
M and a value V in the source calculi, the translations [ ] and ∗ senda term and a value, resp, to terms of pure lambda calculus, To avoid
clutter, we present an η-reduced version here.
def[ V ] = λk1 . k1 V ∗def[ M N ] = λk1 . [ M ] (λm.[[N ] (λn.mnk1 ))def[ hM ii ] = λk1,i+1 . [ M ] θ1,i (λy. θ0 yk1,i+1 )def

00. θ0 yk1,i (λz.θ0 zk1,i+1)}θ1,i[ Si c.M ] = λk1,i . [ M ] {c := λyk1,i+1
def

0 . θ yk }θ
[ Ci c.M ] = λk1,i . [ M ] {c := λyk1,i
0 1,i 1,idefx∗ = xdef(λx.M )∗ = λx.[[M ]0where 1 ≤ i ≤ n, the variables k1 , · · · , ki+1 , k10 , · · · , ki+1
are fresh, anddefθj = λxkj+1 . kj+1 x (for 0 ≤ j ≤ n), The term θj is the image ofthe empty evaluation context [ ]. Although all θj are equal as type-freeterms, we attach indices to distinguish its level.
Let us explain the extended CPS translation. Terms and values without control operators are translated as usual. For the term hM ii , thereset operator installs identity continuations up to level i, and composescontinuations of up to level i with the level i + 1 continuation. The
operator Ci captures the current continuation up to level i and composes
0 . θ yk ), and the variable c is bound to it. At
them (as the term λyk1,i0 1,ithe same time, it installs i identity continuations. The CPS translationof shift (Si ) is slightly more complex than Ci , since it captures a non0
abortive delimited continuation so that we should compose k10 , · · · , ki+1
with the captured continuation. Note that the result of the extended
CPS translation does not depend on n if it is defined.

main.tex; 12/07/2005; 23:57; p.14

15
Since the target terms of the extended CPS translation are in CPS,
they are evaluation-order independent, and we choose βη-equality as
its semantics. We can prove that the operational semantics in Section
3.2 is sound with respect to the CPS translation, namely, M →∗ N
implies [ M ] = [ N ] .
As an example, let us CPS translate the function emit. To do this,
we assume that our source language contains nil and cons as values,
and we do not CPS translate primitive functions, that is, they are CPS
translated4 by:defnil∗ = nil
defcons∗ = λxk. k(λyk 0 .k 0 (cons(x, y)))Then by the extended CPS translation, emit is CPS translated asfollows5 :emit∗ ≡ (λn.S2 c.cons(n, c(nil)))∗→∗ λnkγ. ((λk.c(nil)(λx.k(cons(n, x))))θ1 θ2 ){c := λxk 0 γ 0 δ 0 .kxγ(λy.k 0 yγ 0 δ 0 )}→∗ λnkγδ. k(nil)γ(λy.δ(cons(n, y)))The term emit∗ differs from emit-c2, since the former is the result of
3-CPS translation, while the latter is the result of 2-CPS translation.
If we translate emit-c2 (on the answer type only), we get emit∗ .
To see how the layered control operators work, let p3 be a term
hbegin hemit(1)i1 ; hemit(2)i1 endi2 , and CPS translate it as follows:[ p3 ] →∗ λkγδ. [ emit(1)]]θ1 (λ .[[emit(2)]]θ1 θ2 )(λx.kxγδ)→∗ λk. k(cons(1, cons(2, nil)))
The calculation above does not work if all the occurrences of reset in
p3 have the same level.
For the CPS translation of a complete program (rather than a term),
we need to supply an identity continuation λa.a to its CPS translation
as a term. Since we iterate CPS translations (n+1) times, we need tosupply (n+1) identity continuations, and all but the last of these identity continuations are translated to θj by the successive CPS translations. For instance, the program p3 is CPS translated to [ p3 ] θ1 θ2 (λa.a).
which βη-reduces to cons(1, cons(2, nil)) as expected.
Remark on Complete Programs: In their original article [9], Danvy
and Filinski had an implicit assumption that every complete program4
5

We assume that cons is curryed.
We use k, γ, and δ for the continuation variables k1 , k2 , and k3 for readability.

main.tex; 12/07/2005; 23:57; p.15

16
is implicitly enclosed by a reset of sufficiently high level. For instance,a program S2 c.c0 does not cause an error. Rather, it is executed as if itwere hS2 c.c0i2 . This implicit assumption corresponds to the fact that
we supply a sufficient number of identity continuations to a complete
program.
In this article we will consider only terms (and values), but notconsider complete programs, since every equation over programs can be
deduced from equations over terms; in the calculus λSn , two complete
programs p and q are equal if and only if hpin and hqin are equal as
terms.
4.4. The Target Calculus
We define and analyze the target calculus λTn of the extended CPS
translation in detail.
The set of terms in λTn is the least set which contains all subtermsof the targets of the extended CPS translation, and is closed under theβη-reductions. The grammar of the terms in λTn is defined by:
P, Q ::= x | ki | λx.P | λki .P | P Q for 1 ≤ i ≤ n + 1
where x is an ordinary variable (in the source calculi) and ki is a continuation variable introduced by the CPS translation. We assume thatthe set of the ordinary variables and that of the continuation variables
do not overlap.
A type structure can be introduced to the target terms [9, 11] asfollows:
def

Expi =½

Conti+1 → Expi+1
Ans

for 0 ≤ i ≤ n
for i = n + 1

def

Conti = Value → Expi for 1 ≤ i ≤ n + 1
def

Value = Value → Exp0
Again we need a recursive type for Value, but Ans can be an arbitrary
type, and in fact we can make the answer type parametric as in thework by Thielecke [32]. Since we will use this type structure to definea direct-style translation in Section 6.2, we present the typing rules indetail.
A typing judgment is of the form Γ ` P : σ where P is a term, σ is a
type, and Γ is a set of variable-type pairs consisting of either x : Valueor ki : Conti . As usual, a variable may occur at most once in Γ. We
have the following eight type inference rules (1 ≤ i ≤ n + 1):
Γ ` W : Value Γ ` W 0 : ValueΓ ` W W 0 : Exp0Γ, ki : Conti ` Ti : ExpiΓ ` λki .Ti : Expi−1

main.tex; 12/07/2005; 23:57; p.16

17
Γ ` Ti−1 : Expi−1 Γ ` Ki : ContiΓ ` Ti−1 Ki : ExpiΓ ` Ki : Conti Γ ` W : ValueΓ ` Ki W : ExpiΓ, ki : Conti ` ki : ContiΓ, x : Value ` Ti : ExpiΓ ` λx.Ti : ContiΓ, x : Value ` x : ValueΓ, x : Value ` T0 : Exp0Γ ` λx.T0 : Value

where Γ, x : σ means the set union Γ ∪ {x : σ}.
If we can prove Γ ` P : σ using the typing rules above, we say that
P is a term of type σ in λTn . For instance, the term λk1 . k1 x (≡ [ x]])can be typed as follows:x : Value, k1 : Cont1 ` k1 : Cont1 x : Value, k1 : Cont1 ` x : Valuex : Value, k1 : Cont1 ` k1 x : Exp1
x : Value ` λk1 . k1 x : Exp0
A variable of type Conti is called a level-i continuation variable.
In addition to the type structure above, λTn enjoys the following
important property:(Property-#) A target term of type Expn+1 or Contn+1 has exactly
one free occurrence of level-(n + 1) continuation variables, and atarget term of other types does not have any free occurrences oflevel-(n + 1) continuation variables.
For example, the target term [ hM in ] is of type Exp0 and has no freeoccurrences of level-(n + 1) continuation variables, and it subterm[ M ] θ1,n (λx. θ0 xk1,n+1 ) is of type Expn+1 and has one occurrence ofthe level-(n + 1) continuation variable kn+1 .
Property-# can be explained in this way: recall that we use (n + 1)CPS translation for λSn and λC n . The first n CPS translations map
source terms to pure lambda terms, and the last, (n + 1)-st CPS translation maps them to terms in CPS, which is therefore the standard
CPS translation. It is well known that the standard CPS translation forpure lambda terms needs only one continuation variable, which leads toProperty-#. By this property it is possible to refine our type structure
as Expn = Contn+1 ( Expn+1 where ( is the linear implication [23].
Property-# does not hold for continuation variables of level≤ n, as
can be seen by the CPS translation of [ Si c.M ] and [ Ci c.M ] , whereterms which freely contains continuation variables k1,i are substituted
for c.
For the type structure with Property-#, we have the following theorem.

main.tex; 12/07/2005; 23:57; p.17

18
THEOREM 1. Let Γ ` P : σ mean that we can derive Γ ` P : σ using
the type structure above, and also Property-# holds for any subterm of
the term P . Then we have the following three properties.
(1) Let M be a term and V be a value in λSn or λC n , and their freevariables be x1 , · · · , xn . Then we havex1 : Value, · · · , xn : Value ` [ M ] : Exp0 , andx1 : Value, · · · , xn : Value ` V ∗ : Value.
(2) (Substitution Property) If Γ ` W : Value and Γ, x : Value ` P :σ, we have Γ ` P {x := W } : σ. Similarly, if Γ ` Ki : Conti andΓ, ki : Conti ` P : σ for 1 ≤ i ≤ n + 1, we have Γ ` P {ki := Ki } : σ.
(3) (Subject Reduction) If we have Γ ` P : σ, and P reduces to Q
by βη-reductions, then we have Γ ` Q : σ.
All properties can be proved straightforwardly, and their proofs areomitted.
We introduce βη-equality in the target calculus, and write λTn ` P =Q if P and Q are equal under βη-equality. Given the CPS translation and the target calculus λTn equipped with βη-equality, the source
calculus is given an induced semantics called CPS-semantics. The fundamental question addressed in this article is, what is the equality
theory that coincides with this CPS semantics, or equivalently, how toaxiomatize the CPS semantics in direct style.
5. Axioms for Shift and Reset
In this section we give axioms of the theories λSn and λC n , which will
be proved sound and complete with respect to the extended CPS translation, namely, two terms are equal in λSn (or λC n ) if and only if they
are mapped to equal terms in λTn by the extended CPS translation.
We think that this kind of axiomatization (called Direct-Style Axiomatization) is important and worth studying for the following reasons.
− Reasoning about source terms (by humans) is usually much easierthan reasoning about CPS terms. It is true that we can reason
about a source program after CPS translating and βη-reducing
it. However, the CPS translation makes the resulting term longer
than the source term, and it often obscures the structure of thesource term since it is a global translation. If we have a directstyle axiomatization, we do not have to CPS translate every term
to reason about its properties, and thus we would get a simpler
proof of properties of source programs.

main.tex; 12/07/2005; 23:57; p.18

19
(λx.M )V = M {x := V }λx. V x = Vβv
ηv , if x 6∈ FV(V )(λx.E 0 [x])M = E 0 [M ]hV ii = Vh(λx.M )hN ii ij = (λx.hM ij )hN ii

βΩ , if x 6∈ FV(E 0 )reset-value
reset-lift

Figure 1. Common Axioms for λSn and λC n (1 ≤ j ≤ i ≤ n)

− More importantly, having a simple set of axioms helps us to understand the source calculus intuitively and formally, as has been
proved by several works in the literature, most notably, by Sabry
and Felleisen’s direct-style axiomatization of type-free lambda calculus with and without callcc [29]. Their equational axiomatizationof the calculus without callcc is equivalent to Moggi’s computational lambda calculus [25], and consequently they essentiallygave (another) evidence that computational lambda calculus is the
canonical choice for the call-by-value setting. Their axioms haveanother application in A-normal form translation [16].
We believe that studying direct-style axiomatization is the firstand solid step toward good understanding of control operators inthe source calculus.
5.1. Axioms
In this section we give the following three sets of axioms:− common axioms for λSn and λC n (Figure 1),− specific axioms for λSn (Figure 2), and− specific axioms for λC n (Figure 3).
The theory λSn consists of the axioms in Figures 1 and 2, and thetheory λC n consists of those in Figures 1 and 3.
In the presentation of these axioms, we assume that the levels of
all control operators are equal to or less than n, namely, the indices iand j range over the finite set {1, 2, · · · , n}. Recall that E i is a leveldef

def

i evaluation context, hM i0 = M , and Ai = λx.Ci .x where is ananonymous variable. Note also that i and j cannot be 0, but i − 1 andj − 1 may be 0.
We shall explain axioms in Figure 1. The first three axioms βv ,ηv and βΩ are those for Moggi’s computational lambda calculus[25],main.tex; 12/07/2005; 23:57; p.19

20
or equivalently, Sabry and Felleisen’s axiomatization of pure lambda
calculus in call-by-value [29].
The axiom reset-value corresponds to the reduction rule E[hV ii ] →E[V ].
The axiom reset-lift does not have a direct counterpart in the operational semantics. To explain its role, let us abbreviate (λx.M )N as
let x be N in M , and consider under which condition the following
equation (called β-lift) holds:
let x be N in E[M ] = E[let x be N in M ] for x 6∈ FV(E).
This equation is useful to guarantee the correctness of certain kindsof program transformations, for instance, closure conversion. Anotherexample is the let-insertion technique used in partial evaluation, one of
the successful applications of shift and reset.
In the absence of reset (more precisely, in the case when E is a level-0
evaluation context E 0 ), the equation holds, as can be proved by:let x be N in E 0 [M ] = let x be N in E 0 [let x be x in M ] by βv= E 0 [let x be N in M ] by βΩIn the presence of reset, however, the equation does not hold in general,
as can be seen by CPS translating both sides of the equation. Moreintuitively, h(let x be S1 c.c(c1) in hxi1 ) + 5i1 evaluates to 11, while
hhlet x be S1 c.c(c1) in xi1 + 5i1 evaluates to 6, so the two terms
let x be S1 c.c(c1) in hxi1 and hlet x be S1 c.c(c1) in xi1 cannot be
equal even under contextual equivalence.
The axiom reset-lift partially recovers the equation β-lift under acertain condition. Namely, we can prove the following equation by resetlift when i ≥ j:
let x be hN ii in E j [M ] = E j [let x be hN ii in M ] for x 6∈ FV(E j ).
In other words, we can lift a local binding (a β-redex) through anevaluation context if the bound term (the above N ) is enclosed by areset of “sufficiently” high level.
Besides the common axioms, there are three specific axioms for shift
and three for Ci shown in Figures 2 and 3, resp. The axiom S-reset isa natural extension of its level-1 counterpart S1 k.hM i1 = S1 k.M . The
axiom S-elim is not quite the same as a natural extension of its level-1
counterpart S1 k.kM = M (for k 6∈ FV(M )). In fact, Si k.kM = M is
not sound for i > 1. Danvy and Filinski stated in [9] that the current
formulation of shift/reset is not completely satisfactory since a natural
equality S2 k.kM = M does not hold. We have found that the correct
extension of the level-1 equation is the axiom S-elim. By putting i =main.tex; 12/07/2005; 23:57; p.20

21
Si k.hM ii = Si k.M
Si k.khM ii−1 = hM ii−1

S-resetS-elim, if k 6∈ FV(M )hE j−1 [Sj k.M ]ii = hM {k := λx. hE j−1 [x]ij }ii S-lift, if k 6∈ FV(E j−1 )and x 6∈ FV(kE j−1 )Figure 2. Specific Axioms for λSn (1 ≤ j ≤ i ≤ n)

Ci k.hM ii = Ci k.M
Ci k.khM ii−1 = hM ii−1

C-resetC-elim, if k 6∈ FV(M )hE j−1 [Cj k.M ]ii = hM {k := λx. Aj hE j−1 [x]ij }ii C-lift, if k 6∈ FV(E j−1 )and x 6∈ FV(kE j−1 )Figure 3. Specific Axioms for λC n (1 ≤ j ≤ i ≤ n)

1 in S-elim, we obtain the level-1 S-elim axiom. The last axiom Slift is a direct equational formalization of the corresponding reduction
rule given in Section 3.2. The specific axioms for Ci can be explained
similarly.
We think that these axioms are natural and simple.
They are natural since many axioms have been obtained by replacing
reduction by equality in the operational rules, and the rest can beunderstood by the operational semantics. Moreover if we put all i’s
and j’s to be 1 in λSn , we can obtain the axioms for level-1 shift andreset [23]6 .
They are simple since many existing works proposed a larger numberof more complex axioms for axiomatizing simpler control operators
than we use in our axiomatization. For instance, Sabry and Felleisen’s
axiomatization for callcc has 10 axioms [29], and our axiomatization
for level-2 delimited continuation operator has 14 axioms [22]. We
think that simplicity of our axioms partly comes from the conceptual
simplicity of the definition of shift and reset in terms of CPS translation.
Soundness of these axioms with respect to the extended CPS translation can be proved by calculating both sides of the equations. Completeness of λC n may be surprising, since one may think it lacks many
important equations which were included in our axiomatization of the
6

Strictly speaking, there is a slight difference, for the shift operator wasformulated as a constant in [23], which can be defined as λx.S1 k.xk in λSn .

main.tex; 12/07/2005; 23:57; p.21

22
level-2 delimited continuation operator C2 [22], such as:
hhM ii il = hM imax(l,i)

reset-reseth(λx.M )hN ii−1 ii = h(λx.hM ij )hN ii−1 ii
hCi k.M ij = Ci k.M
hCj k.M ii = hM {k := Aj }ii(λx.C1 k.M )N = C1 k.(λx.M )N

reset-lift-2, j ≤ ireset-C, j < iC-top, j ≤ i
let-C1 , k 6= x

Another seemingly missing axiom is an equation for lifting Ci over an
evaluation context, that is, E[Ci k.M ] = M {k := N } for some appropriate N . In the next theorem we show that all these equations arederivable.
From now on, we will mainly investigate λC n . After proving its
soundness and completeness, we will come back to λSn . The use of λC n
in our proof is not essential, and we can directly prove the completenessfor shift as well. The use of λC n is motivated by the fact that Ci has aslightly simpler CPS translation, and its expressive power is the sameas that of Si .
5.2. Derivable Equations
THEOREM 2. The equations reset-C, C-top, reset-reset, reset-lift-2,
and let-C1 as well as the following equations are derivable in λC n where
k1 , · · · , ki , x are fresh variables, and k is not bound in the context C in
C-abort.
E j [Ai hM ii−1 ] = Ai hM ii−1
j

Ci k.C[E [kV ]] = Ci k.C[kV ]A-abort, j < iC-abort, j < ij

E [Ci k.M ] = Ck1,i . M {k := N } telescope, j < iwhere N is λx. ki hki−1 · · · hk1 (E j [x])i1 · · ·ii−1 .
Proof. (C-top) Putting E j−1 ≡ [ ] and i = j in C-lift and using
reset-value and ηv , we have C-top.
(reset-reset) By putting M ≡ x in reset-lift, we have hh(λx.x)N ii ij =(λx.hxij )hN ii . Using reset-value and βΩ (in the form of (λx.x)L = L
for any L), we obtain hhN ii ij = hN ii for j ≤ i, which constitutes a halfof reset-reset.
We will prove the remaining half of reset-reset, namely, hhN ij ii =hN ii for j ≤ i. By putting E j−1 ≡ (λx.N )[ ] and M ≡ kx in Clift, we have h(λx.N )(Cj k.kx)ii = h(λy.Aj h(λx.N )yij )xii . Using resetvalue, C-elim and βv , the lefthand side is equal to hN ii , and using βv ,main.tex; 12/07/2005; 23:57; p.22

23
the righthand side is equal to hAj hN ij ii . We can further rewrite therighthand side as:hAj hN ij ii = hCj k. khN ij ii by C-top= hCj k. khhN ij ij−1 ii by the half of reset-reset= hhhN ij ij−1 ii by C-elim= hhN ij ii by the half of reset-reset
where we used the already proved half of reset-reset. Hence we havehN ii = hhN ij ii for j ≤ i, proving the remaining half of the reset.
(reset-lift-2) We have the following derivation for 0 ≤ l ≤ i.
h(λx.hM il )hN ii−1 ii = h(λx.hM il )(Ci k.khN ii−1 )ii by C-elim= h(λy.Ai h(λx.hM il )yii )hN ii−1 ii by C-lift= h(λx.Ai hM ii )hN ii−1 ii by βv , reset-reset
The final result does not depend on l, and by putting l = 0 and l = j,
we can obtain reset-lift-2.
For the remaining equations in Theorem 2, we prepare two key
equations. First, we derive by C-elim and C-reset:
N = C1 k1 .hk1 N i1 = C1 k1 .C2 k2 .hk2 hk1 N i1 i2
Iterating this process i-times we obtain:
N = Ck1,i .hki hki−1 · · · hk1 N i1 · · ·ii−1 ii (key eq.-1)
For j < i, by putting N ≡ E j [Ci k.M ] in the key eq.-1 and using C-lift
and reset-reset, we obtain the following equation (k1 , · · · , ki , x are fresh
variables):E j [Ci k.M ] = Ck1,i .hM {k := λx.Ai hki h· · · hk1 (E j [x])i1 · · ·ii−1 ii }ii(key eq.-2, for j < i)(reset-C) By putting E j ≡ [ ] and E j ≡ h[ ]ij in the key eq.-2, we havethat the righthand sides of these two cases are equal by reset-value,
hence we obtain Ci k.M = hCi k.M ij .
(A-abort) We first note that, if j < i, we can derive E j [(λx.N )hM ii−1 ] =(λx.E j [N ])hM ii−1 by reset-lift and βΩ . Also, if k 6∈ FV(M ), then theright-hand side of the key eq.-2 does not contain E j , hence E j [Ci .M ] =Ci .M . Then we can compute as follows (for j < i):E j [Ai hM ii−1 ] ≡ E j [(λx.Ci .x)hM ii−1 ]= (λx.E j [Ci .x])hM ii−1
= (λx.Ci .x)hM ii−1
≡ Ai hM ii−1

by the above equationby the key eq.-2

main.tex; 12/07/2005; 23:57; p.23

24
(C-abort) We compute as follows (where j < i):Ci k.C[E j [kV ]]= Ck1,i .h(C[E j [kV ]]){k := λx.Ai hki h· · · hk1 xi1 · · ·ii−1 ii }ii
by the key eq.-2= Ck1,i .hC[E j [Ai hki h· · · hk1 V i1 · · ·ii−1 ii ]]ii by βv= Ck1,i .hC[Ai hki h· · · hk1 V i1 · · ·ii−1 ii ]ii by A-abort
Since the final result does not contain E j , we obtain C-abort.
(telescope) We first prove Ai hM ii−1 = Ai hM ii . In the following derivation, k1 , · · · , ki are fresh variables.
Ai hM ii−1 = Ck1,i .hki h· · · hk1 (Ai hM ii−1 )i1 · · ·ii−1 iiby the key eq.-1= Ck1,i .hAi hM ii−1 ii by A-abort= Ck1,i .hM ii
The last equation has been derived in the proof of reset-reset. Similarly
we have Ai hM ii = Ck1,i .M , and hence Ai hM ii = Ai hM ii−1 .
The righthand side of the key eq.-2 has a subterm Ai hki h· · ·ii−1 ii ,which is equal to Ai hki h· · ·ii−1 ii−1 by the equation above. Since Ai h[ ]ii−1
is a level-(i − 1) evaluation context, we can apply C-abort to eliminate
it from the righthand side of the key eq.-2 (note that ki is bound by
Ci ki in the the key eq.-2), and finally obtain the telescope axiom7 :E j [Ci k.M ] = Ck1,i . M {k := λx.ki hki−1 · · · hk1 (E j [x])i1 · · ·ii−1 }We also have Ai hM ii−1 = Ci .M from the above derivation and telescope.
(let-C1 ) This equation is not needed in this article, and its verificationis left for the reader.
This finishes the proof of Theorem 2.

6. Completeness Proof
The main results of this article are that the theories λSn and λC n aresound and complete with respect to the extended CPS translation into
λTn . In this section we give a proof for these results.
7This is a generalized version of Murthy’s telescope axiom [26].

main.tex; 12/07/2005; 23:57; p.24

25
6.1. Proof Methods for CompletenessWe first review the proof methods for this kind of completeness proposed in the literature, and then give an overview of our proof method.
A traditional way to prove completeness is to find an inverse † ofthe CPS translation that satisfies the following two properties:(1) For any source term M , we can prove [ M ] † = M in the source
calculus.
(2) For any target terms T and T 0 , if T = T 0 in the target calculus, we
can prove T † = T 0 † in the source calculus.
In fact, Sabry and Felleisen used this strategy to prove the completenessof their axioms for the calculus with callcc[29], and we used it for the
calculus with level-1 shift and reset [23].
Sabry proposed a new proof method to prove the completeness ofthe calculus with level-1 shift and lazy reset [28]. Let us illustrate his
method by an example.
In the standard CPS translation, a source term of the form M N is
CPS translated to:def[ M N ] = λk.[[M ] (λm.[[N ] (λn.mnk)))
Sabry’s key observation is that, as long as the equality of the target
calculus is concerned, we do not have to use the ordinary lambda terms
to represent the CPS translation. Instead, we can represent it as:[ M N ] 0 = get k.send(λm.send(λn.send(k, mn), [ N ] 0 ), [ M ] 0 )with two functions get and send that satisfy the following two equations corresponding to the β and η equations:send(K, get k.P ) = P {k := K}
get k.send(k, T ) = T if k 6∈ FV(T ).
Note that, if [ M ] = [ N ] under βη-equality, then we have [ M ] 0 = [ N ] 0
under βη-equality with the two βη-like equations for send/get (thisproperty will be referred as Property (i)).
The generalized CPS translation is an abstract CPS translation thatcan be interpreted in several ways:
def− An interpretation in the target calculus is defined by send(K, T ) =def

T K and get k.P = λk.P , then [ M ] 0 is identical to the standard
CPS translation [ M ] .

main.tex; 12/07/2005; 23:57; p.25

26
def

− We can interpret it in the source calculus by defining send(K, T ) =def

KT and get k.P = callcc(λk.P ). The notable feature of this implementation is that the generalized CPS translation is the identity
on source terms, namely, [ M ] 0 = M under the direct-style axioms(Property (ii)).

The completeness for the standard CPS translation follows from Properties (i) and (ii).
One may say that Sabry’s new method is merely a reformulation of
the traditional one, since the non-trivial implementation corresponds
to an inverse translation in the traditional method, and Properties (i)and (ii) correspond to Properties (2) and (1), resp. However, we thinkthat his method is valuable, since finding a suitable inverse translationfrom a huge search space is often very difficult, as was the case for our
axiomatization for level-1 shift and reset, and his method is a good
guide to this exploration.
Instead of directly following his method, we will use the type structure of the target calculus to reflect Sabry’s proof method. The useof types has two benefits: first, we can capture the essence of Sabry’s
use of abstract datatypes. Second, it makes explicit hidden details in
Sabry’s proof. As we saw, Sabry replaced some occurrences of λ and application by get and send, leaving others intact, but that this selective
replacement is harmless was not formally expressed nor proved in his
paper. Since our source calculus with layered control operators is much
more complex than his source calculus, we need a way to represent thisproperty explicitly. The subject reduction property of the type system
ensures the non-interference between them.
There is a subtle, but important reason for us not to follow Sabry’s
method directly (see below), hence we will use a traditional proof
method which defines an inverse translation (called a direct-style translation) and prove the two properties (1) and (2) (Theorems 5 and 3,
resp.). These two properties subsume the completeness of λSn .
6.2. Direct-Style Translation
We first define a direct-style (DS) translation † from the target calculus
λTn to the source calculus λC n . Later, we will prove that it is an inverseof the extended CPS translation.
The following eight clauses correspond to the type inference rules in
Section 4.4. Note that, in λTn , the index i can be up to n + 1, that is,main.tex; 12/07/2005; 23:57; p.26

27
1 ≤ i ≤ n + 1.
(
0 † def†(W W ) = W W

0†

def

(Ti−1 Ki )† = Ki † hTi−1 † ii−1
† def

½

ki =

def

x† = xki , if i ≤ nλx.x, o.w.

† def

(λki .Ti ) =Ci ki .Ti † , if i ≤ n
Ti † , o.w.

def

(Ki W )† = Ki † W †
(

† def

(λx.Ti ) =λx.hTi † ii , if i ≤ n
λx.Ti † , o.w.

def

(λx.T0 )† = λx.T0 †where x, ki are variables of type Value and Conti , resp, and W, W 0 , Ti , Ki
are terms of Value, Value, Expi , and Conti , resp.
Let us briefly explain how we obtained the DS translation above. As
in Sabry’s method, we generalize the following four terms in the target
calculus as:
λki .Ti is replaced by get1i ki . Ti
Ti−1 Ki is replaced by send1i (Ki , Ti−1 )λx.Ti is replaced by get2i x. Ti
Ki W is replaced by send2i (Ki , W )for 1 ≤ i ≤ n + 1. The pair of functions (send1i , get1i ) are interfacefunctions of the type Expi−1 = Conti → Expi , and (send2i , get2i ) arethose of the type Conti = Value → Expi . Each of these pairs mustsatisfy βη-like equations as before. We do not generalize other terms
such as terms of type Value = Value → Exp0 .
We then interpret these terms in the source calculus. Here we ignore the case i = n + 1 for simplicity. One can see that the following
definitions can be obtained (after a few trial and errors8 ):def

get1i ki . Ti = Ci ki .Ti
def

send1i (Ki , Ti−1 ) = Ki hTi−1 ii−1
def

get2i x. Ti = λx.hTi ii
def

send2i (Ki , W ) = Ki W
As one can see in the definition of get1i (and (λki .Ti )† ), an abstractionof a continuation variable is sent back to a control operator Ci . In otherwords, the level-i continuation is explicitly grabbed by Ci in the result
8

There are other candidates, but since each pair of send/get must satisfy βη-likeequalities locally, our search space is rather limited.

main.tex; 12/07/2005; 23:57; p.27

28
of the direct-style translation, which Sabry called continuation grabbingstyle.
The DS translation is a simple reformulation of this interpretation
except that we have to treat the case i = n+1 separately. It is necessary
to avoid having the level-(n + 1) control operators in the image of the
DS translation. Note that we have level-(n + 1) continuation variablesin the target calculus, while our source calculus have level ≤ n control
operators.
For this purpose, the DS translation simply forgets about the leveln + 1 continuation variables, in that the abstraction by kn+1 is omittedin (λki .Ti )† , and the variable kn+1 is mapped to the identity function
λx.x. The forgetful translation works well thanks to Property-# of thetarget calculus. Since the level-(n + 1) continuation variable is linear,and moreover every subterm of a target term has at most one freeoccurrence of such variables, we do not have to remember the variablethrough the inverse translation.
This trick appeared in our completeness proof for level-1 shift andreset [23], and in this article we generalize it to higher levels. A similar
technique appeared in Berdine, O’Hearn, Reddy, and Thielecke’s workwhere they investigated linearity in the target calculus and the inverse
translation based on it [4].
Since the trick does not fit in Sabry’s proof method, it seems difficult
to present our proof as an instance of Sabry’s method, and it is thereason why we chose the traditional proof method.
We also remark that, we can define an equivalent DS translation interms of shift and reset instead of Ci and reset. However, the results interms of shift are longer than those by Ci , and this is the (only) reason
why we chose to develop the theory for Ci rather than directly working
on the theory for shift.
In the next section, we prove that the DS translation enjoys Properties (1) and (2) mentioned at the beginning of Section 6.1.
6.3. Completeness Proof for λC n
We first prove Property (2), namely,
target calculus.

†

respects βη-equality in the

THEOREM 3. Let T0 and T00 be terms of type Exp0 in λTn . If λTn ` T0 =T00 , then λC n ` T0 † = T00 † .
This theorem is subsumed by the following general theorem byputting i = 0 in the clause (1).

main.tex; 12/07/2005; 23:57; p.28

29
THEOREM 4. Let 0 ≤ i ≤ n and 1 ≤ j ≤ n, Ti and Ti0 be terms oftype Expi , Kj and Kj0 be terms of type Contj , and W and W 0 be termsof type Value in λTn , and let M be a term in λC n . We have:(1) If λTn ` Ti = Ti0 , then λC n ` hTi † ii = hTi0 † ii .
(2) If λTn ` Kj = Kj0 , then λC n ` hKj † hM ij−1 ij = hKj0 † hM ij−1 ij .
(3) If λTn ` W = W 0 , then λC n ` W † = W 0 † .
00
Let Tn+1 and Tn+1
be terms of type Expn+1 , Kn+1 and Kn+1
be terms
of type Contn+1 in λTn , and let M be a term in λC n . We have:†00.
, then λC n ` Tn+1 † = Tn+1
(1’) If λTn ` Tn+1 = Tn+1††00
hM in .
(2’) If λTn ` Kn+1 = Kn+1 , then λC n ` Kn+1 hM in = Kn+1
In order to prove this theorem, we need three lemmas about substitution. The first one is for an ordinary variable (Lemma 1), and theother two are for a continuation variable. As in the definition of the
DS translation, we divide the substitution property for a continuation
variable kl into two cases, namely, 1 ≤ l ≤ n and l = n + 1, whichcorrespond to Lemmas 2 and 3, resp.
LEMMA 1. For 0 ≤ i ≤ n + 1 and 1 ≤ j ≤ n + 1, let X be a termof type Expi , Contj , or Value, and W be a term of type Value in λTn .
Then we have:
λC n ` (X{x := W })† = X † {x := W † }This lemma is proved by straightforward induction on X.
LEMMA 2. For 0 ≤ i ≤ n, 1 ≤ j ≤ n, and 1 ≤ l ≤ n, let Ti , Tn+1 ,Kj , Kn+1 , W and Kl0 be terms of type Expi , Expn+1 , Contj , Contn+1 ,Value and Contl , and kl be a continuation variable of type Contl , andM be a term in λC n . Then we have:†

λC n ` h(Ti {kl := Kl0 }) ii = hTi † {kl := L}ii†

λC n ` (Tn+1 {kl := Kl0 }) = Tn+1 † {kl := L}†

λC n ` h(Kj {kl := Kl0 }) hM ij−1 ij = h(Kj † {kl := L})hM ij−1 ij†

λC n ` (Kn+1 {kl := Kl0 }) hM in = (Kn+1 † {kl := L})hM in†

λC n ` (W {kl := Kl0 }) = W † {kl := L}†

where L = λx.Al hKl0 xil
Proof. These equations can be proved by simultaneous induction on
the structure of Ti , Tn+1 , Kj , Kn+1 and W . We prove only the third

main.tex; 12/07/2005; 23:57; p.29

30
equation when j = l and Kj ≡ kl :lefthand side = hKj † hM ij−1 ijrighthand side = h(λx.Aj hKj † xij )hM ij−1 ij= h(λx.hAj hKj † xij ij )hM ij−1 ijby reset-lift-2†by (*)= h(λx.Kj x)hM ij−1 ijby reset-lift-2= h(λx.hKj xij )hM ij−1 ij†= hKj † hM ij−1 ijby βΩ

In the derivation of (*), we used hAj hN ij ij = hN ij which was proved
during the proof of reset-reset in Theorem 2.
For the fourth equation when Kn+1 is a continuation variable, itcannot be kl since their levels are different, hence the substitution is
vacuous and we can easily prove the equation.
The other cases of Lemma 2 can be proved similarly.
The next lemma is for the substitution of the level-(n + 1) continuation variable kn+1 , where we only have to treat Tn+1 and Kn+1 , sinceby Property-#, the continuation variable kn+1 occurs freely in theseterms only.
0
LEMMA 3. Let Tn+1 , Kn+1 and Kn+1
be terms of type Expn+1 Contn+1
and Contn+1 , resp., kn+1 be a continuation variable of type Contn+1 ,and M be a term in λC n . Then we have:
†

†

0
0
hTn+1 † in
λC n ` (Tn+1 {kn+1 := Kn+1}) = Kn+1††00hKn+1 † hM in in
λC n ` (Kn+1 {kn+1 := Kn+1}) hM in = Kn+1

Proof. This lemma is proved by induction on Tn+1 and Kn+1 .
0
We only prove the second equation when Kn+1 = λx.Tn+1
for some0
Tn+1 of type Expn+1 and leave other cases to the reader:†00lefthand side ≡ (λx.(Tn+1{kn+1 := Kn+1}) )hM in†0= (λx.Kn+1
hTn+1 † in )hM in by induction hypothesis†0righthand side ≡ Kn+1h(λx.Tn+1 † )hM in in

On the other hand, we can prove (λx.LhN in )hM in = Lh(λx.N )hM in in(for x 6∈ FV(L)) using β-lift in Section 5.1 (which is in turn proved byβΩ ) and reset-lift. Consequently, we have that both sides of the second
equation are provably equal in λC n .

main.tex; 12/07/2005; 23:57; p.30

31
Other cases can be proved similarly.
Proof of Theorem 4. This is proved by simultaneous induction on
the structure of Ti , Tn+1 , Kj , Kn+1 and W .
0
Suppose λTn ` Ti = Ti0 , λTn ` Tn+1 = Tn+1
, λTn ` Kj = Kj0 ,0
λTn ` Kn+1 = Kn+1
, and λTn ` W = W 0 . It suffices to prove the000theorem when Ti , Tn+1 , Kj0 , Kn+1
and W 0 are obtained by one-stepreduction from the corresponding terms. There are several cases toconsider.
(Case 1: reduction of a subterm) This is the case when we reduce a
proper subterm of Ti etc. By careful inspection of the shape of the resultof the DS translation, we can show that the statement of Theorem 4 issufficient to make the whole induction go through.
For instance, suppose Ti = λki .T 00 for 1 ≤ i ≤ n, and Ti0 is obtained by one-step reduction of a redex in T 00 , then we have: hTi † ii ≡hCi ki .T 00 † ii = hCi ki .hT 00 † ii ii under λC n , hence we can apply the induction hypothesis on T 00 . Also all we need about a term Kj of type Contj
is the case when it appears in a subterm hKj † hM ii−1 ij , so the induction
hypothesis suffices.
(Case 2: the whole term is a β-redex or an η-redex which is being
contracted) There are six cases to consider.
(Case 2-β-1) 1 ≤ i ≤ n, Ti ≡ (λki .T )Ki , and Ti0 ≡ T {ki := Ki }.
We can calculate as follows:hTi † ii ≡ hKi † hCi ki .T † ii−1 ii= hT † {ki := λx.Ai hKi † xii }ii by C-lift,reset-value†= hTi0 ii by Lemma 2
0(Case 2-β-2) Tn+1 ≡ (λkn+1 .T )Kn+1 , and Tn+1
≡ T {kn+1 := Kn+1 }.
†
†
†
†
0
We can calculate as Tn+1 ≡ Kn+1 hT in = Tn+1
by Lemma 3.
0(Case 2-β-3) Ti ≡ (λx.T )W and Ti ≡ T {x := W } for 0 ≤ i ≤ n + 1.
This case can be proved using Lemma 1.
(Case 2-η-1) Ti ≡ λki+1 .Ti0 ki+1 , 0 ≤ i ≤ n, and ki+1 6∈ FV(Ti0 ).
If i ≤ n−1, then we have hTi † ii ≡ hCi+1 ki+1 .ki+1 hTi0 † ii ii = hhTi0 † ii ii =hTi0 † ii .
If i = n, then we have hTn † in ≡ h(λx.x)hTn0 † in in = hTn0 † in(Case 2-η-2) Ki ≡ λx.Ki0 x, 1 ≤ i ≤ n + 1, and x 6∈ FV(Ki0 ).
Take any term M in λC n .
If i ≤ n, we have hKi † hM ii−1 ii ≡ h(λx.hKi0 † xii )hM ii−1 ii , and by
reset-lift-2 and ηv , it is equal to hKi0 † hM ii−1 ii .
††00
If i = n+1, we have Kn+1 † hM in ≡ (λx.Kn+1x)hM in = Kn+1
hM in .
(Case 2-η-3) W ≡ λx.W 0 x and x 6∈ FV(W 0 ).

main.tex; 12/07/2005; 23:57; p.31

32This case is easily proved, completing the proof of Theorem 4.
The next theorem corresponds to Property (1), that is, † is a (left)
inverse of the extended CPS translation.
THEOREM 5. If M is a term in λC n , then λC n ` [ M ] † = M .
Proof. We will prove λC n ` [ M ] † = M and λC n ` V ∗ † = V bysimultaneous induction on a term M and a value V in λC n . We list
proofs of a few interesting cases.
(Case: M = N1 N2 )[ N1 N2 ] † = C1 k1 .(λm.h(λn.hk1 (mn)i1 )[[N2 ] † i1 )[[N1 ] †= C1 k1 .(λm.h(λn.hk1 (mn)i1 )N2 i1 )N1 by induction hypothesis= C1 k1 .hλm.hhk1 (mN2 )i1 i1 N1 i1 by reset-lift-2,βΩ ,C-reset= C1 k1 .hk1 (N1 N2 )i1 by reset-lift-2,βΩ ,C-reset= N1 N2 by C-reset,C-elim(Case: M = hN ii ) We can easily show θi † = λx.x.
When 1 ≤ i ≤ n − 1, we have:[ hN ii ] † = Ck1,i+1 .(λx.hki+1 hki · · · hk1 xi1 · · ·ii ii+1 )h(λx.x)h(λx.x) · · · (λx.x)h[[N ] † i1 · · ·ii−1 ii= Ci+1 ki+1 .(λx.hki+1 xii+1 )h[[N ] † ii by telescope, βΩ , reset-reset= h[[N ] † ii by reset-lift-2, ηv , C-elim= hN ii by induction hypothesis
When i = n, we have:[ hN in ] † = Ck1,n .(λx.(λx.x)hkn · · · hk1 xi1 · · ·in )h(λx.x)h(λx.x) · · · (λx.x)h[[N ] † i1 · · ·in−1 inand we can derive [ hN in ] † = hN in in the same way as the previous
derivation.
0 .θ xk . Then L is of type Value,(Case: M = Ci c.N ) Let L = λxk1,i0
1,iand we have
0 .k hk
L† = λx.Ck1,ii i−1 h· · · hk1 h(λy.y)xi1 i2 · · ·ii−2 ii−10 .(λx.k hk= λx.Ck1,ii i−1 h· · · hk1 hxi1 i2 · · ·ii−2 ii−1 )x by βΩ , βv

main.tex; 12/07/2005; 23:57; p.32

33
Then we have:[ Ci c.N ] † = Ck1,i .(λx.x)h(λx.x)h· · · h(λx.x)([[N ] {c := L})† i1 · · ·ii−2 ii−1
= Ck1,i .([[N ] {c := L})† by βΩ , reset-reset, C-reset= Ck1,i .[[N ] † {c := L† } by Lemma 1= Ci k.[[N ] † {c := λx.Ci k 0 .kx} by telescope twice= Ci k.[[N ] † {c := λx.Ai hkxii−1 } by (*)= Ci k.[[N ] † {c := k} by C-abort, ηv= Ci c.N by induction hypothesis
For the derivation of (*), we used Ci .M = Ai hM ii−1 , which has been
already derived in the derivation of telescope (in the proof of Theorem
2).
Now we can prove the completeness of λC n .
THEOREM 6 (Soundness & Completeness). Let M and N be termsin λC n . Then we have:
λC n ` M = N if and only if λTn ` [ M ] = [ N ]Proof. Soundness (the “only-if” direction) can be proved by calculating both sides of axioms in λC n . For completeness (the “if” direction),
suppose λTn ` [ M ] = [ N ] . Since [ M ] and [ N ] are of type Exp0 , wehave λC n ` [ M ] † = [ N ] † by Theorem 3. Using Theorem 5, we conclude
that λC n ` M = N .
6.4. Completeness of λSn
We can also obtain soundness and completeness of λSn .
THEOREM 7 (Soundness & Completeness). Let M and N be termsin λSn . Then we have:
λSn ` M = N if and only if λTn ` [ M ] = [ N ]Proof. Soundness can be proved in the same way as for λC n . For
completeness, let φ be a translation from terms in λSn to terms in λC nwhich replaces Si by its “definition” in Ci given in Section 3. Namely,
φ(Si k.M ) = Ci k 0 .φ(M ){k := λx.hk 0 xii }where k 0 is fresh. φ is homomorphic on other term constructors. Similarly let ψ be a translation from λC n to λSn defined by:ψ(Ci k.N ) = Si k 0 .ψ(N ){k := λx.Si .k 0 x}

main.tex; 12/07/2005; 23:57; p.33

34
where k 0 is fresh. It suffices to prove the following three properties forterms M and M 0 in λSn and terms N and N 0 in λC n :1. λTn ` [ φ(M )]] = [ M ] .
2. λC n ` N = N 0 implies λSn ` ψ(N ) = ψ(N 0 ).
3. λSn ` ψ(φ(M )) = M
The first property can be proved by calculation.
For the second property, we need to show that each of three specificaxioms in λC n is mapped to derivable equations in λSn by ψ. We only
show the case for C-lift, which can be shown as follows (we write E 0 forψ(E j−1 ) and M 0 for ψ(M )):ψ(hE j−1 [Cj k.M ]ii ) ≡ hE 0 [Sj c.M 0 {k := λx.Sj .cx}]ii= hM 0 {k := λx.Sj .hE 0 [x]ij }]ii by S-liftψ(hM {k := λx.Aj hE j−1 [x]ij }ii ) ≡ hM 0 {k := λx.(λx.Sj .x)hE 0 [x]ij }ii )hence the remaining task is to prove Sj .hN ij = (λx.Sj .x)hN ij for any
N in λSn , which can be proved similarly as Cj .hN ij = (λx.Cj .x)hN ij .
To prove the third property, we haveψ(φ(Si k.M )) ≡ Si k 0 .ψ(φ(M )){k := λx.hSi .k 0 xii }= Si k 0 .ψ(φ(M )){k := λx.k 0 x} by (*)= Si k.ψ(φ(M )) by ηv
For the derivation (*), we need telescope in terms of shift in λSn , which
is proved similarly as in Theorem 2 for λC n .
This completes the proof of Theorem 7.

6.5. Type System for the Source Calculus
So far we have been studying type-free source calculi only. Introducing
a type structure into source calculi is an important problem, as mostmodern programming languages have a built-in type system to enhance
the reliability of programs. Another motivation of introducing types isthat, in the presence of appropriate types, we can avoid the full ηv equality (λx.V x = V for x 6∈ FV(V )), which is inconsistent with thepresence of basic values such as natural numbers.

main.tex; 12/07/2005; 23:57; p.34

35
We can introduce a simply typed structure to the source calculus
λSn with a set of basic types such as Nat, the type for natural numbers.
For control operators, the simplest choice of typing would be:Γ ` M : τ0
Γ ` hM ii : τ0

Γ, k : σ → τ0 ` M : τ0
Γ ` Si k.M : σ

where τ0 is a fixed type, and σ is an arbitrary type. We assume thatall shift and reset control operators use the same type for τ0 . Then wecan prove that the extended CPS translation preserves typability if we
add the type information to the classes Exp0 and Value in the target
calculus. All the axioms and the equations in the proof of soundness andcompleteness are typable, and our proof goes through for the simply
typed case.
The simply type system above suffices for Filinski’s implementationof shift and reset [13], but it is too restrictive. Danvy and Filinski [8] andMurthy [26] have proposed more liberal type systems for shift and reset,
both of which essentially assign types induced by the CPS translation
to source terms. Since the work presented in this article is orthogonal
to the type systems in the source calculus, it seems straightforward toextend our axioms to the source calculi with these type systems.
Introduction of types to the source calculi makes explicit the connection of the extended CPS translation and the double negation translation. If we take n = 1, then by the definition of types given in Section
4.4 we have Exp0 = (Value → Ans) → Ans. If we take n = 2, then
Exp0 = (Value → (Value → Ans) → Ans) → (Value → Ans) → Ans
Hence the type Ans in the n = 1 case (which corresponds to ⊥ in the
double negation translation) is CPS translated to (Value → Ans) →Ans in the n = 2 case. Thus, we can say the extended translation represents an iterated double-negation translation. It seems an interesting
challenge to investigate the logical contents of iterated CPS translations(or equivalently, iterated double-negation translations).
Recently Ariola, Herbelin and Sabry [1] gave a type-theoretic study
on control operators for delimited continuations. Their work is conceptually close to our earlier work [21] in that their purpose is to obtain alogical view of these control operators through the type system. They
mainly studied direct-style calculi independently to a CPS translation.

main.tex; 12/07/2005; 23:57; p.35

36
7. Conclusion
In this article, we have studied a family of control operators in the CPS
hierarchy. In particular, we have analyzed the image of the extended
CPS translation with type-theoretic machinery, and have obtained asimple set of axioms which is sound and complete for all such control
operators. To our knowledge this work is the first such result about thehierarchy of delimited continuation operators. Our axioms for level-n
shift/reset are a simple extension of those for level-1 shift/reset, andthe axioms for level-n C/reset are even simpler than those for level-2
C/reset.
The control operators in the CPS hierarchy have also been investigated by Murthy [26], who gave an elaborate type system for level-n
shift and reset, and also gave a set of axioms for them. The difference
between his work and ours is that he only proved the soundness of theaxioms and did not state completeness, and also that his set of axioms
consists of many complex axioms such as the telescope axiom, whileours consists of a small number of simple axioms, which can derive, forinstance, a generalized version of telescope axiom.
In another line of work, Danvy and Yang [11], Murthy [26], andBiernacka, Biernacki and Danvy [5] studied an operational aspect of
the control operators in the CPS hierarchy, and derived an abstract
machine from the CPS translation, and also a set of reduction rules for
shift and reset. Their reduction rules are essentially the same as theones we gave as an operational semantics.
In the study of delimited continuations, there is a question about
which control operators are the best among many proposed ones [12, 19,
20, 21, 1]. Even recently, this question is the target of hot discussion[31, 6]. It is difficult to answer this question if we only look at theoperational semantics. However, if we take the CPS translation as ouressential tool to write applications as well as studying foundations,then shift and reset (and their relatives such as Ci and Di ) are theonly control operators defined solely by (the iteration of) the standard
CPS translation among the proposed control operators. In recent years,
it has been shown that for the case of level-1 control operators fordelimited continuations, shift and reset are the standard choice, foronly shift and reset have found many applications in divergent areas.
For the case of higher level control operators where different delimiters (reset) exist in one program, things have not been settled, andthere are many conflicting views about their necessity and expressiveness. In this article, we have shown that the higher level shift and reset
can be axiomatized by a small set of concise axioms, whose sizes (asterms) are almost the same as those for level-1 shift and reset. Thus, wemain.tex; 12/07/2005; 23:57; p.36

37
believe that we can reinforce the claim that shift and reset are one of thebetter choices for higher level control operators too. Also the existenceof several application programs and the correspondence between the
CPS hierarchy and layered monads [15] seem to give a positive answer
to this question. Recently Asai has studied partial evaluators using
shift and reset and its correctness using our axiomatization for level-1
shift and reset [2, 3]. If the source language contains shift and reset,
then one may need higher level shift and reset, and our direct-styleaxiomatization in this article will be needed to guarantee its correctness, since CPS translating the whole partial evaluator may result in arather complicated program which is difficult to reason about.
Future Work: There are several possibilities for future work on the
topics of this article.
First, while we have built an equational foundation for the control
operators in the CPS hierarchy there remains a question about theapplication of our axioms. It is difficult to use them for automatic
verification because they require a degree of insight. Nevertheless, wehope to use the axioms to prove the correctness of program translations.
In Section 5.1, we briefly mentioned how to use the axioms reset-lift toshow an equation which is useful in the let-insertion technique, but athorough investigation on this direction is yet to be done.
Secondly, it is interesting to see which reduction rules are sound andcomplete with respect to the CPS translation rather than equations.
This question is theoretically interesting as well as practically important in connection with operational semantics and abstract machinesof shift and reset. Still it is a hard question even for the case of callcc.
Finally and most importantly, in order to answer the basic question
about which higher level control operator is the best one, we need tohave more substantial applications using higher level shift and reset.
Acknowledgments: The author would like to thank Olivier Danvy,
Masahito Hasegawa, Kenichi Asai, Dariusz Biernacki, Malgorzata Biernacka, and Amr Sabry for constructive comments and discussions. He
also thanks anonymous referees of CSL’04 and HOSC for many insightful comments and criticisms, and Noam Zeilberger for proofreading.
This work was supported in part by Japan Science and Technology
Agency, and by Grant-in-Aid for Scientific Research No. 16500004 fromJapan Society for the Promotion of Science.
References1.

Ariola, Z. M., H. Herbelin, and A. Sabry: 2004, ‘A Type-Theoretic Foundation of Continuations and Prompts’. Proc. ACM SIGPLAN International
Conference on Functional Programming pp. 40–53.

main.tex; 12/07/2005; 23:57; p.37

38
2.

3.

4.
5.

6.

7.
8.
9.
10.
11.
12.
13.
14.
15.
16.

17.
18.
19.

20.
21.

22.

Asai, K.: 2002, ‘Online Partial Evaluation for Shift and Reset’. In: Proc. ACM
Workshop on Partial Evaluation and Semantics-Based Program Manipulation.
pp. 19–30.
Asai, K.: 2004, ‘Offline Partial Evaluation for Shift and Reset’. In: Proc.
2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based
Program Manipulation. pp. 3–14.
Berdine, J., P. O’Hearn, U. Reddy, and H. Thielecke: 2002, ‘Linear Continuation Passing’. Higher-Order and Symbolic Computation pp. 181–208.
Biernacka, M., D. Biernacki, and O. Danvy: 2004, ‘An Operational Foundation
for Delimited Continuations’. In: Proc. Fourth ACM SIGPLAN Workshop
on Continuations, Technical Report CSR-04-1, School of Computer Science,
University of Birmingham. pp. 25–34.
Biernacki, D. and O. Danvy: 2005, ‘On the Dynamic Extent of Delimited Continuations’. Technical Report BRICS-RS-05-2, BRICS, University of Aarhus,
Denmark.
Danvy, O.: 1996, ‘Type-Directed Partial Evaluation’. In: Proc. 23rd Symposiumon Principles of Programming Languages. pp. 242–257.
Danvy, O. and A. Filinski: 1989, ‘A Functional Abstraction of Typed Contexts’.
Technical Report 89/12, DIKU, University of Copenhagen.
Danvy, O. and A. Filinski: 1990, ‘Abstracting Control’. In: Proc. 1990 ACM
Conference on Lisp and Functional Programming. pp. 151–160.
Danvy, O. and A. Filinski: 1992, ‘Representing Control: a Study of the CPS
Transformation’. Mathematical Structures in Computer Science 2(4), 361–391.
Danvy, O. and Z. Yang: 1999, ‘An Operational Investigation of the CPS
Hierarchy’. In: Proc. 8th European Symposium on Programming. pp. 224–242.
Felleisen, M.: 1988, ‘The Theory and Practice of First-Class Prompts’. In:
Proc. 15th Symposium on Principles of Programming Languages. pp. 180–190.
Filinski, A.: 1994, ‘Representing Monads’. In: Proc. 21st Symposium on
Principles of Programming Languages. pp. 446–457.
Filinski, A.: 1996, ‘Controlling Effects’. Ph.D. thesis, Carnegie Mellon
University, available as Technical Report CMU-CS-96-119.
Filinski, A.: 1999, ‘Representing Layered Monads’. In: Proc. 26th Symposiumon Principles of Programming Languages. pp. 175–188.
Flanagan, C., A. Sabry, B. F. Duba, and M. Felleisen: 1993, ‘The Essenceof Compiling with Continuations’. Proc. ACM SIGPLAN Conference on
Programming Language Design and Implementation pp. 237–247.
Friedman, H.: 1978, ‘Classically and Intuitionistically Provably Recursive
Functions’. In: Lecture Notes in Mathematics 699. pp. 21–28.
Griffin, T.: 1990, ‘A Formulae-as-Types Notion of Control’. In: Proc. 17th
Symposium on Principles of Programming Languages. pp. 47–58.
Gunter, C. A., D. Rémy, and J. G. Riecke: 1995, ‘A Generalization of Exceptions and Control in ML-Like Languages’. In: Proc. Functional Programmingand Computer Architecture. pp. 12–23.
Hieb, R., R. Dybvig, and C. W. Anderson: 1993, ‘Subcontinuations’. Lisp andSymbolic Computation 6, 453–484.
Kameyama, Y.: 2000, ‘A Type-Theoretic Study on Partial Continuations’. In:
Proc. IFIP International Conference on Theoretical Computer Science. pp.
489–504.
Kameyama, Y.: 2004, ‘Axiomatizing Higher Level Delimited Continuations’.
In: Proc. 3rd ACM SIGPLAN Workshop on Continuations, Technical Report
545, Computer Science Department, Indiana University. pp. 49–53.

main.tex; 12/07/2005; 23:57; p.38

39
23.

24.

25.
26.

27.
28.

29.
30.

31.
32.

Kameyama, Y. and M. Hasegawa: 2003, ‘A Sound and Complete Axiomatization of Delimited Continuations’. In: Proc. ACM SIGPLAN International
Conference on Functional Programming. pp. 177–188.
Lawall, J. and O. Danvy: 1994, ‘Continuation-Based Partial Evaluation’. In:
Proc. 1994 ACM Conference on LISP and Functional Programming. pp. 227–
238.
Moggi, E.: 1989, ‘Computational Lambda-Calculus and Monads’. In: Proc. 4th
Symposium on Logic in Computer Science. pp. 14–28.
Murthy, C.: 1992, ‘Control Operators, Hierarchies, and Pseudo-ClassicalType Systems: A-Translation at Work’. In: Proc. First ACM Workshop on
Continuations, Technical Report STAN-CS-92-1426, Stanford University. pp.
49–72.
Plotkin, G. D.: 1975, ‘Call-by-Name, Call-by-Value, and the λ-Calculus’.
Theoretical Computer Science 1, 125–159.
Sabry, A.: 1996, ‘Note on Axiomatizing the Semantics of Control Operators’.
Technical Report CIS-TR-96-03, Dept. of Computer Science, University ofOregon.
Sabry, A. and M. Felleisen: 1993, ‘Reasoning about Programs in ContinuationPassing Style’. Lisp and Symbolic Computation 6(3-4), 289–360.
Sekiguchi, T., T. Sakamoto, and A. Yonezawa: 2001, ‘Portable Implementationof Continuation Operators in Imperative Languages by Exception Handling’.
In: Advances in Exception Handling Techniques. pp. 217–233.
Shan, C.: 2004, ‘Shift to Control’. Proc. 5th Workshop on Scheme andFunctional Programming pp. 99–107.
Thielecke, H.: 2003, ‘From Control Effects to Typed Continuation Passing’. In:
Proc. 30th Symposium on Principles of Programming Languages. pp. 139–149.

main.tex; 12/07/2005; 23:57; p.39

main.tex; 12/07/2005; 23:57; p.40