Equational Axiomatization ofCall-by-Name Delimited Control
Yukiyoshi Kameyama

Asami Tanaka

University of Tsukuba
Tsukuba, Japan
kameyama@acm.org

University of Tsukuba
Tsukuba, Japan
asami@logic.cs.tsukuba.ac.jp

Abstract
Control operators for delimited continuations are useful in various
fields such as partial evaluation, CPS translation, and representationof monadic effects. While many works in the literature study themin call-by-value, several recent works have shown call-by-namedelimited control operators are also worth studying.
In this paper, we study semantic foundation of the call-by-namevariant of the delimited-control operators “shift” and “reset”. In
particular, we give a set of direct-style equations as axioms forthem, and prove that it is sound and complete with respect to the
CPS translation by Biernacka and Biernacki. The key observations
in our proof are (1) we need to use the linearity of certain variablesin the CPS terms, and (2) we must distinguish continuation variables from ordinary variables in the source terms. We also showthat our axiomatization holds for the typed calculus.
Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages
General Terms

Languages,Theory,Verification

Keywords Control Operators, Delimited Continuation, Call-byName, Axiomatization, CPS translation

1. Introduction
Delimited continuation (or delimited control) has been proved useful in many applications from partial evaluation and Continuation
Passing Style (CPS) transformation to representation of arbitrary
monads to mobile computation. The traditional, unlimited continuation represents the whole rest of the computation (as the object
captured by Scheme’s call/cc), but the delimited continuation
represents part of the rest of the computation.
While many works in the literature studied delimited control incall-by-value [6, 8], several recent work studied it in call-by-name.
Herbelin and Ghilezan [11] related the study on classical logic withthe study on delimited continuations, and proposed a call-by-namecalculus for it. Kiselyov [13] proposed a call-by-name calculus
with delimited-control operators and used it in linguistic analysis.
Biernacka and Biernacki [4] introduced a type system for call-by-

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.
PPDP’10, July26–28, 2010, Hagenberg, Austria.
Copyright c 2010 ACM 978-1-4503-0132-9/10/07. . . $10.00

name delimited-control, which is similar to the type system for callby-value delimited-control by Danvy and Filinski [5], and proved
its strong normalization property.
In this paper, we investigate the call-by-name calculi withdelimited-control operators. Specifically, we identify the semantics of such a calculus through a CPS translation, and give a set ofsimple equations in direct style, which is sound and complete withrespect to this semantics.
We think such an axiomatization is useful and worth studying.
Given a set of reductions, one can compute every program (closedterm), however, one cannot optimize open terms using reductions
only. For instance, in a call-by-value calculus, (λx.x) (y z) is equal
to y z in any contexts, but (λx.x) (y z) cannot be reduced using thecall-by-value reductions. On the contrary, they are equal after CPS
translation. Appel [1] demonstrated a way to compiler construction
through CPS translation, and Flanagan et al. [10] showed that, allpossible optimizations after CPS-translating source terms may bedone before CPS-translating them, if we adopt a sufficiently strong
set of equations as axioms. The axioms must be sound in the sensethat all reductions are respected (if e1 reduces to e2 , they must be
equal by the axioms), and must be complete in the sense that all
possible optimizations for CPS terms can be done for direct-styleterms.
In this paper, we choose the control operators “shift” and “reset”
among many delimited-control operators proposed in the literature.
One of the most important merits of them is that they have a simple,
functional CPS translation. Kameyama and Hasegawa [12] axiomatized the call-by-value calculus with shift and reset, namely, they
identified the equational theory which coincides the CPS semantics
for shift and reset. The axioms are simple enough to be used as optimizations, and can be used to reason about programs with shift
and reset without converting the programs into CPS. In this paper
we will carry out the same program for the call-by-name calculi.
Unlike the call-by-value calculi with delimited-control operators, there are a few choices about the semantics of the call-byname calculi:• Whether the calculus admits η-equality or not: full η-equality

is usually assumed for call-by-name calculi, but it turns every
term into a function (a value), and, therefore, interferes with thecontrol operator reset (reset for a value does nothing). Hence,
we need to restrict either of the two (at least), and we decided
to abandon η-equality, since our intended operational semantics
does not admit it.
In Section 8, we will mention yet another calculus which admits
full η-equality but the use of reset is restricted.
• The semantics of the target calculus after the CPS translation:

the standard CPS translation for delimited-control operatorstranslates source terms into non-CPS terms, namely, arguments

of function applications are not necessarily values, and therefore, their meaning depends on the semantics of the target calculus.
We choose the call-by-value semantics for the target calculus,
because it matches the intended operational behavior of control
operators.
To avoid the complicated equality theory having both call-byname βη-equality and call-by-value βη-equality, we will translate the target terms once more by a CPS translation, following
Danvy and Filinski [5].
It should be noted that, a naive adaptation of Kameyama andHasegawa’s completeness proof for the call-by-value calculus did
not work for the call-by-name calculus. To overcome the difficulty,
we need to refine the source calculus (before CPS translation) as
well as the target calculus (after CPS translation) precisely. The key
observations are that (1) the delimited continuations are linear in
the call-by-name setting, and (2) we need to distinguish shift-boundvariables from the ordinary, lambda-bound variables. As for (1), wenote that the relationship between linearity and CPS translations
was studied by Filinski as “linear continuation” [9], and by Berdine
et al. as “linearly used continuations” [3], and, in this paper weneed both kinds of linearity. As for (2), we adopt the formulation
by Biernacka and Biernacki which has a special construct for theapplication of shift-bound variables to terms.
In this paper, we give sound and complete axiomatization for
the type-free and typed call-by-name calculi with delimited-control
operators, and their relationship with axiomatization for the callby-value calculus.
The rest of this paper is organized as follows: in Section 2 weintroduce the call-by-name calculus with delimited-control operators shift and reset. In Section 3 we give a CPS translation by
Biernacka and Biernacki, and then a sound and complete axiomatization for the semantics in Section 4. The completeness proof isgiven in Section 5, and Section 6 discusses these results in typed
setting. Section 7 discusses the use of linearity in our proofs, andSection 8 briefly mentions yet another CPS translation which respects η-equality. Section 9 gives concluding remarks.

2. Type-free Calculus
The calculus we study in this paper is λcbn
s/r , a call-by-name lambda
calculus with delimited-control operators “shift” and “reset”. The
call-by-value version of these control operators was proposed by
Danvy and Filinski [6, 7], and has been used to represent backtracking and various search, let-insertion in partial evaluation, various monads, type safe direct-style implementation of “printf”, andothers.
This section gives a type-free formulation of λcbn
s/r . Its typesystem will be explained later.
2.1 Syntax
In this subsection we give the syntax of terms and related expressions. First, we assume that there are two disjoint sets of variables,
one for ordinary variables (denoted by x, y, z, · · · ) and the otherfor shift-bound variables (denoted by k). x is (eventually) boundby lambda and a term is substituted for x, while k is (eventually)bound by shift, and a delimited context (delimited continuation) is
substituted for k.
Fig. 1 gives the syntax of λcbn
s/r . c is a constant. When we
consider a typed calculus, we restrict c be a constant of basic types
such as integer. An ordinary variable x is a term, while a shiftbound variable itself is not a term. The term λx.e and e1 e2 areabstraction and application as usual. The term Sk.e is a shift-term,in which k is a bound variable. The term k ←֓ e is a throw-term

