Chapter 5

Logical Relations for
Call-by-value Delimited
Continuations
Kenichi Asai1
Abstract: Logical relations, defined inductively on the structure of types, provide a powerful tool to characterize higher-order functions. They often enable
us to prove correctness of a program transformer written with higher-order functions concisely. This paper demonstrates that the technique of logical relations
can be used to characterize call-by-value functions as well as delimited continuations. Based on the traditional logical relations for call-by-name functions,logical relations for call-by-value functions are first defined, whose CPS variant
is used to prove the correctness of an offline specializer for the call-by-value λcalculus. They are then modified to cope with delimited continuations and areused to establish the correctness of an offline specializer for the call-by-value λcalculus with delimited continuation constructs, shift and reset. This is the firstcorrectness proof for such a specializer. Along the development, correctness ofthe continuation-based and shift/reset-based let-insertion and A-normalization isestablished.
5.1 INTRODUCTION
Whenever we build a program transformer, be it a compiler, an optimizer, or a
specializer, we need to establish its correctness. We have to show that the semantics of a program does not change before and after the transformation. As
a program transformer gets sophisticated, however, it becomes harder to proveits correctness. In particular, the non-trivial use of higher-order functions in thetransformer makes the correctness proof particularly difficult. A simple structural
1 Ochanomizu University, 2-1-1 Otsuka, Bunkyo-ku, Tokyo 112-8610, Japan; Email:asai@is.ocha.ac.jp

63induction on the input program does not usually work, because we can not easily
characterize their behavior.
The technique of logical relations [16] is one of the proof methods that is often
used in such a case. With the help of types, it enables us to define a set of relations
that captures necessary properties of higher-order functions. Notably, Wand [20]used this technique to prove correctness of an offline specializer [14] in whichhigher-order functions rather than closures were used for the representation of
abstractions. However, the logical relations used by Wand were for call-by-namefunctions. They were used to prove the correctness of a specializer for the call-byname λ-calculus, but are not directly applicable to the call-by-value languages.
In this paper, we demonstrate that the technique of logical relations can beused to characterize call-by-value functions as well as delimited continuations.
We first modify Wand’s logical relations so that we can use them for call-by-valuefunctions. We then prove the correctness of an offline specializer for the call-byvalue λ-calculus. It is written in continuation-passing style (CPS) and uses thecontinuation-based let-insertion to avoid computation elimination/duplication.
It is well-known that by using delimited continuation constructs, shift and reset, introduced by Danvy and Filinski [7], it is possible to implement the letinsertion in direct style [18]. We demonstrate that the correctness of this directstyle specializer with the shift/reset-based let-insertion can be also established byproperly characterizing delimited continuations in logical relations.
Then, the specializer is extended to cope with shift and reset in the source
language. To this end, the specialization-time delimited continuations are used
to implement the delimited continuations in the source language. To characterize such delimited continuations, we define logical relations based on Danvy andFilinski’s type system [6]. Thanks to the explicit reference to the types of continuations and the final result, we can establish the correctness of the specializer.
This is the first correctness proof for the offline specializer for the call-by-value
λ-calculus with shift and reset. The present author previously showed the correctness of a similar offline specializer [3], but it produced the result of specializationin CPS.
The contributions of this paper are summarized as follows:• We show that the technique of logical relations can be used to characterize
call-by-value functions as well as delimited continuations.
• We show for the first time the correctness of the offline specializer for thecall-by-value λ-calculus with shift and reset.
• Along the development, we establish the correctness of the continuation-based
let-insertion, the shift/reset-based let-insertion, the continuation-based A-normalization [13], and the shift/reset-based A-normalization.
The paper is organized as follows. After showing preliminaries in Section 5.2,
the call-by-name specializer and its correctness proof by Wand are reviewed in
Section 5.3. We then show the logical relations for call-by-value functions in
64Section 5.4, and use (a CPS variant of) them to prove the correctness of a specializer for the call-by-value λ-calculus in Section 5.5. In Section 5.6, we transform the specializer into direct style and prove its correctness. Then, we further extend the specializer to cope with shift and reset. We show an interpreterand an A-normalizer in Section 5.7, a specializer in Section 5.8, a type system
in Section 5.9, and logical relations with which the correctness is established in
Section 5.10. Related work is in Section 5.11 and the paper concludes in Section 5.12. A complete proof of correctness of the offline specializer for shift andreset is found in the technical report [4].
ACKNOWLEDGMENTS
Most of the work has been done while the author was visiting Northeastern University. Special thanks to Mitch Wand for hosting my stay as well as supportand encouragements. The use of de Bruijn levels to avoid the name generation
problem was suggested by Olivier Danvy.
5.2 PRELIMINARIESThe metalanguage we use is a left-to-right λ-calculus extended with shift and reset
as well as datatype constructors. The syntax is given as follows:
M, K= x | λx. M | M M | ξk. M | hMi | n | M + 1 |Var(n) | Lam(n, M) | App(M, M) | Shift(n, M) | Reset(M) |Lam(n, M) | App(M, M) | Shift(n, M) | Reset(M) |Lam(n, M) | App(M, M) | Shift(n, M) | Reset(M)ξk. M and hMi represent shift and reset, respectively, and appear only later in thepaper. Datatype constructors are for representing the input and output terms to our
specializer. In this baselanguage, an integer n is used to represent a variable. For
this purpose, the language contains an integer and an add-one operation. As usual,
we use overline and underline to indicate static and dynamic terms, respectively.
We assume that all the datatype constructors are strict. Among the metalanguage,a value (ranged over by a metavariable V ) is either a variable, an abstraction, an
integer, or one of constructors whose arguments are values.
When a specializer produces its output, it needs to generate fresh variables.
To make the presentation simple, we use so-called the de Bruijn levels [9] (notindices). Define the following five strict operators:var(m)lam( f )app( f1 , f2 )shift( f )reset( f )

