A Call-by-Name CPS Hierarchy
Asami Tanaka and Yukiyoshi Kameyama
University of Tsukuba, Japan
asami@logic.cs.tsukuba.ac.jp,kameyama@acm.org

Abstract. The Continuation-Passing-Style (CPS) translation gives semantics to control operators such as exception and first-class continuations. By iterating this translation, Danvy and Filinski obtained a CPS
hierarchy, and used it to specify a series of control operators, hierarchical(or layered) delimited-control operators,
We introduce a call-by-name variant of the CPS hierarchy. While most of
the work on delimited-control operators is based on call-by-value calculi,
call-by-name delimited-control operators are an active target of recent
studies. Our strategy for developing such a hierarchy is to use the results
for the call-by-value calculi as much as possible. The key tool is Hatcliff
and Danvy’s factorization of Plotkin’s call-by-name CPS translation intoa thunk translation and a call-by-value CPS translation. We show thata call-by-name CPS hierarchy can be obtained by naturally extending
the factorization to the calculi with control operators, and then proveseveral properties for this hierarchy.

1

Introduction

Translating terms into Continuation Passing Style (CPS) is a key to define
and understand control operators such as first-class continuations (Scheme’scall/cc). By iterating the CPS translation, Danvy and Filinski [5] have obtained a hierarchy for CPS translations, and found a series of control operators
indexed by natural numbers. Among the series, the first one corresponds to thedelimited-control operators shift and reset, which allows to capture a delimited continuation, part of the rest of computation. In the last two decades, thesecontrol operators have found many applications such as partial evaluation [14],CPS translations [5], mobile computing [20], and dependently typed programming such as type-safe printf [1].
The second and the rest of the series correspond to the higher-level versionsof shift and reset, similar to layered monads [6], and are useful when we
combine two or more computational effects in a single program [4]. Although the
hierarchical (layered) control operators are less expressive than the arbitrarily
nested control operators [13], the former can express many interesting programs,
and also the existence of the purely functional CPS transform for the former isbeneficial for studying its semantics and foundational issues.
While the above mentioned work has been done for call-by-value calculi,
several authors have recently studied delimited-control operators in the callby-name calculi. Herbelin and Ghilezan [8] and Saurin [19] studied variants of

Parigot’s λµ-calculus and interpreted their computational meaning by call-byname delimited-control operators. Kiselyov [12] proposed a call-by-name calculus
with delimited-control operators and used it in linguistic analysis. Biernacka andBiernacki [3] studied both call-by-value and call-by-name calculi for delimitedcontrol operators in a uniform way. In our previous work [11], we gave a complete
equational axiomatization for the call-by-name calculi with delimited-control
operators.
In this paper, we introduce the call-by-name variant of the CPS hierarchy,
in which we can find a series of delimited-control operators. The key tool we use
is Hatcliff and Danvy’s factorization of a CPS translation [7], which connects
Plotkin’s call-by-name and call-by-value CPS translations by a thunk translation. They have shown that all Plotkin’s criteria for correctness can be established for the thunk translation. We use their methodology in a slightly different
way: rather than defining the call-by-name CPS hierarchy independently fromthe call-by-value one and connect the two by the thunk translation, we use thethunk translation to define, or derive, the call-by-name CPS hierarchy from thecall-by-value one. The effectiveness of our method is supported by the fact that
Biernacka and Biernacki’s call-by-name calculus for shift and reset [3] can beobtained by simply taking the first level of our hierarchy. Note that the thunktranslation is much less complicated than the CPS translation for delimitedcontrol operators, and we can obtain the CPS hierarchy rather smoothly.
The contribution of this paper is summarized as follows: (1) we extend Hatcliff and Danvy’s thunk translation to the calculi with delimited-control operators, (2) we introduce a typed call-by-name CPS hierarchy, and (3) we obtainseveral properties of the hierarchy by the connection made by the thunk translation.
The rest of this paper is organized as follows. Section 2 gives informal explanation for the background of this work. Section 3 formally introduces thecall-by-name calculus in a CPS hierarchy and a thunk translation. In Section
4, we derive a type system for our calculus and prove basic properties. Section
5 gives an equational theory for our calculus. Section 6 compares our work toothers and state concluding remarks.

2

Preliminaries

2.1

Delimited-Control Operators and a CPS Hierarchy

Explicit manipulation of continuations allows various programming styles. Unlike
the standard (unlimited) continuation, a delimited continuation represents partof the rest of computation, and delimited-control operators provide an access todelimited continuations.
IIWe informally explain delimited control-operators in a call-by-value calculus
using the following examples:
h10 + Sk.(k ←- (k ←- 5))i∗hh10 + h10 + 5iii

h20 + h10 + S1 k.(k ←-1 (k ←-1 5))i1 i225h20 + hh10 + h10 + 5i1 i1 i1 i2