e ::= c | x | λx.e | e1 e2 | Sk.e | k ←֓ e | hei

term

E ::= [ ] | Ee | hEi | k ←֓ E

ev. ctxt.

F ::= [ ] | F epure ev. ctxt.

Figure 1. Syntax of the Source Language(λx.e1 ) e2

e1 {x := e2 }hF [Sk.e]ihe{k ⇒ F }ihviv

for v = c, λx.e

Figure 2. Reduction Rules
that applies the (delimited) continuation k to a term e. The variable
k in k ←֓ e is free. The term hei is a reset-term.
Although the distinction between ordinary (lambda-bound)variables and continuation variables appears in the work of Parigot[15], it was Biernacka and Biernacki [4] who have made a clear
distinction between lambda-bound variables and shift-bound variables in the context of call-by-name delimited control. They havealso introduced the notation k ←֓ e.
We identify α-equivalent terms. FV(e) denotes the set of free(ordinary and shift-bound) variables in e, and e1 {x := e2 } represents the result of capture-avoiding substitution of e2 for x in e1 .
E represents an arbitrary evaluation context in call-by-name. F isa pure evaluation context, or a delimited evaluation context, which
does not have reset’s around the hole [ ]. In other words, a pureevaluation context is delimited by a reset, and is exactly a delimited continuation. A general evaluation context is a continuation
outside of a reset, namely, a metacontinuation. E[e] (or F [e]) denotes the term after the hole-filling operation of a term e for a holein E (or F ). Hole-filling of another evaluation context E1 [E2 ] isdefined similarly.
Remarks. Let us briefly argue the design of the source calculus
here, namely, if the distinction between shift-bound and lambdabound variables is necessary or not.
If we are only concerned with the operational behavior of closed
terms, there is no need to distinguish them. In this case, the expression k ←֓ e can be represented by (k e).
However, this distinction is necessary for this paper, since weare concerned with equality theories for open terms: to obtaincomplete axiomatization, we need an axiom which is valid for shiftbound variables but not valid for lambda-bound variables.
We remark that Biernacka and Biernacki introduced this distinction for a different purpose: to develop a type system for the
calculus, which represents the so called answer-type polymorphism
without making use of polymorphism [2]. The details may be foundin [4].
In summary, two distinct classes of variables are necessary inthe call-by-name calculi for delimited continuations. This is a sharp
contrast with the call-by-value case, for which the above-mentioned
distinction is not necessary [12].
2.2 Reduction Rules
To understand the operational behavior of shift and reset, we givethe reduction rules of λcbn
s/r in Fig. 2.
The reduction rules are essentially the same as those in Biernacka and Biernacki, but we have slightly changed them in the following point: their calculus has an expression F ←֓ e for a pureevaluation context F and an expression e. It is the result of substituting F for k in k ←֓ e (here we assume that k does not appear

in e freely). On the other hand, our calculus does not have such an
expression, and such a substitution is realized by a meta-operation{k ⇒ F }.
The substitution {k ⇒ F } is defined as follows:defc{k ⇒ F } = c• Reduction semantics: e1 = e2 if and only if they are equal up

to the equality induced by the reduction rules.2• CPS semantics. e1 = e2 if and only if they are translated to thedefsame term by a CPS translation.

x{k ⇒ F } = xdef• Observational equivalence. e1 = e2 if and only if, for any

defcontext C such that C[e1 ] and C[e2 ] are closed, C[e1 ] andC[e2 ] both terminate, or both do not terminate under (a certain
notion of) the operational semantics.

(λx.e){k ⇒ F } = λx.(e{k ⇒ F })where x 6∈ FV(F )(e1 e2 ){k ⇒ F } = (e1 {k ⇒ F }) (e2 {k ⇒ F })def(Sk′ .e){k ⇒ F } = Sk′ .(e{k ⇒ F })where k′ 6∈ {k} ∪ FV(F )def(k ←֓ e){k ⇒ F } = hF [e{k ⇒ F }]idef(k′ ←֓ e){k ⇒ F } = k′ ←֓ (e{k ⇒ F })where k′ 6∈ {k} ∪ FV(F )defhei{k ⇒ F } = he{k ⇒ F }i
Let us look at the reduction rules in detail. The first reduction in
Fig. 2 is the standard, call-by-name β-reduction.
In the second reduction rule, the evaluation context up to thenearest delimiter (reset) is F , and it is captured and substituted fork using the substitution {k ⇒ F }. The key case in this substitutionis (k ←֓ e){k ⇒ F }, which is defined to be hF [e{k ⇒ F }]i.
This means that, by the substitution {k ⇒ F }, a functional object
λx.hF [x]i is substituted for k, if we identify k ←֓ e′ with (k e′ ).
Hence, the second reduction hF [Sk.e]ihe{k ⇒ F }i may beunderstood as
hF [Sk.e]i

The following three semantics are often studied for computational calculi:he{k := λx.hF [x]i}iThis is the same reduction rule as the one in the literature [12].
The third rule means: when a value is delimited by reset, thenthe delimiter is simply discarded. It may be strange to have thenotion of values in the call-by-name calculus, but this rule naturally
reflects the abstract-machine semantics for shift and reset in callby-name1 . Note that, a variable x is not a value in λcbn
s/r , so hxi
does not reduce to x.
In Section 4, we will need to extend the above substitution to theform {k ⇒ (k′ ←֓ F )}, namely, we need to extend the substituted
context F to the form k′ ←֓ F , which is not a pure evaluation
context. The definition of the extended substitution remains thesame except that F in the above definition may be in the formk′ ←֓ F ′ . For example, the key case is:def(k ←֓ e){k ⇒ (k′ ←֓ F )} = hk′ ←֓ (F [e{k ⇒ (k′ ←֓ F )}])i
We remark that reset in the right-hand side of this definition is notnecessary as hk′ ←֓ e′ i = k′ ←֓ e′ can be proved by our axioms
introduced later.

3. Semantics based on CPS Translation
3.1 CPS Semantics
A CPS translation is a syntax-directed translation from a source
calculus (λcbn
s/r in this paper) to a target calculus. It is a useful theoretical tool to give a precise semantics to a calculus with control
operators, and may be used as an intermediate language for compilers, since we can perform various kinds of optimizations on thetarget terms of a CPS translation. Using the axioms in this paper,
one can perform the optimizations on the source terms.
1 This semantics is attributed to Olivier Danvy in the literature [11].

Under reasonable assumptions, the strength of the three semantics increases in the order above, namely, if two programs are equalin the reduction semantics (CPS semantics, resp.), they are equal in
the CPS semantics (observational equivalence, resp.). The converse
direction does not, in general, hold. For instance, (λx.xx)(λx.xx)
and (λx.xxx)(λx.xxx) are equal under the observational equivalence, but they are not CPS-translated to equal terms for any standard CPS translations.
Although CPS semantics is weaker than observational equivalence, it is in many cases sufficient for reasoning about programs, as
shown by literature (for instance, [1]). Indeed we often prefer CPS
semantics than observational equivalence, since the latter is fragile
in language extensions; under observational equivalence, two equalterms may not be equal after a new construct is added to the calculus, as we may be able to distinguish these terms using the new construct. On the contrary, CPS semantics is robust in the sense that,
two equal terms remain equal even after a new construct is added,
since their images of a CPS translation do not (usually) change.
3.2 1CPS Translation
Our task is to precisely determine the CPS translation we use, andwe choose a CPS translation based on Plotkin’s one, as we willargue below.
For call-by-name calculi, there are two choices for CPS translations: Plotkin’s [16] and Streicher and Reus’ [18]. The latter respects full η-equality (η-equal terms are translated to equal terms),
while the former does not. Using full η-equality, we can infer thatthe control operator “reset” becomes totally useless:hei =η hλx.exi