=
=
=
=
=

λn. Var(m)λn. Lam(n, f (n + 1))
λn. App( f1 n, f2 n)
λn. Shift(n, f (n + 1))
λn. Reset( f n)

They are used to represent a term parameterized with a variable name. Given aterm M in the de Bruijn level notation, we define the operation ↓n M of obtaining65

a concrete term as: ↓n M = M n. Thus, we have:↓3 (app(lam(λx. lam(λy. var(x))), lam(λy. var(y))))= App(Lam(3, Lam(4, Var(3))), Lam(3, Var(3))) .
Since we can freely transform a term with de Bruijn levels into the one without,
we will use the former as the output of specializers.
Throughout this paper, we use three kinds of equalities between terms in themetalanguage: = for definition or α-equality, ∼n for β-equality under call-byname semantics, and ∼v for β-equality under call-by-value semantics. The callby-value β-equality in the presence of shift and reset is defined by Kameyama andHasegawa [15, Fig. 2].
5.3 SPECIALIZER FOR CALL-BY-NAME λ-CALCULUS
In this section, we review the specializer for the call-by-name λ-calculus and its
correctness proof using the technique of logical relations presented by Wand [20].
A specializer reduces expressions that are known (or static) at specialization
time and leaves unknown (or dynamic) expressions intact. Thus, it consists of
two parts: an interpreter for static expressions and a residualizer for dynamic
expressions. An interpreter for the input language is defined as follows:

I 1 [[Var(n)]] ρ = ρ (n)I 1 [[Lam(n, M)]] ρ = λx. I 1 [[M]] ρ[x/n]I 1 [[App(M1 , M2 )]] ρ = (I 1 [[M1 ]] ρ) (I 1 [[M2 ]] ρ)
where ρ[x/n] is the same environment as ρ except that ρ (n) = x.
The residualizer is almost the identity function except for the use of de Bruijn
levels to avoid name clashes:

D 1 [[Var(n)]] ρ = ρ (n)D 1 [[Lam(n, M)]] ρ = lam(λx. D 1 [[M]] ρ[var(x)/n])D 1 [[App(M1 , M2 )]] ρ = app(D 1 [[M1 ]] ρ, D 1 [[M2 ]] ρ)
An offline specializer is given by putting the interpreter and the residualizer
together:

P 1 [[Var(n)]] ρ = ρ (n)P 1 [[Lam(n,W )]] ρ = λx. P 1 [[W ]] ρ[x/n]P 1 [[Lam(n,W )]] ρ = lam(λx. P 1 [[W ]] ρ[var(x)/n])P 1 [[App(W1 ,W2 )]] ρ = (P 1 [[W1 ]] ρ) (P 1 [[W2 ]] ρ)
P 1 [[App(W1 ,W2 )]] ρ = app(P 1 [[W1 ]] ρ, P 1 [[W2 ]] ρ)
The specializer goes wrong if the input term is not well-annotated. Well-annotatedness of a term is specified as a binding-time analysis that, given an unannotatedterm, produces a well-annotated term. Here, we show a type-based binding-time
analysis. Define binding-time types of expressions as follows:τ = d |τ→τ66

An expression of type d denotes that the expression is dynamic, while an expression of type τ → τ shows that it is a static function. We use a judgment of theform A ` M : τ [W ], which reads: under a type environment A, a term M has abinding-time type τ and is annotated as W . The binding-time analysis is definedby the following typing rules:
A[n : τ] ` Var(n) : τ [Var(n)]A[n : σ] ` M : τ [W ]A ` M1 : σ → τ [W1 ] A ` M2 : σ [W2 ]A ` Lam(n, M) : σ → τ [Lam(n,W )]A ` App(M1 , M2 ) : τ [App(W1 ,W2 )]A[n : d] ` M : d [W ]A ` Lam(n, M) : d [Lam(n,W )]A ` M1 : d [W1 ] A ` M2 : d [W2 ]A ` App(M1 , M2 ) : d [App(W1 ,W2 )]To show the correctness of the specializer, Wand [20] uses the technique oflogical relations. Define logical relations between terms in the metalanguage by
induction on the structure of binding-time types as follows:(M, M 0 ) ∈ Rd
(M, M 0 ) ∈ Rσ→τ⇐⇒ I 1 [[↓n M]] ρid ∼n M 0 for any large n (defined below)⇐⇒ ∀(N, N 0 ) ∈ Rσ . (M N, M 0 N 0 ) ∈ Rτwhere ρid (n) = zn for all n. It relates free variables in the base- and metalanguage.
Since the logical relations are defined on open terms, we need to relate free variables in the base- and metalanguage in some way. We choose here to relate abaselanguage variable Var(n) to a metalanguage variable zn .
In the definition of Rd , M is a metalanguage term in the de Bruijn level notationthat is either a value representing a baselanguage term or a term that is equal to (orevaluates to) a value representing a baselanguage term in the underlying semanticsof the metalanguage (in this section, call-by-name).
The choice of n in Rd needs a special attention. Since M is possibly an open
term, n has to be chosen so that it does not capture free variables in M. We ensure
this property by the side condition “for any large n.” n is defined to be large if n isgreater than any free variables in the baselanguage term M.
For environments ρ and ρ0 , we say (ρ, ρ0 ) |= A iff (ρ (n), ρ0 (n)) ∈ RA(n) for alln ∈ dom(A), where dom(A) is the domain of A. Then, we can show the following
theorem by structural induction over types:
Theorem 5.1 (Wand [20]). If A ` M : τ [W ] and (ρ, ρ0 ) |= A, then(P 1 [[W ]] ρ, I 1 [[M]] ρ0 ) ∈ Rτ .
By instantiating it to an empty environment ρφ , we obtain the following corollary,which establishes the correctness of specialization.
Corollary 5.2 (Wand [20]). If ` M : d [W ], then I 1 [[↓0 (P 1 [[W ]] ρφ )]] ρid ∼n I 1 [[M]] ρφ .
67