h20 + h10 + S2 k.(k ←-2 (k ←-2 5))i1 i2∗45hh20 + h10 + h20 + h10 + 5i1 i2 i1 i2 i2∗

h20 + h10 + S1 k.(k ←-1 (k ←-1 5))i2 i1

65

h20 + hh10 + h10 + 5i1 i1 i2 i1

∗

45

∗

In these examples,
denotes a one-step reduction, anddenotes a manystep reduction. Sk.e is a shift-term and hei is a reset-term. The shift-term
captures the evaluation context up to the nearest reset, namely, a continuationdelimited by a reset. In the first example, the (delimited) continuation is h10 +[ ]i, which is bound to k. The captured continuation is used in the subtermk ←- e. Note that shift eliminates the current delimited continuation, and thatthe throw-term is not abortive, unlike the continuation captured by the call/cc
primitive in Scheme. After the first step, there remains no shift, and, therefore,
the occurrences of reset are ignored.
We cannot mix two or more uses of shift and reset in one program if they
do not have names to distinguish one from the other. To avoid unwanted interference between different uses of control operators, we attach natural numbers toeach control operator as their indices. As the second and third examples show,
shift chooses the nearest reset as the one with the same index as shift.
The above explanation is not completely precise: the index is not merely aname. Rather, they are linearly ordered (hence a natural number is used). In
the fourth example, shift indexed by 1 chooses the nearest reset as the one
indexed by 2, rather than the one by 1. In general, a higher-level reset delimits
the continuation captured by a lower-level shift. Put differently, a lower-level
shift cannot escape from a higher-level reset, thus control operators are layered
or hierarchical.
2.2

The Thunk Translation

The thunk translation introduces a “thunk” (a lambda closure) to freeze a computation, and can be regarded as a translation from a call-by-name calculus toa call-by-value calculus. Hatcliff and Danvy [7] showed that Plotkin’s call-byname CPS translation can be factored into the thunk translation and Plotkin’s
call-by-value CPS translation, and that all Plotkin’s correctness criteria [16] canbe derived using this factorization. In this subsection, we briefly review theirresults to the extent that is necessary for this paper.
Fig. 1 gives the source and target calculi where c is a constant and v is a value
in call-by-value. Λ denotes the set of terms defined in this figure. The reductions(β) and (βv ), resp., are the call-by-name and call-by-value β-reductions, resp.
Bound and free variables are defined in the standard way, and we identify αequivalent terms. The term e1 {x := e2 } denotes the result of capture-avoiding
substitution.
III(term in Λ)e ::= c | x | λx.e | ee(term in Λfd )e ::= · · · | force(e) | delay(e)(cbn-value)v ::= c | λx.e

(cbv-value)v ::= c | x | λx.e

(β)(λx.e1 )e2

e1 {x := e2 }(βv )(λx.e1 )v

e1 {x := v}(fd)

force(delay(e))

eFig. 1. Syntax and Reduction Rules of the Basic Calculusdef

T [ λx.e]] = λx.T [ e]]defT [ e1 e2 ] = T [ e1 ] (delay(T [ e2 ] ))T [ c]] = c
T [ x]] = force(x)

def

def

Fig. 2. Thunk Translation

The thunk translation gives a simulation of the call-by-name calculus in thecall-by-value calculus in terms of the following two functions: (1) delay for creating a suspended computation as a value (thunk), and (2) force for re-invoking
the suspended computation. For a term e, the term delay(e) is a value, andforce(delay(e)) reduces to e. Although we can express delay(e) by λx.e, andforce(e) by ex, for a fresh variable x, it is convenient to distinguish thunks fromthe ordinary lambda abstractions. Λfd denotes the set of terms with delay andforce.
The thunk translation is a syntactic translation from Λ to Λfd defined inFig. 2. It is easy to see that a one-step β-reduction in the source calculus one-toone corresponds, by the thunk translation, to a one-step β-reduction in the target
calculus modulo the (fd) reduction. Also, since all the arguments of functions inΛfd are values, the reductions (β) and (βv ) coincide on Λfd .
Theorem 1 (Simulation [Hatcliff and Danvy]). Let e1 and e2 be terms in
Λ. We have that e1 reduces to e2 by the (β) reduction if and only if T [ e1 ] reduces
to T [ e2 ] by the (βv ) reduction followed by the (fd) reductions. Moreover, (βv )may be replaced by (β) in the above sentence.
We consider equality over terms induced by a set of reduction rules r1 , · · · , rn ,which is defined as the least congruence relation that subsumes r1 , · · · , rn . We
write (r1 , · · · , rn ) ` e1 = e2 if e1 = e2 holds under the equality induced by
r1 , · · · , rn . For instance, (β) ` e1 = e2 means that e1 and e2 are equal under βequality.
Fig. 3 defines the call-by-value and call-by-name CPS transformations due
to Plotkin [16], where the variables κ, m, and m0 are fresh.
IVC n [ c]] = λκ.κcdef