λx.ex =η eWithout the reset operator, our calculus does not make sense. Consequently, we use a CPS translation based on Plotkin’s. We willrevisit this choice in Section 8.
Fig. 3 gives the CPS translation for the calculus λcbn
s/r where weassume that the variables κ and m are fresh. The CPS translation
is essentially due to Biernacka and Biernacki, which is based on
Plotkin’s call-by-name CPS translation, and is extended to thecalculus with shift and reset. The translation [ ] 1 maps a termin λcbns/r to a term in the type-free lambda calculus. We call it
1CPS translation. For terms without control operators, this CPS
translation is identical to Plotkin’s one. Unlike the call-by-value
one, a variable x is translated to λκ.xκ. This reflects the fact thata variable in the call-by-name calculus λcbn
s/r is not a value, but
represents a computation, so its CPS counterpart should receive acontinuation κ. We will assume that the target calculus of the CPS
translation admits η-equality for the continuation variable κ, hence[ x]]1 could be defined as x.
The translation for a reset-term hei is identical to that in thecall-by-value setting [6]. It is also not difficult to understand thetranslation of a shift-term Sk.e. It captures the current continuation
2 The equality is the reflexive, transitive, and congruent closure of the
reduction rules.

def[ x]]2 = x

def[ c]]2 = λκ.κc[ c]]1 = λκ.κc[ x]]1 = λκ.xκ

def

def

def

[ λx.e]]2 = λκ.κ(λx.[[e]]2 )def[ e1 e2 ] 2 = λκ.[[e1 ] 2 (λm.m[[e2 ] 2 κ)def

[ Sk.e]]2 = λκ.([[e]]2 {k := κ})I2

def[ k ←֓ e]]2 = λκ.λγ.[[e]]2 k(κ ⊕ γ)def

[ hei]]2 = λκ.λγ.[[e]]2 I2 (κ ⊕ γ)

[ λx.e]]1 = λκ.κ(λx.[[e]]1 )[ e1 e2 ] 1 = λκ.[[e1 ] 1 (λm.m[[e2 ] 1 κ)
[ Sk.e]]1 = λκ.([[e]]1 {k := κ})I1[ k ←֓ e]]1 = λκ.κ([[e]]1 k)[ hei]]1 = λκ.κ([[e]]1 I1 )def

I1 = λm.m

def

def

def

def

def

def

I2 = λm.λγ.γm
defFigure 3. 1CPS Translation(κ ⊕ γ) = λm.κmγ
Figure 4. 2CPS Translation

κ, binds it to the shift-bound variable k, and then installs theidentity continuation I1 . The translation of a throw-term k ←֓ eis to install the continuation k, compute e, and then re-activates thecontinuation κ by applying κ to the result of e. The translation ofa reset-term is to save the current (delimited) continuation κ, andinstall the identity continuation I1 (which corresponds to an empty
evaluation context) as the current continuation.
3.3 Semantics of CPS terms
Our purpose is to axiomatize the CPS semantics, and in order to doso, we need to precisely define the semantics of the target calculus.
In the presence of delimited-control operators in the source calculus
λcbn
s/r , the image of 1CPS translation is not strictly in CPS. Namely,
the arguments in function applications may not be values. For
instance, the image of a reset-term contains a subterm κ([[e]]1 I1 ), in
which κ is applied to a non-value term [ e]]1 I1 , thus the evaluationof this term is dependent on the evaluation strategy. If we evaluate
it in call-by-value, [ e]]1 I1 is computed first, and κ is applied to its
result. If we evaluate it in call-by-name, [ e]]1 I1 is not computed
now, and κ is applied to the unevaluated subterm [ e]]1 I1 .
As for this choice, we again follow Biernacka and Biernacki
who have chosen the call-by-value semantics for the target calculus.
Rather than introducing the call-by-value semantics into the target
calculus directly (such as Moggi’s computational lambda calculus[14]), we translate the CPS terms once again [6], by the call-byvalue CPS translation.
The successive CPS translations may be represented by a single
CPS translation, which we call a 2CPS translation. The images ofthe 2CPS translation are terms in CPS, and we no longer have to be
worried about different semantics.
3.4 2CPS Translation
Fig. 4 defines the 2CPS translation for λcbn
s/r , which introduces two
continuation variables κ and γ. These variables as well as m areassumed to be fresh. If we decompose the 2CPS translation into
two CPS translations, κ is introduced by the first (call-by-name)
CPS translation, and γ is introduced by the second (call-by-value)
CPS translation.
The definition of the 2CPS translation looks like that of the
1CPS translation. The trick is that we η-reduce the results of
2CPS translation whenever possible. For instance, [ x]]2 should be
λκ.λγ.xκγ, however, since we will introduce η-equality for thedefvariable γ, it is equal to λκ.xκ, so we define it as [ x]]2 = λκ.xκ
(which is in turn equal to x by η-reduction for κ). Since the imagesof the 1CPS translation of the throw-term k ←֓ e and the reset-term
hei contain non-CPS forms, their images of the 2CPS translations
must use the second continuation variable γ.

We also note that the identity continuation I1 (= λm.m) becomes I2 (= λm.λγ.γm), and that (κ ⊕ γ) (which is simply an
abbreviation for λm.κmγ) corresponds to the push-operation forthe stack of meta-continuations in the abstract machine semantics.
(See [4] for details.)
In the following, we simply write [ e]] for [ e]]2 , since we do not
use the 1CPS translation.
3.5 Analysis of Target Calculus
In order to define the CPS semantics, we shall precisely define thesemantics of the target calculus of the 2CPS translation.
By inspecting the images of the translation, we can easily showthat terms in the target calculus are generated by the following
grammar:T ::= x | λκ.P | V T
P ::= KV | T K | λγ.A
A ::= GV | P G

V ::= c | m | λx.T
K ::= κ | λm.P
G ::= γ | λm.A

The target calculus has six sorts: T is the image of expressions
in λcbns/r . P is a pre-term and A is an answer. V is the image ofvalues (constant or abstraction). K is the image of pure evaluation
contexts (delimited context). G is the image of (general) evaluation
contexts. Variables belong to some specific sorts: x is a variable for
T , m for V , κ for K, and γ for G.
It is important to note that βη-reductions in the target calculus
preserve the sorts, which is easily proved.
For a term in the target calculus t1 and t2 , we write ⊢CPS t1 =t2 if they are proved equal using the following equations andthe standard equality rules (reflexivity, symmetry, transitivity, andsubstitution):• β-equality for x: (λx.T1 ) T2 = T1 {x := T2 }.
• βη-equality for m: (λm.P )V = P {m := V }, λm.Km =K (where m 6∈ FV(K)), (λm.A)V = A{m := V }, andλm.Gm = G (where m 6∈ FV(G)).
• βη-equality for κ: (λκ.P )K = P {κ := K} and λκ.T κ = T(where κ 6∈ FV(T )).
• βη-equality for γ: (λγ.A)G = A{γ := G} and λγ.P γ = P(where γ 6∈ FV(P )).
Note that we have excluded η-equality for x, namely, λx.V x =V is not allowed in general. This choice reflects the fact that thesource calculus λcbn
s/r does not allow η-equality as we argued before.

