Axioms for Delimited Continuationsin the CPS Hierarchy
Yukiyoshi Kameyama
Department of Computer Science, University of Tsukuba
Tennodai 1-1-1, Tsukuba, 305-8573, JAPANandJapan Science and Technology Agency
kameyama@acm.org

Abstract. A CPS translation is a syntactic translation of programs,
which is useful for describing their operational behavior. By iterating thestandard call-by-value CPS translation, Danvy and Filinski discovered
the CPS hierarchy and proposed a family of control operators, shift andreset, that make it possible to capture 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 level of the hierarchy, namely, to level-1 shift and reset.
In this article, we investigate the whole family of shift and reset. We givea simple calculus with level-n shift and level-n reset for an arbitraryn > 0. We then give a set of equational axioms for them, and prove thatthese axioms are sound and complete with respect to the CPS translation. The resulting set of axioms is concise and a natural extension of
those for level-1 shift and reset.
Keywords: CPS Translations, Control Operators, Delimited Continuations, Axiomatization, Type System.

1

Introduction

A CPS translation transforms a source term into continuation-passing style (CPSfor short). It can be regarded as a compilation step, since it makes explicit theevaluation order of the source program and gives names to intermediate results.
Another motivating fact for CPS is that it 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 [12]. The control mechanisms added to the source language canbe also understood logically. For instance, Griffin [13] has revealed the CurryHoward correspondence between the calculus with callcc and classical logic.
Danvy and Filinski [7, 8] observed that there is room for a more refined
control mechanism. By CPS translating the answer type of the standard CPS

translation, they obtained what they call a CPS hierarchy. Furthermore, they
proposed a family of control operators shift and reset to abstract delimited
continuations in this hierarchy. In the literature, many different control operatorsfor delimited continuations have been proposed [10, 14–16]. In contrast to theseother control operators, shift and reset are solely defined in terms of the CPS
translation. In addition, they have found applications in partial evaluation [19],one-pass CPS translations [8], and normalization by evaluation [4], as well as torepresent layered monads [11] and mobile computation [24].
In this article, we study a theoretical foundation of the control operators in
the CPS hierarchy. Specifically, we address the problem of finding direct-styleaxioms for them. While these operators are used in many applications and theirsemantics is given by a CPS translation (be it iterated or extended), we often
want to reason about source programs directly, rather than treating the imageof CPS translations, since the CPS translation is sometimes said to obscure
the overall structure of source programs. Also finding a good set of direct-styleaxioms could lead one to a better understanding of these operators.
We give a simple set of axioms consisting of only three equations for shift
and three equations for reset, and then prove that this set of equations is soundand complete with respect to the iterated CPS translation. This work builds on
our previous work, in which we gave a sound and complete axiomatization forlevel-1 shift and reset operators [18], and for level-2 [17]. Since completenessproofs of this kind often require quite a lot of calculations, we make the proof
more structured by following an idea due to Sabry [22, 23] and reconstructing it
in a type-theoretic setting, which further simplifies our proof.
Overview: The rest of this article is organized as follows. In Section 2, we informally introduce shift and reset and we explain their operational aspect. In
Sections 3 and 4, we formally introduce the calculi with these control operators
and a CPS translation for them. In Section 5 we present the axioms for control
operators. In Section 6, we give a type-theoretic analysis of the CPS translation
and we prove completeness. In Section 7, we conclude and mention future work.
Prerequisites: We assume that readers have some familiarity with CPS translations.

2

Control Operators in the CPS hierarchy

We introduce the shift and reset operators through some examples.
2.1

A Simple Example

The following example uses these operators in a simple way:
3 + h4 ∗ S(λk. 5 + (k (k 2)))i = let k be λx.h4 ∗ xi
in 3 + h5 + (k (k 2))i
= 3 + h5 + h4 ∗ h4 ∗ 2iii
2where h i is the reset operator and S is the shift operator.1 Unlike the continuation captured by callcc, the continuation captured by S is not the whole
rest of the computation (such as 3 + h4 ∗ [ ]i), but a part which is delimited
by a reset, that is, h4 ∗ [ ]i. Also it is not abortive, and thus we can compose
the captured continuation with ordinary functions. When several occurrences ofreset enclose an occurrence of shift, the (dynamically determined) closest one
is chosen as the delimiter.
As more substantial examples, we borrow the ones by Danvy and Filinski [7].
2.2

Nondeterminism