C v [ c]] = λκ.κc

def

def

C v [ x]] = λκ.κxdef

C n [ x]] = λκ.xκ
def

C v [ λx.e]] = λκ.κ(λx.C v [ e]])

def

def

C v [ e1 e2 ] = λκ.C v [ e1 ] (λm.C v [ e2 ] (λm0 .mm0 κ))

C n [ λx.e]] = λκ.κ(λx.C n [ e]])def

C n [ e1 e2 ] = λκ.C n [ e1 ] (λm.mC n [ e2 ] κ)def

C v [ force(e)]] = λκ.C v [ e]](λm.mκ)def

C v [ delay(e)]] = λκ.κC v [ e]]Fig. 3. Call-by-Name (left) and Call-by-Value (right) CPS Translations

The CPS translations in Fig. 3 are standard except the cases for delay
and force. The terms force(e) and delay(e) are intuitively understood as e x
and λx.e for a fresh variable x. Then C v [ force(e)]] is understood as C v [ ex]] =λκ.C v [ e]](λm.C v [ x]](λn.m n k)), which reduces to λκ.C v [ e]](λm.m x k)). We also
understand C v [ delay(e)]] as C v [ λx.e]], which reduces to λκ.κ(λx.C v [ e]]). Since x
is useless, we omit it in both terms, and obtain the translation in Fig. 3.
Hatcliff and Danvy proved the following key theorem.
Theorem 2 (Factorization [Hatcliff and Danvy]). For any term e in Λ,
we have (β) ` C n [ e]] = C v [ T [ e]]] .
Note that η-equality (and η-reduction) is not preserved by the thunk translation: we have T [ λx. y x]] = λx.force(y) (delay(force(x))) and T [ y]] = force(y).
In order to equate these terms, we need delay(force(x)) = x and λx.force(y)x =force(y), and the latter subsumes full η-equality, but it is not admissible in thetarget of the thunk translation (a call-by-value calculus).

3

The Calculi: Syntax and Reduction Rules

We introduce the calculi λns/r for a call-by-name CPS hierarchy where n is anatural number which denotes an upper bound of indices (or levels). In otherwords, the indices of shift and reset must be equal to or less than n. We fix
this n throughout this paper.
We assume that there are two disjoint sets of variables, one for ordinary
variables (ranged over by x, y, z, · · · ) and the other for continuation variables(ranged over by k). An ordinary variable is bound by lambda, and a term may
be substituted for it, while a continuation variable is bound by shift, and adelimited continuation may be substituted for it. We also assume that eachcontinuation variable k is (implicitly) annotated by a level i (for 1 ≤ i ≤ n), andthat Si k.e and k ←-i e are terms only when the (implicit) level of k is i.
Fig. 4 defines the syntax of the calculi with delimited-control operators wherec is a basic constant. The term Si k.e is a shift-term of level i, in which k isV(Λsr )

e ::= c | x | λx.e | ee | Si k.e | heii | k ←-i e(Λsr,fd )e ::= · · · | force(e) | delay(e)where 1 ≤ i ≤ nFig. 4. Terms with Delimited-Control Operators(cbv-value)v ::= c | x | λx.e | delay(e)(cbv-context)

E i ::= [ ] | E i e | vE i | force(E i ) | hE i ih(βv )(λx.e)v(fd)

force(delay(e))(rvv )

hvii(rsv )

hE i [Si k.e]ij

where h < ie{x := v}ev
he{k ⇐i hE i ii }ij

where i ≤ j

Fig. 5. Call-by-Value Reductions

bound. The term heii is a reset-term of level i. The term k ←-i e is a throwterm of level i which applies k to the term e. Note that the continuation variable
k is free in k ←-i e.
Following Biernacka and Biernacki [3], we explicitly distinguish lambdabound (ordinary) variables from shift-bound (continuation) variables. Thisdistinction is important to get simpler definitions, and is necessary to give anaxiomatization for call-by-name calculus [11].
We identify α-equivalent terms. FV(e) and FCV(e), resp., denote the set offree ordinary variables and the set of free continuation variables, resp., in e, ande1 {x := e2 } represents the result of capture-avoiding substitution of e2 for x ine1 . E i is an evaluation context which does not have a level-i or higher reset
enclosing the hole E 1 is a pure evaluation context, or a delimited continuation,
which does not have reset around the hole. We write E instead of E i if theindex does not matter. E[e] denotes the term after the hole-filling operation ofa term e for a hole in E. Hole-filling of an evaluation context E1 [E2 ] is definedsimilarly.
Fig. 5 gives the reduction rules for the call-by-value calculi, which are essentially due to Biernacka and Biernacki [3] with the following difference. While
their calculus reifies an evaluation context E i , and substitute it for a continuation variable k (thus k ←-i e becomes E i ←-i e0 ), our calculus uses structural
substitution {k ⇐i E i } defined in Fig. 6.
The thunk translation is naturally extended to this calculus as in Fig. 7.
Fig. 8 defines the reduction rules of the call-by-name calculus. The reduction (β) is standard. The reduction (rvn ) (meaning “reset-value”) eliminates areset if its body is a value. The only interesting reduction is (rsn ) (meaning“reset-shift”) for a level-i shift-term. By this reduction, shift captures a leveli (delimited) evaluation context E i , and substitutes it for k. The corresponding
VI

def

c{k ⇐i E} = cdefx{k ⇐i E} = xdef(λx.e){k ⇐i E} = λx.(e{k ⇐i E})

where x 6∈ FV(E)def(e1 e2 ){k ⇐i E} = (e1 {k ⇐i E}) (e2 {k ⇐i E})
def(Sp k0 .e){k ⇐i E} = Sp k0 .(e{k ⇐i E})

where k0 6∈ {k} ∪ FCV(E)def(k ←-i e){k ⇐i E} = E[e{k ⇐i E}]
def(k0 ←-p e){k ⇐i E} = k0 ←-p (e{k ⇐i E})

where k0 6= k

defheip {k ⇐i E} = he{k ⇐i E}ip
Fig. 6. Substitution for Continuation Variablesdef

T [ heii ] = hT [ e]]ii

def

def

T [ k ←-i e]] = k ←-i T [ e]]T [ e]] = · · · for e = c, x, λx.e, e1 e2

def

T [ Si k.e]] = Si k.T [ e]]Fig. 7. Thunk Translation

reset for this shift is the nearest one which has the level i or higher, because
E i does not have such a reset that encloses the hole.
The reduction rules in both calculi are extended to arbitrary contexts ase1
e2 implies C[e1 ]C[e2 ] for any context C. We write (r1 , · · · , ri ) ` e1
e2
if e1 reduces to e2 by these reductions. We also write ∗ for zero or more step
reductions.
We can show that the notions of the reductions in call-by-name/call-by-value
calculi correspond to each other via the thunk translation.
Theorem 3 (Simulation). Let e1 and e2 be terms in Λsr . Then we have(β, rvn , rsn ) ` e1 ∗ e2 if and only if (β, fd, rvv , rsv ) ` T [ e1 ] ∗ T [ e2 ] .
Proof. From call-by-name to call-by-value, the proof is straightforward.
For the inverse direction, we only have to consider the image of the thunktranslation, namely, for any application e1 e2 , the term e2 has the form delay(e3 ),which is a value. Then it is not difficult to prove the inverse direction.