3.6 Properties of 2CPS Translation
In this subsection we show several useful properties of the 2CPS
translation.
We first define |F | for a pure evaluation context F . The purposeof | | is to CPS-translate a pure evaluation context F , and it isdefined as follows:def|[ ]| = λκ.κ

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

hF [Sk.e]i = he{k ⇒ F }ireset-shiftk′ ←֓ (F [Sk.e]) = he{k ⇒ (k′ ←֓ F )}i

throw-shift

hvi = v for v = c, λx.e

reset-value

Sk.(k ←֓ e) = e where k 6∈ FV(e)shift-elim

Sk.hei = Sk.edefshift-reset|F e| = λκ.|F | (λm.m[[e]]κ)Figure 5. Axioms for λcbn
s/r (call-by-name)Now we can state the following lemma which is useful in thesoundness proof.
L EMMA 1. We have the following properties for the 2CPS translation.
(1) ⊢CPS(2) ⊢CPS(3) ⊢CPS(4) ⊢CPS[ F [e]]] = λκ.[[e]](|F |κ) where κ 6∈ FV(e).
[ e{x := e′ }]] = [ e]]{x := [ e′ ] }.
[ e{k ⇒ F }]] = [ e]]{k := |F | I2 }.
[ e{k ⇒ (k′ ←֓ F )}]] = [ e]]{k := |F | k′ }.

Proof. (1) The equation is proved by induction on F . When F =[ ], it is trivial. When F = F1 e1 , we can prove it as follows:[ F [e]]] ≡ [ F1 [e] e1 ]≡ λκ.[[F1 [e]]] (λm.m[[e1 ] κ)
= λκ.(λκ′ .[[e]](|F1 |κ′ )) (λm.m[[e1 ] κ) by I.H.
= λκ.[[e]](|F1 |(λm.m[[e1 ] κ))= λκ.[[e]](|F1 e1 | κ)
From the second line to the third, we used induction hypothesis on
F1 .
(2) The equation is easily proved by induction on e.
(3) The equation is proved by induction on e. The only interesting case is e ≡ k ←֓ e1 , and we can prove the case as follows:[ (k ←֓ e1 ){k ⇒ F }]]≡ [ hF [e1 {k ⇒ F }]i]]≡ λκ.λγ.[[F [e1 {k ⇒ F }]]]I2 (κ ⊕ γ)
= λκ.λγ.[[e1 {k ⇒ F }]](|F | I2 )(κ ⊕ γ) by (1)= λκ.λγ.[[e1 ] {k := |F | I2 }(|F | I2 )(κ ⊕ γ) by I.H.
= (λκ.λγ.[[e1 ] k(κ ⊕ γ)){k := |F | I2 }≡ [ (k ←֓ e1 )]]{k := |F | I2 }(4) This case is proved in the same way as (3). Here we show
the case e ≡ k ←֓ e1 .

βv

λx.v x = v where x 6∈ FV(v)ηv(λx.F [x])e = F [e] where x 6∈ FV(F )βΩhF [Sk.e]i = he{k ⇒ F }ireset-shiftk′ ←֓ (F [Sk.e]) = he{k ⇒ (k′ ←֓ F )}i

throw-shift

hvi = vSk.(k ←֓ e) = e where k 6∈ FV(e)reset-value
shift-elim

Sk.hei = Sk.e

shift-reseth(λx.e1 )he2 ii = (λx.he1 i)he2 i

reset-lift

where v and F are defined as follows:v ::= c | x | λx.e
F ::= [ ] | F e | v F
Figure 6. Axioms for λcbv
s/r (call-by-value)
4.1 Axioms
cbn
Fig. 5 gives our axioms for λcbn
s/r . We write ⊢s/r e1 = e2 if we canprove the equation using these axioms and the standard inference
rules for equality.
For the purpose of comparison, Fig. 6 gives the axioms forthe call-by-value calculus λcbv
s/r by Kameyama and Hasegawa [12].
Although their calculus does not have the throw expression k ←֓ e,
we introduce it for the purpose of comparison. Their axioms areslightly modified accordingly. Note that the definitions for a value
v and the pure evaluation context F for the call-by-value calculus
are different from those for λcbn
s/r .
We will explain the axioms in Fig. 5 by comparing them to thosein Fig. 6.

• The call-by-name calculus λcbn
s/r has a single strong axiom for[ (k ←֓ e1 ){k ⇒ (k′ ←֓ F )}]]β, while the call-by-value one λcbv
s/r has three weaker axioms
βv , βΩ , and reset-lift. The former subsumes the latter.

≡ [ k′ ←֓ F [e1 {k ⇒ (k′ ←֓ F )}]]]≡ λκ.λγ.[[F [e1 {k ⇒ (k′ ←֓ F )}]]]k′ (κ ⊕ γ)′′

= λκ.λγ.[[e1 {k ⇒ (k ←֓ F )}]](|F | k )(κ ⊕ γ) by (1)′(λx.e1 ) v = e1 {x := v}′= λκ.λγ.[[e1 ] {k := |F | k }(|F | k )(κ ⊕ γ) by I.H.
′= (λκ.λγ.[[e1 ] k(κ ⊕ γ)){k := |F | k }≡ [ k ←֓ e1 ] {k := |F | k′ }4. Axiomatizing the Semantics
In this section, we provide a set of axioms for λcbn
s/r , and show that
it is sound with respect to the CPS semantics. Its completeness will
be proved in the next section.

cbv• No axiom for η-equality exists in λcbn
s/r , while λs/r has the call-by-value version of η-equality as ηv .
• The axioms shift-elim and shift-reset are contained in both

calculi.
• Two axioms reset-shift and reset-value are contained in both

calculi, but their actual meanings differ between the calculi,
since the definitions of F and v differ.
• The axiom throw-shift is contained in both calculi.

For the call-by-value calculus, this is only because k ←֓ e is a
special form. If we do not distinguish shift-bound and lambdabound variables, then k ←֓ e may be represented by (k e),and the axiom throw-shift is subsumed by reset-shift (note that(k F ) is an evaluation context in λcbv
s/r if k is a variable).
On the contrary, the axiom throw-shift is necessary for the callby-name calculus, and it seems difficult to formulate this axiom without distinguishing shift-bound variables from lambdabound variables. Without such a distinction, throw-shift would
become unsound.
We believe that our axioms for the call-by-name calculus are
simple enough to be used for reasoning about open programs, andthat the similarity of the axioms for the two calculi is an evidence
that our axioms are natural and stable.
We emphasize that establishing this kind of axioms is not trivial
even after getting to know the axiomatization for the call-by-value
case, since the CPS translation of the shift term in call-by-name is
not quite the same as that in call-by-value.
It is easy to prove that the reduction semantics is subsumed by
our axioms.

(throw-shift, k′ 6= k)[ k′ ←֓ (F [Sk.e])]]≡ λκ.λγ.[[F [Sk.e]]] k′ (κ ⊕ γ)
= λκ.λγ.[[Sk.e]](|F | k′ ) (κ ⊕ γ) by Lemma 1 (1)≡ λκ.λγ.(λκ′ .[[e]]{k := κ′ }I2 )(|F | k′ ) (κ ⊕ γ)
= λκ.λγ.([[e]]{k := |F | k′ }) I2 (κ ⊕ γ)
= λκ.λγ.[[e{k ⇒ (k′ ←֓ F )}]] I2 (κ ⊕ γ) by Lemma 1 (4)≡ [ he{k ⇒ (k′ ←֓ F )}i]](reset-value) We define v ∗ for a value v by:defc∗ = cdef(λx.e)∗ = λx.[[e]]Then we can prove:[ hvi]] ≡ λκ.λγ.(λκ′ .κ′ v ∗ ) I2 (κ ⊕ γ)
= λκ.λγ.I2 v ∗ (κ ⊕ γ)