5.4 LOGICAL RELATIONS FOR CALL-BY-VALUE λ-CALCULUS
Define logical relations for the call-by-value λ-calculus as follows:(M, M 0 ) ∈ Rd
(M, M 0 ) ∈ Rσ→τ⇐⇒ I 1 [[↓n M]] ρid ∼v M 0 for any large n⇐⇒ ∀(V,V 0 ) ∈ Rσ . (MV, M 0 V 0 ) ∈ RτThere are two differences from the logical relations in the previous section. First,
call-by-value equality ∼v is used instead of call-by-name equality ∼n in the definition of Rd . Secondly, M and M 0 are allowed to be in Rσ→τ if they transform
only related values (rather than arbitrary terms) into related terms.
If we could prove Theorem 5.1 with this definition of Rτ , we would haveobtained as a corollary the correctness of the specializer in the call-by-value semantics. However, the proof fails for static applications. In fact, the specializer is
not correct under the call-by-value semantics.
5.5 SPECIALIZER IN CPS
The correctness under the call-by-value semantics does not hold for the specializer in Section 5.3 because it may discard a non-terminating computation. The
standard method to recover the correctness is to perform let-insertion [5]. Since
let-insertion requires explicit manipulation of continuations, we first rewrite our
specializer into CPS as follows:

P 2 [[Var(n)]] ρ κ = κ (ρ (n))
P 2 [[Lam(n,W )]] ρ κ = κ (λx. λk. P 2 [[W ]] ρ[x/n] k)
P 2 [[Lam(n,W )]] ρ κ = κ (lam(λx. P 2 [[W ]] ρ[var(x)/n] λx. x))
P 2 [[App(W1 ,W2 )]] ρ κ = P 2 [[W1 ]] ρ λm. P 2 [[W2 ]] ρ λn. m n κ
P 2 [[App(W1 ,W2 )]] ρ κ = P 2 [[W1 ]] ρ λm. P 2 [[W2 ]] ρ λn. κ (app(m, n))
We then replace the last rule with the following:

P 2 [[App(W1 ,W2 )]] ρ κ = P 2 [[W1 ]] ρ λm. P 2 [[W2 ]] ρ λn.

let(app(m, n), lam(λt. κ (var(t))))where let(M1 , lam(λt. M2 )) is an abbreviation for app(lam(λt. M2 ), M1 ). Whenever an application is residualized, we insert a let-expression to residualize it exactly once with a unique name t, and continue the rest of the specialization withthis name. Since the residualized application is not passed to the continuation κ,
it will never be discarded even if κ discards its argument.
The let-insertion technique can be regarded as performing A-normalization[13] on the fly during specialization. If we extract the rules for variables, dynamic
abstractions, and dynamic applications from P 2 , we obtain the following one-pass
A-normalizer written in CPS [13]:A 1 [[Var(n)]] ρ κ = κ (ρ (n))
A 1 [[Lam(n, M)]] ρ κ = κ (lam(λx. A 1 [[M]] ρ[var(x)/n] λx. x))
A 1 [[App(M1 , M2 )]] ρ κ = A 1 [[M1 ]] ρ λm. A 1 [[M2 ]] ρ λn.
let(app(m, n), lam(λt. κ (var(t))))68

We now want to show the correctness of the specializer P 2 under the callby-value semantics. Namely, we want to show I 1 [[↓0 (P 2 [[W ]] ρφ λx. x)]] ρid ∼v
I 1 [[M]] ρφ along the similar story as we did in Section 5.3. Let us define the basecase Rd as follows:⇐⇒ I 1 [[↓n M]] ρid ∼v M 0 for any large n .

(M, M 0 ) ∈ Rd

Then, we want to show (P 2 [[W ]] ρφ λx. x, I 1 [[M]] ρφ ) ∈ Rd with a suitable definition of Rσ→τ . To prove it, we first generalize the statement to make induction
work. Rather than proving only the case where environments and continuations
are the empty ones, we prove something like:(P 2 [[W ]] ρ λv. K, (λv0 . K 0 ) (I 1 [[M]] ρ0 )) ∈ Rτfor some suitable ρ, ρ0 , λv. K, and λv0 . K 0 . Since I 1 is written in direct style, we
introduce its continuation as a form of a direct application.
Now, how can we define Rσ→τ ? Unlike Section 5.3, it is not immediately clear
how to define Rσ→τ because the specializer is written in CPS. We need to relate
P 2 [[W ]] ρ λv. K and (λv0 . K 0 ) (I 1 [[M]] ρ0 ) properly. To do so, we need to characterize precisely the two continuations, λv. K and λv0 . K 0 , and the final results. Goingback to the definition of P 2 , we notice two things:• P 2 [[W ]] ρ λv. K as a whole returns a dynamic expression.
• λv. K returns a dynamic expression, given some value v.
In ordinary CPS programs, the return type of continuations is polymorphic. It canbe of any type, usually referred to as a type Answer. Here, we used continuations
in a non-standard way, however. We instantiated the Answer type into a type ofdynamic expressions and used it to construct dynamic expressions.
Taking into account that the type of dynamic expressions is d, the above observation leads us to the following definition of logical relations:(M, M 0 ) ∈ Rd
(M, M 0 ) ∈ Rσ→τ⇐⇒ I 1 [[↓n M]] ρid ∼v M 0 for any large n⇐⇒ ∀(V,V 0 ) ∈ Rσ . ∀(λv. K, λv0 . K 0 ) |= τ ; d.
(M V λv. K, (λv0 . K 0 ) (M 0 V 0 )) ∈ Rd