4

Type System

The thunk translation is not only useful to investigate the operational aspect,
but can be also used to design a type system. As a concrete instance, we designa type system for the call-by-name calculus with delimited-control operatorsfrom the one for the call-by-value calculus. In this process, we do not have toVII(cbn-value)v ::= c | λx.e

(cbn-context)

E i ::= [ ] | E i e | hE i ih(β)(λx.e1 )e2(rvn )

hvii(rsn )

hE i [Si k.e]ij

where h < ie1 {x := e2 }vhe{k ⇐i hE i ii }ij

where i ≤ j

Fig. 8. Call-by-Name Reductions

consult with the CPS translation. Although the hierarchical control operators arecomplicated, and in particular, a CPS translation for them is hard to understand,we can give the type system quite smoothly thanks to Hatcliff and Danvy’s
factorization.
Biernacka and Biernacki [3] proposed a call-by-name typed calculus with thelevel-1 shift and reset. While they developed the calculus and its properties
independently from the call-by-value counterpart, they can be derived from thecall-by-value counterpart using the thunk translation. In this section, we showthat it is possible for the calculus of an arbitrarily higher level.
4.1

Type System for Call-by-Value CPS Hierarchy

We review a monomorphic type system for the call-by-value calculus with hierarchical delimited-control operators.
Murthy [15] was the first to give a type system for this calculus, which wasderived from the CPS translation. The basic idea of his type system is that thetyping judgment of a term e should carry the same information as its CPS image
C v [ e]]. For instance, if n = 1, namely, we have only one level, the CPS image ofa term takes the form λκ1 .λκ2 .· · ·, which suggests the type of the CPS image is(σ → (τ → ∗) → ∗) → (ρ → ∗) → ∗. Here we assume that the images of the
CPS translation are in (strictly) continuation-passing style, so the (final) answer
type is polymorphic [21, 22], and we write it as an anonymous type ∗. In thisCPS type, σ is the type corresponding to the source term, τ and ρ are so calledanswer types of level 1. Murthy further assumed that, the answer types do notchange, which means that τ and ρ in the above type must be the same. This
assumption greatly simplifies the type system, and we only need n answer types
for any term if the maximum level is n.
Answer types may be regarded as computational effects, and therefore weneed to modify a function type σ → τ to an effectful function type Funcbv [σ →τ /α], whose inhabitants are functions from σ to τ that works under the answer
types α. Here α is a sequence of types α1 , α2 , · · · , αn .
Let us formally define the type system. The syntax of types is given by:(type) σ, τ, α ::= b | Susp[σ/α] | Funcbv [σ → τ /α]
VIII