T HEOREM 1. Let e1 and e2 be expressions in λcbn
e2 by
s/r . If e1
one of the reduction rules in Fig. 2, then ⊢cbn
s/r e1 = e2 is derivable.
Proof. The three reductions, respectively, are subsumed by theaxioms β, reset-shift, and reset-value, respectively.
The rest of this paper is devoted to establish that the axioms in
Fig. 5 are sound and complete with respect to the CPS semantics
induced by the 2CPS translation.

= λκ.λγ.(κ ⊕ γ) v ∗= λκ.λγ.κ v ∗ γ= λκ.κ v ∗≡ [ v]](shift-elim, k 6∈ FV(e))[ Sk.(k ←֓ e)]] ≡ λκ.([[k ←֓ e]]{k := κ}) I2= λκ.(λκ′ .λγ.[[e]] k (κ′ ⊕ γ)){k := κ}) I2= λκ.λγ.[[e]] κ (I2 ⊕ γ)
= λκ.λγ.[[e]] κ γ= [ e]]

4.2 Soundness of Axioms
Soundness of the axioms means that equal terms in the source
calculus λcbn
s/r are CPS-translated to equal terms. Soundness may
be thought as a sort of correctness for a CPS translation.

(shift-reset)[ Sk.hei]] = λκ.([[hei]]{k := κ}) I2

T HEOREM 2 (Soundness). Let e1 and e2 be terms in λcbn
s/r . If
⊢cbn
e
=
e
is
derivable,
then
⊢
[
e
]
=
[
e
]
is
derivable.
1
2
CPS
1
2
s/r
Proof. It suffices to prove the theorem when e1 = e2 is obtainedby one of the axioms. We list the proofs of all the cases, since they
are instructive to know the details of the CPS translation.
(β)[ (λx.e1 ) e2 ] ≡ λκ.[[λx.e1 ] (λm.m [ e2 ] κ)
= λκ.(λκ′ .κ′ (λx.[[e1 ] )) (λm.m [ e2 ] κ)
= λκ.(λx.[[e1 ] ) [ e2 ] κ= λκ.[[e1 ] {x := [ e2 ] } κ= [ e1 ] {x := [ e2 ] }= [ e1 {x := e2 }]] by Lemma 1 (2)(reset-shift)[ hF [Sk.e]i]]≡ λκ.λγ.[[F [Sk.e]]] I2 (κ ⊕ γ)
= λκ.λγ.[[Sk.e]] (|F | I2 ) (κ ⊕ γ) by Lemma 1 (1)≡ λκ.λγ.((λκ′ .[[e]]{k := κ′ }) I2 )(|F | I2 ) (κ ⊕ γ)
= λκ.λγ.([[e]]{k := |F | I2 }) I2 (κ ⊕ γ)
= λκ.λγ.[[e{k ⇒ F }]] I2 (κ ⊕ γ) by Lemma 1 (3)≡ [ he{k ⇒ F }i]]= λκ.(λκ′ .λγ.[[e]] I2 (κ′ ⊕ γ)){k := κ}) I2= λκ.λγ.([[e]] I2 (I2 ⊕ γ)){k := κ}= λκ.λγ.([[e]] I2 γ){k := κ}= [ Sk.e]]

5. CompletenessCompleteness is the converse of soundness: if the images of the
CPS translation of two terms are equal in the target calculus, thenthey are equal in the source calculus. Completeness ensures that
all equational reasoning for CPS terms can be done in the source
calculus.
T HEOREM 3 (Completeness). Let e1 and e2 be (type-free) terms
cbn
in λcbne1 = e2 is
s/r . If ⊢CPS [ e1 ] = [ e2 ] is derivable, then ⊢s/r
derivable.
Let us give an overview of the proof of completeness.
We will basically follow the general recipe by Sabry andFelleisen [17] as follows:
1. Analyze the structure of target terms of CPS translation, anddefine a grammar for it, which should be closed under the
reductions in the target calculus.
2. Define a translation from the target to the source calculus, andprove that it is an inverse of the CPS translation.
3. Prove that equality in the target calculus is preserved by the
inverse translation.

However, we encountered a problem when the grammar in Section 3.5 is used for this purpose; we could not define a suitable image of the inverse function for the variable m (the variable for the
V -sort) with the desired property. Let us explain this in more detail.
In the completeness proof, we will need the property hv ◦ i = v ◦ forany term v of the V -sort where v ◦ is the image of v by the inverse
function. As a special case, we need hm◦ i = m◦ . However, if m◦
is a variable in λcbn
s/r , this property does hold in general. (Note that avariable in λcbn
s/r represents an arbitrary expression, and not necessarily a value, thus hxi = x does not hold in general.) In addition,no other choice for m◦ seems to exist as m is a variable.
We can overcome this difficulty by investigating the target calculus more carefully. The variable m in the target calculus is not
used in an arbitrary way, but is used linearly. Linearity of the variable m reflects the fact that a delimited continuation (a pure evaluation context) in the call-by-name calculus is linear in its hole:F ::= [ ] | F e. 3
Since m is linear, we do not have to keep the name of m throughthe inverse function, and we may discard it. The same technique
was used by Kameyama and Hasegawa’s axiomatization of shift
and reset in call-by-value, where the metacontinuation variable γ islinear, and thus can be discarded by the inverse function. Here, we
discard not only the name of γ, but also the name of m.
In the following proof, we do not directly formulate linear
lambda calculus as the target calculus. Instead, we refine the grammar to reflect the linearity of the variable m. Therefore we do not
explicitly mention the linearity in the proof, but it is embedded in
the grammar of the target calculus, and the definition of the inverse
translation from the target calculus. The point here is that this simple trick is sufficient to avoid the problem above.
5.1 Refined Grammar and Inverse Function
We give a refined grammar for the target calculus as:
T ::= x | λκ.P | V T
P ::= KV | T K | λγ.A
A ::= GV | P G
V ::= c | λx.T
K ::= κ | λm.m T K | λm.λγ.γ m
G ::= γ | λm.K m G

term
preterm
answervalue
continuation
metacontinuation

The difference from the previous grammar is that we no longer
regard m as a member of the V -sort. Instead, the K- and G-sorts
contain a few more terms using m, and m is a linear variable.
The equality of the target calculus remains the same, however,since η-redex for m does not exist in the terms generated by the
new grammar, it is discarded. In summary, the equality of the terms
generated by the new grammar is induced by β-equality for thevariables x and m, and βη-equality for the variables κ and γ.
In the following, we use T, P, A, V, K and G not only for thenames of sorts, but also for meta-variables of the corresponding
sorts, for instance, T is used as a meta-variable for terms of the
T -sort.
We can easily prove the following lemma for the refined grammar.
L EMMA 2.
• If e is a λcbn
s/r -term, then [ e]] belongs to the T -sort.
• Each of the above sorts is closed under β-reduction for x andm, and βη-reduction for κ and γ.
3 This linearity has been already mentioned in the literature, for instance, in
Herbelin and Ghilezan [11].