A non-deterministic choice can be represented by backtracking in direct styleusing shift and reset:defflip(x) = S1 (λc. begin c(true); c(false); fail( ) end)def

fail(x) = S1 (λc. "no")defchoice(n) = if n < 1 then fail( )else if flip( ) then choice(n − 1)else nwhere is a dummy value, true, false are truth values, and begin· · · end is forsequencing.
To understand these programs, we CPS translate these three functions as:
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))
Let us consider the program hdisplay(choice(3))i1 . It is CPS translated to theprogram choice-c(3, display), which will display 1, 2 and 3 in this order. It
is easy to see that shift captures the current continuation, which is composable with functions (including other continuations), and that reset installs theidentity continuation.
2.3

Collecting Successive Results

As a next step, one may wants to collect all answers generated by non-deterministic
choices. This is implemented by the function emit defined by:defemit(n) = S1 (λc. cons(n, c(nil)))
For instance, hbegin emit(1); emit(2); emit(3) endi1 will return a list (1 2 3).
1

Danvy and Filinski used the notation ξk.M for S(λk.M ).

3

It is then natural to expect that a combined program hemit(choice(3))i1
would work. However it does 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))i1 is CPS translated to choice-c(3, λx.emit-c(x, λa.a)),which will generate three lists (1), (2) and (3), but never collect these answers.
A correct way of combining these programs is to make them layered. The
continuation captured in emit should be in a higher level than that captured inchoice. To achieve this, the CPS counterpart of emit should be:defemit-c2(n, k, γ) = cons(n, γ(k(nil)))where γ is a level-2 continuation. Its direct-style counterpart is:defemit-c1(n, k) = k(S1 (λc. cons(n, c(nil))))which passes a continuation, even though it is not in CPS since the argument of
k is not a trivial term. 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 in the CPS hierarchy.
Executing the term hemit(choice(3))i2 returns (1 2 3) as expected.
2.4

Summary and Conclusion

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 thisprogram yields a real CPS program where all calls are tail calls and all subterms
are trivial. The family of layered control operators thus corresponds to the CPS
hierarchy.
A similar situation occurs when we perform partial evaluation of a programusing shift/reset when the partial evaluator itself uses shift/reset. We referto the reader to Asai’s recent work [1, 2].

3

The Calculi with Control Operators

In this section, we define the language of our calculi, and postpone giving axioms
until the next section.
The calculus we choose here is a type-free lambda calculus with control operators for delimited continuations. Later we briefly mention simply typed calculi.
We consider the call-by-value evaluation order only.
We shall define calculi λS n and λC n for a natural number n. The former is acalculus with shift/reset, and the latter a calculus with C/reset. The control
4operator C has a slightly different semantics as shift, which will be explainedlater.
We first assume there are infinitely many variables (written x, y, z and so on).
Terms of λS n are type-free lambda terms augmented with control operators, anddefined by:(terms) M, N ::= x | λx.M | M N | hM ii | Si
where 1 ≤ i ≤ n. Terms of λC n are defined in the same way with Si being
replaced by Ci .
The index i denotes the level, which is conceptually the number of iterationsof CPS translations that are necessary to interpret the control operator. The
construct h ii is level-i reset, and Si is shift. Note that Si (and Ci ) is a constant rather than a constructor. We use the abbreviations: Si k.M ≡ Si (λk.M ),Ci k.M ≡ Ci (λk.M ), and Ai ≡ λx.Ci (λk.x). We also define hM i0 ≡ M .
A value (written V ) is either a variable, λ-abstraction, or a constant (Si in
λS n and Ci in λC n ). Variables are bound by λ, and free and bound variables ofterms are defined as usual. F V (M ) denotes the set of free variables in M . We
identify two terms which differ only in renaming of bound variables. M {x := N }is the result of the usual capture-avoiding substitution of N for x in M .
Contexts and evaluation contexts are defined as follows:
C ::= [ ] | CM | M C | hCii
E ::= [ ] | EM | V E | hEii
E i ::= [ ] | E i M | V E i | hE i ij for j ≤ i
E is an evaluation context in call by value, and E i is a level-i evaluation context
in which the level of reset operators enclosing the hole must be equal to or smaller
than i. For example, hx[ ]i2 and hx[ ]i2 hyzi3 are level-2 evaluation contexts. Asa special case, E 0 is an evaluation context in which no reset may enclose thehole.
The operational semantics is given by the following rules (where f 6∈ F V (E j−1 )):
E[hE

j−1

E[hV ij ] → E[V ][Sj V ]ij ] → E[hV (λf.hE j−1 [f ]ij )ij ]The first rule says that delimiting a value does nothing. The second rule shows
how the S-operator works. It captures the continuation delimited by the (dynamically determined) closest reset-operator, as the evaluation context E j−1
does not contain a level-j reset operator which encloses the hole. Note that thecontinuation captured by Sj is a function, whose body is enclosed by a level-j reset operator. This is an essential difference between Danvy and Filinski’s shiftoperator and Felleisen’s control operator [10].
The rule above is only a special case of the general rule given below. As we
explained before, the level of the corresponding reset operator can be higher thanj. Therefore a general rule for the second line is (where j ≤ i and f 6∈ F V (E j−1 )):E[hE j−1 [Sj V ]ii ] → E[hV (λf.hE j−1 [f ]ij )ii ]5