cbv

Γ, x : σ `

var

x:σ|α

(c is a constant of basic type b)constΓ `cbv c : b | α

Γ, x : σ `cbv e : τ | αΓ `cbv λx.e : Funcbv [σ → τ /α] | βfunΓ `cbv e1 : σ | αΓ `cbv e0 : Funcbv [σ → τ /α] | αΓ `cbv e0 e1 : τ | αΓ `cbv e : σ | σ, · · · , σ, αi+1 , · · · , αn
Γ `cbv heii : σ | α

app

reset

Γ, k : Funcbv [σ → τ /α] `cbv e : τ | τ, · · · , τ, αi+1 , · · · , αn
Γ `cbv Si k.e : σ | β1 , · · · , βi−1 , τ, αi+1 , · · · , αnshiftΓ, k : Funcbv [τ → σ/σ, · · · , σ, αi+1 , · · · , αn ] `cbv e : τ | σ, · · · , σ, αi+1 , · · · , αn
Γ `cbv k ←-i e : σ | αΓ `cbv e : Susp[σ/α] | αΓ `cbv force(e) : σ | αforceΓ `cbv e : σ | αΓ `cbv delay(e) : Susp[σ/α] | β

throw

delay

Fig. 9. Type System for the Call-by-Value Calculus (First Version)

where b is a metavariable for basic types such as integer and boolean. The type
Susp[σ/α] is the one for suspended computation generated by delay. The typeFuncbv [σ → τ /α] is an effectful function type. A typing context Γ is a (possibly
empty) sequence consisting of the form x : τ for a lambda-bound variable x, ork : Funcbv [σ → τ /α] for a continuation variable k. A judgment takes the form
Γ `cbv e : τ | α where Γ is a typing context, τ is a type, α is a sequence of types,
and e is a term. The length of the sequence α must be n.
Fig. 9 gives the type system for the call-by-value calculus.
The types for a variable, a constant, lambda, and application are standard if
we take into account the answer types. The typing rule for reset means that, fora level-i reset, the answer type of the body e must be the same as the type of e
itself. This reflects the hierarchical nature of this calculus: as a lower-level shiftcannot escape from a higher-level reset, whenever there is a level-i reset, theanswer types of lower levels must be identical. After the level-i reset, the answer
types of these levels can be arbitrary types, so the types α1 , · · · , αi can be chosen
arbitrarily in the typing judgment of heii . The typing rule for the shift-term
can be understood by noting the facts that Si k.e has the same denotation as
Si k.heii , and a level-i shift-term captures a delimited continuation whose typeis roughly a function from some type to the level-i answer type. As for the typing
rule for throw, it is instructive to know k ←-i e may be represented by hk eii if weforget the distinction between lambda-bound and shift-bound variables. The
typing rules for force and delay can be understood by the following intuition:
force(e) is ex and delay(e) is λx.e for a fresh variable x.
IXΓ, k : Conti [σ → τ /αi+1 , · · · , αn ] `cbv e : τ | τ, · · · , τ, αi+1 , · · · , αn
Γ `cbv Si k.e : σ | β1 , · · · , βi−1 , τ, αi+1 , · · · , αnΓ, k : Conti [τ → σ/αi+1 , · · · , αn ] `cbv e : τ | σ, · · · , σ, αi+1 , · · · , αn
Γ `cbv k ←-i e : σ | α

shift
throw

Other typing rules are the same as Fig. 9.
Fig. 10. Type System for the Call-by-Value Calculus (Second Version)

4.2

Refining the Type System