def

def

x◦ = x(λκ.P )◦ = Sκ.P ◦def(V T )◦ = V ◦ T ◦
def

def

(KV )◦ = K ◦ [V ◦ ](T K)◦ = K ◦ [T ◦ ]def(λγ.A)◦ = A◦
def

def

(P G)◦ = G◦ [hP ◦ i]

(GV )◦ = G◦ [V ◦ ]defc◦ = cdef(λx.T )◦ = λx.T ◦def(λm.m T K)◦ = K ◦ [[ ] T ◦ ]κ◦ = κ ←֓ [ ]

def

def

(λm.λγ.γ m)◦ = [ ]
def

def

γ◦ = [ ](λm.K m G)◦ = G◦ [hK ◦ [ ]i]Figure 7. Inverse Function

We then define an inverse function ( )◦ from the target calculus
to source calculus in Fig. 7. By the inverse function, a term in the
T , P , A, or V -sort is mapped to a term in λcbn
s/r , a term in the K or
G-sort to an evaluation context.
Note that reset is introduced in (P V )◦ and (λm.K m G)◦ ,and the names of the variables m and γ are discarded through theinverse, since these variables are linear.
We prove that the above “inverse” function is actually a (left)
inverse of the 2CPS translation.
L EMMA 3 (Inverse). Let e be an expression in λcbn
s/r . We have◦⊢cbns/r [ e]] = e.
Proof. This lemma can be proved by a straightforward induction
on e. Let us show a few interesting cases.
For e = he′ i, we have:[ e]]◦ = (λκ.λγ.[[e′ ] I2 (κ ⊕ γ))◦◦= Sκ.(λm.κ m γ)◦ [hI2 ◦ [[[e′ ] ]i]◦◦= Sκ.κ ←֓ h[[e′ ] i = h[[e′ ] i = he′ i
For e = Sk.e′ , we have:[ e]]◦ = (λκ.([[e′ ] {k := κ})I2 )= (λk.[[e′ ] I2 )◦◦◦= Sk.I2 ◦ [[[e′ ] ] = Sk.e′
5.2 Properties of Inverse Function
We present several technical properties about substitution and theinverse.
L EMMA 4. Substitutions for x, κ, and γ commute with the inverse
function in the following sense.
◦◦◦(1) ⊢cbns/r (t{x := T1 }) = t {x := T1 } is derivable if t is a T -,P -, A-, V -, K-, or G-term.
(2) Let φ be {κ := K1 } and ψ be {κ ⇒ K1 ◦ }. Then we have:◦◦• ⊢cbns/r (tφ) = t ψ if t is a T - or V -term.
◦cbn• ⊢s/r h(tφ) i = ht◦ ψi if t is a P - or A-term.
◦◦cbn• ⊢cbns/r h(Kφ) [e]i = h(K ψ)[e]i for any term e in λs/r .
◦
cbn
◦
cbn
• ⊢s/r (Gφ) [hei] = (G ψ)[hei] for any term e in λs/r .
◦◦◦(3) ⊢cbn
s/r h(A{γ := G1 }) i = hG1 [hA i]i.
◦◦cbn(4) ⊢s/r (G{γ := G1 }) [hei] = G1 [hG◦ [hei]i] for any term ein λcbns/r .

Proof. This lemma can be proved by simultaneous induction oneach term. Note that (P φ)◦ = P ◦ ψ does not hold in general, but
it suffices to prove h(P φ)◦ i = hP ◦ ψi to make the induction go
through, since P always appears immediately under reset. Similarly for K, we only have to consider the form hK ◦ [e]i. We also
make use of the fact that γ does not appear free in T , P , V or K.
Here, we prove a few interesting cases.
(Case K ≡ κ for h(Kφ)◦ [e]i = h(K ◦ ψ)[e]i)We may assume that κ 6∈ FV(e). The left-hand side is hK1 ◦ [e]i,and the right-hand side is h(κ◦ ψ)[e]i, which is equal to h(κ ←֓e){κ ⇒ K1 ◦ }i. Then we have:
◦
◦
◦
⊢cbn
s/r h(κ ←֓ e){κ ⇒ K1 }i = hhK1 [e]ii = hK1 [e]i(Case G ≡ λm.KmG2 for (4))
The left-hand side of (4) is (G2 {γ := G1 })◦ [hK ◦ [hei]i],
which is equal to G1 ◦ [hG2 ◦ [hK ◦ [hei]i]i] by induction hypothesis, which is equal to the right-hand side.
L EMMA 5 (Inverse preserves reduction). Suppose ⊢CPS t1 = t2 isderivable for target terms t1 and t2 , then we have:• ⊢cbnt1 ◦ = t2 ◦ if t1 and t2 are T - or V -terms.
s/r• ⊢cbnht1 ◦ i = ht2 ◦ i if t1 and t2 are P - or A-terms.
s/r• ⊢cbnht1 ◦ [e]i = ht2 ◦ [e]i if t1 and t2 are K-terms and e is as/rterm in λcbn
s/r .
◦• ⊢cbn[hei] = t2 ◦ [hei] if t1 and t2 are G-terms and e is a
t
1
s/r
cbn
term in λs/r .
Proof. It suffices to prove the lemma when t2 is obtained from t1
by β or η reduction.
There are six β-redexes, and two η-redexes. For each reduction◦◦
t1
t2 , it is not difficult to prove ⊢cbn
s/r t1 = t2 .
The most interesting case is β-reduction for κ, namely, the case◦◦⊢cbn
s/r h((λκ.P )K) i = h(P {κ := K}) i. We have:h((λκ.P )K)◦ i = hK ◦ [Sκ.P ◦ ]iandh(P {κ := K})◦ i = hP ◦ {κ ⇒ K ◦ }i
by Lemma 4. By inspecting the definition of K ◦ , it is either a pureevaluation context, or the form κ′ ←֓ F for some κ′ and F . In theformer case, we use the axiom reset-shift to prove:
◦
◦
◦
◦
⊢cbn
s/r hK [Sκ.P ]i = hP {κ ⇒ K }i

while in the latter case, we use the axiom throw-shift to prove thesame equation. Hence we are done.
The other cases can be proved easily.
It should be emphasized that the proof of this theorem actuallyneeds the axiom throw-shift.
Proof. of Theorem 3 Let e and e′ be terms in λcbn
s/r . Suppose⊢CPS [ e]] = [ e′ ] is derivable. Since [ e]] and [ e′ ] are T-terms, we◦have ⊢cbn[ e]]◦ = [ e′ ] by Lemma 5, and then ⊢cbn
e = e′ bys/rs/r
Lemma 3.

6. Typed Calculus
We have so far studied the type-free calculus only, and a natural
question is whether our axioms work for typed calculus. In thissection we give a positive answer to it.

Γ ∪ {x : (α | σ | β)} | α ⊢ x : σ | βvar(c is a constant of base type b)
const
Γ|α⊢c:b|αΓ, x : (α | σ | β) | α′ ⊢ e : σ ′ | β ′Γ | γ ⊢ λx.e : (α | σ | β) → (α′ | σ ′ | β ′ ) | γ
Γ | β ′ ⊢ e0 : (α | σ | β) → (α′ | σ ′ | β ′ ) | γ′funΓ | α ⊢ e1 : σ | β′

Γ | α ⊢ e0 e1 : σ | γ
Γ|α⊢e:α|βreset
Γ | γ ⊢ hei : β | γΓ ∪ {k : σ ⊲ τ } | α ⊢ e : α | βshiftΓ | τ ⊢ Sk.e : σ | βΓ|τ ⊢e:σ|βthrowΓ ∪ {k : σ ⊲ τ } | α ⊢ k ←֓ e : β | αFigure 8. Type System• Our syntax does not have an expression F ←֓ e for a pureevaluation context F and an expression e, so the corresponding
typing rule is not contained.
• As a consequence, we do not need typing rules for delimited

contexts and metacontexts, so they are omitted.
• We use a slightly different notation for function types. This is

only notational difference: we write (α | σ | β) → (α′ | σ ′ |β ′ ) for their type σ α,β α′ →β ′ σ ′ .
A type (denoted by α, β, σ, τ, · · · ) is either a basic type b (suchas integer and boolean), or a function type (α | τ | β) → (α′ |τ ′ | β ′ ). The function type may be understood as the type of afunction whose argument has the type τ with an effect of type α
to β, and whose return type is τ ′ with an effect of type α′ to β ′ .
Here, “an effect of type α to β” is a computational effect invokedby a shift-expression, which changes the answer type of the current
continuation from α to β. See [2] for the detailed discussion on theanswer-type modification. If there is no effect by a shift-expression,then α and β are the same type (which can be an arbitrary type[19].)We also define a context-type σ ⊲ τ where σ and τ are types. A
context-type is used for typing a delimited continuation, or a pureevaluation context.
A typing context Γ is a (possibly empty) set consisting ofx : (α | τ | β) and k : σ ⊲ τ . The former intuitively
means that an ordinary variable x has type τ with an effect oftype α to β, while the latter represents the type of a delimited
continuation corresponding to k. Since a delimited continuation isalways a pure function, we do not have to consider its effects, so
the type of k needs only two subtypes. A judgement takes the form
Γ | α ⊢ e : τ | β where Γ is a typing context, α, τ, β are types,
and e is an expression.
Fig. 8 gives the type system.
As Biernacka and Biernacki proved, the reduction rules in Fig. 2
enjoy the subject reduction property under this type system.

6.1 Type System
We define a type system for our call-by-name calculus with delimited control. The type system defined in this section is essentiallythe same as the type system by Biernacka and Biernacki modulo
the following modifications.

6.2 Typed CPS Translation
For the purpose of this paper, namely, axiomatization, we define a
CPS translation for the typed calculus. Not surprisingly, we use thesame CPS translation, the 2CPS translation in Fig. 4 for expressionsapp

in the typed calculus. The remaining task is to define the CPS
translation of types and typing contexts.
For a simple type4 A, we define ¬A as A →⊥ where ⊥ is anarbitrary fixed type.
def
The CPS translation of a type is defined by b∗ = b and((α | τ | β) → (α′ | τ ′ | β ′ ))∗def= ((τ ∗ → ¬¬α∗ ) → ¬¬β ∗ ) → ((τ ′∗ → ¬¬α′∗ ) → ¬¬β ′∗ )The definition above needs several occurrences of double negation¬¬ since we use 2CPS translation.
Finally, we define the CPS translation of a typing context as:
def(x : (α | τ | β))∗ = x : (τ ∗ → ¬¬α∗ ) → ¬¬β ∗def(k : σ ⊲ τ )∗ = k : σ ∗ → ¬¬τ ∗T HEOREM 4. If Γ | α ⊢ e : τ | β is derivable, then Γ∗ ⊢ [ e]] :(τ ∗ → ¬¬α∗ ) → ¬¬β ∗ is derivable in the simply typed lambda
calculus.
Proof. The theorem can be proved by induction on the derivationof Γ | α ⊢ e : τ | β.
6.3 Axiomatization
We now axiomatize the CPS semantics for the typed calculus.
Perhaps surprisingly, exactly the same axioms in Fig. 5 work forthe typed calculus.
T HEOREM 5 (Soundness and Completeness). Let e1 and e2 becbn
typed terms in λcbn
s/r , then ⊢s/r e1 = e2 if and only if ⊢CPS [ e1 ] =[ e2 ] .
Proof. Since the proof is mostly the same as the type-free case, weonly show an overview of the proof.
• We first establish that, if the term in the left-hand side of eachaxiom is typable, then the term in its right-hand side is typableand has the same typing judgement.
• We must check that all intermediate terms used in the complete-ness proof preserve the typing judgement.
• We must also check that the inverse translation preserves typ-ing, and also, if e is typable in the source calculus, [ e]]◦ has thesame typing judgement.
• Finally, we must check that the reductions in the target calculus

are mapped to typable equations in the source calculus.
We must check a lot of things, but each check can be done
straightforwardly.

7. Discussion on the use of linearity
We briefly discuss the use of linearity in the target of a CPS
translation, which plays a significant role in our proof.
A (rough) type structure of the image of the 2CPS translation
can be given as:
Term = Cont →1 MetaCont →2 Answer
Cont = Value →3 MetaCont →4 Answer
MetaCont = Value →5 Answer
where the indices 1, 2, . . . , 5 are for reference, and we have omitted
to write the definition of type Value. As we have seen, somefunction types can be refined to linear function types:
4 A simple type means a type in the simply typed lambda calculus.

[ c]]SR= λκ.κc2=x[ x]]SR2= λ(x, κ).[[e]]SR[ λx.e]]SR2 κ2SR= λκ.[[e1 ] SR
[ e1 e2 ] SR
2 ([[e2 ] 2 , κ)2

= λκ.([[e]]SR[ Sk.e]]SR
2 {k := κ})I2
2[ k ←֓ e]]SR= λκ.λγ.[[e]]SR22 k(κ ⊕ γ)
= λκ.λγ.[[e]]SR[ hei]]SR
2 I2 (κ ⊕ γ)
2
Figure 9. SR-style 2CPS Translation• →2 and →4 can be made linear function space ⊸, which cor-