The two operators Si and Ci are inter-definable:
Si = λz.Ci (λk.z(λx.hkxii ))Ci = λz.Si (λk.z(λx.Si (λd.kx)))
These equations are formally justified by the CPS translation in the next section.

4

CPS Translation

The CPS translation we consider is due to Danvy and Filinski [7]. It translates
terms of the source calculi (λS n or λC n ) to the type-free lambda calculus without
control operators. As we explained in the introduction, their CPS translation canbe thought of as a standard CPS translation followed by n − 1 successive CPS
translations of the answer type for n > 1. If we fix the number of iterations, then
the whole translations can be expressed by a single, uncurried CPS translation,
which we call an extended CPS translation. It takes n continuation parameters,
each being introduced by the i-th CPS translation (for 1 ≤ i ≤ n). This extended
CPS translation gives a precise semantics to the level-i control operators (fori < n). The n continuation parameters are represented by the variables ki ,which we call a continuation variable of level i (for 1 ≤ i ≤ n).
For a fixed n, and given a term M and a value V in the source calculi, wedefine two translations [ ] and ∗ , which send a term and a value to terms oftype-free lambda calculus. To avoid clutter we present a βη-reduced version. In
the following we assume 1 ≤ i < n.
def

[ V ] = λk1 . k1 V ∗def[ M N ] = λk1 . [ M ] (λm.[[N ] (λn.mnk1 ))def[ hM ii ] = λk1 . · · · λki+1 . [ M ] θ1 · · · θi (λx. θ0 xk1 k2 · · · ki+1 )defx∗ = xdef(λx.M )∗ = λx.[[M ]def00Si ∗ = λxk1 · · · ki . x(λyk10 · · · ki+1
.θ0 yk1 k2 · · · ki (λz.θ0 zk10 k20 · · · ki+1))θ1 · · · θidefCi ∗ = λxk1 · · · ki . x(λyk10 · · · ki0 .θ0 yk1 k2 · · · ki )θ1 · · · θiwhere θi = λxki+1 .ki+1 x. The term θi can be thought of as the image of theidentity continuation (the empty evaluation context [5]) of level i.
Let us briefly explain the extended CPS translation. Terms and values without control operators are translated as usual. For the term hM ii , the reset operator installs identity continuations up to level i, and composes all continuationsof up to level i with the continuation of level i + 1. The operator Ci captures
the current continuation up to level i, which results in λyk10 · · · ki0 .θ0 yk1 k2 · · · ki
in this context, then applies it to the argument. It also installs instances of
the identity continuation up to level i. The CPS translation of Si is slightly
6more complex, since it captures a non-abortive delimited continuation so that
we should compose k10 , · · · , kn0 with the captured continuation. Note that theresult of the extended CPS translation does not depend on n (if the result isdefined).
We show a few examples of the extended CPS translation and βη-reductionsin the target calculus:[ C2 (λf.f x)]] = λk1 .(λk1 .k1 C2 ∗ )(λm.(λk1 .k1 (λf.f x)∗ )(λn.mnk1 ))→βη λk1 . k1 x
[ hxyi2 ] = λk1 k2 k3 . [ xy]]θ1 θ2 (λz. θ0 zk1 k2 k3 )→βη λk1 k2 k3 . xyθ1 θ2 (λz. k1 zk2 k3 )The semantics of the target terms is given by the standard βη-equality (thetype-free lambda calculus with βη-equality will be denoted by λβη .) Given a
CPS translation and the target theory λβη , the source calculus is given a rigid
semantics (CPS semantics). The fundamental question addressed in this article
is, what is the equality theory that coincides with this CPS semantics. We first
give an answer to this question, and then prove it.