We can refine the type system to the one in Fig. 10 where a continuation variablek has a distinguished continuation type Conti [σ → τ /αi+1 , · · · , αn ] (for 1 ≤ i ≤n), and σ, τ, αi+1 , · · · , αn are types.
The continuation variable is treated differently from the ordinary functions,and also its type does not have the information of answer types of level ≤ i,which means that it is polymorphic over these answer types. The answer type
polymorphism of continuations have been studied by several authors [21, 2, 3] forthe level-1 (single level) delimited-control operators, and here we use it in higher
levels.
Theorem 4 (Type Soundness). (1) If Γ `cbv e1 : τ | α is derivable, ande1 ∗ e2 , then Γ `cbv e2 : τ | α is derivable.
(2) If `cbv he1 in : τ | α is derivable, then there exists a term e2 such that
he1 ine2 . Moreover, if e2 is not a value, it must be he02 in for some term e02 .
The second part (progress) takes an unusual form since the term he1 in has
an outermost reset of the maximum level n. Having such a reset is necessary,
since a term with “free shift” (such as S1 k.e) can be a closed and typable term,
but it is not a value.
The first part of this theorem is essentially due to Murthy [15], and the proofof the second part is standard.
4.3

Type System for Call-by-Name CPS Hierarchy

We now derive a type system for the call-by-name calculus from the one forcall-by-value calculus. Our design principle is to have the property: a term e istypable in the former if and only if its translation T [ e]] is typable in the latter.
First, we consider the case T [ x]] = force(x) which can be typed (and is only
typed) in the call-by-value calculus as:
Γ, x : Susp[σ/α] `cbv x : Susp[σ/α] | αΓ, x : Susp[σ/α] `cbv force(x) : σ | αHence, in the call-by-name calculus we should have the following typing rule:Γ, x : Susp[σ/α] `cbn x : σ | αXΓ, x : (σ | α) `cbn x : σ | αvarΓ, (x : σ | α) `cbn e : τ | β
Γ `

cbn

λx.e : Funcbn [(σ/α) → (τ /β)] | γΓ `cbn e0 : Funcbn [(σ/α) → (τ /β)] | βfunΓ `cbn e1 : σ | αΓ `cbn e0 e1 : τ | βapp

The typing rules for const, shift, reset and throw are the same as those in Fig. 10.
Fig. 11. Type System for Call-by-Name Calculus

For notational reasons, we will write (σ | α) for Susp[σ/α] in typing contexts.
The change in the type of a variable affects the function type: the call-byvalue type Funcbv [Susp[σ/α] → τ /β] will be written as the call-by-name typeFuncbn [(σ/α) → (τ /β)], and the typing rule for (fun) is changed accordingly.
For the case T [ e0 e1 ] = T [ e0 ] (delay(T [ e1 ] )), we have:Γ `cbv T [ e1 ] : ρ | βΓ `cbv T [ e0 ] : Funcbv [σ → τ /α] | αΓ `cbv delay(T [ e1 ] ) : σ | αΓ `cbv T [ e0 ] (delay(T [ e1 ] )) : τ | α
where σ = Susp[ρ/β]. Hence we should have the following rule:Γ `cbn e0 : Funcbv [Susp[ρ/β] → τ /α] | αΓ `cbn e1 : ρ | βΓ `cbn e0 e1 : τ | α
These changes are all what we need to do for the call-by-name type system. In
particular, since the thunk translation is homomorphic for control operators, noessential changes are necessary in the typing rules for them.
To summarize, the types are defined by:(type) σ, τ, α, β ::= b | Funcbn [(σ/α) → (τ /β)](cont-type) φ ::= Conti [σ → τ /αi+1 , · · · , αn ]A typing context Γ is a finite sequence of the form x : (σ | α) or k : Conti [σ →τ /αi+1 , · · · , αn ]. A judgment in this type system takes the form of Γ `cbn e : σ |α, and the call-by-name type system is given in Fig. 11.
Typability is preserved by the thunk translation. To state this property formally, we define the thunk-translation for types, typing contexts, and judgment
as follows (the following definitions extend to sequences naturally):def

T [ b]] = b
def

T [ Funcbn [(σ/α) → (τ /β)]]] = Funcbv [Susp[T [ σ]]/T [ α]]] → T [ τ ] /T [ β]]]def

T [ x : (σ | α)]] = x : Susp[T [ σ]]/T [ α]]]def

T [ k : Conti [σ → τ /αi+1 , · · · , αn ]]] = k : Conti [T [ σ]] → T [ τ ] /T [ αi+1 , · · · , αn ] ]XIThen we can prove the following theorem easily.
Theorem 5 (Thunk Translation Preserves Typability). We have thatΓ `cbn e : τ | α is derivable if and only if T [ Γ ] `cbv T [ e]] : T [ τ ] | T [ α]] isderivable.
Combining the above theorem with the property of the call-by-value CPS
translation, we obtain that the call-by-name CPS translation preserves typability.
Subject reduction property can be also derived easily.
Theorem 6 (Subject Reduction). If Γ `cbn e1 : τ | α is derivable, ande1 ∗ e2 , then Γ `cbn e2 : τ | α is derivable.
Proof. Suppose Γ `cbn e1 : τ | α is derivable, and e1 ∗ e2 in the call-by-namecalculus. By Theorem 3, we have T [ e1 ] ∗ T [ e2 ] . By the subject property of thecall-by-value calculus and Theorem 5, we have T [ Γ ] `cbv T [ e2 ] : T [ τ ] | T [ α]].
Again by Theorem 5, we have Γ `cbn e2 : τ | α.
We also have the progress property for the call-by-name calculus.
Theorem 7 (Progress). If `cbn he1 in : τ | α is derivable, there exists a term
e2 such that he1 in
e2 . Moreover, if e2 is not a value, it must be he02 in for0
some term e2 .
Proofs of these theorems are straightforward and omitted.
We have derived a type system for the call-by-name CPS hierarchy. Note
that, by taking n = 1, we can reproduce Biernacka and Biernacki’s call-by-nametype system [3] modulo notational difference. A merit of our approach is that
we do not have to directly consult the iterated CPS translation.