responds to the metacontinuation variable γ. In the terminology
of Berdine et al. [3], it is a linearly used continuation.
• →3 and →5 can be made linear function space ⊸, whichcorresponds to the variable m. This linearity reflects the factthat evaluation contexts are linear, and is specific to the callby-name calculus. This is related to what Filinski called linear
continuations [9].
In our proof, we have used both linearity, hence →i for i =2, 3, 4, 5 is linear function space. The remaining (non-linear) function space →1 corresponds to the non-linear uses of delimited continuations, which are useful for representing, e.g., backtracking.
Berdine et al. [3] proposed to restrict this function space to be linear, and claimed that it is a “stylized” use of control.

8. Revisiting η -equality
We have argued the interaction between reset and full η-equality,
and concluded that we should give up full η-equality, because it isunsound with respect to the intended operational semantics.
However, there can be a typed calculus which admits full ηequality if the use of reset is limited. More precisely, if we restrict
the type of reset-terms to be basic types (no function types areallowed as the return type of any delimited continuation captured
by shift), we can formulate a calculus in which η-equality is sound.
To develop the semantics of such a calculus, we extend Streicher
and Reus’ CPS translation [18]. Fig. 9 gives a 2CPS translation for
λcbn
s/r as an extension of Streicher and Reus’ CPS translation.
The target calculus of this CPS translation is the simply typed
lambda calculus augmented with pairing, denoted by (t1 , t2 ). Pairs
are decomposed by an abstraction λ(x, y).t with the additional
equality (λ(x, y).t0 ) (t1 , t2 ) = t0 {x := t1 }{y := t2 }, andλ(x, y).e(x, y) = e for x, y 6∈ FV(e). It should be noted the CPS
translation preserves η-equality as:SR[ λx.ex]]SR=β λ(x, k).[[e]]SR22 (x, k) =pair [ e]]2

