Logical Relations for
Call-by-value Delimited Continuations
Kenichi Asai
Ochanomizu University
2-1-1 Otsuka, Bunkyo-ku, Tokyo 112-8610, Japan
http://pllab.is.ocha.ac.jp/˜asai
Abstract
Logical relations, deﬁned inductively on the structure of types, provide a powerful tool tocharacterize higher-order functions. They often enable us to prove correctness of a programtransformer written with higher-order functions concisely. This paper demonstrates that thetechnique 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 ﬁrst deﬁned, whose CPS variant is used to provethe correctness of an oﬄine specializer for the call-by-value λ-calculus. They are then modiﬁed
to cope with delimited continuations and are used to establish the correctness of an oﬄine specializer for the call-by-value λ-calculus with delimited continuation constructs, shift and reset.
This is the ﬁrst correctness proof for such a specializer. Along the development, correctness ofthe continuation-based and shift/reset-based let-insertion and A-normalization is established.
As another application of the logical relations, a direct proof of the strong normalization for thetyped call-by-value λ-calculus with shift and reset is shown. Thanks to the natural deﬁnition oflogical relations, the proof is simple even with the presence of shift and reset.

keywords Logical relations, oﬄine specialization, delimited continuations, correctness, type systems, let-insertion, A-normalization

1

Introduction

Whenever we build a program transformer, be it a compiler, an optimizer, or a specializer, we needto 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 prove its correctness. In particular, the non-trivial use of higher-order functionsin the transformer makes the correctness proof particularly diﬃcult. A simple structural induction
on the input program does not usually work, because we can not easily characterize their behavior.
The technique of logical relations [17] is one of the proof methods that is often used in sucha case. With the help of types, it enables us to deﬁne a set of relations that captures necessary
properties of higher-order functions. Notably, Wand [22] used this technique to prove correctnessof an oﬄine specializer [15] in which higher-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-by-name λ-calculus,
but are not directly applicable to the call-by-value languages.
1

In this paper, we demonstrate that the technique of logical relations can be used to characterize
call-by-value functions as well as delimited continuations. We ﬁrst modify Wand’s logical relations
so that we can use them for call-by-value functions. We then prove the correctness of an oﬄine
specializer for the call-by-value λ-calculus. It is written in continuation-passing style (CPS) anduses the continuation-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 let-insertion in direct style [20]. We demonstrate that the correctness of this direct-style specializer with the shift/reset-based let-insertion canbe also established by properly 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 continuationsin the source language. To characterize such delimited continuations, we deﬁne logical relations
based on Danvy and Filinski’s type system [6]. Thanks to the explicit reference to the types ofcontinuations and the ﬁnal result, we can establish the correctness of the specializer. This is the ﬁrst
correctness proof for the oﬄine specializer for the call-by-value λ-calculus with shift and reset. The
present author previously showed the correctness of a similar oﬄine specializer [3], but it produced
the result of specialization in CPS.
The basic idea behind the logical relations shown in this paper is not restricted to proving thecorrectness of specializers. As another application of the logical relations, a direct proof of thestrong normalization for the typed call-by-value λ-calculus with shift and reset is shown. Thanks
to the natural deﬁnition of logical relations, the proof is simple even with the presence of shift andreset. Previously, this result was shown only indirectly by embedding shift and reset into a strongly
normalizing calculus called λ→−-calculus [1].
CThe contributions of this paper are summarized as follows:• We show that the technique of logical relations can be used to characterize call-by-valuefunctions as well as delimited continuations.
• We show for the ﬁrst time the correctness of the oﬄine specializer for the call-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 [14], and the shift/reset-based A-normalization.
• We show a direct proof of the strong normalization for the typed call-by-value λ-calculus withshift and reset.
The paper is organized as follows. After showing preliminaries in Section 2, the call-by-namespecializer and its correctness proof by Wand are reviewed in Section 3. We then show the logicalrelations for call-by-value functions in Section 4, and use (a CPS variant of) them to prove thecorrectness of a specializer for the call-by-value λ-calculus in Section 5. In Section 6, we transformthe specializer into direct style and prove its correctness. Then, we further extend the specializer tocope with shift and reset. We show an interpreter and an A-normalizer in Section 7, a specializer in
Section 8, a type system in Section 9, and logical relations with which the correctness is establishedin Section 10. Section 11 proves the strong normalization for the typed call-by-value λ-calculus
with shift and reset. Related work is in Section 12 and the paper concludes in Section 13. The
appendix contains a complete proof of correctness of the oﬄine specializer for shift and reset.
2

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 support and encouragements. The use of deBruijn levels to avoid the name generation problem was suggested by Olivier Danvy.

2

Preliminaries

The 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 | hM i | 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 hM i represent shift and reset, respectively, and appear only later in the paper. Their
intuitive meaning is brieﬂy described below. Datatype constructors are for representing the input
and output terms to our specializer. In this baselanguage, an integer n is used to represent avariable. 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. We usually use M to range over the metalanguage terms,
but K is also used for the body of continuations.
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:V= x | λx. M | n |Var(n) | Lam(n, V ) | App(V, V ) | Shift(n, V ) | Reset(V ) |Lam(n, V ) | App(V, V ) | Shift(n, V ) | Reset(V ) |Lam(n, V ) | App(V, V ) | Shift(n, V ) | Reset(V )When a specializer produces its output, it needs to generate fresh variables. To make thepresentation simple, we use so-called the de Bruijn levels [10] (not indices). Deﬁne the following
ﬁve strict operators:var(m) = λn. Var(m)lam(f ) = λn. Lam(n, f (n + 1))
app(f1 , f2 ) = λn. App(f1 n, f2 n)
shift(f ) = λn. Shift(n, f (n + 1))
reset(f ) = λn. Reset(f n)They are used to represent a term parameterized with a variable name. For example,
App(Lam(1, Lam(2, Var(1))), Lam(2, Var(2)))
is represented using the above operators as:app(lam(λx. lam(λy. var(x))), lam(λy. var(y))) .

3

When this term is given an integer n, it produces a complete term using the variable names fromn. For example, the above term becomes as follows
App(Lam(3, Lam(4, Var(3))), Lam(3, Var(3)))
if given an integer 3.
Given a term M in the de Bruijn level notation, we deﬁne the operation ↓n M of obtaining 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 theformer as the output of specializers.
Throughout this paper, we use three kinds of equalities between terms in the metalanguage: =for deﬁnition or α-equality, ∼n for β-equality under call-by-name semantics, and ∼v for β-equality
under call-by-value semantics. The call-by-value β-equality in the presence of shift and reset isdeﬁned by Kameyama and Hasegawa [16, Fig. 2].
Shift and Reset Intuitively, a shift expression ξk. M takes its current continuation up to its
enclosing reset, binds it to k, and discards the current continuation with which the whole shiftexpression was called. For example, in the expression 1 + h10 + ξk. k (k 100)i, k is bound to acontinuation λv. 10 + v. Applying it twice to 100 yields 120, the continuation h10 + ·i is discarded,
the value of h10 + ξk. k (k 100)i is thus 120, and the ﬁnal result is 121. The precise semantics ofshift and reset is typically given by a CPS interpreter or by CPS transformation [7].

3Specializer 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 [22].
A specializer consists of two parts: an interpreter for static expressions and a residualizer for
dynamic expressions. An interpreter for the input language is deﬁned 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:
D1 [[Var(n)]] ρ = ρ (n)D1 [[Lam(n, M )]] ρ = lam(λx. D1 [[M ]] ρ[var(x)/n])D1 [[App(M1 , M2 )]] ρ = app(D1 [[M1 ]] ρ, D1 [[M2 ]] ρ)
An oﬄine specializer is given by putting the interpreter and the residualizer together:
P 1 [[Var(n)]] ρP 1 [[Lam(n, W )]] ρP 1 [[Lam(n, W )]] ρP 1 [[App(W1 , W2 )]] ρP 1 [[App(W1 , W2 )]] ρ

=
=
=
=
=

ρ (n)
λx. P 1 [[W ]] ρ[x/n]lam(λx. P 1 [[W ]] ρ[var(x)/n])(P 1 [[W1 ]] ρ) (P 1 [[W2 ]] ρ)app(P 1 [[W1 ]] ρ, P 1 [[W2 ]] ρ)
4