5

Equational Theory

This section studies an equational theory for the call-by-name CPS hierarchy inthe typed setting. Sabry and Felleisen [17] first established equational axiomatization of the calculus with control operators for first-class (unlimited) continuations. Regarding delimited-control operators, Kameyama and Hasegawa [10]and Kameyama [9], resp., axiomatized level-1 and higher-level, resp, shift andreset in the call-by-value calculi. For reference, Fig. 13 in the appendix lists thelatter axiomatization.
We obtain an equational theory for the call-by-name calculus in the same
spirit as the previous sections: we formulate them as a back image of the thunktranslation and the call-by-value counterpart. The result is given in Fig. 12.
The call-by-name axioms (Fig. 12) and the call-by-value axioms (Fig. 13)
have several differences. It should also be noted that, even if the axioms rsv andrsn have the same form, they have different meaning as the definitions of theevaluation contexts differ from each other.
XII(λx.e1 ) e2 = e1 {x := e2 }
i

(β)

i

hE [Si k.e]ij = he{k ⇐ hE ii }ij where i ≤ j
0

0

i

i

k ←-j (E [Si k.e]) = he{k ⇐ (k ←-j E )}ij where i ≤ j and k 6= k(rsn )
0hvii = v
Si k.(k ←-i heii−1 ) = heii−1(ts)(rvn )

where k 6∈ FCV(e)Si k.heii = Si k.e

(se)
(sr)

Fig. 12. Equational Theory for the Call-by-Name Calculus

We write `cbn e1 = e2 if the equation is derivable using the equations in
Fig. 12. Similarly we write `cbv e1 = e2 for the equations in Fig. 13. It is easy
to prove that the reduction semantics is subsumed by these our equations.
Theorem 8. If (β, rvn , rsn ) ` e1∗e2 , then `cbn e1 = e2 is derivable.

We can also prove that the call-by-name equations are sound with respect tothe thunk translation, and hence the call-by-name CPS translation.
Theorem 9 (Soundness). If `cbn e1 = e2 , then `cbv T [ e1 ] = T [ e2 ] .
This theorem can be proved by simple calculations for each equation. It
immediately implies soundness of call-by-name equations with respect to thecall-by-name CPS translation in the appendix.
Corollary 1. If `cbn e1 = e2 , then (β, η) ` C n [ e1 ] = C n [ e2 ] .
Finally, an interesting question is whether the equations are complete withrespect to the thunk translation. Unfortunately, we have not succeeded in directly
proving completeness using the thunk translation, since we cannot define theinverse of the thunk translation which preserves equality1 . However, we can use
our previous results [11] to connect the call-by-name and call-by-value theories
for the first level:
Theorem 10 (Correspondence in the First Level). Suppose the maximum
level n is 1, and e1 , e2 ∈ Λsr . Then we have `cbn e1 = e2 if and only if `cbv
T [ e1 ] = T [ e2 ] .
Proof. Theorem 9 states soundness (the only-if direction). For completeness (theif direction), suppose `cbv T [ e1 ] = T [ e2 ] . By the soundness of the call-byvalue equational theory, we have (β, η) ` C v [ T [ e1 ] ] = C v [ T [ e2 ] ] , and hence(β, η) ` C n [ e1 ] = C n [ e2 ] . By the completeness of the call-by-name equations forthe first-level [11], we have `cbn e1 = e2 .
1Note that ηv is admissible in the call-by-value calculus, while η-equality is not admissible in the call-by-name calculus.

XIII

6

Concluding Remarks

We have introduced the CPS hierarchy in call-by-name. Based on the thunktranslation and factorization, we have derived a calculus and a type system,and proved several interesting properties of our system. The simplicity of the
thunk translation makes it easy to treat a complex machinery such as the CPS
hierarchy, and we do not have to directly consult the iterated CPS translations
for most of the time.
This work builds on Danvy and Filinski’s CPS Hierarchy, and is related torecent works on call-by-name delimited continuations. Among all, Saurin [18]proposed “Stream Hierarchy” as a call-by-name CPS Hierarchy, and developed
a very interesting theory for this calculus, as it combines λµ-calculus in logic
and streams in functional programming. He used a quite different CPS translation than ours, namely, η-equality is admissible in his theory, and thus his
delimiter (reset) behaves quite differently from ours. Our theory does not admit η-equality since it badly interacts not only with the CPS translation, butalso with the semantics of reset, since if we have full η-equality, we can convert
every term to a value, which makes reset meaningless.2
As future work, we hope to relate the call-by-name calculi with the call-byvalue one in the sense of duality, and also with classical logic.