where =pair means the equality induced by the two equations forpairs.
Using the CPS translation in Fig. 9, we can develop yet anothertype system for λcbn
s/r . The type system obtained through Streicher
and Reus’ CPS translation is different from the one obtained by
Biernacka and Biernacki CPS translation.
We could axiomatize such a calculus in a similar way to thispaper. Unfortunately, the result is not really illuminating; the obtained axioms are the same axioms as those given in this paperwith η-equality (λx.ex = e for x 6∈ FV(e)) being added. Notethat a reset-term hei is restricted to be of basic types, and therefore
hλx.ei is not well-typed in this calculus.
We did not develop this calculus in this paper, because we do
not know any practical meaning of such a calculus.

9. Concluding Remarks

References

In this paper we have investigated the CPS semantics of the call-byname calculi with delimited-control operators. We have obtained asound and complete axiomatization for the calculus in the sensethat:[1] A. W. Appel. Compiling with Continuations. Cambridge University
Press, 1992. ISBN 0-521-41695-7.

⊢cbn
s/r e1 = e2 if and only if ⊢CPS [ e1 ] = [ e2 ] .
Since η-equality interferes with reset, our axioms for the source
calculus do not contain η-equality. We have proved that the same
axioms work for type-free and typed cases, where the type systemis (essentially) given by Biernacka and Biernacki.
Our theoretical tool was the 2CPS translation, which mixes acall-by-name translation with a call-by-value one. For the completeness proof, we need to use linearity of evaluation contexts
in a non-trivial way. Also we have formulated the source calculus
carefully so that lambda-bound variables and shift-bound variables
must be treated differently.
We also briefly mentioned yet another typed calculus for thecall-by-name shift and reset. In this calculus, η-equality is admittedwith no restriction, but the type of a reset-term hei is restricted to abasic type.
Although we do not claim that the calculus proposed by Biernacka and Biernacki (or our calculus as its small variant) is the right
one for call-by-name delimited control, we believe our results canbe basis for further study on call-by-name delimited-control.
Relation with Other Works. In this paper, we have concentrated on the delimited-control operators “shift” and “reset” in thestyle of Danvy and Filinski and of Biernacka and Biernacki, andhave not considered the relationship with others.
Herbelin and Ghilezan proposed a call-by-name calculus with
control operators and connected it with classical logic [11]. They
have obtained the calculus from the call-by-value calculus withdelimited-control operators, but the counterpart of the reset-operator
behaves quite differently from those presented in this paper. In their
ˆ tp]Mˆ
call-by-value calculus, hM i is represented by µtp.[
whereˆ is a variable for the top-level continuation. However, in theirtpcall-by-name calculus, this term reduces to M , so its behavior isquite different from the usual behavior of reset. Consequently, it isdifficult to relate their calculus with other calculi. Their calculus
is also different from the calculus in Section 8, since, in the latter
calculus hei = e does not hold if e has a basic type.
As an application of a call-by-name calculus with delimited
control, Kiselyov proposed to use it in linguistic analysis [13]. His
calculus has an explicit representation of evaluation contexts, andtherefore it is similar to Biernacka and Biernacki’s formulation. He
has not given a CPS translation for his calculus, so we do not know
if we can axiomatize his calculus as in this paper.
Future work. There are a number of future works, and let us
list only a few of them. (1) To investigate other delimited-control
operators such as Felleisen’s “control” and “prompt” in call-byname, and if possible axiomatizing them. (2) To relate the callby-name calculi with the call-by-value one in the sense of duality,
and also with classical logic. (3) To relate our calculus with logicbased calculi such as Herbelin and Ghilezan’s, and give the logicalaccount to “reset”.

Acknowledgments
We would like to thank Olivier Danvy, Masahito Hasegawa andOleg Kiselyov for insightful comments. Special thanks go toanonymous reviewers of FLOPS and PPDP, who have pointed out
errors in the earlier versions of this paper.
The first author was partly supported by JSPS Grant-in-Aid for
Scientific Research (B) 21300005.

[2] K. Asai and Y. Kameyama. Polymorphic Delimited Continuations. In
Proc. Asian Programming Languages and Systems, LNCS 4807, pages
239–254, Nov-Dec 2007.
[3] J. Berdine, P. O’Hearn, U. Reddy, and H. Thielecke.
LinearContinuation-Passing. Higher-Order and Symbolic Computation, 15(2-3):191–208, 2002.
[4] M. Biernacka and D. Biernacki. Context-based proofs of termination
for typed delimited-control operators. In PPDP 2009, pages 289–300,
2009.
[5] O. Danvy and A. Filinski. A Functional Abstraction of Typed Contexts. Technical Report 89/12, DIKU, University of Copenhagen, July
1989.
[6] O. Danvy and A. Filinski. Abstracting Control. In Proc. 1990 ACM
Conference on Lisp and Functional Programming, pages 151–160,
1990.
[7] O. Danvy and A. Filinski. Representing Control: a Study of the CPS
Transformation. Mathematical Structures in Computer Science, 2(4):361–391, 1992.
[8] M. Felleisen. The Theory and Practice of First-Class Prompts. In Proc.
15th Symposium on Principles of Programming Languages, pages
180–190, 1988.
[9] A. Filinski. Linear Continuations. In POPL, pages 27–38, 1992.
[10] C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence ofcompiling with continuations. In PLDI, pages 237–247, 1993.
[11] H. Herbelin and S. Ghilezan. An Approach to Call-by-Name Delimited Continuations. In POPL 2008, pages 383–394, 2008.
[12] Y. Kameyama and M. Hasegawa. A sound and complete axiomatization for delimited continuations. In ICFP, pages 177–188, 2003.
[13] O. Kiselyov. Call-by-name Linguistic Side Effects. In ESSLLI, 2008.
[14] E. Moggi. Computational lambda-calculus and monads. In LICS,
pages 14–23. IEEE Computer Society, 1989.
[15] M. Parigot. Lambda-my-calculus: An algorithmic interpretation ofclassical natural deduction. In A. Voronkov, editor, LPAR, volume 624
of Lecture Notes in Computer Science, pages 190–201. Springer, 1992.
ISBN 3-540-55727-X.
[16] G. D. Plotkin. Call-by-Name, Call-by-Value, and the λ-Calculus.
Theoretical Computer Science, 1: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] T. Streicher and B. Reus. Classical Logic, Continuations Semantics
and Abstract Machines. J. Functional Programming, 8(6):543–572,
1998.
[19] H. Thielecke. From Control Effects to Typed Continuation Passing. In
POPL, pages 139–149, New York, January 2003. ACM Press.