where (λv. K, λv0 . K 0 ) |= τ ; d is simultaneously defined as follows:(λv. K, λv0 . K 0 ) |= τ ; d⇐⇒ ∀(V,V 0 ) ∈ Rτ . ((λv. K)V, (λv0 . K 0 )V 0 ) ∈ Rd

Intuitively, (λv. K, λv0 . K 0 ) |= τ ; d means that λv. K and λv0 . K 0 are related continuations that, given related values of type τ, produce related results of type d.
Using this definition, (M, M 0 ) ∈ Rσ→τ states that M and M 0 are related if they
produce related results of type d, given related values of type σ and related continuations of type τ ; d. In the following, we use ; for the type of continuations.
With this definition of logical relations, we can prove the correctness of P 2
under the call-by-value semantics.
69

Theorem 5.3. If A ` M : τ [W ], (ρ, ρ0 ) |= A, and (λv. K, λv0 . K 0 ) |= τ ; d, then(P 2 [[W ]] ρ λv. K, (λv0 . K 0 ) (I 1 [[M]] ρ0 )) ∈ Rd .
The proof of this theorem is by induction on the structure of the proof of A `M : τ [W ]. Even though P 2 is written in CPS, the induction does work thanks tothe explicit reference to the types of continuations and the final result. The proof
proceeds in a CPS manner. In particular, the cases for (both static and dynamic)
applications go from left to right. We use the induction hypotheses for the function
part and the argument part in this order.
By instantiating the theorem to the case where both the environment and thecontinuation are empty, we obtain the following corollary that establishes the correctness of a specializer using the continuation-based let-insertion:
Corollary 5.4. If ` M : d [W ], then I 1 [[↓0 (P 2 [[W ]] ρφ λx. x)]] ρid ∼v I 1 [[M]] ρφ .
If we annotate the input to the specializer completely dynamic, the specializer behaves exactly the same as the A-normalizer. Thus, the theorem can be instantiatedto the following corollary, which proves the correctness of the continuation-based
A-normalization.
Corollary 5.5. I 1 [[↓0 (A 1 [[M]] ρφ λx. x)]] ρid ∼v I 1 [[M]] ρφ for any closed M.
5.6 SPECIALIZER IN DIRECT STYLE
In this section, we present a specializer written in direct style and show its correctness under the call-by-value semantics. Since we have already established thecorrectness of a specializer written in CPS in the previous section, the development in this section is easy. Roughly speaking, we transform the results in theprevious section back to direct style [8]. During this process, we use the firstclass delimited continuation constructs, shift and reset, to cope with non-standard
use of continuations. Intuitively, shift captures the current continuation up to its
enclosing reset [7]. Here is the definition of the specializer written in direct style:P 3 [[Var(n)]] ρ = ρ (n)P 3 [[Lam(n,W )]] ρ = λx. P 3 [[W ]] ρ[x/n]P 3 [[Lam(n,W )]] ρ = lam(λx. hP 3 [[W ]] ρ[var(x)/n]i)
P 3 [[App(W1 ,W2 )]] ρ = (P 3 [[W1 ]] ρ) (P 3 [[W2 ]] ρ)
P 3 [[App(W1 ,W2 )]] ρ = ξκ. let(app(P 3 [[W1 ]] ρ, P 3 [[W2 ]] ρ), lam(λt. κ (var(t))))As in the previous section, we obtain the one-pass A-normalizer written in
direct style with shift and reset [3] by extracting dynamic rules from P 3 :

A 2 [[Var(n)]] ρ = ρ (n)A 2 [[Lam(x, M)]] ρ = lam(λx. hA 2 [[M]] ρ[var(x)/n]i)
A 2 [[App(M1 , M2 )]] ρ = ξκ. let(app(A 2 [[M1 ]] ρ, A 2 [[M2 ]] ρ), lam(λt. κ (var(t))))To define suitable logical relations for the specializer written in direct style(with shift and reset), we need to correctly handle delimited continuations. This70

is done by observing the exact correspondence between continuations in the previous section and delimited continuations in this section. In particular, we typethe result of the delimited continuations as d.
Logical relations for the direct-style specializer with delimited continuations
are defined as follows:(M, M 0 ) ∈ Rd
(M, M 0 ) ∈ Rσ→τ⇐⇒ I 1 [[↓n M]] ρid ∼v M 0 for any large n⇐⇒ ∀(V,V 0 ) ∈ Rσ . ∀(λv. K, λv0 . K 0 ) |= τ ; d.
(h(λv. K) (M V )i, (λv0 . K 0 ) (M 0 V 0 )) ∈ Rd

where (λv. K, λv0 . K 0 ) |= τ ; d is simultaneously defined as follows:(λv. K, λv0 . K 0 ) |= τ ; d⇐⇒ ∀(V,V 0 ) ∈ Rτ . (h(λv. K)V i, (λv0 . K 0 )V 0 ) ∈ Rd

Then, the correctness of the specializer is stated as follows:
Theorem 5.6. If A ` M : τ [W ], (ρ, ρ0 ) |= A, and (λv. K, λv0 . K 0 ) |= τ ; d, then(h(λv. K) (P 3 [[W ]] ρ)i, (λv0 . K 0 ) (I 1 [[M]] ρ0 )) ∈ Rd .
Although both the specializer and the interpreter are written in direct style, theproof proceeds in a CPS manner. In particular, the cases for applications go fromleft to right, naturally reflecting the call-by-value semantics.
By instantiating the theorem to the case where both the environment and thecontinuation are empty, we obtain the following corollary that establishes the correctness of a specializer using the shift/reset-based let-insertion:
Corollary 5.7. If ` M : d [W ], then I 1 [[↓0 hP 3 [[W ]] ρφ i]] ρid ∼v I 1 [[M]] ρφ .
As before, if we annotate the input to the specializer completely dynamic, thespecializer behaves exactly the same as the A-normalizer. Thus, the theorem canbe instantiated to the following corollary, which proves the correctness of thedirect-style A-normalization.
Corollary 5.8. I 1 [[↓0 hA 2 [[M]] ρφ i]] ρid ∼v I 1 [[M]] ρφ for any closed M.
5.7 INTERPRETER AND A-NORMALIZER FOR SHIFT AND RESET
So far, shift and reset appeared only in the metalanguage. In the following sections, we develop a specializer written in direct style that can handle shift andreset in the baselanguage. We first define an interpreter, a residualizer, and an
A-normalizer for the call-by-value λ-calculus with shift and reset. We then try to
combine the interpreter and the A-normalizer to obtain a specializer in the next
section. Here is the interpreter written in direct style:I 2 [[Var(n)]] ρ = ρ (n)I 2 [[Lam(n, M)]] ρ = λx. I 2 [[M]] ρ[x/n]
I 2 [[App(M1 , M2 )]] ρ = (I 2 [[M1 ]] ρ) (I 2 [[M2 ]] ρ)
I 2 [[Shift(n, M)]] ρ = ξk. I 2 [[M]] ρ[k/n]
I 2 [[Reset(M)]] ρ = hI 2 [[M]] ρi71

We used shift and reset operations themselves to interpret shift and reset expressions. A residualizer is defined as follows:

D 2 [[Var(n)]] ρ = ρ (n)D 2 [[Lam(n, M)]] ρ = lam(λx. D 2 [[M]] ρ[var(x)/n])D 2 [[App(M1 , M2 )]] ρ = app(D 2 [[M1 ]] ρ, D 2 [[M2 ]] ρ)
D 2 [[Shift(n, M)]] ρ = shift(λk. D 2 [[M]] ρ[var(k)/n])D 2 [[Reset(M)]] ρ = reset(D 2 [[M]] ρ)It simply renames bound variables and keeps other expressions unchanged. As before, this residualizer is not suitable for specializers. We instead use the following
A-normalizer:

A 3 [[Var(n)]] ρ = ρ (n)A 3 [[Lam(n, M)]] ρ = lam(λx. hA 3 [[M]] ρ[var(x)/n]i)
A 3 [[App(M1 , M2 )]] ρ = ξk. let(app(A 3 [[M1 ]] ρ, A 3 [[M2 ]] ρ), lam(λt. k (var(t))))A 3 [[Shift(n, M)]] ρ = shift(λk. hA 3 [[M]] ρ[var(k)/n]i)
A 3 [[Reset(M)]] ρ = reset(hA 3 [[M]] ρi)
It replaces all the application expressions in the body of abstractions, shift expressions, and reset operations with a sequence of let-expressions.
5.8 SPECIALIZER FOR SHIFT AND RESETIn this section, we show a specializer for the call-by-value λ-calculus with shift
and reset. Our first attempt is to combine the interpreter and the A-normalizer as
we did before for the calculi without shift and reset:

P 4 [[Var(n)]] ρ = ρ (n)P 4 [[Lam(n,W )]] ρ = λx. P 4 [[W ]] ρ[x/n]P 4 [[Lam(n,W )]] ρ = lam(λx. hP 4 [[W ]] ρ[var(x)/n]i)
P 4 [[App(W1 ,W2 )]] ρ = (P 4 [[W1 ]] ρ) (P 4 [[W2 ]] ρ)
P 4 [[App(W1 ,W2 )]] ρ = ξk. let(app(P 4 [[W1 ]] ρ, P 4 [[W2 ]] ρ), lam(λt. k (var(t))))P 4 [[Shift(n,W )]] ρ = ξk. P 4 [[W ]] ρ[k/n]P 4 [[Shift(n,W )]] ρ = shift(λk. hP 4 [[W ]] ρ[var(k)/n]i)
P 4 [[Reset(W )]] ρ = hP 4 [[W ]] ρi
P 4 [[Reset(W )]] ρ = reset(hP 4 [[W ]] ρi)
Although this specializer does seem to work for carefully annotated inputs, it ishard to specify the well-annotated term as a simple binding-time analysis. The
difficulty comes from the inconsistency between the specialization-time continuation and the runtime continuation.
In the rule for the static shift, a continuation is grabbed at specialization time,
which means that we implicitly assume the grabbed continuation coincides withthe actual continuation at runtime. This was actually true for the interpreter: we
implemented shift in the baselanguage using shift in the metalanguage. In the72specializer, however, the specialization-time continuation does not always coincide with the actual continuation. To be more specific, in the rule for dynamic
abstractions, we specialize the body W in a static reset (i.e., in the empty continuation) to perform A-normalization, but the actual continuation at the time when
W is executed is not necessarily the empty one. Rather, it is the one when the
abstraction is applied at runtime.
Given that the specialization-time continuation is not always consistent withthe actual one, we have to make sure that the continuation is captured statically
only when it represents the actual one. Furthermore, we have to make sure thatwhenever shift is residualized, its enclosing reset is also residualized. One way toexpress this information in the type system would be to split all the typing rules
into two, one for the case when the specialization-time continuation and the actual
continuation coincide (or, the continuation is known, static) and the other for thecase when they do not (the continuation is unknown, dynamic). We could thenstatically grab the continuation only when it represents the actual one.
However, this solution leads to an extremely weak specialization. Unless an
enclosing reset is known at specialization time, we cannot grab continuations statically. Thus, under dynamic abstractions, no shift operation is possible at specialization time. Furthermore, because we use a type-based binding-time analysis,
it becomes impossible to perform any specialization under dynamic abstractions.
Remember that a type system does not tell us what subexpressions appear in agiven expression, but only the type of the given expression. From a type system,
we cannot distinguish the expression that does not contain any shift expressions
from the one that does. Thus, even if W1 turns out to have a static function typein App(W1 ,W2 ) (and thus it appears that this application can be performed statically), we cannot actually perform this application, because the toplevel operatorof W1 might be a shift operation that passes a function to the grabbed continuation. In other words, we cannot determine the binding-time of App(W1 ,W2 ) fromthe binding-time of W1 , which makes it difficult to construct a simple type-based
binding-time analysis.
The solution we employ takes a different approach. We maintain the consistency between specialization-time continuations and actual ones all the time. In
other words, we make the continuation always static. The modified specializer ispresented as follows:

P 5 [[Var(n)]] ρ = ρ (n)P 5 [[Lam(n,W )]] ρ = λx. P 5 [[W ]] ρ[x/n]P 5 [[Lam(n,W )]] ρ = lam(λx. shift(λk. hreset(app(var(k), P 5 [[W ]] ρ[var(x)/n]))i))
P 5 [[App(W1 ,W2 )]] ρ = (P 5 [[W1 ]] ρ) (P 5 [[W2 ]] ρ)
P 5 [[App(W1 ,W2 )]] ρ = ξk. reset(let(app(P 5 [[W1 ]] ρ, P 5 [[W2 ]] ρ), lam(λt. k (var(t)))))
P 5 [[Shift(n,W )]] ρ = ξk. P 5 [[W ]] ρ[k/n]P 5 [[Shift(n,W )]] ρ = ξk. P 5 [[W ]] ρ[lam(λv. hk (var(v))i)/n]
P 5 [[Reset(W )]] ρ = hP 5 [[W ]] ρi
There are four changes from P 4 . The first and the most important change is in therule for dynamic abstractions. Rather than specializing the body W of a dynamic
73

abstraction in the empty context, we specialize it in the context reset(app(var(k), ·)).
This specialization-time continuation reset(app(var(k), ·)) turns out to be consistent with the runtime continuation, because the variable k is bound in the dynamic
shift placed directly under the dynamic abstraction and represents the continuation when the abstraction is applied at runtime.
The second change is in the rule for dynamic applications where dynamic resetis inserted around the residualized let-expression. The third change is in the rulefor dynamic shift. Rather than residualizing a dynamic shift, which requires residualization of the corresponding reset, the current continuation is grabbed and it isturned into a dynamic expression via η-expansion. Finally, the rule for dynamic
reset is removed since all the shift operations are taken care of during specialization time, and there is no need to residualize reset. (This does not necessarilymean that the result of specialization does not contain any reset expressions. Resetis residualized in the rule for dynamic abstractions and applications.)
These changes not only define a correct specializer but result in a quite powerful one. It can now handle partially static continuations. Consider the term
Lam( f , Lam(x, App(Var( f ), Shift(k, App(Var(k), App(Var(k), Var(x))))))). (Thisterm is well-annotated in the type system shown in the next section.) When we
specialize this term, the continuation k grabbed by Shift(k, · · ·) is partially static:
we know that the first thing to do when k is applied is to pass its argument tof , but the computation that should be performed after that is unknown. It is thecontinuation when Lam(x, · · ·) is applied to an argument. Even in this case, P 5
can expand this partial continuation into the result of specialization. By naming
the unknown continuation h, P 5 produces the following output (after removing
unnecessary dynamic shift and inlining the residualized let-expressions):lam(λ f . lam(λx. shift(λh.
reset(app(var(h), app(var( f ), reset(app(var(h), app(var( f ), var(x)))))))))) .
Observe that the partial continuation reset(app(var(h), app(var( f ), ·))) is expanded
twice in the result. If f were static, we could have been able to perform further
specialization, exploiting the partially static information of the continuation.
On the other hand, the above changes cause an interesting side-effect to theresult of specialization: all the residualized lambda abstractions now have a ‘standardized’ form lam(λx. shift(λk. · · ·)) (and this is the only place where shift isresidualized). In particular, even when we specialize Lam(x,W ) where shift is
not used during the evaluation of W , the residualized abstraction has typically theform lam(λx. shift(λk. reset(app(var(k), M)))) where k does not occur free in M.
(If let-expressions are inserted, the result becomes somewhat more complicated.)
If we used P 3 instead, we would have obtained the equivalent but simpler result:lam(λx. M). In other words, P 5 is not a conservative extension of P 3 .
A question then is whether it is possible to obtain the latter result on the fly
using P 5 with some extra work. We expect that it is not likely. As long as asimple type-based binding-time analysis is employed, it is impossible to tell if
the execution of the body of a dynamic abstraction includes any shift operations.
So, unless we introduce some extra mechanisms to keep track of this information,74

there is no way to avoid the insertion of a dynamic shift in the rule for dynamic
abstractions. Then, rather than making the specializer complicated, we would
employ a simple post-processing to remove unnecessary shift expressions.
5.9 TYPE SYSTEM FOR SHIFT AND RESET
Since our proof technique relies on the logical relations, we need to define a typesystem for the call-by-value λ-calculus with shift and reset to prove the correctness of P 5 . In this section, we briefly review Danvy and Filinski’s type system[6]. More thorough explanation is found in [3, 6].
In the presence of first-class (delimited) continuations, we need to explicitly
specify the types of continuations and the final result. For this purpose, Danvy
and Filinski use a judgment of the form A, α ` M : τ, β [W ]. It reads: under thetype assumption A, an expression M has a type τ in a continuation of type τ ; αand the final result is of type β. Since we use this type system as the static part ofour binding-time analysis, we decorate it with [W ] to indicate that M is annotatedas W . If M does not contain any shift operations, the types α and β are always thesame, namely, the Answer type. In the presence of shift and reset, however, they
can be different and of any type.
The type of functions also needs to include the types of continuations and thefinal result. It has the form: σ/α → τ/β. It is a type of functions that receive an
argument of type σ and returns a value of type τ to a continuation of type τ ; αand the final result is of type β. As a result, types are specified as follows:τ= d | τ/τ → τ/τ .