5

Axioms of λS n and λC n

We give axioms for the theories λS n and λC n . The common axioms for these
theories are shown in Figure 1, the specific axioms for λS n are in Figure 2, andthe specific axioms for λC n are in Figure 3. In the presentation of axioms, we
assume the levels of all control operators are less than n, namely, 1 ≤ i, j < n. For
the purpose of comparison, we list the axioms for the base level control operators
S1 and h i1 in Figure 4 which were given in our joint work with Hasegawa [18].
Recall that E i is a level-i evaluation context, Si k.M ≡ Si (λk.M ), Ci k.M ≡Ci (λk.M ), and hM i0 ≡ M . The last abbreviation is used when i = 1 in reset-lift-2
and others. (Note that i − 1 may be 0.)
Let us explain Figure 1. The first three axioms βv , ηv and βΩ are those for
Moggi’s computational lambda calculus, the canonical calculus in call-by-value[20]. The axiom reset-value is essentially the same as that in level-1 theory (Figure 4). The axioms reset-lift and reset-lift-2 lift a β-redex over a reset operator.
The axiom βΩ can be applied to the level-0 evaluation context only, but withthe help of these axioms we can lift a β-redex over a general evaluation context.
The axiom reset-lift is a natural extension of its level-1 counterpart, while nocounterpart of reset-lift-2 exists in level-1 axioms. The axiom may look strange
since the index j appears only in the right-hand side. We may restrict j to i inreset-lift-2 in the presence of the axiom hhM ij ii = hM ii for j ≤ i.
Besides the common axioms, each theory has three specific axioms for Si
or Ci . The axiom S-reset is a natural extension of its level-1 counterpart, while
the axiom S-elim is not quite the same as a natural extension of its level-1
counterpart. In fact, Si k.kN = N is not sound for i > 1. Danvy and Filinski [7]stated that the current formulation of shift/reset is not completely satisfactory7

(λx.M )V = M {x := V }βv

λx. V x = V

ηv , if x 6∈ F V (V )(λx.E 0 [x])M = E 0 [M ]βΩ , if x 6∈ F V (E 0 )hV ii = V

reset-valueh(λx.M )hN ii ij = (λx.hM ij )hN ii

reset-lift, j ≤ ih(λx.M )hN ii−1 ii = h(λx.hM ij )hN ii−1 ii

reset-lift-2, j ≤ iFig. 1. Common Axioms for λS n and λC n (1 ≤ i, j < n)Si k.hM ii = Si k.M

S-resetSi k.khM ii−1 = hM ii−1jS-elim, if k 6∈ F V (M )jhE [Si k.M ]ii = hM {k := λf. hE [f ]ii }ii

S-liftif k 6∈ F V (E j ), f 6∈ F V (kE j ), and j < iFig. 2. Specific Axioms for λS n (1 ≤ i, j < n)Ci k.hM ii = Ci k.M

C-resetCi k.khM ii−1 = hM ii−1jC-elim, if k 6∈ F V (M )jhE [Ci k.M ]ii = hM {k := λf. Ai hE [f ]ii−1 }ii

C-liftif k 6∈ F V (E j ), f 6∈ F V (kE j ), and j < iFig. 3. Specific Axioms for λC n (1 ≤ i, j < n)since S2 k.kN = N does not hold. However, by restricting N to hM ii , we haveobtained a sound axiom.
The last axiom S-lift is a natural extension of its level-1 counterpart (called
reset-S formerly).2 It is also a direct formulation of the operational semantics
given in the earlier section, by changing reduction to equality.
We believe that the resulting axioms are simple to understand, and the soundness of these axioms is not surprising. The completeness of λC n may be surprising, since one may think it lacks many important equations which were included
in our axiomatization of C2 [17], such as:
hhM ii il = hM imax(l,i)
hCi k.M ij = Ci k.M
hCi k.M ii = hM {k := Ai }ii(λx.C1 k.M )N = C1 k.(λx.M )N
C1 M = C1 k.M k
2

reset-reset
reset-C, if j < i
C-top
let-C1 , if k 6= x
C1 -fun, if k 6∈ F V (M )S-lift does not immediately subsume reset-S, since the latter allows an arbitrary M
in S1 M , while the former restricts it to be a function. However, this difference does
not matter since we can prove S1 M = S1 k.M k for k 6∈ F V (M ) in λS n .

8hV i1 = V

reset-valueh(λx.M )hN i1 i1 = (λx.hM i1 )hN i1