References
1. K. Asai. On typing delimited continuations: three new solutions to the printf
problem. Higher-Order and Symbolic Computation, 22(3):275–291, 2009.
2. K. Asai and Y. Kameyama. Polymorphic Delimited Continuations. In APLAS,
LNCS 4807, pages 239–254, 2007.
3. M. Biernacka and D. Biernacki. Context-based Proofs of Termination for Typed
Delimited-Control Operators. In PPDP, pages 289–300, 2009.
4. M. Biernacka, D. Biernacki, and O. Danvy. An Operational Foundation for Delimited Continuations in the CPS Hierarchy. Logical Methods in Computer Science,
1(2), 2005.
5. O. Danvy and A. Filinski. Abstracting Control. In LFP, pages 151–160, 1990.
6. A. Filinski. Representing Layered Monads. In POPL, pages 175–188, 1999.
7. J. Hatcliff and O. Danvy. Thunks and the Lambda-Calculus. J. Funct. Program.,7(3):303–319, 1997.
8. H. Herbelin and S. Ghilezan. An Approach to Call-by-Name Delimited Continuations. In POPL, pages 383–394, 2008.
9. Y. Kameyama. Axioms for Control Operators in the CPS Hierarchy. Higher-Orderand Symbolic Computation, 20(4):339–369, 2007.
10. Y. Kameyama and M. Hasegawa. A Sound and Complete Axiomatization of Delimited Continuations. In ICFP, pages 177–188, 2003.
11. Y. Kameyama and A. Tanaka. Equational Axiomatization of Call-by-Name Delimited Control. In PPDP, pages 77–86, 2010.
12. O. Kiselyov. Call-by-name Linguistic Side Effects. In ESSLLI, 2008.
2

Using η-equality, we can derive heii = hλy.eyii = λy.ey = e.

XIV

13. O. Kiselyov, C. c. Shan, and A. Sabry. Delimited Dynamic Binding. ICFP, pages
26–37, 2006.
14. J. L. Lawall and O. Danvy. Continuation-based partial evaluation. In LFP, pages
227–238, 1994.
15. C. Murthy. Control Operators, Hierarchies, and Pseudo-Classical Type Systems:
A-Translation at Work. In Proc. ACM Workshop on Continuations, pages 49–71,
1992.
16. G. D. Plotkin. Call-by-Name, Call-by-Value and the Lambda-Calculus. Theor.
Comput. Sci., 1(2):125–159, 1975.
17. A. Sabry and M. Felleisen. Reasoning about Programs in Continuation-Passing
Style. Lisp and Symbolic Computation, 6(3-4):289–360, 1993.
18. A. Saurin. A Hierarchy for Delimited Control in Call-by-Name. In FOSSACS,
pages 374–388, 2010.
19. A. Saurin. Standardization and Böhm Trees for Λµ-Calculus. In FLOPS, pages
134–149, 2010.
20. E. Sumii. An implementation of transparent migration on standard scheme. In
Scheme and Functional Programming, pages 61–63, 2000.
21. H. Thielecke. From Control Effects to Typed Continuation Passing. In POPL,
pages 139–149, 2003.
22. H. Thielecke. Answer type polymorphism in call-by-name continuation passing. In
ESOP, pages 279–293, 2004.

A

Equational Axioms for the Call-by-Value Calculus

Fig. 13 lists the axioms for the call-by-value calculus with hierarchical shift
and reset due to [9] modulo small notational difference.

E i ::= [ ] | E i e | vE i | force(E i ) | k ←-h E i where h < i(λx.e1 ) v = e1 {x := v}(βv )λx.v x = v where x 6∈ FV(v)
1

1

(ηv )
1

(λx.E [x])e = E [e] where x 6∈ FV(E )
i

(βΩ )

i

hE [Si k.e]ij = he{k ⇐i hE ii }ij where i ≤ j
0

0

i

i

k ←-j (E [Si k.e]) = he{k ⇐ (k ←-j E )}ij where i ≤ j and k 6= k(rsv )
0hvii = v
Si k.(k ←-i heii−1 ) = heii−1(thv )(rvv )

where k 6∈ FCV(e)Si k.heii = Si k.e

(se)
(sr)

h(λx.e1 )he2 ii ih = (λx.he1 ih )he2 ii where h ≤ iforce(delay(e)) = e(reset-lift)(fd)Fig. 13. Axioms for Call-by-Value with Force/Delay

XV