The specializer goes wrong if the input term is not well-annotated. Well-annotatedness of a termis speciﬁed as a binding-time analysis that, given an unannotated term, produces a well-annotatedterm. Here, we show a type-based binding-time analysis. Deﬁne binding-time types of expressions
as follows:τ = d|τ →τ
An expression of type d denotes that the expression is dynamic, while an expression of type τ → τshows that it is a static function. (We do not need a type s for static constants, because ourbaselanguage does not have any constants. It is straightforward to include them.) We use a
judgment of the form 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 deﬁned by 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 [22] uses the technique of logical relations.
Deﬁne logical relations between terms in the metalanguage by induction on the structure of bindingtime types as follows:(M, M 0 ) ∈ Rd
(M, M 0 ) ∈ Rσ→τ⇐⇒ I 1 [[↓n M ]] ρid ∼n M 0 for any large n (deﬁned 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 logicalrelations are deﬁned on open terms, we need to relate free variables in the base- and metalanguage
in some way. We choose here to relate a baselanguage variable Var(n) to a metalanguage variablezn .
In the deﬁnition of Rd , M is a metalanguage term in the de Bruijn level notation that is either
a value representing a baselanguage term or a term that is equal to (or evaluates to) a value
representing a baselanguage term in the underlying semantics of the metalanguage (in this section,
call-by-name). The semantic brackets are usually used to enclose syntactic objects only, but here
we use them to enclose a term that evaluates to a syntactic object.
The choice of n in Rd needs a special attention. Since M is possibly an open term, n has tobe 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 deﬁned to be large if n is greater than any free variables in thebaselanguage term M . The free variables of M represented in de Bruijn level notation are deﬁned∪
as the union of the free variables for all the instantiations: n ↓n M . The intention here is thatthe free variables are deﬁned as those of ↓n M for suﬃciently large n that does not capture the freevariables of M .
For environments ρ and ρ0 , we say (ρ, ρ0 ) |= A iﬀ (ρ (n), ρ0 (n)) ∈ RA(n) for all n ∈ dom(A),where dom(A) is the domain of A. Then, we can show the following theorem:
Theorem 1 (Wand [22]) If A ` M : τ [W ] and (ρ, ρ0 ) |= A, then (P 1 [[W ]] ρ, I 1 [[M ]] ρ0 ) ∈ Rτ .
5

By instantiating it to an empty environment ρφ , we obtain the following corollary, which establishes
the correctness of specialization.
Corollary 1 (Wand [22]) If ` M : d [W ], then I 1 [[↓0 (P 1 [[W ]] ρφ )]] ρid ∼n I 1 [[M ]] ρφ .
The proof of Theorem 1 proceeds by induction on the structure of the proof of A ` M : τ [W ].
Since there are ﬁve typing rules for this judgment, the proof is split into ﬁve cases. Among them,
the logical relations play an important role in the case for static applications. Let us review thiscase. We will later see how this case fails for the call-by-value semantics.
Proof Case (Static Application)

AssumeA ` M1 : σ → τ [W1 ] A ` M2 : σ [W2 ]A ` App(M1 , M2 ) : τ [App(W1 , W2 )]We must show

(P 1 [[App(W1 , W2 )]] ρ, I 1 [[App(M1 , M2 )]] ρ0 ) ∈ Rτassuming (ρ, ρ0 ) |= A. By the deﬁnition of P 1 and I 1 , it suﬃces to show((P 1 [[W1 ]] ρ) (P 1 [[W2 ]] ρ), (I 1 [[M1 ]] ρ0 ) (I 1 [[M2 ]] ρ0 )) ∈ Rτ .
By the induction hypotheses, we have
(P 1 [[W1 ]] ρ, I 1 [[M1 ]] ρ0 ) ∈ Rσ→τand

(P 1 [[W2 ]] ρ, I 1 [[M2 ]] ρ0 ) ∈ Rσ .

Thus, from the deﬁnition of Rσ→τ , we have((P 1 [[W1 ]] ρ) (P 1 [[W2 ]] ρ), (I 1 [[M1 ]] ρ0 ) (I 1 [[M2 ]] ρ0 )) ∈ Rτ ,2which proves the theorem for this case.

The crucial part appears at the end of the proof. The last derivation relies on the deﬁnitionof Rσ→τ showing that P 1 [[W1 ]] ρ and I 1 [[M1 ]] ρ0 transform the related arguments to the related
results.
The use of logical relations is essential here. It might appear at ﬁrst that we could prove
I 1 [[P 1 [[W ]] ρ]] ρid ∼n I 1 [[M ]] ρ0 directly by induction on the structure of A ` M : τ [W ]. It is not
the case, however. The proof fails for the static application, because we cannot prove
I 1 [[(P 1 [[W1 ]] ρ) (P 1 [[W2 ]] ρ)]] ρid ∼n (I 1 [[M1 ]] ρ0 ) (I 1 [[M2 ]] ρ0 )from the two induction hypotheses
I 1 [[P 1 [[W1 ]] ρ]] ρid ∼n I 1 [[M1 ]] ρ0and

I 1 [[P 1 [[W2 ]] ρ]] ρid ∼n I 1 [[M2 ]] ρ0 .
6

Recall the deﬁnition of I 1 . We have
(I 1 [[P 1 [[W1 ]] ρ]] ρid ) (I 1 [[P 1 [[W2 ]] ρ]] ρid ) ∼n I 1 [[App(P 1 [[W1 ]] ρ, P 1 [[W2 ]] ρ)]] ρidbut not(I 1 [[P 1 [[W1 ]] ρ]] ρid ) (I 1 [[P 1 [[W2 ]] ρ]] ρid ) ∼n I 1 [[(P 1 [[W1 ]] ρ) (P 1 [[W2 ]] ρ)]] ρid .
Without properly characterizing the behavior of the higher-order function P 1 [[W1 ]] ρ, we cannot
prove any statement about (P 1 [[W1 ]] ρ) (P 1 [[W2 ]] ρ). With logical relations, an abstraction in themetalanguage is related to the one in the object language. They essentially bridge the propertiesof higher-order functions in the two languages.
If both P 1 and I 1 used a closure rather than a higher-order function as a representation ofan abstraction, we might have been able to prove the correctness by induction on the number of
evaluation steps. However, this method would make the proof signiﬁcantly more complicated. We
also need to establish the relationship between higher-order functions and closures (in other words,
the correctness of defunctionalization). Moreover, it discourages us to use higher-order functions
even though we all know how they behave and how useful they are. Rather than transforming our
implementation back to the old style, we should go forward and ﬁnd a method to directly reason
about the new style.

4

Logical Relations for Call-by-value λ-calculus

Although the specializer shown in the previous section is correct in the call-by-name semantics, it
is not correct in the call-by-value semantics. For example,
App(Lam(x, Lam(y, Var(y))), W )will be specialized to Lam(y, Var(y)) even if W is a non-terminating term, such as
App(Lam(x, App(Var(x), Var(x))), Lam(x, App(Var(x), Var(x))))which is well-annotated. To see exactly why the correctness proof fails, we try to prove the theorem
in the call-by-value semantics. Deﬁne 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σ . (M V, M 0 V 0 ) ∈ RτThere are two diﬀerences 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 deﬁnition of Rd . Secondly, M andM 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 1 with this deﬁnition of Rτ , we would have obtained as a corollary
the correctness of the specializer in the call-by-value semantics. However, the proof fails for static
applications. Although we could proceed the proof as the same way as the one in the previous
section, we would get stuck at the last step where we used the deﬁnition of Rσ→τ . We need toshow that both P 1 [[W2 ]] ρ and I 1 [[M2 ]] ρ0 are values, but they are in fact not values if M2 had aform App(M21 , M22 ). In fact, the specializer is not correct under the call-by-value semantics.
7

5

Specializer in CPS

The correctness under the call-by-value semantics does not hold for the specializer in Section 3
because it may discard a non-terminating computation. The standard method to recover thecorrectness is to perform let-insertion [4]. Since let-insertion requires explicit manipulation ofcontinuations, we ﬁrst rewrite our specializer into CPS as follows:
P 2 [[Var(n)]] ρ κ
P 2 [[Lam(n, W )]] ρ κ
P 2 [[Lam(n, W )]] ρ κ
P 2 [[App(W1 , W2 )]] ρ κ
P 2 [[App(W1 , W2 )]] ρ κ

=
=
=
=
=

κ (ρ (n))κ (λx. λk. P 2 [[W ]] ρ[x/n] k)κ (lam(λx. P 2 [[W ]] ρ[var(x)/n] λx. x))
P 2 [[W1 ]] ρ λm. P 2 [[W2 ]] ρ λn. m n κ
P 2 [[W1 ]] ρ λm. P 2 [[W2 ]] ρ λn. κ (app(m, n))Note that lam(λx. · · ·) and app(m, n) in the dynamic rules are not CPS-transformed because they
are merely data representing baselanguage terms. If we transformed them into CPS, we would
obtain the result of specialization in CPS, as we did in the previous work [3].
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 applicationis residualized, we insert a let-expression to residualize it exactly once with a unique name t, andcontinue the rest of the specialization with this name. Since the residualized application is notpassed to the continuation κ, it will never be discarded even if κ discards its argument.
The let-insertion technique can be regarded as performing A-normalization [14] on the ﬂy 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 [14]:A1 [[Var(n)]] ρ κ = κ (ρ (n))
A1 [[Lam(n, M )]] ρ κ = κ (lam(λx. A1 [[M ]] ρ[var(x)/n] λx. x))
A1 [[App(M1 , M2 )]] ρ κ = A1 [[M1 ]] ρ λm. A1 [[M2 ]] ρ λn.
let(app(m, n), lam(λt. κ (var(t))))We now want to show the correctness of the specializer P 2 under the call-by-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 3. Since the direct proof would get stuck for static
applications, we use logical relations. Let us deﬁne the base case Rd as follows:(M, M 0 ) ∈ Rd ⇐⇒ I 1 [[↓n M ]] ρid ∼v M 0 for any large n .
Then, we want to show
(P 2 [[W ]] ρφ λx. x, I 1 [[M ]] ρφ ) ∈ Rd
with a suitable deﬁnition of Rσ→τ .

8

To prove it, we ﬁrst 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, (λv 0 . K 0 ) (I 1 [[M ]] ρ0 )) ∈ Rτfor some suitable ρ, ρ0 , λv. K, and λv 0 . 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 deﬁne Rσ→τ ? Unlike Section 3, it is not immediately clear how to deﬁne
Rσ→τ . Obviously, we can not use the previous deﬁnition:(M, M 0 ) ∈ Rσ→τ⇐⇒ ∀(V, V 0 ) ∈ Rσ . (M V, M 0 V 0 ) ∈ Rτ

because the specializer is written in CPS. Even though W has a type σ → τ , P 2 [[W ]] ρ λv. K is nota function from σ to τ , so we cannot pass it a value of type σ. Instead, a function of type σ → τis consumed by the continuation λv. K, and P 2 [[W ]] ρ λv. K produces the ﬁnal result which can beof any type.
To relate P 2 [[W ]] ρ λv. K and (λv 0 . K 0 ) (I 1 [[M ]] ρ0 ) properly, we need to characterize precisely
the two continuations, λv. K and λv 0 . K 0 , and the ﬁnal results. Going back to the deﬁnition 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.
They are particularly evident in the rule for dynamic applications:
P 2 [[App(W1 , W2 )]] ρ κ = P 2 [[W1 ]] ρ λm. P 2 [[W2 ]] ρ λn.
let(app(m, n), lam(λt. κ (var(t))))We assumed here that κ returns a dynamic expression, which is then used to construct a letexpression (and hence, P 2 also returns a dynamic expression). In ordinary CPS programs, thereturn type of continuations is polymorphic. It can be 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 of dynamic 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 deﬁnition 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, λv 0 . K 0 ) |= τ ; d.
(M V λv. K, (λv 0 . K 0 ) (M 0 V 0 )) ∈ Rd

where (λv. K, λv 0 . K 0 ) |= τ ; d is simultaneously deﬁned as follows:(λv. K, λv 0 . K 0 ) |= τ ; d ⇐⇒ ∀(V, V 0 ) ∈ Rτ . ((λv. K) V, (λv 0 . K 0 ) V 0 ) ∈ Rd
Intuitively, (λv. K, λv 0 . K 0 ) |= τ ; d means that λv. K and λv 0 . K 0 are related continuations that,given related values of type τ , produce related results of type d. Using this deﬁnition, (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 typeof continuations.
With this deﬁnition of logical relations, we can prove the correctness of P 2 under the call-byvalue semantics.
9

Theorem 2 If A ` M : τ [W ], (ρ, ρ0 ) |= A, and (λv. K, λv 0 . K 0 ) |= τ ; d, then(P 2 [[W ]] ρ λv. K, (λv 0 . 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 to the explicit reference to the typesof continuations and the ﬁnal result. The proof proceeds in a CPS manner. In particular, the casesfor (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 the continuation are
empty, we obtain the following corollary that establishes the correctness of a specializer using thecontinuation-based let-insertion:
Corollary 2 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 thesame as the A-normalizer. Thus, the theorem can be instantiated to the following corollary, which
proves the correctness of the continuation-based A-normalization.
Corollary 3 I 1 [[↓0 (A1 [[M ]] ρφ λx. x)]] ρid ∼v I 1 [[M ]] ρφ for any closed M .

6Specializer in Direct Style

In this section, we present a specializer written in direct style and show its correctness under thecall-by-value semantics. Since we have already established the correctness of a specializer written
in CPS in the previous section, the development in this section is easy. Roughly speaking, wetransform the results in the previous section back to direct style [5, 9]. During this process, we use
the ﬁrst-class delimited continuation constructs, shift and reset, to cope with non-standard use ofcontinuations. Here is the deﬁnition of the specializer written in direct style:P 3 [[Var(n)]] ρP 3 [[Lam(n, W )]] ρP 3 [[Lam(n, W )]] ρP 3 [[App(W1 , W2 )]] ρP 3 [[App(W1 , W2 )]] ρ

=
=
=
=
=

ρ (n)
λx. P 3 [[W ]] ρ[x/n]lam(λx. hP 3 [[W ]] ρ[var(x)/n]i)(P 3 [[W1 ]] ρ) (P 3 [[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 withshift and reset [3] by extracting dynamic rules from P 3 :A2 [[Var(n)]] ρ = ρ (n)A2 [[Lam(x, M )]] ρ = lam(λx. hA2 [[M ]] ρ[var(x)/n]i)A2 [[App(M1 , M2 )]] ρ = ξκ. let(app(A2 [[M1 ]] ρ, A2 [[M2 ]] ρ), lam(λt. κ (var(t))))To deﬁne suitable logical relations for the specializer written in direct style (with shift andreset), we need to correctly handle delimited continuations. This is done by observing the exact
correspondence between continuations in the previous section and delimited continuations in thissection. In particular, we type the result of the delimited continuations as d.

10

Logical relations for the direct-style specializer with delimited continuations are deﬁned asfollows:(M, M 0 ) ∈ Rd⇐⇒ I 1 [[↓n M ]] ρid ∼v M 0 for any large n(M, M 0 ) ∈ Rσ→τ ⇐⇒ ∀(V, V 0 ) ∈ Rσ . ∀(λv. K, λv 0 . K 0 ) |= τ ; d.
(h(λv. K) (M V )i, (λv 0 . K 0 ) (M 0 V 0 )) ∈ Rd
where (λv. K, λv 0 . K 0 ) |= τ ; d is simultaneously deﬁned as follows:(λv. K, λv 0 . K 0 ) |= τ ; d ⇐⇒ ∀(V, V 0 ) ∈ Rτ . (h(λv. K) V i, (λv 0 . K 0 ) V 0 ) ∈ Rd
Then, the correctness of the specializer is stated as follows:
Theorem 3 If A ` M : τ [W ], (ρ, ρ0 ) |= A, and (λv. K, λv 0 . K 0 ) |= τ ; d, then(h(λv. K) (P 3 [[W ]] ρ)i, (λv 0 . K 0 ) (I 1 [[M ]] ρ0 )) ∈ Rd .
Although both the specializer and the interpreter are written in direct style, the proof proceeds in
a CPS manner. In particular, the cases for applications go from left to right, naturally reﬂecting
the call-by-value semantics.
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 specializer using theshift/reset-based let-insertion:
Corollary 4 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, the specializer behaves
exactly the same as the A-normalizer. Thus, the theorem can be instantiated to the following
corollary, which proves the correctness of the direct-style A-normalization.
Corollary 5 I 1 [[↓0 hA2 [[M ]] ρφ i]] ρid ∼v I 1 [[M ]] ρφ for any closed M .

7

Interpreter and A-normalizer for Shift and Reset

So far, shift and reset appeared only in the metalanguage. In the following sections, we developa specializer written in direct style that can handle shift and reset in the baselanguage. We ﬁrst
deﬁne 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)]] ρI 2 [[Lam(n, M )]] ρI 2 [[App(M1 , M2 )]] ρI 2 [[Shift(n, M )]] ρI 2 [[Reset(M )]] ρ

=
=
=
=
=

ρ (n)
λx. I 2 [[M ]] ρ[x/n](I 2 [[M1 ]] ρ) (I 2 [[M2 ]] ρ)
ξk. I 2 [[M ]] ρ[k/n]hI 2 [[M ]] ρi

We used shift and reset operations themselves to interpret shift and reset expressions.

11A residualizer is deﬁned as follows:
D2 [[Var(n)]] ρ
D2 [[Lam(n, M )]] ρ
D2 [[App(M1 , M2 )]] ρ
D2 [[Shift(n, M )]] ρ
D2 [[Reset(M )]] ρ

=
=
=
=
=

ρ (n)
lam(λx. D2 [[M ]] ρ[var(x)/n])app(D2 [[M1 ]] ρ, D2 [[M2 ]] ρ)
shift(λk. D2 [[M ]] ρ[var(k)/n])reset(D2 [[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:
A3 [[Var(n)]] ρ
A3 [[Lam(n, M )]] ρ
A3 [[App(M1 , M2 )]] ρ
A3 [[Shift(n, M )]] ρ
A3 [[Reset(M )]] ρ

=
=
=
=
=

ρ (n)
lam(λx. hA3 [[M ]] ρ[var(x)/n]i)ξk. let(app(A3 [[M1 ]] ρ, A3 [[M2 ]] ρ), lam(λt. k (var(t))))shift(λk. hA3 [[M ]] ρ[var(k)/n]i)
reset(hA3 [[M ]] ρi)

It replaces all the application expressions in the body of abstractions, shift expressions, and reset
operations with a sequence of let-expressions.

8

Specializer for Shift and Reset

In this section, we show a specializer for the call-by-value λ-calculus with shift and reset. Our ﬁrst
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)]] ρP 4 [[Lam(n, W )]] ρP 4 [[Lam(n, W )]] ρP 4 [[App(W1 , W2 )]] ρP 4 [[App(W1 , W2 )]] ρP 4 [[Shift(n, W )]] ρP 4 [[Shift(n, W )]] ρP 4 [[Reset(W )]] ρP 4 [[Reset(W )]] ρ

=
=
=
=
=
=
=
=
=

ρ (n)
λx. P 4 [[W ]] ρ[x/n]lam(λx. hP 4 [[W ]] ρ[var(x)/n]i)(P 4 [[W1 ]] ρ) (P 4 [[W2 ]] ρ)ξk. let(app(P 4 [[W1 ]] ρ, P 4 [[W2 ]] ρ), lam(λt. k (var(t))))ξk. P 4 [[W ]] ρ[k/n]shift(λk. hP 4 [[W ]] ρ[var(k)/n]i)hP 4 [[W ]] ρi
reset(hP 4 [[W ]] ρi)

Although this specializer does seem to work for carefully annotated inputs, it is hard to specify thewell-annotated term as a simple binding-time analysis. The diﬃculty 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 meansthat we implicitly assume the grabbed continuation coincides with the actual continuation at runtime. This was actually true for the interpreter: we implemented shift in the baselanguage using
shift in the metalanguage. In the specializer, however, the specialization-time continuation does
not always coincide with the actual continuation. To be more speciﬁc, 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. For example,
consider the term Lam(x, App(Var(f ), Shift(k, · · ·))). The above specializer incorrectly captures12

the continuation App(Var(f ), ·) as k, but actually k should be bound to App(h, App(Var(f ), ·))where h is the continuation at the time when Lam(x, App(Var(f ), Shift(k, · · ·))) is applied to anargument.
Given that the specialization-time continuation is not always consistent with the actual one, wehave to make sure that the continuation is captured statically only when it represents the actualone. Furthermore, we have to make sure that whenever shift is residualized, its enclosing reset isalso residualized. One way to express this information in the type system would be to split all thetyping 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 the case when they
do not (the continuation is unknown, dynamic). We could then statically grab the continuation
only when it represents the actual one.
However, this solution leads to an extremely weak specialization. Unless an enclosing resetis 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 underdynamic abstractions. Remember that a type system does not tell us what subexpressions appear
in a given 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 type in App(W1 , W2 ) (and thus it appears
that this application can be performed statically), we cannot actually perform this application,
because the toplevel operator of W1 might be a shift operation that passes a function to thegrabbed continuation. In other words, we cannot determine the binding-time of App(W1 , W2 ) fromthe binding-time of W1 , which makes it diﬃcult to construct a simple type-based binding-time
analysis.
The solution we employ takes a diﬀerent 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 modiﬁed specializer is presented 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 ﬁrst and the most important change is in the rule fordynamic abstractions. Rather than specializing the body W of a dynamic 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 thecontinuation when the abstraction is applied at runtime.
Another way to understand the rule for dynamic abstractions is by rewriting the rule for static
abstractions as follows:
P 5 [[Lam(n, W )]] ρ = λx. ξk. hk (P 5 [[W ]] ρ[x/n])i13

In this equivalent deﬁnition, the continuation k for the body of the static abstraction is madeexplicit by inserting a shift operation. Comparing this rule to the rule for dynamic abstractions,
we can easily see the correspondence between them. In the rule for dynamic abstractions, the body
W is specialized in the yet unknown context reset(app(var(k), ·)) that corresponds to the correctcontext hk (·)i.
This insertion of a dynamic shift is reminiscent of η-expansion. To remove administrative
redexes in the one-pass CPS transformation, Danvy and Filinski [8] turned all the continuations
that are unknown at transformation time into static functions using η-expansion. The above
insertion of the dynamic shift does exactly the same thing in the direct-style program.
The second change is in the rule for dynamic applications where dynamic reset is inserted aroundthe residualized let-expression. The third change is in the rule for dynamic shift. Rather thanresidualizing a dynamic shift, which requires residualization of the corresponding reset, the current
continuation is grabbed and it is turned into a dynamic expression via η-expansion. Finally, the rulefor 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 necessarily mean that the result ofspecialization does not contain any reset expressions. Reset is residualized in the rule for dynamic
abstractions and applications.)
These changes not only deﬁne 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))))))) .
(This term is well-annotated in the type system shown in the next section.) When we specialize thisterm, the continuation k grabbed by Shift(k, · · ·) is partially static: we know that the ﬁrst thing to
do when k is applied is to pass its argument to f , but the computation that should be performed
after that is unknown. It is the continuation when Lam(x, · · ·) is applied to an argument. Even inthis 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 thepartially static information of the continuation.
On the other hand, the above changes cause an interesting side-eﬀect to the result of specialization: all the residualized lambda abstractions now have a ‘standardized’ form lam(λx. shift(λk. · · ·))(and this is the only place where shift is residualized). In particular, even when we specializeLam(x, W ) where shift is not used during the evaluation of W , the residualized abstraction has
typically the form lam(λx. shift(λk. reset(app(var(k), M )))) where k does not occur free in M . (Iflet-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 ﬂy using P 5 withsome extra work. We expect that it is not likely. As long as a simple type-based binding-time
analysis is employed, it is impossible to tell if the execution of the body of a dynamic abstraction
14

includes any shift operations. So, unless we introduce some extra mechanisms to keep track ofthis information, 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 postprocessing to remove unnecessary shift expressions, if it is important at all to do so. Currently, we
are investigating if the standardized occurrence of shift has any eﬀects on the eﬃcient and direct
implementation of delimited continuations.

9Type System for Shift and Reset

Since our proof technique relies on the logical relations, we need to deﬁne a type system for thecall-by-value λ-calculus with shift and reset to prove the correctness of P 5 . In this section, we
brieﬂy review Danvy and Filinski’s type system [6]. More thorough explanation is found in [3, 6].
In the presence of ﬁrst-class (delimited) continuations, we need to explicitly specify the typesof continuations and the ﬁnal result. For this purpose, Danvy and Filinski use a judgment of theformA, α ` M : τ, β [W ] .
It reads: under the type assumption A, an expression M has a type τ in a continuation of typeτ ; α and the ﬁnal result is of type β. Since we use this type system as the static part of ourbinding-time analysis, we decorate it with [W ] to indicate that M is annotated as W .
If M does not contain any shift operations, the types α and β are always the same, namely, theAnswer type. In the presence of shift and reset, however, they can be diﬀerent and of any type.
The type of functions also needs to include the types of continuations and the ﬁnal 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 ﬁnal result is of type β. As a result,types are speciﬁed as follows:τ = d | τ /τ → τ /τHere goes the type system:
A[n : τ ], α ` Var(n) : τ, α [Var(n)]A, σ ` M : σ, τ [W ]A[n : σ], α ` 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 where types of continuations are made explicit. In Section 6, the result type of continuations and the type of ﬁnal
results were always d. In the above type system, it means that a judgment had always the formA, 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 3).

15

The dynamic rules can be obtained by simply replacing all the static function types with d (andtypes that occur within the function type). The dynamic rules 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 )]10

Logical Relations for Shift and Reset

In this section, we deﬁne 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 8. They are thegeneralization of the logical relations in Section 6 in that the types of the ﬁnal result and the resultof continuations are not restricted to d.
(M, M 0 ) ∈ Rd⇐⇒ I 1 [[↓n M ]] ρid ∼v M 0 for any large n(M, M 0 ) ∈ Rσ/α→τ /β ⇐⇒ ∀(V, V 0 ) ∈ Rσ . ∀(λv. K, λv 0 . K 0 ) |= τ ; α.
(h(λv. K) (M V )i, h(λv 0 . K 0 ) (M 0 V 0 )i) ∈ Rβ
where (λv. K, λv 0 . K 0 ) |= τ ; α is simultaneously deﬁned as follows:(λv. K, λv 0 . K 0 ) |= τ ; α ⇐⇒ ∀(V, V 0 ) ∈ Rτ . (h(λv. K) V i, h(λv 0 . K 0 ) V 0 i) ∈ RαThen, the correctness of the specializer is stated as follows:
Theorem 4 If A, α ` M : τ, β [W ], (ρ, ρ0 ) |= A, and (λv. K, λv 0 . K 0 ) |= τ ; α, then(h(λv. K) (P 5 [[W ]] ρ)i, h(λv 0 . 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 6 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 Appendix.

11

Strong Normalization

The basic idea behind the logical relations shown in this paper is not restricted to proving thecorrectness of specializers. To see how it can be applied to other proofs, we present in this section
the proof of strong normalization for the typed call-by-value λ-calculus with shift and reset. Ariola,
Herbelin, and Sabry [1] presented a similar result by embedding shift and reset into their λ→−C→−calculus and then showing that λC - -calculus is strongly normalizing. We give a more direct proof
here. Thanks to the natural deﬁnition of the logical relations, the proof is a simple exercise,following the standard proof technique found in a textbook [18, Chapter 12].
We ﬁrst extend the metalanguage with a datatype for integers:
M= · · · | Num(n)16as well as the interpreter:
I 2 [[Num(n)]] ρ = n
Types are deﬁned by:τ= int | τ /τ → τ /τTyping rules are given by:
A, α ` Num(n) : int, α
together with the ﬁve static rules in Section 9 (ignoring the parts for annotated terms “[W ]”).
Now, deﬁne the logical relations (or predicates) Nτ on the metalanguage terms by induction on the
structure of types as follows:
M ∈ Nint⇐⇒ M halts
M ∈ Nσ/α→τ /β ⇐⇒ M halts, and ∀V ∈ Nσ . ∀λv. K |= τ ; α. h(λv. K) (M V )i ∈ Nβ
where λv. K |= τ ; α is simultaneously deﬁned as follows:
λv. K |= τ ; α ⇐⇒ ∀V ∈ Nτ . h(λv. K) V i ∈ Nα
For an environment ρ, we deﬁne ρ |= A iﬀ for all n ∈ dom(A), ρ (n) ∈ NA(n) . Then, we can show
the following theorem:
Theorem 5 If A, α ` M : τ, β, ρ |= A, and λv. K |= τ ; α, then h(λv. K) (I 2 [[M ]] ρ)i ∈ Nβ .
We can instantiate this theorem in many ways according to which initial continuation we use, but if
we instantiate it to an empty continuation λv. v of type α ; α together with an empty environment,
we obtain the following corollary:
Corollary 7 If α ` M : α, τ for some α and τ , then hI 2 [[M ]] ρφ i halts.
Namely, if M is typed under an empty environment and an empty continuation, the execution of
M in the empty context always terminates.

12

Related Work

This work extends our earlier work [3] where we presented oﬄine specializers for λ-calculus withshift 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 deﬁnition of logical relations for shift and reset. We
also presented the online specializers for the λ-calculus with shift and reset [2]. However, theircorrectness has not been formally proved.
Thiemann [19] presented an oﬄine partial evaluator for Scheme including call/cc. In his partial evaluator, call/cc is reduced if the captured continuation and the body of call/cc are both
static. This is close to our ﬁrst attempt in Section 8. Our solution is more liberal and reduces
more continuation-capturing constructs, but with a side-eﬀect that all the residualized abstractions include a toplevel shift, which could be removed by a simple post-processing. More recently,
Thiemann [21] showed a sophisticated eﬀect-based type system to show the equivalence of thecontinuation-based let-insertion and the state-based let-insertion. His type system captures theinformation on the let-residualized code as an eﬀect. It might be possible to extend his framework
to avoid unnecessary shift at the front of dynamic abstractions on the ﬂy.
17

The correctness proof for oﬄine specializers using the technique of logical relations appears in
Jones et al. [15, Chapter 8]. Wand [22] used it to prove the correctness of an oﬄine specializer
for the call-by-name λ-calculus. The present work is a non-trivial extension of his work to copewith delimited continuations. Wand’s formulation was based on substitution, but we used theenvironment-based 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 [11]and the computational λ-calculus [12]. He showed their correctness denotationally using logicalrelations. The same framework is extended to the untyped λ-calculus by Filinski and Rohde [13].
The type system used in this paper is due to Danvy and Filinski [6]. A similar type system isstudied by Ariola, Herbelin, and Sabry [1], which explicitly mentions the type of continuations.

13

Conclusion

This paper demonstrated that logical relations can be deﬁned to characterize not only call-byname higher-order functions but also call-by-value functions as well as delimited continuations.
They were used to show the correctness of various oﬄine specializers, including the one for the callby-value λ-calculus with shift and reset. Along the development, we established the correctnessof the continuation-based let-insertion, the shift/reset-based let-insertion, the continuation-based
A-normalization, and the shift/reset-based A-normalization. Finally, the idea of logical relations
was used to give a simple and direct proof of the strong normalization for the typed call-by-value
λ-calculus with shift and reset.

References[1] Ariola, Z. M., H. Herbelin, and A Sabry “A Type-Theoretic Foundation of Continuations andPrompts,” 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 (January2002).
[3] Asai, K. “Oﬄine Partial Evaluation for Shift and Reset,” ACM SIGPLAN Symposium on
Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’04), pp. 3–14 (August2004).
[4] 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).
[5] Danvy, O. “Back to Direct Style,” Science of Computer Programming, Vol. 22, pp. 183–195,
Elsevier (February 1994).
[6] Danvy, O., and A. Filinski “A Functional Abstraction of Typed Contexts,” Technical Report
89/12, DIKU, University of Copenhagen (July 1989).

18

[7] Danvy, O., and A. Filinski “Abstracting Control,” Proceedings of the 1990 ACM Conferenceon Lisp and Functional Programming, pp. 151–160 (June 1990).
[8] Danvy, O., and A. Filinski “Representing Control, a Study of the CPS Transformation,”
Mathematical Structures in Computer Science, Vol. 2, No. 4, pp. 361–391 (December 1992).
[9] Danvy, O., and J. L. Lawall “Back to Direct Style II: First-Class Continuations,” Proceedingsof the 1992 ACM Conference on Lisp and Functional Programming, pp. 299–310 (June 1992).
[10] 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).
[11] 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).
[12] Filinski, A. “Normalization by Evaluation for the Computational Lambda-Calculus,” In S.
Abramsky, editor, Typed Lambda Calculi and Applications (LNCS 2044), pp. 151–165 (May2001).
[13] 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).
[14] 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).
[15] Jones, N. D., C. K. Gomard, and P. Sestoft Partial Evaluation and Automatic Program Generation, New York: Prentice-Hall (1993).
[16] 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).
[17] Mitchell, J. C. Foundations for Programming Languages, Cambridge: MIT Press (1996).
[18] Pierce, B. C. Types and Programming Languages, Cambridge: MIT Press (2002).
[19] Thiemann, P. “Towards Partial Evaluation of Full Scheme,” Proceedings of Reﬂection’96,
pp. 105–115 (April 1996).
[20] Thiemann, P. J. “Cogen in Six Lines,” Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’96), pp. 180–189 (May 1996).
[21] Thiemann, P. “Continuation-Based Partial Evaluation without Continuation,” In R. Cousot,
editor, Static Analysis (LNCS 2694), pp. 366–382 (June 2003).
[22] 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).
19

Appendix
The appendix shows the correctness proof for the specializer P 5 . In the appendix, we write P for
P 5 , I for I 2 and ∼ for ∼v .

A

Axioms for Shift and Reset(Pure) evaluation contexts:
F= [ ] | F M | V F | ξk. F |Lam(x, F ) | App(F, M ) | App(V, F ) | Shift(k, F ) | Reset(F ) |Lam(x, F ) | App(F, M ) | App(V, F ) | Shift(k, F ) | Reset(F ) |Lam(x, F ) | App(F, M ) | App(V, F ) | Shift(k, F ) | Reset(F )Note that static reset is not permitted in this context except for appearing within M .
Sound and complete axioms for the call-by-value λ-calculus with shift and reset presented by
Kameyama and Hasegawa [16]:(λx. M ) V
λx. V x(λx. F [x]) MhV ih(λx. M1 ) hM2 ii
ξk. k MhF [ξk. M ]iξk. hM i

∼
∼
∼
∼
∼
∼
∼
∼

M [V /x]V
F [M ]
V(λx. hM1 i) hM2 iMh(λk. M ) (λx. hF [x]i)i
ξk. M

βv
ηv
βΩ
reset-value
reset-lift
if k 6∈ FV(M ) shift-elim
if x 6∈ FV(F ) reset-shift
shift-reset

if x 6∈ FV(V )if x 6∈ FV(F )We also use the following axioms proved in [16]:hhM ii ∼ hM i
reset-reseth(λx. hF [x]i) M i ∼ hF [M ]i βΩ -reset-1

B

Some Propositions

Lemma 1 (Admissibility, Wand [22]) If M1 ∼ M10 and M2 ∼ M20 , then (M1 , M2 ) ∈ Rτ ⇐⇒(M10 , M20 ) ∈ Rτ .
Proof By induction on the length |τ | of τ , deﬁned by |d| = 0 and |σ/α → τ /β| = |β| + 1. If thetype is d, then for any large n(M1 , M2 ) ∈ Rd ⇐⇒ I 2 [[↓n M1 ]] ρid ∼ M2⇐⇒ I 2 [[↓n M10 ]] ρid ∼ M20⇐⇒ (M10 , M20 ) ∈ Rd .
If the type is σ/α → τ /β, then |β| < |σ/α → τ /β|, so we have
(M1 , M2 ) ∈ Rσ/α→τ /β⇐⇒ ∀(V1 , V2 ) ∈ Rσ . ∀(λv1 . K1 , λv2 . K2 ) |= τ ; α. (h(λv1 . K1 ) (M1 V1 )i, h(λv2 . K2 ) (M2 V2 )i) ∈ Rβ⇐⇒ ∀(V1 , V2 ) ∈ Rσ . ∀(λv1 . K1 , λv2 . K2 ) |= τ ; α. (h(λv1 . K1 ) (M10 V1 )i, h(λv2 . K2 ) (M20 V2 )i) ∈ Rβ⇐⇒ (M10 , M20 ) ∈ Rσ/α→τ /β220

Proposition 1 (λx. x, λx0 . x0 ) |= τ ; τ for any τ .
Proof

Let (V, V 0 ) ∈ Rτ . We need to show (h(λx. x) V i, h(λx0 . x0 ) V 0 i) ∈ Rτ . Sinceh(λx. x) V i ∼ hV i ∼ V

and the same for V 0 , the statement follows from the Admissibility Lemma.

2

Proposition 2 (λv. reset(app(var(n), v)), λv 0 . zn v 0 ) |= d ; d for any n.
Proof Let (V, V 0 ) ∈ Rd . From the deﬁnition of Rd , we have I [[↓m V ]] ρid ∼ V 0 for any large m.
We need to show(h(λv. reset(app(var(n), v))) V i, h(λv 0 . zn v 0 ) V 0 i) ∈ Rd .
The two terms reduce as follows:h(λv. reset(app(var(n), v))) V i ∼ hreset(app(var(n), V ))i ∼ reset(app(var(n), V ))h(λv 0 . zn v 0 ) V 0 i ∼ hzn V 0 i
From the Admissibility Lemma, we now need to show
(reset(app(var(n), V )), hzn V 0 i) ∈ Rd .
We calculate:I [[↓m (reset(app(var(n), V )))]] ρid ∼
∼
∼
∼
∼
∼

I [[Reset(↓m (app(var(n), V )))]] ρidhI [[↓m (app(var(n), V ))]] ρid i
hI [[App(↓m (var(n)), ↓m V )]] ρid ih(I [[↓m (var(n))]] ρid ) (I [[↓m V ]] ρid )ih(I [[Var(n)]] ρid ) V 0 i
hzn V 0 i
2

C

Correctness

Theorem 4 If A, α ` M : τ, β [W ], (ρ, ρ0 ) |= A, and (λv. K, λv 0 . K 0 ) |= τ ; α, then(h(λv. K) (P [[W ]] ρ)i, h(λv 0 . K 0 ) (I [[M ]] ρ0 )i) ∈ Rβ .
Proof

By induction on the structure of the proof of A, α ` M : τ, β [W ].

Case 1 (Variable). Assume n ∈ dom(A). Then A[n : τ ], α ` Var(n) : τ, α [Var(n)]. We need toshow(h(λv. K) (P [[Var(n)]] ρ)i, h(λv 0 . K 0 ) (I [[Var(n)]] ρ0 )i) ∈ Rα
assuming (ρ, ρ0 ) |= A[n : τ ] and (λv. K, λv 0 . K 0 ) |= τ ; α. From the deﬁnition of P and I and theAdmissibility Lemma, we have:(h(λv. K) (P [[Var(n)]] ρ)i, h(λv 0 . K 0 ) (I [[Var(n)]] ρ0 )i) ∈ Rα⇐⇒ (h(λv. K) (ρ (n))i, h(λv 0 . K 0 ) (ρ0 (n))i) ∈ Rα
which holds because (ρ, ρ0 ) |= A and (λv. K, λv 0 . K 0 ) |= τ ; α.
21Case 2 (Static Abstraction).

AssumeA[n : σ], α ` M : τ, β [W ]A, δ ` Lam(n, M ) : σ/α → τ /β, δ [Lam(n, W )]We need to show(h(λv. K) (P [[Lam(n, W )]] ρ)i, h(λv 0 . K 0 ) (I [[Lam(n, M )]] ρ0 )i) ∈ Rδassuming (ρ, ρ0 ) |= A and (λv. K, λv 0 . K 0 ) |= (σ/α → τ /β) ; δ. From the deﬁnition of P and I,
we have:(h(λv. K) (P [[Lam(n, W )]] ρ)i, h(λv 0 . K 0 ) (I [[Lam(n, M )]] ρ0 )i) ∈ Rδ⇐⇒ (h(λv. K) (λx. P [[W ]] ρ[x/n])i, h(λv 0 . K 0 ) (λx0 . I [[M ]] ρ0 [x0 /n])i) ∈ Rδ .
Since (λv. K, λv 0 . K 0 ) |= (σ/α → τ /β) ; δ, it suﬃces to show that
(λx. P [[W ]] ρ[x/n], λx0 . I [[M ]] ρ0 [x0 /n]) ∈ Rσ/α→τ /β .
So assume that (V, V 0 ) ∈ Rσ and (λv. L, λv 0 . L0 ) |= τ ; α. We want to show(h(λv. L) ((λx. P [[W ]] ρ[x/n]) V )i, h(λv 0 . L0 ) ((λx0 . I [[M ]] ρ0 [x0 /n]) V 0 )i) ∈ Rβ
which β-reduces to(h(λv. L) (P [[W ]] ρ[V /n])i, h(λv 0 . L0 ) (I [[M ]] ρ0 [V 0 /n])i) ∈ Rβ .
This statement holds by the induction hypothesis, because (ρ[V /n], ρ0 [V 0 /n]) |= A[n : σ] and(λv. L, λv. L0 ) |= τ ; α.
Case 3 (Dynamic Abstraction).

AssumeA[n : d], d ` M : d, d [W ]A, δ ` Lam(n, M ) : d, δ [Lam(n, W )]We need to show(h(λv. K) (P [[Lam(n, W )]] ρ)i, h(λv 0 . K 0 ) (I [[Lam(n, M )]] ρ0 )i) ∈ Rδassuming (ρ, ρ0 ) |= A and (λv. K, λv 0 . K 0 ) |= d ; δ. From the deﬁnition of P and I, we have:(h(λv. K) (P [[Lam(n, W )]] ρ)i, h(λv 0 . K 0 ) (I [[Lam(n, M )]] ρ0 )i) ∈ Rδ⇐⇒ (h(λv. K) (lam(λx. shift(λk. hreset(app(var(k), P [[W ]] ρ[var(x)/n]))i)))i,h(λv 0 . K 0 ) (λx0 . I [[M ]] ρ0 [x0 /n])i) ∈ Rδ
Since (λv. K, λv 0 . K 0 ) |= d ; δ, it suﬃces to show that(lam(λx. shift(λk. hreset(app(var(k), P [[W ]] ρ[var(x)/n]))i)), λx0 . I [[M ]] ρ0 [x0 /n]) ∈ Rd
that is,I [[↓m (lam(λx. shift(λk. hreset(app(var(k), P [[W ]] ρ[var(x)/n]))i)))]] ρid ∼ λx0 . I [[M ]] ρ0 [x0 /n]
22for any large m.
Now, (var(m), zm ) ∈ Rd holds, so we have (ρ[var(m)/n], ρ0 [zm /n]) |= A[n : d]. Furthermore, wehave (λv. reset(app(var(m + 1), v)), λv 0 . zm+1 v 0 ) |= d ; d from Proposition 2. Therefore, by the
induction hypothesis, we know that(h(λv. reset(app(var(m + 1), v))) (P [[W ]] ρ[var(m)/n])i, h(λv 0 . zm+1 v 0 ) (I [[M ]] ρ0 [zm /n])i) ∈ Rd
that is,I [[↓m0 h(λv. reset(app(var(m + 1), v))) (P [[W ]] ρ[var(m)/n])i]] ρid∼ h(λv 0 . zm+1 v 0 ) (I [[M ]] ρ0 [zm /n])ifor any large m0 . Since m is chosen to be large with respect tolam(λx. shift(λk. hreset(app(var(k), P [[W ]] ρ[var(x)/n]))i)) ,m + 2 is large with respect toh(λv. reset(app(var(m + 1), v))) (P [[W ]] ρ[var(m)/n])i .
Thus, we can take m0 = m + 2 and have:I [[↓m+2 h(λv. reset(app(var(m + 1), v))) (P [[W ]] ρ[var(m)/n])i]] ρid∼ h(λv 0 . zm+1 v 0 ) (I [[M ]] ρ0 [zm /n])i(1)

Now, to establish(lam(λx. shift(λk. hreset(app(var(k), P [[W ]] ρ[var(x)/n]))i)), λx0 . I [[M ]] ρ0 [x0 /n]) ∈ Rd
we calculate:I [[↓m (lam(λx. shift(λk. hreset(app(var(k), P [[W ]] ρ[var(x)/n]))i)))]] ρid= {propagation of ↓m }I [[Lam(m, Shift(m + 1, ↓m+2 hreset(app(var(m + 1), P [[W ]] ρ[var(m)/n]))i))]] ρid= {deﬁnition of I (twice)}
λzm . ξzm+1 . I [[↓m+2 hreset(app(var(m + 1), P [[W ]] ρ[var(m)/n]))i]] ρid [zm /m, zm+1 /m + 1]
= {deﬁnition of ρid }λzm . ξzm+1 . I [[↓m+2 hreset(app(var(m + 1), P [[W ]] ρ[var(m)/n]))i]] ρid∼ {βΩ }
λzm . ξzm+1 . I [[↓m+2 h(λv. reset(app(var(m + 1), v))) (P [[W ]] ρ[var(m)/n])i]] ρid∼ {equation (1)}λzm . ξzm+1 . h(λv 0 . zm+1 v 0 ) (I [[M ]] ρ0 [zm /n])i∼ {ηv }
λzm . ξzm+1 . hzm+1 (I [[M ]] ρ0 [zm /n])i∼ {shift-reset}
λzm . ξzm+1 . zm+1 (I [[M ]] ρ0 [zm /n])∼ {shift-elim}
λzm . I [[M ]] ρ0 [zm /n]= {renaming}
λx0 . I [[M ]] ρ0 [x0 /n]
23Case 4 (Static Application).

AssumeA, δ ` M1 : σ/α → τ /², β [W1 ]A, ² ` M2 : σ, δ [W2 ]A, α ` App(M1 , M2 ) : τ, β [App(W1 , W2 )]We must show(h(λv. K) (P [[App(W1 , W2 )]] ρ)i, h(λv 0 . K 0 ) (I [[App(M1 , M2 )]] ρ0 )i) ∈ Rβ
assuming (ρ, ρ0 ) |= A and (λv. K, λv 0 . K 0 ) |= τ ; α. From the deﬁnition of P and I, we have:(h(λv. K) (P [[App(W1 , W2 )]] ρ)i, h(λv 0 . K 0 ) (I [[App(M1 , M2 )]] ρ0 )i) ∈ Rβ⇐⇒ (h(λv. K) ((P [[W1 ]] ρ) (P [[W2 ]] ρ))i, h(λv 0 . K 0 ) ((I [[M1 ]] ρ0 ) (I [[M2 ]] ρ0 ))i) ∈ Rβ
which can be rewritten using βΩ to:(h(λw1 . (λv. K) (w1 (P [[W2 ]] ρ))) (P [[W1 ]] ρ)i, h(λm1 . (λv 0 . K 0 ) (m1 (I [[M2 ]] ρ0 ))) (I [[M1 ]] ρ0 )i) ∈ Rβ
Since (ρ, ρ0 ) |= A, we are done by the induction hypothesis if we can prove(λw1 . (λv. K) (w1 (P [[W2 ]] ρ)), λm1 . (λv 0 . K 0 ) (m1 (I [[M2 ]] ρ0 ))) |= (σ/α → τ /²) ; δ .
So take any values (w10 , m01 ) ∈ Rσ/α→τ /² . We then need to show(h(λv. K) (w10 (P [[W2 ]] ρ))i, h(λv 0 . K 0 ) (m01 (I [[M2 ]] ρ0 ))i) ∈ Rδwhich can be rewritten using βΩ to:(h(λw2 . (λv. K) (w10 w2 )) (P [[W2 ]] ρ)i, h(λm2 . (λv 0 . K 0 ) (m01 m2 )) (I [[M2 ]] ρ0 )i) ∈ Rδ
Since (ρ, ρ0 ) |= A, we are again done by the induction hypothesis if we can prove(λw2 . (λv. K) (w10 w2 ), λm2 . (λv 0 . K 0 ) (m01 m2 )) |= σ ; ² .
So take any values (w20 , m02 ) ∈ Rσ . We then need to show(h(λv. K) (w10 w20 )i, h(λv 0 . K 0 ) (m01 m02 )i) ∈ R²
which holds because (λv. K, λv 0 . K 0 ) |= τ ; α.
Case 5 (Dynamic Application).

AssumeA, δ ` M1 : d, β [W1 ] A, d ` M2 : d, δ [W2 ]A, d ` App(M1 , M2 ) : d, β [App(W1 , W2 )]We need to show(h(λv. K) (P [[App(W1 , W2 )]] ρ)i, h(λv 0 . K 0 ) (I [[App(M1 , M2 )]] ρ0 )i) ∈ Rβ24

assuming (ρ, ρ0 ) |= A and (λv. K, λv 0 . K 0 ) |= d ; d. Because we have:h(λv. K) (P [[App(W1 , W2 )]] ρ)i= {deﬁnition of P}h(λv. K) (ξk. reset(let(app(P [[W1 ]] ρ, P [[W2 ]] ρ), lam(λt. k (var(t))))))i∼ {reset-shift}h(λk. reset(let(app(P [[W1 ]] ρ, P [[W2 ]] ρ), lam(λt. k (var(t)))))) (λx. h(λv. K) xi)i
∼ {βv }
hreset(let(app(P [[W1 ]] ρ, P [[W2 ]] ρ), lam(λt. (λx. h(λv. K) xi) (var(t)))))i∼ {βv }
hreset(let(app(P [[W1 ]] ρ, P [[W2 ]] ρ), lam(λt. h(λv. K) (var(t))i)))i∼ {βΩ }h(λw1 . reset(let(app(w1 , P [[W2 ]] ρ), lam(λt. h(λv. K) (var(t))i)))) (P [[W1 ]] ρ)iandh(λv 0 . K 0 ) (I [[App(M1 , M2 )]] ρ0 )i= {deﬁnition of I}h(λv 0 . K 0 ) ((I [[M1 ]] ρ0 ) (I [[M2 ]] ρ0 ))i∼ {βΩ }
h(λm1 . (λv 0 . K 0 ) (m1 (I [[M2 ]] ρ0 ))) (I [[M1 ]] ρ0 )i ,we need to show(h(λw1 . reset(let(app(w1 , P [[W2 ]] ρ), lam(λt. h(λv. K) (var(t))i)))) (P [[W1 ]] ρ)i,h(λm1 . (λv 0 . K 0 ) (m1 (I [[M2 ]] ρ0 ))) (I [[M1 ]] ρ0 )i) ∈ Rβ .
Since (ρ, ρ0 ) |= A, we are done by the induction hypothesis if we can prove(λw1 . reset(let(app(w1 , P [[W2 ]] ρ), lam(λt. h(λv. K) (var(t))i))),λm1 . (λv 0 . K 0 ) (m1 (I [[M2 ]] ρ0 ))) |= d ; δ .
So take any values (w10 , m01 ) ∈ Rd . We then need to show
(hreset(let(app(w10 , P [[W2 ]] ρ), lam(λt. h(λv. K) (var(t))i)))i, h(λv 0 . K 0 ) (m01 (I [[M2 ]] ρ0 ))i) ∈ Rδwhich can be rewritten using βΩ to:(h(λw2 . reset(let(app(w10 , w2 ), lam(λt. h(λv. K) (var(t))i)))) (P [[W2 ]] ρ)i,h(λm2 . (λv 0 . K 0 ) (m01 m2 )) (I [[M2 ]] ρ0 )i) ∈ Rδ
Since (ρ, ρ0 ) |= A, we are again done by the induction hypothesis if we can prove(λw2 . reset(let(app(w10 , w2 ), lam(λt. h(λv. K) (var(t))i))), λm2 . (λv 0 . K 0 ) (m01 m2 )) |= d ; d .
So take any values (w20 , m02 ) ∈ Rd . We then need to show
(hreset(let(app(w10 , w20 ), lam(λt. h(λv. K) (var(t))i)))i, h(λv 0 . K 0 ) (m01 m02 )i) ∈ Rd
which can be reduced (using reset-value) to:(reset(let(app(w10 , w20 ), lam(λt. h(λv. K) (var(t))i))), h(λv 0 . K 0 ) (m01 m02 )i) ∈ Rd .
25

We calculate (for any large n):
=
=
=
∼
∼
∼
∼

I [[↓n (reset(let(app(w10 , w20 ), lam(λt. h(λv. K) (var(t))i))))]] ρid{deﬁnition of let}I [[↓n (reset(app(lam(λt. h(λv. K) (var(t))i), app(w10 , w20 ))))]] ρid{propagation of ↓n }I [[Reset(App(Lam(n, ↓n+1 h(λv. K) (var(n))i), App(↓n w10 , ↓n w20 )))]] ρid{deﬁnition of I (four times)}h(λzn . I [[↓n+1 h(λv. K) (var(n))i]] ρid ) ((I [[↓n w10 ]] ρid ) (I [[↓n w20 ]] ρid ))i{(w20 , m02 ) ∈ Rd }h(λzn . I [[↓n+1 h(λv. K) (var(n))i]] ρid ) ((I [[↓n w10 ]] ρid ) m02 )i{(w10 , m01 ) ∈ Rd }h(λzn . I [[↓n+1 h(λv. K) (var(n))i]] ρid ) (m01 m02 )i{(λv. K, λv 0 . K 0 ) |= d ; d and (var(n), zn ) ∈ Rd }h(λzn . h(λv 0 . K 0 ) zn i) (m01 m02 )i{βΩ -reset-1 }h(λv 0 . K 0 ) (m01 m02 )i

Case 6 (Static Shift).

AssumeA[n : τ /δ → α/δ], σ ` M : σ, β [W ]A, α ` Shift(n, M ) : τ, β [Shift(n, W )]We need to show(h(λv. K) (P [[Shift(n, W )]] ρ)i, h(λv 0 . K 0 ) (I [[Shift(n, M )]] ρ0 )i) ∈ Rβ
assuming (ρ, ρ0 ) |= A and (λv. K, λv 0 . K 0 ) |= τ ; α. From
=
∼
∼
∼
and
=
∼
∼
∼

h(λv. K) (P [[Shift(n, W )]] ρ)i{deﬁnition of P}h(λv. K) (ξk. P [[W ]] ρ[k/n])i{reset-shift}h(λk. P [[W ]] ρ[k/n]) (λa. h(λv. K) ai)i{βv }hP [[W ]] ρ[λa. h(λv. K) ai/n]i{βΩ }h(λx. x) (P [[W ]] ρ[λa. h(λv. K) ai/n])ih(λv 0 . K 0 ) (I [[Shift(n, M )]] ρ0 )i{deﬁnition of I}h(λv 0 . K 0 ) (ξk. I [[M ]] ρ0 [k/n])i{reset-shift}h(λk. I [[M ]] ρ0 [k/n]) (λa0 . h(λv 0 . K 0 ) a0 i)i{βv }hI [[M ]] ρ0 [λa0 . h(λv 0 . K 0 ) a0 i/n]i{βΩ }h(λx0 . x0 ) (I [[M ]] ρ0 [λa0 . h(λv 0 . K 0 ) a0 i/n])i26

we have:(h(λv. K) (P [[Shift(n, W )]] ρ)i, h(λv 0 . K 0 ) (I [[Shift(n, M )]] ρ0 )i) ∈ Rβ⇐⇒ (h(λx. x) (P [[W ]] ρ[λa. h(λv. K) ai/n])i, h(λx0 . x0 ) (I [[M ]] ρ0 [λa0 . h(λv 0 . K 0 ) a0 i/n])i) ∈ Rβ
Since (λx. x, λx0 . x0 ) |= σ ; σ, we are done by the induction hypothesis if we can prove(ρ[λa. h(λv. K) ai/n], ρ0 [λa0 . h(λv 0 . K 0 ) a0 i/n]) |= A[n : τ /δ → α/δ]or in other words,(λa. h(λv. K) ai, λa0 . h(λv 0 . K 0 ) a0 i) ∈ Rτ /δ→α/δ .

So take any (V, V 0 ) ∈ Rτ and (λu. L, λu0 . L0 ) such that (λu. L, λu0 . L0 ) |= α ; δ. We need to prove(h(λu. L) h(λv. K) V ii, h(λu0 . L0 ) h(λv 0 . K 0 ) V 0 ii) ∈ Rδwhich holds since (λv. K, λv 0 . K 0 ) |= τ ; α.
Case 7 (Dynamic Shift).

AssumeA[n : d], σ ` M : σ, β [W ]A, d ` Shift(n, M ) : d, β [Shift(n, W )]We need to show(h(λv. K) (P [[Shift(n, W )]] ρ)i, h(λv 0 . K 0 ) (I [[Shift(n, M )]] ρ0 )i) ∈ Rβ
assuming (ρ, ρ0 ) |= A and (λv. K, λv 0 . K 0 ) |= d ; d. From
=
∼
∼
∼
∼
∼

h(λv. K) (P [[Shift(n, W )]] ρ)i{deﬁnition of P}h(λv. K) (ξk. P [[W ]] ρ[lam(λu. hk (var(u))i)/n])i{reset-shift}h(λk. P [[W ]] ρ[lam(λu. hk (var(u))i)/n]) (λa. h(λv. K) ai)i{βv }hP [[W ]] ρ[lam(λu. h(λa. h(λv. K) ai) (var(u))i)/n]i{βv }hP [[W ]] ρ[lam(λu. hh(λv. K) (var(u))ii)/n]i{reset-reset}hP [[W ]] ρ[lam(λu. h(λv. K) (var(u))i)/n]i{βΩ }h(λx. x) (P [[W ]] ρ[lam(λu. h(λv. K) (var(u))i)/n])i

and
=
∼
∼
∼

h(λv 0 . K 0 ) (I [[Shift(n, M )]] ρ0 )i{deﬁnition of I}h(λv 0 . K 0 ) (ξk. I [[M ]] ρ0 [k/n])i{reset-shift}h(λk. I [[M ]] ρ0 [k/n]) (λu0 . h(λv 0 . K 0 ) u0 i)i{βv }hI [[M ]] ρ0 [λu0 . h(λv 0 . K 0 ) u0 i/n]i{βΩ }h(λx0 . x0 ) (I [[M ]] ρ0 [λu0 . h(λv 0 . K 0 ) u0 i/n])i ,27

we have:(hλv. K (P [[Shift(n, W )]] ρ)i, hλv 0 . K 0 (I [[Shift(n, M )]] ρ0 )i) ∈ Rβ⇐⇒ (h(λx. x) (P [[W ]] ρ[lam(λu. h(λv. K) (var(u))i)/n])i,h(λx0 . x0 ) (I [[M ]] ρ0 [λu0 . h(λv 0 . K 0 ) u0 i/n])i) ∈ Rβ

Since (λx. x, λx0 . x0 ) |= σ ; σ, we are done by the induction hypothesis if we can prove(ρ[lam(λu. h(λv. K) (var(u))i)/n], ρ0 [λu0 . h(λv 0 . K 0 ) u0 i/n]) |= A[n : d]or in other words,(lam(λu. h(λv. K) (var(u))i), λu0 . h(λv 0 . K 0 ) u0 i) ∈ Rd .
Now, (var(m), zm ) ∈ Rd holds, so we have (h(λv. K) (var(m))i, h(λv 0 . K 0 ) zm i) ∈ Rd because(λv. K, λv 0 . K 0 ) |= d ; d. If m is suﬃciently large, then we haveI [[↓m+1 h(λv. K) (var(m))i]] ρid ∼ h(λv 0 . K 0 ) zm i .

(2)

To obtain (lam(λu. h(λv. K) (var(u))i), λu0 . h(λv 0 . K 0 ) u0 i) ∈ Rd , we calculate for any large m:
I [[↓m (lam(λu. h(λv. K) (var(u))i))]] ρid= {propagation of ↓m }I [[Lam(m, ↓m+1 h(λv. K) (var(m))i)]] ρid= {deﬁnition of I}
λzm . I [[↓m+1 h(λv. K) (var(m))i]] ρid [zm /m]= {deﬁnition of ρid }λzm . I [[↓m+1 h(λv. K) (var(m))i]] ρid∼ {equation (2)}λzm . h(λv 0 . K 0 ) zm i
= {renaming}
λu0 . h(λv 0 . K 0 ) u0 i
Case 8 (Reset).

AssumeA, σ ` M : σ, τ [W ]A, α ` Reset(M ) : τ, α [Reset(W )]We need to show(h(λv. K) (P [[Reset(W )]] ρ)i, h(λv 0 . K 0 ) (I [[Reset(M )]] ρ0 )i) ∈ Rα
assuming (ρ, ρ0 ) |= A and (λv. K, λv 0 . K 0 ) |= τ ; α. From the deﬁnition of P and I, we have:(h(λv. K) (P [[Reset(W )]] ρ)i, h(λv 0 . K 0 ) (I [[Reset(M )]] ρ0 )i) ∈ Rα⇐⇒ (h(λv. K) hP [[W ]] ρii, h(λv 0 . K 0 ) hI [[M ]] ρ0 ii) ∈ Rα⇐⇒ (h(λv. K) h(λx. x) (P [[W ]] ρ)ii, h(λv 0 . K 0 ) h(λx0 . x0 ) (I [[M ]] ρ0 )ii) ∈ Rα
From (λv. K, λv 0 . K 0 ) |= τ ; α, it suﬃces to show(h(λx. x) (P [[W ]] ρ)i, h(λx0 . x0 ) (I [[M ]] ρ0 )i) ∈ Rτwhich holds by the induction hypothesis since (λx. x, λx0 . x0 ) |= σ ; σ.
This completes the cases for the proof.
282