reset-lift

S1 k.kM = M

S-elim, if k 6∈ F V (M )S1 k.hM i1 = S1 k.M
0

S-reset0reset-S, if x 6∈ F V (E 0 )hE [S1 M ]i1 = hM (λx.hE [x]i1 )i1

Fig. 4. Axioms for λS other than βv , ηv , and βΩ

Another seemingly missing axiom is an equation for lifting Ci over an evaluation
context such as E[Ci k.M ] = M {k := · · · }. In the next theorem we show thatthese equations are derivable.
From now on, we will mainly investigate λC n . After proving its completeness,
we will come back to λS n .
Theorem 1. The equations reset-reset, reset-C, C-top, let-C1 and C1 -fun as wellas the following equations are derivable in λC n where k1 , · · · , ki , f are fresh variables, and k is not bound by C in C-abort.
E j [Ai hM ii−1 ] = Ai hM ii−1

A-abort, if j < i

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

E [Ci k.M ] = C1 k1 . · · · Ci ki .M {k := N }telescope, if j < ijwhere N is λf.ki hki−1 · · · hk1 (E [f ])i1 · · ·ii−1
Proof. The equation reset-reset is obtained in this way. By putting M = x in
reset-lift, we obtain hhN ii ij = (λx.hxij )hN ii , and by reset-value and βΩ , weobtain hhN ii ij = hN ii for j ≤ i. Similarly by putting N = x in reset-lift-2, we
obtain hM ii = hhM ij ii for j ≤ i, hence we are done.
The equation reset-C is obtained by putting E j = [ ] and E j = h[ ]ij in C-lift
and comparing the results. The equation C-top is obtained by putting E j = [ ]in C-lift and using reset-value and ηv .
For the remaining equations, we first derive by C-elim and C-reset:
M = C1 k1 .k1 M = C1 k1 .hk1 M i1 = C1 k1 .C2 k2 .hk2 hk1 M i1 i2
Iterating this process i-times we obtain:
M = C1 k1 .C2 k2 . · · · Ci ki .hki · · · hk2 hk1 M i1 i2 · · ·ii
By this equation and C-lift, we obtain the following key equation (where j < i):E j [Ci k.M ] = C1 k1 . · · · Ci ki .hki h· · · hk1 (E j [Ci k.M ])i1 · · ·ii−1 ii= C1 k1 . · · · Ci ki .hM {k := λf.Ai hki h· · · hk1 (E j [f ])i1 · · ·ii−1 ii−1 }ii
For A-abort, we first note that, if j < i then 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∈ F V (M ), then the right-hand
9

side of the key equation does not contain E j , hence E j [Ci k.M ] = Ci k.M . Then
we can compute as follows (for j < i):E j [Ai hM ii−1 ] = E j [(λx.Ci (λk.x))hM ii−1 ]j= (λx.E [Ci (λk.x)])hM ii−1
= (λx.Ci (λk.x))hM ii−1
= Ai hM ii−1

by definitionby the above equationby the key equation

For C-abort we compute as follows (where j < i):Ci k.C[E j [kV ]]= C1 k1 . · · · Ci ki .h(C[E j [kV ]]){k := λf.Ai hki h· · · hk1 f i1 · · ·ii−1 ii−1 }ii= C1 k1 . · · · Ci ki .hC[E j [Ai hki h· · · hk1 V i1 · · ·ii−1 ii−1 ]]ii
= C1 k1 . · · · Ci ki .hC[Ai hki h· · · hk1 V i1 · · ·ii−1 ii−1 ]ii
by A-abort
Since the final result does not contain E j , we have Ci k.C[E1j [kV ]] = Ci k.C[E2j [kV ]]for any level-j evaluation contexts E1j and E2j . The axiom C-abort then follows.
Applying C-abort to the key equation (by putting E j = Ai h[ ]ii−1 in Cabort), we obtain the telescope axiom.3 Verification of let-C1 and C1 -fun is left
for the reader.
This finishes the proof of the theorem.

6

Completeness Proof

The main results of this article are that the theories λS n and λC n are soundand complete with respect to the extended CPS translation into the theory λβη .
In the previous work, we proved completeness by the following strategy; (1) weanalyzed the syntax of the image of CPS translation, (2) defined an inverse CPS
translation, i.e., a direct-style transformation, and (3) proved that the equality
is preserved through this inverse translation. The most difficult part was to finda suitable inverse translation, and we found it by trial and error. In this article
our source calculus is much more complex than those in the previous studies,and therefore a better strategy is called for.
The proof method we present here is based on an idea by Sabry, who applied
it to the axiomatization of a calculus with level-1 shift and lazy reset [22]. In thissection, we develop his method in the type-theoretic framework so as to makethe proof more structured.
6.1