Here goes the type system:
A[n : τ], α ` Var(n) : τ, α [Var(n)]A[n : σ], α ` M : τ, β [W ]A, σ ` M : σ, τ [W ]A, δ ` Lam(n, M) : σ/α → τ/β, δ [Lam(n,W )] A, α ` Reset(M) : τ, α [Reset(W )]A, δ ` M1 : σ/α → τ/ε, β [W1 ]A, ε ` M2 : σ, δ [W2 ]A[n : τ/δ → α/δ], σ ` M : σ, β [W ]A, α ` App(M1 , M2 ) : τ, β [App(W1 ,W2 )] A, α ` Shift(n, M) : τ, β [Shift(n,W )]The above type system is a generalization of the standard type system wheretypes of continuations are made explicit. In Section 5.6, the result type of continuations and the type of final results were always d. In the above type system, itmeans that a judgment had always the form A, d ` M : τ, d [W ] and the function
type had always the form σ/d → τ/d. So if we write them as A ` M : τ [W ] andσ → τ, respectively, we obtain exactly the same type system as the one for theordinary λ-calculus (the three static rules shown in Section 5.3).
The dynamic rules can be obtained by simply replacing all the static function
types with d (and types that occur within the function type). The dynamic rules
75are as follows:A[n : d], d ` M : d, d [W ]A[n : d], σ ` M : σ, β [W ]A, δ ` Lam(n, M) : d, δ [Lam(n,W )] A, d ` Shift(n, M) : d, β [Shift(n,W )]A, δ ` M1 : d, β [W1 ] A, d ` M2 : d, δ [W2 ]A, d ` App(M1 , M2 ) : d, β [App(W1 ,W2 )]5.10 LOGICAL RELATIONS FOR SHIFT AND RESETIn this section, we define the logical relations for the call-by-value λ-calculus
with shift and reset, which are used to prove the correctness of the specializer P 5
presented in Section 5.8. They are the generalization of the logical relations in
Section 5.6 in that the types of the final result and the result of continuations are
not restricted to d.
(M, M 0 ) ∈ Rd
(M, M 0 ) ∈ Rσ/α→τ/β⇐⇒ I 1 [[↓n M]] ρid ∼v M 0 for any large n⇐⇒ ∀(V,V 0 ) ∈ Rσ . ∀(λv. K, λv0 . K 0 ) |= τ ; α.
(h(λv. K) (M V )i, h(λv0 . K 0 ) (M 0 V 0 )i) ∈ Rβ

where (λv. K, λv0 . K 0 ) |= τ ; α is simultaneously defined as follows:(λv. K, λv0 . K 0 ) |= τ ; α⇐⇒ ∀(V,V 0 ) ∈ Rτ . (h(λv. K)V i, h(λv0 . K 0 )V 0 i) ∈ RαThen, the correctness of the specializer is stated as follows:
Theorem 5.9. If A, α ` M : τ, β [W ], (ρ, ρ0 ) |= A, and (λv. K, λv0 . K 0 ) |= τ ; α,then (h(λv. K) (P 5 [[W ]] ρ)i, h(λv0 . K 0 ) (I 2 [[M]] ρ0 )i) ∈ Rβ .
By instantiating the theorem to the case where both the environment and the continuation are empty, we obtain the following corollary that establishes the correctness of a direct-style specializer that can handle shift and reset:
Corollary 5.10. If d ` M : d, d [W ], then I 2 [[↓0 hP 5 [[W ]] ρφ i]] ρid ∼v hI 2 [[M]] ρφ i.
The complete proof of the theorem is found in the technical report [4].
5.11 RELATED WORKThis work extends our earlier work [3] where we presented offline specializers for
λ-calculus with shift and reset that produced the output in CPS. The present work
is a direct-style account of the previous work, but it contains non-trivial definitionof logical relations for shift and reset. We also presented the online specializers
for the λ-calculus with shift and reset [2]. However, their correctness has not beenformally proved.
Thiemann [17] presented an offline partial evaluator for Scheme including
call/cc. In his partial evaluator, call/cc is reduced if the captured continuation andthe body of call/cc are both static. This is close to our first attempt in Section 5.8.
76

Our solution is more liberal and reduces more continuation-capturing constructs,
but with a side-effect that all the residualized abstractions include a toplevel shift,which could be removed by a simple post-processing. More recently, Thiemann[19] showed a sophisticated effect-based type system to show the equivalenceof the continuation-based let-insertion and the state-based let-insertion. His typesystem captures the information on the let-residualized code as an effect. It might
be possible to extend his framework to avoid unnecessary shift at the front ofdynamic abstractions on the fly.
The correctness proof for offline specializers using the technique of logicalrelations appears in Jones et al. [14, Chapter 8]. Wand [20] used it to prove thecorrectness of an offline specializer for the call-by-name λ-calculus. The present
work is a non-trivial extension of his work to cope with delimited continuations.
Wand’s formulation was based on substitution, but we used the environmentbased formulation, which is essentially the same but is more close to the implementation.
Filinski presented normalization-by-evaluation algorithms for the call-by-value
λ-calculus [10] and the computational λ-calculus [11]. He showed their correctness denotationally using logical relations. The same framework is extended tothe untyped λ-calculus by Filinski and Rohde [12].
The type system used in this paper is due to Danvy and Filinski [6]. A similar type system is studied by Ariola, Herbelin, and Sabry [1], which explicitly
mentions the type of continuations.
5.12 CONCLUSION
This paper demonstrated that logical relations can be defined to characterize not
only call-by-name higher-order functions but also call-by-value functions as well
as delimited continuations. They were used to show the correctness of various offline specializers, including the one for the call-by-value λ-calculus with shift andreset. Along the development, we established the correctness of the continuationbased let-insertion, the shift/reset-based let-insertion, the continuation-based Anormalization, and the shift/reset-based A-normalization.
REFERENCES[1] Ariola, Z. M., H. Herbelin, and A Sabry “A Type-Theoretic Foundation of Continuations and Prompts,” Proceedings of the ninth ACM SIGPLAN International Conference on Functional Programming (ICFP’04), pp. 40–53 (September 2004).
[2] Asai, K. “Online Partial Evaluation for Shift and Reset,” ACM SIGPLAN Workshop
on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’02),
pp. 19–30 (January 2002).
[3] Asai, K. “Offline Partial Evaluation for Shift and Reset,” ACM SIGPLAN Symposium
on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’04),
pp. 3–14 (August 2004).

77

[4] Asai, K. “Logical Relations for Call-by-value Delimited Continuations,” Technical
Report OCHA-IS 06-1, Department of Information Sciences, Ochanomizu University(April 2006).
[5] Bondorf, A., and O. Danvy “Automatic autoprojection of recursive equations with
global variables and abstract data types,” Science of Computer Programming, Vol. 16,
pp. 151–195, Elsevier (1991).
[6] Danvy, O., and A. Filinski “A Functional Abstraction of Typed Contexts,” Technical
Report 89/12, DIKU, University of Copenhagen (July 1989).
[7] Danvy, O., and A. Filinski “Abstracting Control,” Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pp. 151–160 (June 1990).
[8] Danvy, O., and J. L. Lawall “Back to Direct Style II: First-Class Continuations,”
Proceedings of the 1992 ACM Conference on Lisp and Functional Programming,
pp. 299–310 (June 1992).
[9] de Bruijn, N. G. “Lambda Calculus Notation with Nameless Dummies, a Tool for
Automatic Formula Manipulation, with Application to the Church-Rosser Theorem,”Indagationes Mathematicae, Vol. 34, pp. 381–392 (1972).
[10] Filinski, A. “A Semantic Account of Type-Directed Partial Evaluation,” In G. Nadathur, editor, Principles and Practice of Declarative Programming (LNCS 1702),
pp. 378–395 (September 1999).
[11] Filinski, A. “Normalization by Evaluation for the Computational Lambda-Calculus,”
In S. Abramsky, editor, Typed Lambda Calculi and Applications (LNCS 2044),
pp. 151–165 (May 2001).
[12] Filinski, A., and H. K. Rohde “A Denotational Account of Untyped Normalization by
Evaluation,” In I. Walukiewicz, editor, Foundations of Software Science and Computation Structures (LNCS 2987), pp. 167–181 (March 2004).
[13] Flanagan, C., A. Sabry, B. F. Duba, and M. Felleisen “The Essence of Compiling with
Continuations,” Proceedings of the ACM SIGPLAN ’93 Conference on Programming
Language Design and Implementation (PLDI), pp. 237–247 (June 1993).
[14] Jones, N. D., C. K. Gomard, and P. Sestoft Partial Evaluation and Automatic Program
Generation, New York: Prentice-Hall (1993).
[15] Kameyama, Y., and M. Hasegawa “A Sound and Complete Axiomatization of Delimited Continuations,” Proceedings of the eighth ACM SIGPLAN International Conference on Functional Programming (ICFP’03), pp. 177–188 (August 2003).
[16] Mitchell, J. C. Foundations for Programming Languages, Cambridge: MIT Press(1996).
[17] Thiemann, P. “Towards Partial Evaluation of Full Scheme,” Proceedings of Reflection’96, pp. 105–115 (April 1996).
[18] Thiemann, P. J. “Cogen in Six Lines,” Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’96), pp. 180–189 (May 1996).
[19] Thiemann, P. “Continuation-Based Partial Evaluation without Continuation,” In R.
Cousot, editor, Static Analysis (LNCS 2694), pp. 366–382 (June 2003).
[20] Wand, M. “Specifying the Correctness of Binding-Time Analysis,” Journal of Functional Programming, Vol. 3, No. 3, pp. 365–387, Cambridge University Press (July
1993).

78