The Target Calculus and its Type Structure

We analyze the set of terms which contains the image of the extended CPS
translation and is closed under βη-reductions. We call this language (under theβη-equality) the target language or the target calculus.
3This is a generalized version of Murthy’s telescope axiom [21].

10An important observation on the target calculus is that it is typed by thefollowing type structure:
Termi = Conti+1 → Termi+1 for 0 ≤ i < nTermn = AnsConti = Value → Termi for 1 ≤ i ≤ nValue = Value → Term0
where Ans is an arbitrary, fixed type, called the answer type [7, 9].4 The above
definition of types makes sense if we have recursive types, that is, if the recursive
equation for Value has a solution. Note that if we were working in the typed
setting from the beginning, that is, our source calculi were simply typed lambda
calculi, we would not need recursive types for Value.
Using the type structure, terms of the target calculus can be introduced as
typed terms. A typing judgment is of the form Γ ` P : T where Γ is a setof variable-type pairs consisting of either x : Value or ki : Conti . As usual, avariable may occur at most once in Γ . We have the following eight type inference
rules for 0 < i ≤ n:
Γ ` W : Value Γ ` W 0 : ValueΓ ` W W 0 : Term0Γ ` Ti−1 : Termi−1 Γ ` Ki : ContiΓ ` Ti−1 Ki : Termi

Γ, ki : Conti ` Ti : TermiΓ ` λki .Ti : Termi−1Γ ` Ki : Conti Γ ` W : ValueΓ ` Ki W : Termi

Γ, ki : Conti ` ki : ContiΓ, x : Value ` Ti : TermiΓ ` λx.Ti : ContiΓ, x : Value ` x : ValueΓ, x : Value ` T0 : Term0Γ ` λx.T0 : Value

where Γ, x : Value means the set union Γ ∪ {x : Value}.
If we can prove Γ ` P : T using the typing rules above, we say that P is aterm (of type T ) in the target calculus. For instance, the term λk1 . k1 x (whichis the βη-reduced term of [ C2 (λf.f x)]]) can be typed as follows:x : Value, k1 : Cont1 ` k1 : Cont1 x : Value, k1 : Cont1 ` x : Valuex : Value, k1 : Cont1 ` k1 x : Term1
x : Value ` λk1 . k1 x : Term0
For this type structure, it is not difficult to prove the following theorem.
Theorem 2. (1) Let M and V be a term and a value, resp. in λC n . Then we
can derive Γ ` [ M ] : Term0 and Γ 0 ` V ∗ : Value for some Γ and Γ 0 .
(2) If we can derive Γ ` P : T in the target calculus, and P reduces to Q byβη-reductions, then we can derive Γ ` Q : T .
4

We can make the answer type parametric, as investigated by Thielecke [25].

11

6.2

Direct-Style Translation

We define an extended direct-style translation from the target calculus to thesource calculus λC n . We first give it as a syntactic translation † based on thetype structure of target terms as follows (for 0 < i ≤ n):† def(W W 0 ) = W † W 0

† def

†

(λki .Ti ) = Ci ki .Ti †† def(Ki W ) = Ki † W †def(λx.Ti ) = λx.hTi † ii

def

(λx.T0 ) = λx.T0 †(Ti−1 Ki ) = Ki † hTi−1 † ii−1

† def
† def

ki † = ki† defx† = x

The next theorem ensures that † is in fact a translation from λβη to λC n .
Theorem 3. The translation † respects the βη-equality in the target calculus,
namely, if P and Q are typable terms in the target calculus and λβη ` P = Q,
then λC n ` P † = Q† .
We also have that † is really an inverse of the extended CPS translation.
†

Theorem 4. If M is a term in λC n , then λC n ` [ M ] = M .
The proofs of these theorems are not shown here due to lack of space.
Now we can prove the completeness of λC n .
Theorem 5 (Soundness & Completeness). Let M and N be terms in λC n .
Then we have:
λC n ` M = N if and only if λβη ` [ M ] = [ N ]Proof. Soundness (the “only-if” direction) can be proved by calculating bothsides of axioms in λC n . For completeness (the “if” direction), suppose λβη ` [ M ] =††[ N ] . Since [ M ] and [ N ] are of type T0 , we have λC n ` [ M ] = [ N ] by Theorem
3. Using Theorem 4, we conclude λC n ` M = N .
6.3

Completeness of λS n

We finally obtain the completeness of λS n .
Theorem 6 (Soundness & Completeness). Let M and N be terms in λS n .
Then we have:
λS n ` M = N if and only if λβη ` [ M ] = [ N ]Proof. Soundness can be proved in the same way as λC n . For completeness, let
φ be a translation from terms in λS n to terms in λC n which replaces Si by its“definition” in Ci given in Section 3. Similarly let ψ be a translation from λC n
to λS n . It suffices to prove the following properties with M and M 0 being termsin λS n , and N and N 0 being terms in λC n :1. λβη ` [ φ(M )]] = [ M ] .
2. λC n ` N = N 0 implies λS n ` ψ(N ) = ψ(N 0 ).
3. λS n ` ψ(φ(M )) = M
All these properties can be proved by calculation.
12

6.4

Typing Source Calculi

So far we have been studying the simplest possible source calculi. Introducing
type structure into the source calculi is an important problem, as most modern
programming languages have a built-in type system. Another benefit of introducing types is that, in the presence of appropriate types, we can avoid the fullηv -equality (λx.V x = V for x 6∈ F V (V )), which is inconsistent with the presence of basic values such as natural numbers. In order to restrict V in ηv to afunctional value, we need a type system in the source calculus.
A simple choice of the typing rules of control operators would be:Γ `M :ΦΓ ` hM ii : ΦΓ ` Si : ((A → Φ) → Φ) → A

where Φ is a designated atomic type, and A is an arbitrary type. Then we canprove that the extended CPS translation preserves the typability if we add thetype information to the classes Term0 and Value in the target calculus (in whichcase, the type structure of the target calculus does not need recursive types).
All the axioms and the proof of soundness and completeness in this article go
through for the simply typed case.
Introduction of types to the source calculi makes explicit the connection of
the extended CPS translation and the double negation translation. If we taken = 1, then by the definition of types given in Section 6.1 we have Term0 =(Value → Ans) → Ans. If we take n = 2, thenTerm0 = (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 doublenegation translation.
In the literature, Danvy and Filinski [6] and Murthy [21] have proposed more
liberal type systems for shift and reset. Since these type systems are quite
complicated, it is not obvious whether our axioms work for them.

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 a simple set of axioms which issound and complete for all such control operators. To our knowledge this workis the first such result about the hierarchy of delimited continuation operators.
Our axioms for level-n shift/reset are a simple extension of those for level-1
shift/reset, and the axioms for level-n C/reset are even simpler than thosefor level-2 C/reset.
The control operators in the CPS hierarchy have also been investigated by
Murthy [21], who gave an elaborate type system for level-n shift and reset, andalso gave a set of axioms for them. The difference between his work and ours is13

that he only proved the soundness of the axioms and did not state completeness,
and also that his set of axioms consists of many complex axioms such as thetelescope axiom, while ours consists of a small number of simple axioms.
In another line of work, Danvy and Yang [9], Murthy [21], and Biernacka,
Biernacki and Danvy [3] studied an operational aspect of the control operatorsin the CPS hierarchy by giving abstract machines for shift and reset. It seems
interesting to study how our axioms fit with these abstract machines.
Future Work: Besides studying the connection to abstract machines, there
are two major avenues for future work:(1) While we have built a theoretical foundation for the control operatorsin the CPS hierarchy there remains a question about the application of our axioms. It is almost impossible to use them for automatic verification because theyrequire a degree of insight. Nevertheless, besides obtaining a better understanding of control operators, we hope to use the axioms to prove the correctness ofprogram translations such as compiler optimization.
(2) An even more fundamental question of this study is whether one needs
these hierarchical control operators at all. The existence of several application
programs and the correspondence between the CPS hierarchy and layered monads [11] seem to give a positive answer to this question. However, there is muchroom for further work.
Acknowledgments: The author would like to thank Olivier Danvy, Masahito
Hasegawa, Amr Sabry and Kenichi Asai for constructive comments and discussions. He also thanks anonymous referees for many insightful comments andcriticisms. This work was supported in part by Grant-in-Aid for Scientific Research No. 16500004 from Japan Society for the Promotion of Science.

References
1. K. Asai. Online Partial Evaluation for Shift and Reset. In Proc. ACM Workshop
on Partial Evaluation and Semantics-Based Program Manipulation, pages 19–30,
2002.
2. K. Asai. Offline Partial Evaluation for Shift and Reset. In Proc. ACM Workshop
on Partial Evaluation and Semantics-Based Program Manipulation, to appear.
3. M. Biernacka, D. Biernacki, and O. Danvy. 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, pages 25–34, 2004.
4. O. Danvy. Type-directed partial evaluation. In Proc. 23rd Symposium on Principles
of Programming Languages, pages 242–257, 1996.
5. O. Danvy. On evaluation contexts, continuations, and the rest of the computation.
In Proc. Fourth ACM SIGPLAN Workshop on Continuations, Technical Report
CSR-04-1, School of Computer Science, University of Birmingham, pages 13–23,
2004.
6. O. Danvy and A. Filinski. A functional abstraction of typed contexts. Technical
Report 89/12, DIKU, University of Copenhagen, 1989.
7. O. Danvy and A. Filinski. Abstracting Control. In Proc. 1990 ACM Conferenceon Lisp and Functional Programming, pages 151–160, 1990.

14

8. O. Danvy and A. Filinski. Representing Control: a Study of the CPS Transformation. Mathematical Structures in Computer Science, 2(4):361–391, 1992.
9. O. Danvy and Z. Yang. An Operational Investigation of the CPS Hierarchy. In
Proc. 8th European Symposium on Programming, Lecture Notes in Computer Science 1576, pages 224–242, 1999.
10. M. Felleisen. The Theory and Practice of First-Class Prompts. In Proc. 15th
Symposium on Principles of Programming Languages, pages 180–190, 1988.
11. A. Filinski. Representing Layered Monads. In Proc. 26th Symposium on Principles
of Programming Languages, pages 175–188, 1999.
12. H. Friedman. Classically and intuitionistically provably recursive functions. Lecture Notes in Mathematics 699, pages 21–28, 1978.
13. T. Griffin. A Formulae-as-Types Notion of Control. In Proc. 17th Symposium on
Principles of Programming Languages, pages 47–58, 1990.
14. C. A. Gunter, D. Rémy, and J. G. Riecke. A Generalization of Exceptions andControl in ML-Like Languages. In Proc. Functional Programming and Computer
Architecture, pages 12–23, 1995.
15. R. Hieb, R. Dybvig, and C. W. Anderson. Subcontinuations. Lisp and Symbolic
Computation, 6:453–484, 1993.
16. Y. Kameyama. A Type-Theoretic Study on Partial Continuations. In Proc. IFIP
International Conference on Theoretical Computer Science, Lecture Notes in Computer Science 1872, pages 489–504, 2000.
17. Y. Kameyama. Axiomatizing higher level delimited continuations. In Proc. 3rd
ACM SIGPLAN Workshop on Continuations, Technical Report 545, Computer
Science Department, Indiana University, pages 49–53, 2004.
18. Y. Kameyama and M. Hasegawa. A Sound and Complete Axiomatization of Delimited Continuations. In Proc. ACM International Conference on Functional Programming, pages 177–188, 2003.
19. J. Lawall and O. Danvy. Continuation-based partial evaluation. In Proc. 1994
ACM Conference on LISP and Functional Programming, pages 227–238, 1994.
20. E. Moggi. Computational Lambda-Calculus and Monads. In Proc. 4th Symposiumon Logic in Computer Science, pages 14–28, 1989.
21. C. Murthy. Control operators, hierarchies, and pseudo-classical type systems: Atranslation at work. In Proc. First ACM Workshop on Continuations, Technical
Report STAN-CS-92-1426, Stanford University, pages 49–72, 1992.
22. A. Sabry. Note on Axiomatizing the Semantics of Control Operators. Technical
Report CIS-TR-96-03, Dept. of Computer Science, University of Oregon, 1996.
23. A. Sabry and M. Felleisen. Reasoning about Programs in Continuation-Passing
Style. Lisp and Symbolic Computation, 6(3-4):289–360, 1993.
24. T. Sekiguchi, T. Sakamoto, and A. Yonezawa. Portable Implementation of Continuation Operators in Imperative Languages by Exception Handling. In Advances in
Exception Handling Techniques, Lecture Notes in Computer Science 2022, pages
217–233, 2001.
25. H. Thielecke. Answer type polymorphism in call-by-name continuation passing.
In Proc. 13th European Symposium on Programming, Lecture Notes in Computer
Science 2986, pages 279–293, 2004.

15