数理解析研究所講究録1106 巻 1999 年 37-49

37

Domain-Free$\lambda\mu$-Calculus for Polymorphism and$\mathrm{C}\mathrm{a}\mathrm{l}1_{-}\mathrm{b}\mathrm{y}-\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{u}\mathrm{e}^{*}$

Ken-etsu Fujita (藤田憲悦)
Kyushu Institute of Technology, Iizuka 820-8502, Japanfujiken@dumbo.ai.kyutech.ac.jp
Abstract

We introduce a domain-free -calculus of call-by-value as a short-hand for thesecond order Church-style. Our motivation comes from the observation that
Curry-style polymorphic calculi, control operators such as callcc or -operators
cannot, in general, treat the terms placed on the control operator’s left. Following
the continuation semantics, we also discuss the notion of values in classical system,and propose an extended forrn of values. It isthat the CPS-translation issound with respect to domain-free(2nd-order -calculus).
$\lambda\mu$$\mathrm{i}_{11}$$\mu$$\mathrm{s}1_{10}\mathrm{W}\mathrm{l}1$$\lambda 2$

1$\lambda$

Introduction

On the basis of the-De Bruijn isomorphism [How80], proof reductions canbe regarded as computational rules, and the algorithmic contents of proofs can be used toobtain correct programs that satisfy logical specifications. The computational meaning of
proofs has been investigated in a wide range of fields, including not only intuitionistic logic
but also classical logic alld modal logic [Koba97]. In the area of classical logic, there havebeen a number of noteworthy investigations including,
Rehof&S\emptyset rensen|RS94], deand. As far as we know, however, polymorphic call-by-valuc calculus is lessstudied from the viewpoint of classical logic. In this paper, we introduce a domainfree -calculus of call-by-value as a short-hand for the second order Church-style. Our
motivation comes from the observation that in Curry-style polymorphic calculi, control
operators such as callcc or -operators cannot, in general, treat the terlns placed on
the control operator’s left. Following the continuation semantics, we also discuss thenotion of values in classical system, and propose an extended form of values. It is shownthat the CPS-translation is sound with respect to domain-free(Systemof Girard,
Polymorphic calculus of Reynolds). We observe that the inverse of the soundness does nothold, and that adding -reduction in Ong&Stewart [OS97] breaks down the soundnessof the CPS-translation. As one of by-products, it can be obtained that the second ordercall-by-value -calculus in domain-free style has the strong normalization property.
$\mathrm{c}_{\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}}- \mathrm{H}\mathrm{o}\mathrm{w}\mathrm{a}\mathrm{r}\mathrm{d}$$\mathrm{G}\mathrm{r}\mathrm{i}\mathrm{f}\mathrm{f}\mathrm{i}\mathrm{n}[\mathrm{G}\mathrm{r}\mathrm{i}\mathrm{f}90],$$\mathrm{P}\mathrm{a}\mathrm{r}\mathrm{i}\mathrm{g}\mathrm{o}\mathrm{t}[\mathrm{P}\mathrm{a}\mathrm{r}\mathrm{i}92],$$\mathrm{B}\mathrm{e}\mathrm{r}\mathrm{a}\mathrm{r}\mathrm{d}\mathrm{i}\ \mathrm{B}\mathrm{a}\mathrm{r}\mathrm{b}\mathrm{a}\mathrm{n}\mathrm{e}\mathrm{r}\mathrm{a}1^{\mathrm{B}}\mathrm{B}93],$$\mathrm{M}\mathrm{u}\mathrm{r}\mathrm{t}\mathrm{h}\mathrm{y}[\mathrm{M}\mathrm{u}\mathrm{r}\mathrm{t}91]$$\mathrm{G}\mathrm{r}\mathrm{o}\mathrm{O}\mathrm{t}\mathrm{e}[\mathrm{G}\mathrm{r}\mathrm{o}\mathrm{o}95]$$\mathrm{O}\mathrm{n}\mathrm{g}[\mathrm{O}\mathrm{n}\mathrm{g}96]$$\lambda\mu$$\mu$$\lambda 2$$F$$\perp$$\lambda\mu$*This is aversion of Explicitly Typedsented at the 4th International Conferellce Typed Lambda
Italy, Apri11999.
$\mathrm{r}\mathrm{e}_{\lrcorner}\mathrm{v}\mathrm{i}\mathrm{s}\mathrm{e}\mathrm{d}$$\lambda\mu- c_{a}lculn\mathit{8}$for Polymorphism and Call-by-Va,lv.e pre-$CalC\gamma rxi$

and Applications (TLCA ’99), L’Aquila.

38

2

Style of (Typed) -Terms; Curry-Style, ChurchStyle, and Domain-free$\lambda$

There are well-known two style of typed lambda calculi, i.e., Curry-style and Churchstyle. Those styles are also called implicitly typed and explicitly typed, respectively.
, there is a forgetful map from
With respect to the simply typed lambda calculus-Curry can be\‘a la Church to \‘a la Curry, and conversely, well-typed terms in-Church [Bare92]. In the case of ML [Mi178], there also
lifted to well-typed terms inexists implicitly typed and explicitly typed systems, and they are essentially equivalent[HM93]. Hence, the implicitly typed system serves as a short-hand for the explicitly
typed system. However, the equivalence between Curry-style and Church-style does not-calculus in Curry-stylealways hold for complex systems. Parigot [Pari92] introduced
as second order classical logic although -calculus \‘a la Church was also given [Pari97].
An intrinsically classical reduction is called the structural reduction that is a kind of
permutative proof reductions in Prawitz [Praw71] or the so-called cornmutative cut. The-calculus of Parigot is now known as a call-by-name system. If we construct a call-calculus, then the Curry-style cannot work for a consistent system. In a
by-valuecall-by-value system of , we can adopt a certain permutative reduction [Pari92, OS97],
called the symmetric structural reduction, to manage the terms placed on theleft. However, the symmetric structural proof reduction, in general, violates the subject
reduction property in the Curry-style. Consider the following figure in which erasing type
information of polymorphic terms makes it possible to apply the symmetric structural
reduction uncorrectly:$\lambda^{arrow}$$\lambda^{arrow}$$\lambda^{arrow}$$\lambda^{arrow}$$\lambda\mu$$\lambda\mu$$\lambda\mu$$\lambda\mu$$\lambda\mu$$\mu- \mathrm{o}\mathrm{p}\mathrm{e}\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{o}\mathrm{r}’ \mathrm{s}$$\frac{M_{1}.\sigma_{1}}{M_{1}\cdot\forall t.\sigma_{1}}.\cdot(\forall I)^{*}$$\frac{M_{1}.\cdot.\sigma_{1}}{[\alpha]M_{1}\cdot\perp\cdot\sigma 1\alpha}$,::$V:(\forall t.\sigma_{1})arrow\sigma_{2}$$\overline{VM_{1}\cdot.\sigma_{2}}$$M:\perp;\sigma_{1}^{\alpha}$$\overline{[\alpha](VM1.)\cdot.\perp\cdot,\sigma_{2}^{\alpha}}$.
$. \frac{V.(\forall t.\sigma_{1})arrow\sigma_{2}\frac{\mu\alpha.M\cdot\sigma_{1}}{\mu\alpha.M\cdot\forall t.\sigma_{1}}}{V(\mu\alpha.M).\sigma_{2}}.\cdot$$\frac{I\mathcal{V}I[V\Rightarrow\alpha]\cdot\perp\backslash .\sigma^{\alpha}2}{\mu\alpha.M[V\Rightarrow\alpha].\sigma_{2}}.’..\cdot$$\triangleright$

denotes a term obtained by replacing each subterm of the form
where
and the type
in $M$ with $[\alpha](VN)$ . Here, when $M$ is in the form of$x_{i}(1\leq
i\leq
7l)$
is broken, the eigenvariable condition of
depends on type of somedown. For instance,$[\alpha]N$$\Lambda I[V\Rightarrow a]$$[\alpha](\lambda x_{1}\cdots X_{n}.\Lambda\phi’)$$\sigma_{1}$$(\forall I)^{*}$$\lambda x.(\lambda f.(\lambda X_{1}x_{2}.X_{2})(fx)(f(\lambda X.X)))(\mu\alpha.[\alpha](\lambda y.\mu\beta.[\alpha](\lambda v.y)))$has type $tarrow tarrow t$ . But this term is reduced totural reduction. Let
Then similarly$\lambda x.x$

$P\equiv\lambda f.(\lambda X_{1}x_{2^{X_{2}}}.)(t\prime X)(f(\lambda_{X}.X))$$\lambda g.(\lambda x.g(PQ_{X)})(\lambda x.g(PQX))$:

by the use of the symmetric struc.
and$Q\equiv\mu\alpha.[\alpha](\lambda y.\mu\beta.[\alpha](\lambda v.y))$$(\forall t’.(t’arrow t’))arrow tarrow t$. On the other hand, the caseis reduced to
is a special case where the symmetric structural reduction is, and then, for example,
phic$\lambda g.(\lambda x.g(xx))(\lambda x.g(xx))$$\mu\alpha.M$

of$\mu\alpha.[\alpha](\lambda v.\mu\beta.[\alpha](\lambda x$.licable even to polymor-$\mathrm{a}\mathrm{p}\mathrm{p}$$\mu\alpha.\Lambda T$: $tarrow t$. This kind of phenomenon was first discovered by Harper &Lillibis reduced tocounterexample[HL91]
for ML with callcc. From the viewpoint of classical
a
as
ridge
-calculus la Curry
proof reductions, the fatal defect can be explained such that in(-order classical logic), an application of the symmetric structural reduction, in general, breaks down the eigenvariable condition of polymorphic generalization, and then the$\lambda x.((\lambda f.(\lambda X_{1}x_{2}.X_{2})(fx)(f(\lambda_{X}.X)))(\mu\alpha.[\alpha](\lambda v.\mu\beta.[\alpha](\lambda_{X.X})))x)$$\lambda x.x$$\lambda\mu$$2\mathrm{n}\mathrm{d}$$\grave{‘}\mathrm{a}$39terms placed on the polymorphic
left cannot be managed by the symmetricstructural reduction. In terms of explicit polymorphism, in other words, an evaluation
under A-abstractions cannot be allowed without restricting At.M to At.V
. Evenin the Damas-Milner style [DM82] (implicitly typed) plus control operators, a simil\‘aarr
defect still happens under a-like call-by-value. To avoid such a problem in implicitly typed ML with control operators, one can adopt an -like expansion forpolymorphic control operators [Fuji98], such that
let $f=\mu\alpha.M_{1}$ in
let,inwhere each subterm in the form ofinis replaced with.
Another natural way to avoid the problem is to take a domain-free system introducedby Barthe&S\emptyset rensen [BS97], see the following table:$\mu- \mathrm{o}\mathrm{p}\mathrm{e}\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{o}\mathrm{r}’ \mathrm{s}$$[\mathrm{H}\mathrm{L}93\mathrm{a}]$$\mathrm{M}\mathrm{L}$$\mathrm{M}\mathrm{L}$$[\mathrm{H}\mathrm{L}93\mathrm{a}, \mathrm{H}\mathrm{L}93\mathrm{b}]$$\eta$$f=\lambda x.\mu\alpha.M1[\alpha\Leftarrow x]$$M_{2}\triangleright$$[\alpha](\lambda y.w)$$M_{2}$$[\alpha](\lambda y.w)x$$M_{1}$$\ovalbox{\tt\small REJECT}_{\mathrm{C}-\mathrm{s}}^{\mathrm{c}\mathrm{h}\mathrm{h}1\mathrm{e}\lambda x_{M}}\mathrm{D}_{0}\mathrm{m}\mathrm{a}\mathrm{i}^{-\mathrm{s}}\mathrm{n}-\mathrm{f}\mathrm{r}\mathrm{e}\mathrm{e}\lambda_{X}\Lambda \mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}\mathrm{t}\mathrm{y}1\mathrm{u}\mathrm{r}\mathrm{C}\mathrm{t}\mathrm{y}\sigma \mathrm{e}\lambda XMMM\Lambda ttM,M\sigma M,M\sigma$

In the above example, the term is a polymorphic term, and this type becomes
Here, thc explicitly typed term as a form of a value,is used forsuch that$Q$$l/^{\mathit{7}}\equiv\Lambda t.Q$$\forall t.(tarrow t)$.

$\beta_{v}- \mathrm{r}\mathrm{C}\mathrm{d}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{s}\vdash$’$\lambda x.(\lambda f.(\lambda X_{1}X_{2}.X_{2})(ft_{X})(f’(tarrow t)(\lambda_{X.X})))V:tarrow tarrow t$

is now reduced to. In the next section, under the call-by-value
we introduce
a domain-free -calculus, which is regarded as a short-hand for the complete Churchstyle. To obtain the results in this paper, it is enough to consider a system suc.h thatis represented simply as
such as a lifting andas $M()$ , andisreduced to $M$ . A similar observation is given for let-polymorphism by nanie in Leroy[Lero93]. The annotations andfor polymorphic terms play a role of choosing anappropriate computation under call-by-value. However, from the viewpoint of logic, adomain-free -calculus is considered here rather than such a simplified polymorphism
using the annotations.
On the other hand, Harper&Lillibridge
extensively studied explicit polymorphism and CPS-conversion forwith callcc. The call-by-value system
introduced
in section 3 can be regarded as a meaningful simplification of the second order fragmentof their system.
$\lambda vx.x$$\mathrm{S}\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{g}\mathrm{y}^{\Gamma}$$\lambda\mu$$\Lambda t.\Lambda_{i}l$$\Lambda M$$M\sigma$$(\Lambda M)()$$()$$\Lambda$$\lambda\mu$$[\mathrm{H}\mathrm{L}93\mathrm{a}]$$F_{w}$

3$\lambda_{V}\mu$$\lambda_{V}\mu$-Calculus in Domain-Free Style

Following the observation in the previous section, we introduce a domain-free -calculusof-value for polymorphisnu. Terms in domain-free style have domain-free.bstraction[BS97].
The types are defined from type variables and a type constant . We have a
set of term variables, and a set of names (that will be called continuation
variables later). The type assumptions are defined as usual, and is used for aset of name-indexed types. The terms [ are defined as term variables, -abstractions,applications, -abstractions, or named terms. Since wesorted variables, i.e., term
variable alud type variable , we have cxplicit distinction between terms and types, andthen -abstraction is used for both term variable and type variable abstractions.
From a logical viewpoint, the typing ruleforis regarded as a classicalinference rule such that infer: from:. The$\lambda\mu$$\mathrm{c}\mathrm{a}\mathrm{l}1_{-}\mathrm{b}\mathrm{y}$$\lambda- \mathrm{a}$$t$$\sigma$$x,$ $y,$ $z,$$\alpha,$$\beta,$$\perp$$\cdots$$\cdots$$\triangle$$\Lambda/$$\lambda$$\mathrm{h}\mathrm{a}1’\cdot \mathrm{e}$

$\mu$

$x$

$t$

$\lambda$$(\perp E)$$\Gamma,$$\urcorner\triangle\vdash\mu\alpha.M$$\sigma$$\mu\alpha.M$$\Gamma,$$\neg\Delta,$$\alpha$$\urcorner\sigma\vdash\Lambda C$$:\perp$40
can be considered as a special case of -introduction by thefortyping ruleuse of $(arrow E)$ . On the basis of the continuation selnantics in the next section, a name, the continuation variable
can be interpreted as a continuation variable. In the ruleappears only in the function-position, but not in the argument-position. Here, the.
can be discharged only byofcorresponding tonegative assumption-introduction is called a regularThis style of proofs consisting of the special caseproof in Andou [Ando95]. The notion of values is introduced below as an extended
and left
form; the class of values is closed under both value-substitutions induced byof theThe
definition
later.
,
asbydefinedcontext-replacements
inducedand right
reduction rules is given below under call-by-value. In particular, the classical reductions
below can be explained as a logical permutative reduction in the sense of Prawitz,[Praw71] and Andou [Ando95]. Here, in the reduction of$M$$M’$
can beinwith the form
and type of each subterm
since both type of
application,theconsidered as members of the segments ending with the type of$M’$ , and then $M[y\Leftarrow N]$ (each$(arrow
E,\forall
E)$
is
up
each
occurrencetoisshiftedofreplaced with $[\alpha](M^{;}N))$ is obtained. This reduction is also called a structural reduction
is not regardedin Parigot [Pari92]. On the other hand, since a term of the form
will not be a -contractum, but will be a contractum of
as a value,
below, which can be considered as a symmetric structural reduction. $FV(M)$ stands forthe set of free variables in $M$ , and $FN(M)$ for the set of free names in $M$ .
:Types aType Assumptions
Ma $|\mu\alpha.M|[\alpha]M$
Terms $M::=x|\lambda x.M|$ MM
Type Assignment$(\perp I)$$\perp$$[\alpha]M$$(\perp I)$$\alpha$$(\perp E)$$(\perp I)$$\sigma^{a}$$\alpha:\urcorner\sigma$$\mathrm{o}\mathrm{f}\perp$$(\beta_{v})$$(\mu_{l,r})$$(\mu_{l,r},t)$$(\mu\alpha.M)N\triangleright\mu\alpha.M[\alpha\Leftarrow N]$$[\alpha]M’$$\mu\alpha.M$$\mu\alpha.M$$[\alpha]M’$$\mu\alpha.M$$(\lambda x.M_{1})(\mu\alpha.M_{2})$$(\mu_{l})$$\beta$$\lambda_{V}\mu$$::=t|\perp|\sigmaarrow\sigma|\forall t.\sigma$$\triangle::=\langle\rangle|\triangle,$$\Gamma::=\langle\rangle|\Gamma,$ $x:\sigma$$\sigma^{\alpha}$$|\lambda t.M|$:$\Gamma\vdash x$$\Gamma(x);\Delta$$.. \frac{\Gamma\vdash M_{1}.\sigma_{1}arrow\sigma 2,\triangle\Gamma.\vdash M2\cdot\sigma_{1\prime}\Delta}{\Gamma\vdash M_{12\cdot 2}M\cdot\sigma,\triangle}..\cdot(arrow E)$$. \frac{\Gamma,x.\sigma_{1}\vdash.M.\sigma_{2},\Delta}{\mathrm{r}\vdash\lambda x.M\cdot\sigma_{1}arrow\sigma 2,\triangle}...(arrow I)$$\frac{\Gamma\vdash\Lambda\phi.\sigma\cdot\triangle}{\Gamma\vdash\lambda t.M\cdot\forall t.\sigma\cdot\triangle}..\backslash ,(\forall I)^{*}$$\frac{\Gamma\vdash M.\forall t.\sigma_{1}\cdot\Delta}{\Gamma\vdash M\sigma 2\cdot\sigma_{1}[t\cdot=\sigma 2],\triangle}.\cdot.’.(\forall E)$$\frac{\Gamma\vdash_{1}\mathrm{W}.\perp\cdot.\triangle,\sigma^{\alpha}}{\Gamma\vdash\mu\alpha.M’.\sigma\cdot\triangle}.,(\perp E)$$\frac{\Gamma\vdash M.\cdot\sigma_{l}\triangle}{\Gamma\vdash[\alpha]M.\perp\cdot\triangle,\sigma\alpha}.,\cdot.(\perp I)$

denotes the eigenvariable condition.
where
Values $V::=x|\lambda x.M|\lambda t.M|[\alpha]M$
Term reductions$(\beta_{v})(\lambda x.M)V\triangleright M[x:=V]$ ;if.
Al $[t:=\sigma]$ ;;;if $\alpha\not\in FN(M))$;
replacing each subterm of thedenotes a term obtained bywhere the term$M$$[\alpha](M’N)$
right is(context) placed on. That is, the
in
with
folm
denotes a. In turn, the term
replaced in an argulnent position of $M’$ inin $M$ with $[\alpha](VM’)$ .
term obtained by $M$ replacing each subterm of the form
eta–reduction and $(rn)$ , renaming rules,
Values are reduced to simpler values by
and those rules are restricted to values, whose condition is necessary to establish a sound
CPS-translation in section 4. We note that as observed in Ong&Stewart [OS97], there areclosed normal forms which are not values, called canonical forms, e.g.,in [OS97], but in this case,in [Pari93] orThose terms can be reduced by$(\forall I)^{*}$$(\eta_{v})\lambda x.Vx\triangleright V$$x\not\in FV(V)_{\backslash }$$(\beta_{f})(\lambda t.M)\sigma\triangleright$$(\mu_{t})(\mu\alpha.\mathrm{J}/I)\sigma\triangleright\mu_{\alpha.M},[\alpha\Leftarrow\sigma])$$(\ell\iota_{r})(\mu\alpha.\Lambda\phi_{1})M_{2}\triangleright\mu\alpha.M_{1}[\alpha\Leftarrow M_{2}]$$(\mu_{l})V(\mu\alpha.M)\triangleright\mu\alpha.\Lambda l[V\Rightarrow\alpha]$$(rn)[\alpha](\mu\beta.V)\triangleright V[\beta:=\alpha]$$(\mu-\eta)\mu\alpha.[a]l\iota/I\triangleright M$$\Lambda_{i}I$$M[\alpha\Leftarrow \mathit{1}\mathrm{V}]$$[\alpha]M’$$\mu\alpha.M’ \mathrm{s}$$\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{n}\mathrm{l},\mathrm{s}$$M[V\Rightarrow\alpha]$$[\alpha]M’$$[\alpha]M’$$(\eta_{1},),$$\mu\alpha.[\alpha](\lambda_{X}.\mu\beta.[\alpha](\lambda v.x)\mathrm{I}\cdot$$(S_{3})$$\zeta_{fu}^{ext}n$41
is reduced in the two ways (not confluent). Note also that the failurc ofoperational extensionality foris demonstrated in [OS97]. In fact,
becomes
admissible under the. Here, however a term in the form of-reduction andis not a value, and we have the value-restricted
rather than the-reduction itself.
Weby the one-step reduction induced. We write
for the reflexive,
symmetric, transitive closure. The notations such
, etc. aredefined as usual,denotes -step -reductions $(i\geq 0)$ .
$(\mu\alpha.M)(\mu\beta.N)$$\mu \mathrm{P}\mathrm{C}\mathrm{F}^{-}\tau$$(_{fun}^{ext}$’$(\mu_{r})$$\mathrm{e}\mathrm{t}\mathrm{a}$$\mu\alpha.M$$(\eta_{v})$$\mathrm{e}\mathrm{t}\mathrm{a}$$\mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{e}\triangleright_{\mu}$$\mathrm{b}\mathrm{y}\triangleright$$=/\mathit{1}$$\mathrm{o}\mathrm{f}\triangleright_{\mu}$$\triangleright_{\beta}^{+},$$\mathrm{a}\mathrm{s}\triangleright_{\beta},$$i$$\mathrm{a}\mathrm{n}\mathrm{d}\triangleright_{\beta}^{i}$$\Gamma\vdash M_{2}$$\lambda_{V}\mu$$\triangleright_{\beta\eta}^{*},$$=_{\beta\eta}$$\beta$Proposition 1 (Subject Reduction Property for, then
and
in
:
.
in
$M_{1}\triangleright_{\mu}M_{2}$$\triangleright_{\beta\eta},$$\sigma;\triangle$

If we have$\lambda_{V}\mu\rangle$$\Gamma\vdash M_{1}$:$a;\triangle$$\lambda_{V}\mu$

Proof. By induction on the derivation of. Note that in, typing
are uniquely determined depending on the shape of terms.
The well-known type erasure
is defined as follows:
;
;
;
;
.
Then it can be seen that the typing relation is preserved between
and implicitly:
typed(i) If we have
, then:in:in implicit.
(ii) If we have:in implicit, then there exists
such that
and
in
:
.
The set of types inhabited by terms coincides between implicit. However,anderasing type information makes much more reductions possible, such as -reduction of theerasure in Mitchell [Mit88], and the subject reduction property foris broken down,
for example, a counterexample in section 2.
$M_{1}\triangleright_{\mu}M_{2}$$\lambda_{V}\mu$$\mathrm{r}\mathrm{u}\mathrm{l}\mathrm{e}\mathrm{s}\square$$M^{\mathrm{O}}$$(x)^{\mathrm{o}}=x$$(\lambda x.M)^{\circ}=\lambda x.M^{\circ};$$(\lambda t.M)^{\mathrm{o}}=M^{\circ};$$(M_{1}M_{2})^{\circ}=M_{1}^{\mathrm{o}}M_{2^{\circ}}$$(M\sigma)^{\mathrm{o}}=M^{\circ}$$(\mu\alpha.M)^{\circ}=\mu\alpha.M^{\mathrm{O}}$$([\alpha]M)^{\mathrm{o}}=[\alpha]M\circ$$\lambda_{V}\mu$$\lambda\mu$$\Gamma\vdash M$$a;\triangle$$\Gamma\vdash M_{1}$$\Gamma\vdash M_{2}$$a;\triangle$$\Gamma\vdash M^{\mathrm{O}}$$\lambda_{V\mu}$$\sigma;\Delta$$\sigma;\triangle$$\lambda\mu$$M_{2}$$\lambda\mu$$M_{1}=M_{2}^{\mathrm{O}}$$\lambda_{V}\mu$$\lambda\mu$$\lambda_{V}\mu$$\eta$$M^{\mathrm{O}}$4$\mathrm{c}\mathrm{p}\mathrm{s}_{-}\mathrm{R}\mathrm{a}\mathrm{n}\mathrm{S}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$for$\lambda_{V}\mu$-Calculus

To provide the CPS-translation, we define a domain-free(see also [BS97]) as theintuitionistic fragment of. Here, besides -variables
used in -calculus as
usual, the system
has the distinguished variables
called continuation variables.
Reduction rules in domain-free
are also defined as usual under call-by-name. The termwith the form
(value) will be interpreted as, where the representation ofis consumed by the continuation , such as the case of -abstraction. The translationfromto domain-free , with all auxiliary function for values, comes from Plotkin[Plot75].
$\lambda 2$$\lambda$$\lambda_{V}\mu$$x,$ $y,$ $z,$ $\cdots$$\lambda 2$$\alpha,$$\beta,$$\lambda$$\cdots$$\lambda 2$$[\alpha]M$$\lambda k.k(\overline{M}\alpha)$$\overline{\mathrm{J}f}\alpha$$k$$\lambda 2$$\lambda_{V}\mu$$\Psi$

Definition 1 (CPS-Translation)$\overline{M_{1}lVI_{2}}=\lambda k.\overline{M_{1}}(\lambda m.\overline{\mathrm{J}I_{2}}(\lambda n.mnk\mathrm{I})i$$\overline{M\sigma}=\lambda k.\overline{M}(\lambda m.m\sigma qk)j$$\Psi(x)=x_{i}$$t^{q}=t_{j}$$\lambda$$\overline{\lambda x.M}=\lambda k.k(\lambda X.\overline{M})i$$\overline{x}=\lambda k.kx_{i}$$\overline{\lambda t.\Lambda f}=\lambda k.k(\lambda t.\overline{M}\mathrm{I}\mathrm{z}$$\overline{\mu\alpha.M}=\lambda\alpha.\overline{M}(\lambda X.x)i$$\Psi(\lambda X.M)=\lambda_{X_{\mathit{1}}}.\overline{\lambda ff}_{f}$’$\overline{[\alpha]\Lambda/I}=\lambda k.k(\overline{\mathit{1}\mathcal{V}I}\alpha)$$\Psi(\lambda t.M)=\lambda t.\overline{M}_{i}$$(a_{1}arrow a_{2})^{q}=a_{1}^{q}arrow\neg\neg\sigma_{2j}^{tj}$.

$\Psi([a]l\downarrow f)=\overline{\Lambda/I}\alpha$$(\forall t.a)^{q}=\forall t.\neg\urcorner a^{q}$.

.

According to the continuation semantics of Meyer&Wand [MW85], our definition of the
CPS-translation can be read as follows: If we have a variable , then the value is passed
on to the colltinu‘ation . In the case of a -abstraction, a certain function that will taketwo arguments is passed on to the continuation . If we have a term with a continuation
variable , then a certain function with the argument is passed on to the continuation, where the variable will be substituted by a continuation. Here, it would be natural
$x$

$k$

$\lambda$$k$$\alpha$$k$$\alpha$$\alpha$$x$

42that a value is regarded as the term that is mapped by to some term consumed by thecontinuation , since the continuation is the context in which a term is evaluated and thento which the value is sent. Our notion of values as an extended form is derived following
this observation.
$\Psi$$k$

Lemma 1 $Let=$ denote the definitional equality of the CPS-translation.
.
(i) For any term $M$ where $k\not\in FV(M),$.
(ii) For any value$M$
and type , we have $\overline{M1x\cdot.=V]}=\overline{M}[x:=\Psi(V)]$ andFor any term , value$\lambda k.\overline{M}k\triangleright_{\beta}\overline{M}$$V_{\gamma}\overline{V}=\lambda k.k\Psi(V)$$V_{f}$$\underline{(iii)}$$M[t:=a]=\overline{M}[t:=a^{q}]$$\sigma$.

The above lemma can be proved by straightforward induction. On the basis of the CPScan beandtranslation, the left and right context-replacements
respectively.
variables,interpreted as the following substitutions for continuation$M[V\Rightarrow\alpha]$$M[\alpha\Leftarrow M_{1}]$Lemma 2 Let $M$ contain$i$free occurrences$\overline{M[\alpha\Leftarrow M_{1}]}\triangleright_{\beta}^{i}\overline{M}[\alpha:=\lambda m.\overline{M1}(\lambda n.mn\alpha)]$Case of$[\alpha]M$, whereandThen we have that$M[\alpha\Leftarrow a]\triangleright_{\beta}^{i}\overline{M}[\alpha:=\lambda m.m\sigma^{q}\alpha]$.

. We show only the following case:contains free occurrences of :Proof. By induction on the structure of$M$

where $i\geq 0$ .

$\mathit{0}\underline{f[\alpha]}$$M$$[\alpha]$$i$$\overline{([\alpha]M)[a\underline{\Leftarrow M_{1}]}}=\lambda k.k((\lambda k’.\overline{M1\alpha\Leftarrow M_{1}]}\lambda m.\overline{M_{1}}(\lambda n.mnk/))\alpha)$$\triangleright_{\beta}\lambda k.k(M[\alpha\Leftarrow M_{1}]\lambda m.\overline{\Lambda\phi_{1}}(\lambda n.mn\alpha))$$\triangleright_{\beta}^{i}\lambda k.k(\overline{M}[\alpha:=\lambda m.\overline{\Lambda I_{1}}(\lambda n.mn\alpha)](\lambda m.\overline{M_{1}}(\lambda n.m\uparrow\iota\alpha)))$$=\overline{[\alpha]M}[\alpha:=\lambda m.\overline{M_{1}}(\lambda n.mn\alpha)]$.

$\square$Lemma 3 For any term $M$ and value $V,$
where $M$ contains free occurrences of .

$\overline{M[V\Rightarrow\alpha]}\triangleright_{\beta}^{3i}\overline{M}[\alpha:=\lambda n.\Psi(V)n\alpha]$$[\alpha]$$i$

Proof. By induction on the structure of$M$,

contains -occurrences of$i$$[\alpha]$$M$. Only the case of$[\alpha]M$

is shown, where:$\overline{([\alpha]M)[V\Rightarrow\alpha]}=\lambda k.k((\lambda k’.\overline{V}(\lambda m.\overline{M[V\Rightarrow\alpha]}(\lambda n.mnk’)))\alpha)$$\triangleright_{\beta}\lambda k.k((\lambda k’.k’\Psi(V))(\lambda m.\overline{M[V\Rightarrow\alpha]}(\lambda n.mn\alpha)))$$\triangleright_{\beta}^{2}\lambda k.k(\overline{M[V\Rightarrow\alpha]}(\lambda n.\Psi(V)n\alpha))\triangleright_{\beta}^{3i}\lambda k.k(\overline{M}[\alpha:=\lambda n.\Psi(V)n\alpha](\lambda n.\Psi(V)n\alpha))$$\square$$=\overline{[\alpha]M}[\alpha:=\lambda n.\Psi(V)n\alpha 1\cdot$

Lemma 4 If we havein$M\triangleright_{/4}N$$\lambda_{V}\mu_{f}$thenProof. By induction on the derivation of$(\beta_{v})(\lambda x.M)V\triangleright M[x:=V]$$\overline{M}=_{\beta\eta}\overline{N}$$M\triangleright_{\mu}N$in domain-free$\lambda 2$.

. We show some of the cases::$\overline{(\lambda X.M)V}=\lambda k_{1}.(\lambda k_{2}.k2(\lambda x.\overline{M}))(\lambda m.\overline{V}(\lambda\uparrow l.m7lk_{1}))$$\triangleright_{\beta}^{2}\lambda k_{1}.\overline{V}(\lambda_{7}l.(\lambda X.\overline{M})nk_{1})$$\triangleright_{\beta}\lambda k_{1}.\overline{V}(\lambda x.\overline{\Lambda/I}k_{1})=\lambda k_{1}.(\lambda k.k\Psi(\iota/^{\Gamma}))(\lambda x.\overline{M}k_{1})$.

$\triangleright_{\beta}^{2}\lambda k_{1}.\overline{f\downarrow f}[x:=\Psi(V)]k_{1}=\lambda k_{1}.M[x:=V]k_{1}\triangleright_{\beta}\overline{M[x\cdot.=V]}$$(\eta_{v})\lambda x.Vx\triangleright V$:$\overline{\lambda x.Vx}=\lambda k.k(\lambda x.(\lambda k/.(\overline{V}(\lambda m.\overline{x}(\lambda?l.mnk’)))))$$\triangleright_{\beta}^{2}\lambda k.k(\lambda_{X}.(\lambda k/.(\overline{V}(\lambda m.nlxk’))))=\lambda k.k(\lambda x.(\lambda k’.(\lambda k’/.k’/\Psi(V))(\lambda\prime n.mXk/)))$$\triangleright_{\beta}^{2}\lambda k.k(\lambda x.(\lambda k’.\Psi(V)xk’))$$\triangleright_{\eta}\lambda k.k(\lambda_{X}.\Psi(V)x)\triangleright_{\eta}\lambda k.k\Psi(V)=\overline{V}$.

43$(\beta_{t})(\lambda t.M)\sigma\triangleright M$:$\overline{(\lambda t.M)a}=\lambda k.(\lambda k’.k’(\lambda t.\overline{M}))(\lambda m_{\text{ノ}}.maqk)$.

$\triangleright_{\beta}^{2}\lambda k.(\lambda t.\overline{M})\sigma^{q}k\triangleright_{\beta}\lambda k.\overline{M}[t:=\sigma^{q}]k\triangleright_{\beta}\overline{M[t.=\sigma]}$$(\mu_{t})(\mu\alpha.M)a\triangleright\mu\alpha.lI[\alpha\Leftarrow\sigma]$:$\overline{(\mu\alpha.M)\sigma}=\lambda k.(\lambda\alpha.\overline{M}(\lambda X.X))(\lambda m.makq)$.

$\triangleright_{\beta}\lambda\alpha.\overline{M}[\alpha:=\lambda m.?n\sigma^{q}\alpha](\lambda_{X}.x)=_{\beta}\lambda\alpha.\overline{M1\alpha\Leftarrow\sigma]}(\lambda_{X}.x)=\overline{\mu\alpha.M[\alpha\Leftarrow\sigma]}$$(\mu_{r})(\mu\alpha.M)N\triangleright\mu\alpha.M[\alpha\Leftarrow N]$:$\overline{(\mu\alpha.M)N}=\lambda k.(\lambda\alpha.\overline{M}(\lambda x.x))(\lambda m.\overline{N}(\lambda n.mnk))$$\triangleright_{\beta}\lambda k.\overline{M}\underline{[\alpha\cdot.=\lambda m.}\overline{N}(\lambda n.mnk)](\lambda_{X}.x)=\lambda\alpha.\overline{M}[\alpha:=\lambda \mathit{0}l.\overline{N}(\lambda n.mn\alpha)](\lambda_{X.x})$$=_{\beta}\lambda\alpha.M[\alpha\Leftarrow N|(\lambda x.x)=\overline{\mu\alpha.M[\alpha\Leftarrow N]}$$(\mu_{l})V(\mu\alpha M)\triangleright\mu\alpha.M[V\Rightarrow\alpha]$.

:$\overline{V(\mu\alpha.M)}=\lambda k.\overline{V}(\lambda m.(\lambda\alpha.\overline{M}(\lambda X.x))(\lambda n.mnk))$$\triangleright_{\beta}\lambda k.(\lambda k’.k^{\prime_{\Psi}}(V))(\lambda m.\overline{M}[\alpha:=\lambda n.mnk](\lambda_{X}.x))$$\triangleright_{\beta}^{2}\lambda k.\overline{M}[\alpha:=\lambda n.\Psi(V)nk](\lambda X.X)=\lambda\alpha.\overline{M}[\alpha:=\lambda n.\Psi(V)n\alpha](\lambda_{X}.x)$$=_{\beta}\lambda\alpha.\overline{M[V\Rightarrow\alpha]}(\lambda_{X}.x)=\overline{\mu\alpha.M[V\Rightarrow\alpha]}$$(rn)[\alpha](\mu\beta.V)\triangleright V[\beta:=\alpha 1$.

:$\overline{[\alpha](\mu\beta.V)}=\lambda k.k((\lambda\beta.\overline{V}(\lambda_{X.X}))\alpha)$$\triangleright_{\beta}\lambda k.k(\overline{V}[\beta:=\alpha](\lambda X.x))=\lambda k.k((\lambda k’.k;\Psi(V)[\beta:=\alpha])(\lambda X.X))$.

$\triangleright_{\beta}^{2}\lambda k.k\Psi(V)[\beta:=\alpha]=\overline{|^{\gamma}/[\beta.\cdot=\alpha]}$$(\mu-\eta)\mu\alpha.[\alpha]M\triangleright M$:$\overline{\mu\alpha.[\alpha]M}=\lambda\alpha.(\lambda k.k(\overline{l\downarrow/I}\alpha))(\lambda_{X.x})$$\triangleright_{\beta}^{2}\lambda\alpha.\overline{M}\alpha\triangleright_{\beta}\overline{M}$.

$\square$Now, we have confirmed the soundness of the translation in the sense that equivalent-terms are translated into equivalent doln‘din-free -terms. This property essentiallyholds for untyped terms.
$\lambda_{V}\mu$$\lambda 2$

Proposition 2 (Soundness of thethen thenin domain-free .

) If we have $l\mathcal{V}I=/4N$ in$\mathrm{C}\mathrm{P}\mathrm{S}-\mathrm{R}\mathrm{a}\mathrm{n}\mathrm{S}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}$The translation logically establishes the double negation translation of
set of name-indexed formulae , we define.
as$\Delta$

Proposition 3 If$\lambda_{V}\mu$$\lambda_{V\mu}$,$\lambda 2$$\overline{M}=_{\beta\eta}\overline{N}$has$(\sigma^{\alpha}, \triangle)^{q}$$\Gamma\vdash M:a_{\backslash }\triangle$, thenhas$\lambda 2$$\alpha:\neg\sigma^{q},$$\Delta^{q}\vdash\overline{l\vee I}$$\Gamma^{q},$. For a$\mathrm{I}^{r}\backslash \mathrm{u}\mathrm{r}\mathrm{o}\mathrm{d}\mathrm{a}$$\Delta^{q}$:$\neg\neg a^{q}$.

Proof. By induction on the derivation.

$\square$From the consistency of domain-free , it is derived thatis consistent in the sensethat there is no closed term $M$ suchin.
With respect to Proposition 2, it is known that the implication is, in general, not reversible. The counterexample in [Plot75] is not well-typed. Even though we consider welltyped, the completeness does not hold for
If we have
and
in
then
in , butin. Note thatin this counterexample, if one excluded -reduction, then
. Following Hofmann[Hof95], the rewriting rules ofare weak from the viewpoint of the semantics, since
Ident, $(\lambda X.x)M=M$ is necessary in this case.
According to Ong&Stewart [OS97], their call-by-value -calculus has more reduction
rules with the help of type annotation; -reduction:
if.
Here. assume that we have
and $N_{2}\equiv x([a]y)$ , such that:
: $a;\sigma^{\alpha}(i=1,2)$ where. Thenandare reduced toby the use-reduction. Now, we haveinbut$\lambda 2$.

$\mathrm{t}\mathrm{h}\mathrm{a}\dagger$$\lambda_{V}\mu$$\vdash M:\perp\backslash$$\lambda_{V}\mu$$\lambda_{V}\mu-\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{n}\mathrm{l}\mathrm{S}$$\mathrm{J}/I_{2}\equiv xy$$M_{1}\equiv(\lambda_{X}.x)(xy\mathrm{I}$$\lambda_{V\mu:}$$\lambda_{V}\mu,$$\overline{M_{1}}=_{\beta\eta}xy=_{\beta\eta}\overline{\Lambda/I_{2}}$$\lambda 2$$M_{1}\neq_{\mu}\Lambda/I_{2}$$\lambda_{V}\mu$$\overline{M_{1}}\neq_{\beta}\overline{M_{2}}$$\eta$$\lambda_{Vl}\iota$$\lambda\mu$$\perp$$V^{\perparrow\sigma}M\perp\mu\triangleright\beta\sigma.M^{\perp}$$\sigma\not\equiv\perp$$N_{1}\equiv(\lambda x.x)(X([\alpha]y))$$\sigma\vdash \mathit{1}\mathrm{V}_{i}$$a\not\equiv\perp \mathrm{i}\mathrm{n}\lambda_{V}\mu$$\mathrm{o}\mathrm{f}\perp$$x:\perparrow\sigma,$ $y$$N_{1}$$N_{2}$$\overline{\mathit{1}\mathrm{V}_{1}}=_{\beta\eta}X(\alpha y)=_{\beta\eta}\overline{N_{2}}$$N_{3}\equiv\mu\beta.[\alpha]y$$\lambda 2,$$\overline{N_{3}}=_{\beta}\lambda\beta.\alpha y$44. This example means that the soundness of the CPS-translation is broken down
-reduction, even in the absence of -reduction. However, on the basis offorthe correspondence between -operator and Felleisen’s -operator [FFKD86] such that$\mu\alpha.M=C(\lambda\alpha.M)$ and $[\alpha]M=\alpha M$ , one obtains that $x(\alpha y)=_{C}(\lambda X.A(X))(\alpha y)=c$
the naive observation,[Hof95].
in the equational theory
would also work for an equational version of call-byHofmann’s categorical models forvalue -calculus.
be one-step, or $(rn)$ .
consisting ofbe, then. Following the proof of lemma 2, if, orconsisting of-step from $M$ does not simply induce -steps from. On the one hand,, i.e., -conversion may be used. To demonstrate the strong normalization for wellif $M$ has an-terms, it is enough to construct an infinite reduction path fromtyped
, following lemmata 2 and 3, the CPS-translated
infinite reduction path. In the case-redexes to construct all infinite
terms without the -conversion still have enough, whereof $(V(\mu\alpha.M))N$ , we have
reduction. For instance, in the caseasreducedcan be. Here,andfollows:,. We now have
, and
where
.
or
be either
. Let
and
in

$\lambda 2$$\lambda_{V}\mu \mathrm{w}\mathrm{i}\mathrm{t}\mathrm{h}\perp$$\eta$$C$$\mu$$\mathrm{F}\mathrm{r}\mathrm{o}\dot{\mathrm{l}}\mathrm{n}$$A(\alpha y)=_{C}C(\lambda\beta.\alpha y)$$\lambda_{C}$$\lambda_{C}$$\lambda\mu$$((i_{v}), (\beta_{t}),$$\mathrm{o}\mathrm{n}\mathrm{e}-\mathrm{s}\mathrm{t}\mathrm{e}\mathrm{P}\triangleright_{/\mathit{4}}$$\mathrm{L}\mathrm{e}\mathrm{t}\triangleright_{\beta\eta r}$$(\mu_{l}),$$(\mu_{r})$$(\mu-\eta)$$(\eta_{v}),$$\mathrm{L}\mathrm{e}\mathrm{t}\triangleright_{st}$$M_{1}\triangleright_{\beta\eta r}M_{2}$$(\mu_{t})$$\triangleright_{\mu}$$\beta$$\mathrm{e}\mathrm{a}\mathrm{c}\mathrm{h}\triangleright_{st}$$\overline{M_{1}}\triangleright_{\beta\eta}^{+}\overline{M_{2}}$$\overline{M}$$\beta$$\overline{\Lambda I}$$\lambda_{V}\mu$$\mathrm{o}\mathrm{f}\triangleright_{st}$$\beta-,$$\beta$$\eta$$M_{1}\triangleright_{st}M_{2}\triangleright_{st}M_{3}$$M_{1}$$\overline{M_{1}}$$M_{3}\equiv\mu\alpha.M[V\Rightarrow\alpha][\alpha\Leftarrow N]$$M_{2}\equiv(\mu\alpha.M[V\Rightarrow\alpha])N$$\overline{M_{1}}\triangleright_{\beta}^{+}N2^{-}--\lambda k.(\lambda\alpha.\overline{M}id\theta_{1\mathrm{I}}(\lambda m.\overline{N}(\lambda n.mnk))\triangleright\beta N3\equiv\lambda\alpha.\overline{\Lambda l}id\theta_{1}\theta_{2}$$\theta_{2}=[\alpha:=\lambda m.\overline{N}(\lambda n.mn\alpha)]$$id=\lambda_{X.X},$ $\theta_{1}=[\alpha:=\lambda n.\Psi(V)n\alpha]$thenLemma 5 (i) If.
andsuch that$\alpha\not\in
FN(N)$then. If(ii) Let
substitutions and such that$M_{1}\triangleright_{st}M_{2}\triangleright_{st}M_{3f}$$\overline{M_{1}}\triangleright_{\beta}^{+}N_{2}\triangleright_{\beta}^{+}N_{3}$for$\mathit{8}ome\lambda 2$-terms$N_{2}$

and$N_{3}$$\overline{M_{3^{\triangleright_{\beta}^{*}}}}N3$$\overline{M_{2}}\triangleright_{\beta}^{*}N_{2}$$M_{1}[N/\alpha]\triangleright_{\beta\eta r}M_{2},$$\overline{M_{11}}\theta\triangleright_{\beta\eta}^{+}\overline{N_{2}}\theta_{2}$$\overline{M_{1}[N/\alpha]}\triangleright_{\beta}^{*}\overline{M1}\theta_{1}$$\theta_{2}$$\theta_{1}$$[\alpha\Leftarrow N]$$[N\Rightarrow\alpha]$$[N/\alpha]$$\overline{M_{3}}\triangleright_{\beta}^{*}N_{3}$$\overline{M_{2}}\triangleright_{\beta}^{*}N_{2}$andfor some$\overline{M_{2}}\triangleright_{\beta}^{*}\overline{N_{2}}\theta_{2}$$\lambda_{V}\mu$-term$N_{2}$

and

.

for
, or
be
$id=\lambda
X.X$.
some $N,$ , and . Let
if we have an infinite -path from $M$ , it
-path
from
(i) To construct anin the case where-path fromthat we have an
is enough to
weon
the derivations
Therefore,
by induction-redex.
reduction induces asuch thatfor sonue -termshow that if.
:

Proof. Let$V$$\theta_{1}^{\gamma}$$[\gamma:=\lambda m.\overline{N}(\lambda n.mtl\gamma)],$$[\gamma:=\lambda m.ma^{q}\gamma]$$[\gamma’:=\lambda n.\Psi(V)n\gamma]$$a$$\overline{M}$$\triangleright_{s\mathrm{f}}$$\mathrm{i}\mathrm{n}\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{e}\triangleright_{\beta}$$\overline{M}$$\mathrm{o}\mathrm{n}\mathrm{e}\triangleright_{\mathit{8}t^{-}}$$\mathrm{i}\mathrm{n}\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{e}\triangleright_{\beta}$$\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{i}\sigma\gamma$$\mathrm{o}\mathrm{f}\triangleright_{st}$$\mathrm{n}\mathrm{e}\mathrm{w}\triangleright_{\epsilon \mathrm{f}}$$N_{2}$$\lambda 2$$M_{1}[N/z]\triangleright\dagger M2\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{n}\overline{M}S’ 1\theta\triangleright_{\beta}^{+}N2$$\overline{M_{1}[N/Z]}\triangleright^{*}\overline{M_{1}}\theta\beta$$\mathrm{a}\mathrm{n}\mathrm{d}_{\mathit{1}}\overline{I_{2}}\triangleright_{\beta}^{*}N_{2}$$([a](\mu\beta.M))[\alpha\Leftarrow N]\triangleright_{st}[\alpha](\mu\beta.M[\alpha\Leftarrow N][\beta\Leftarrow N])$$\overline{([\alpha](\mu\beta.\Lambda/I))[\alpha\Leftarrow N]}\triangleright\beta*\overline{[\alpha](\mu\beta.M)}\theta_{1}^{\alpha}$$\triangleright_{\beta}\lambda k.k(\overline{\Lambda\ell}id\theta_{1}\alpha\theta_{2}^{\beta})=\lambda k.k(\overline{M}id[\beta:=a]\theta_{1}^{\alpha})$where$\theta_{2}^{\beta}=[(\beta:=\lambda m.\overline{\mathrm{A}\mathrm{V}}(\lambda n.m\uparrow l\alpha)]$$([\alpha](\mu\beta.M))[V\Rightarrow\alpha]\triangleright_{st}[\alpha](\mu,\beta.M[V\Rightarrow\alpha][l/^{r}\Rightarrow\beta])$.

:$\overline{([\alpha](\mu\beta.M))[V\Rightarrow\alpha]}\triangleright^{*}\beta[\alpha](\mu\oint\beta.M)\theta_{1}^{\alpha}$$\triangleright_{\beta}\lambda k.k(\overline{M}id[\beta:=\alpha]\theta^{\alpha}1)$.
:$([\alpha]V)[\alpha\Leftarrow\mu\beta.M]\triangleright_{s}t[\alpha](\mu\beta.M[(V[a\Leftarrow\mu\beta.\dot{M}])\Rightarrow\beta])$$\overline{([\alpha]V)[\alpha\Leftarrow\mu\beta.M]}\triangleright_{\beta}^{*}\overline{[\alpha]V}\theta_{1}^{\alpha}$$\triangleright_{\beta}\lambda k.k((\lambda m.\overline{\mu\beta.\Lambda f}(\lambda n.m\prime l\alpha))(\Psi(V)\theta 1\alpha))\triangleright\beta\lambda k.k(\overline{\mu\beta.\Lambda l}(\lambda n.(\Psi(V)\theta_{1}\alpha)n\alpha)1$$\triangleright_{\beta}\lambda k.k(\overline{M}id\theta^{\beta}2)$

where

where

. Moreover,, and$\theta_{2}^{\beta}=[\beta:=\lambda n.(\Psi(V)\theta_{1}\alpha)n\alpha]$$\theta_{2}^{\beta’}=[\beta:=\lambda|l.\Psi(V’)n\alpha],$$V/=l/^{\mathit{7}}[\alpha:=\alpha/]$$\lambda k.k(_{\mathit{1}v}\overline{I}id\theta^{\beta}2)=\lambda k.k(\overline{M}id\theta/2\theta j^{l}1\alpha’)$$\theta_{1}^{\alpha’}=[\alpha’:=\lambda m.\overline{\mu\beta.M}(\lambda n.\mathfrak{j}?l7l\alpha)]$.

is disappeared byobtained fromin
In the above cases, the symbol-path, since when the. However, this gives no defects to have an, the arguments must be
performs
corresponding to the disappeared$\lambda\beta$$\overline{\mu\beta.M}$$\lambda k.k(\lambda\beta.\overline{M})$$\mathrm{i}\mathrm{n}\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{c}\triangleright_{\beta}$$\mathrm{e}\mathrm{x}\mathrm{e}\mathrm{C}\mathrm{u}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g}\triangleright_{\theta}$$\mu\beta.\Lambda f$$\lambda\beta$$\mathrm{i}\mathrm{n}\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{e}\triangleright_{s7}$45provided infinitely by
the redex of$\mathrm{r}\mathrm{e}\mathrm{n}\mathrm{a}\mathrm{n}\dot{\mathrm{u}}\mathrm{n}\mathrm{g},$, and theinduce$[\alpha](\mu\beta.M[N/z])$ can be simulated$\mathrm{o}\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{r}\triangleright_{st}$$\mathrm{i}\mathrm{n}\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{e}\triangleright_{s\dagger}$$\mathrm{b}\mathrm{y}\triangleright_{\beta}$(ii) By induction on the derivation$\mathrm{o}\mathrm{f}\triangleright_{\beta\eta r}$-steps. Moreover,-steps in.

$\mathrm{i}\mathrm{n}\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{e}\triangleright_{\beta}$$N_{2}$. We show some of the cases.

$(\beta_{v})([\alpha](\lambda x.M))[\alpha\Leftarrow V]\triangleright_{\beta v}[\alpha](M[\alpha\Leftarrow V][_{X:=}V]\mathrm{I}$:$\overline{([\alpha](\lambda_{X}.M))[\alpha\Leftarrow V]}\triangleright_{\beta}^{*}\overline{[\alpha](\lambda X.M)}\theta_{1}\alpha=\lambda k.k((\lambda k;.k’(\lambda X.\overline{M}))\alpha)\theta_{1}^{\alpha}$$\triangleright_{\beta}\lambda k.k((\lambda m.\overline{V}(\lambda n.mn\alpha))(\lambda X.\overline{M}\theta_{1}^{\alpha}))\triangleright_{\beta}\lambda k.k(\overline{V}(\lambda n.(\lambda X.\overline{M}\theta\alpha)1n\alpha))$$\triangleright_{\beta}\lambda k.k(\overline{V}(\lambda X.\overline{M}\theta_{1}\alpha\alpha))\triangleright_{\beta}^{2}\lambda k.k(\overline{M}[x:=\Psi(V)]\theta_{1}^{\alpha}\alpha)$$=\lambda k.k(\overline{M[X.=V]}\theta\alpha)1\alpha=\lambda k.k(\overline{M\prime[x.=V]}\theta\alpha^{l}\alpha 2)=\overline{[\alpha]M\prime[X.=V]}\theta_{2}\alpha’$$\alpha’]$and$\theta_{2}^{\alpha’}=[\alpha’:=\lambda m.\overline{V}(\lambda n.mn\alpha)]$.

$(\beta_{v})([\alpha]V)[\lambda X.M\Rightarrow\alpha]\triangleright_{\beta_{v}}[\alpha](M1X:=(V[\lambda_{X.M}\Rightarrow\alpha])])$

where$\Lambda I’=M[\alpha$$:=$$\theta_{2}^{\alpha’}=[\alpha’$

$:=$

:

$\overline{([\alpha]V)[\lambda x.M\Rightarrow\alpha]}\triangleright_{\beta}\overline{[}*\alpha]V\theta_{1}^{\alpha}--\lambda k.k(\overline{V}\alpha)\theta_{\iota}^{\alpha}$$\triangleright_{\beta}\lambda k.k((\lambda n.\Psi(\lambda X.M)\mathit{7}l\alpha)(\Psi(V)\theta 1\alpha))\triangleright_{\beta}\lambda k.k(\Psi(\lambda_{X}.M)(\Psi(V)\theta_{1}\alpha)\alpha)$$=\lambda k.k((\lambda x.\overline{M})(\Psi(V)\theta^{\alpha})1\alpha)\triangleright\lambda k\mapsto^{k}((\overline{M}[X=\Psi(V)]\theta_{1}^{\alpha})\alpha)$

where $V’=V[\alpha:=\alpha’]$ and$=\lambda k.k((M[X:=V]\theta 1\alpha)\alpha)=[\alpha]M\iota x:=V’]\theta_{2}\alpha’$$\lambda n.\Psi(\lambda X.M)n\alpha]$.

:$(\beta_{t})([\alpha](\lambda t.M))[\alpha\Leftarrow a]\triangleright_{\beta t}[\alpha](l\mathfrak{l}f[\alpha\Leftarrow\sigma][t:=a])$$\overline{([\alpha](\lambda t.M))[\alpha\Leftarrow a]}\triangleright^{*}\beta\overline{[\alpha](\lambda i.M)}\theta_{1}\alpha=\lambda k.k((\lambda k’.k/(\lambda t.\overline{M}))\alpha)\theta_{1}\alpha$$\triangleright_{\beta}\lambda k.k((\lambda m.ma^{q}\alpha)(\lambda t.\overline{M}\theta_{1}^{\alpha}))\triangleright_{\beta}\lambda\underline{k.k((\lambda t.\overline{M}}\theta_{1}^{\alpha})aq\alpha)$$\triangleright_{\beta}\lambda k.k((\overline{M}1t:=\sigma^{q}]\theta 1\alpha)\alpha)=\lambda k.k((M[t:=\sigma]\theta 1\alpha)\alpha)$

where $M’=M[\alpha:=\alpha’]$ and$(rn)([\alpha](\mu\beta.V))[N/\gamma]$ where:$=\overline{[\alpha]M’[t\cdot.=\sigma]}\theta_{2}^{\alpha’}$$\theta_{2}^{\alpha’}=[\alpha’:=\lambda m.\sigma^{q}\alpha]$.

$\alpha\not\equiv\gamma’$$\overline{([\alpha](\mu\beta.V))[N/\gamma]}\triangleright^{*}\beta\overline{[\alpha](\mu\beta.V)}\theta 1\gamma=\lambda k.k((\lambda\beta.\overline{V}id)\alpha)\theta^{\gamma}1$$\triangleright_{\beta}^{3}\lambda k.k(\Psi(V)[\beta:=\alpha])\alpha)\theta^{\gamma}1=\overline{V[\beta.\cdot=\alpha]}\theta_{1}^{\gamma}$$(\eta_{v})([\alpha](\lambda_{X}.VX))[N/\gamma]$

where

.

$x\not\in FV(V)$$\overline{([\alpha](\lambda X.Vx))[l\mathrm{v}/\gamma]}\triangleright^{*}\beta\overline{[\alpha](\lambda_{X}.Vx)}\theta^{\gamma+}1\beta\eta\overline{[}\triangleright\alpha]V\theta^{\gamma}1$

Moreover, we have that
and$\Psi(\lambda X.Vx)\triangleright_{\beta\eta}^{+}\Psi(V)$.

$\Psi([\alpha](\mu\beta.V))\triangleright_{\beta}^{+}\Psi(V[\beta:=\alpha])$Lemma 6 If there exits anan-reduction path.

$infinite\triangleright_{\mu}$$ha\mathit{8}$:.

$\square$-reduction path from$\lambda_{V}\mu$-term $M$ , then$\overline{M}$also$infinite\triangleright_{\beta\eta}$

Proof. From Lemma 5 and the proof of Lemma 4.

$\square$From Proposition 3, Lennma 6 and the fact that domain-free
is strongly normalizing[BS97], the strong normalization property forcan be obtained.
$\lambda 2$$\lambda_{V}\mu$

Proposition 4 (Strong Normalization Property foris strongly normalizable.

$\lambda_{V}\mu$) A $ny$ well-typed$\lambda_{V}\mu$-term

It is observed [Fuji97] that the straightforward use of the Tait&Martin-L\"of parallel reduction [Taka89] could not work for proving the Church-Rosser property forincludingrenaming rule, contrary to the comments on Theorem 2.5 in [OS97]. Even though one
defines parallel reduction
as usual, we cannot establish that if $A\mathrm{W}_{i}\gg N_{i}(i=1,2)$ ,then; fact (iv) in the proof of Theorem 1 in [Pari92].
$\lambda\mu$$\gg$$\Lambda\ell_{1}[\alpha\Leftarrow M_{2}]\gg N_{1}[\alpha\Leftarrow N_{2}]$Lemma 7 (Weak Church-Rosser Property forandfor some $N$ .
$M_{1}\triangleright_{\mu}^{*}N$$M_{2}\triangleright_{\mu}^{*}N$$\lambda_{V}\mu$) If$M\triangleright_{/4}M_{1}$and$M\triangleright_{\mu}M_{2_{f}}$

then

46
From Proposition 4 and Lemma 7, we can obtain the Church-Rosser property using Newman’s lemma [Bare84].

Proposition 5 (Church-Rosser Theorem)
well-typed terms.

$\lambda_{V}\mu$

has the Church-Rosser property for

Comparison with Related Work and Concluding
Remarks

5, see [Fuji99]) with ML [Mi178, DM82] together with(
We briefly compare, the class of type variables is partitioned into two subclasses,
callcc [HDM93]. In
i.e., the applicative and the imperative type variables. The type of callcc is declared withimperative type variables to guarantee the soundness of the type inference. On the basisof the classification, the typing rule for let-expression is given such that if the let-boundexpression is not a value, then generalization is allowed only for applicative type variables;
otherwise generalization is possible with no restriction. There is a simple translation from-terms, such that the two subclasses of type variables in ML-programs to thethe)are degenerated into a single class:isfresh.
where
However, there are some distinctions; according to Harper et al. [HDM93], the program:( true)inletwith imperative type variables, since callcc
is not typable inis not a value, and in the case of non-value expressions, polymorphism is allowed only
for expressions with applicative type variables. If it were typable with bool, then thiswas reduced to 1 following the operational semantics. On the other hand, under the[Fuji99] we havetogether with type annotation, intranslation
int )( bool true)(inletplus callcc under ll-by-value,with type bool, and this is now reduced to true, as in. In turn, the following term
-like call-by-value
not under$\lambda\mu_{ml}$$\mathrm{M}\mathrm{L}+\mu$$\mathrm{M}\mathrm{L}$$\lambda\mu_{ml}$$\mathrm{M}\mathrm{L}$$\lceil \mathrm{c}\mathrm{a}11_{\mathrm{C}\mathrm{C}(M}$$1=\mu\alpha.[\alpha](\lceil M\rceil(\lambda x.1\alpha]X))\backslash$$\beta$$\lceil \mathrm{t}\mathrm{h}\mathrm{r}\mathrm{o}\mathrm{W}MN\rceil=\mu\beta.\lceil M\rceil\lceil N\rceil$$f=\mathrm{C}\mathrm{a}\mathrm{l}\mathrm{l}\mathrm{C}\mathrm{C}(\lambda k.\lambda X.\mathrm{t}\mathrm{h}\mathrm{r}\mathrm{o}\mathrm{w}k(\lambda v.x))$$(\lambda_{X_{1^{X}2}}.x_{2})(f1)$$(\lambda k.\lambda X.\mathrm{t}\mathrm{h}\mathrm{r}\mathrm{o}\mathrm{w}k(\lambda v.x))$$\mathrm{M}\mathrm{L}$$\lambda\mu_{eml}$$\lceil\rceil$$f=At.\mu\alpha.[\alpha]\lambda_{X}.\mu\beta.[\alpha](\lambda v.X)$$(\lambda x_{12}x.x_{2})$

$1$

$f$

$F_{\omega}$$\mathrm{M}\mathrm{L}$

let

$f$

$f$

$\mathrm{C}‘ \mathrm{a}$$[\mathrm{H}\mathrm{L}93\mathrm{a}]$$f=\mu\alpha.[\alpha]\lambda x.\mu\beta.[\alpha](\lambda v.X)$

in $(\lambda x_{1^{X}2^{X}2}.)(f. 1)(f2)$with type int is reduced to 1 by the symmetric structural reduction. On the other hand,[Fuji99] we havein .
( true)in
letcould overcome the counterexample
with type bool, and this is also reduced to true.
moreover,typingtheconditions for let-expression could,andof polymorphic callcc in
is another candidate for implicit polymorphism by value,
be deleted. In particular,
compared with implicit polymorphism by name in Leroy [Lero93].
Ong&Stewart [OS97] extensively studied a call-by-value programming language basedon a call-by-value variant of finitely typed -calculus. There are some distinctions between Ong&Stewart and our finite type fragment; their reduction rules have type annotations like the complete Church-style, and, using the annotation, more reduction rules
are defined than ours, which can give a stronger normal form. In addition, our notion of values is an extended one, which would be justified by observation based on the
CPS-translation. Moreover, our renaming rule is applied for the extended values, andfollowing the proof of lemma 4, this distinction is essential for the CPS-translation ofrenaming rule. Otherwise the reductions by renaming rule would not be simulated byof Hofmann [Hof95], one-reductions. On the other hand, in the equational theory$\lambda$$\mu_{iml}$$f=\mu\alpha.[\alpha]\lambda x.\mu\beta.1\alpha](\lambda v.X)$$(\lambda x_{1^{X}2\cdot 2}x)(f1)$$f$$\lambda\mu_{ml}$$\mathrm{M}\mathrm{L}$$\lambda\mu_{iml}$$\lambda\mu$$\lambda_{C}$$\beta$47
obtains
without restricting to values, which would be distinction between equational theory and rewriting theory.
We used the CPS-translation as a useful tool to show consistency and strong normalization of the system. With respect to Proposition 2 (soundness of CPS-translation); forcall-by-name , on the one hand, the completeness is obtained in de Groote [Groo94], i.e.,the call-by-name CPS-translation is injective. For a call-by-value system with Felleisen’scontrol operators [FFKD86], on the other hand, the completeness is established with respect to categorical models [Hof95], and moreover, this method is successfully applied tocall-by-name[HS97]. We believe that our CPS-translation would be natural along theline of [Plot75], and it is worth pursuing the detailed relation to such categorical models$\alpha(C(\lambda\beta.M))=_{C}M[\beta:=\alpha]$$\lambda\mu$$\lambda\mu$[HS97, SR96].

Acknowledgements I am grateful to Susumu Hayashi, Yukiyoshi Kameyama, and themembers of the Proof Animation Group for helpful discussions.

References[Ando95] Y.Andou: A Normalization-Procedure for the First Order Classical Natural Deduction
with Full Logical Sylnbols. Tstlkuba Journal of Mathematics 19 (1) pp.153162, 1995.

[Bare84] H.P.Barendregt:
North-Holland, 1984.

The Lambda Calculus, Its Syntax and Semantics (revised edition),[Bare92] H.P.Barendregt: Lambda Calculi with Types, Halldbook of Logic in Computer Sciellce
Vol.II, Oxford University Press, pp.1-189, 1992.
[BB93] F.Barbanera and S.Berardi: Extracting Constructive Context from Classical Logic via
Control-like Reduction8, Lecture Notes in Computer Science 664, pp.45-59, 1993.
[BS97] G.Barthe and: Domain-free Pure Type Systems, Lecture Notes in Computer Science 1234, pp.9-20, 1997.
$\mathrm{M}.\mathrm{H}.\mathrm{S}\emptyset \mathrm{r}\mathrm{e}\mathrm{n}\mathrm{s}\mathrm{e}\mathrm{n}$[DM82] L.Damas and R.Milner:

Principal type-schemes for functional programs, Proc. 9th
Annual ACM Symposium on Principles of Programming Languages, pp.207-212, 1982.

[Groo94] P.de Groote: A
Science 787, pp.85-99, 1994.

$\mathrm{C}\mathrm{P}\mathrm{S}_{-}\mathrm{R}\mathrm{a}11\mathrm{s}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$for the$\lambda\mu$-Calculus, Lecture Notes in Computer[Groo95] P.de Groote: A Simple Calculus of Exception Handling, Lecture Notes in Colnputer
Science 902, pp.201-215, 1995.
[FFKD86] M.Felleisen, D.P.Friedman, E.Kohlbccker, and B.Duba: Reasoluing witll Contilluations, Proc. Annual IEEE Sy’rnpo8ium on Logic in Computer Science, pp.131-141, 1986.
[Fuji97] K.Ftljita: Calculus of Classical Proofs I, Lectllre Notes in Computer Science 1345,
pp.321-335, 1997.

[Fuji98] K.Fujita: Polymorphic Call-by-Value Calculus based on Classical Proofs, Lecture Notes
in Artificial Intelligence 1476, pp.170-182, 1998.
[Fuji99] K.Fujita: Explicitly Typed-Calculus for
Notes in Conlputer Science 1581, pp.162-176, 1999.
$\lambda\mu$$\mathrm{p}\mathrm{o}\mathrm{l}\mathrm{y}\mathrm{n}\mathrm{l}\mathrm{o}\mathrm{r}\mathrm{p}\iota_{\dot{\mathrm{u}}\mathrm{S}}\mathrm{m}$and Call-by-Value, Lecture[Grif90] T.G.Griffii: A-Types Notion of Colltrol, Proc. 17th Annual ACM Symposium on Principles of Programming Languages, pp.47-58, 1990.
$\mathrm{F}_{\mathrm{o}\mathrm{r}}\mathrm{m}n1\mathrm{a}\mathrm{e}-\mathrm{a}\mathrm{S}$48, B.F.Duba, and D.MacQueen: Typing First-Class Continuations ill ML.
J.Functional Programming, 3 (4) pp.465-484, 1993.

[HDM93]$\mathrm{R}.\mathrm{H}\mathrm{a}\iota \mathrm{p}\mathrm{c}\mathrm{r}$[HL91] R.Harper and M.Lillibridge: ML with callcc is unsound, The Types Form, 8, July, 1991.

and CPS conversion, Proc. 20th
[HL93a] R.Harper and M.Lillibridge: Explicit
Annual ACM Symposium on Principles of Programming Languages, pp.206-219, 1993.
$\mathrm{p}\mathrm{o}\mathrm{l}\mathrm{y}\mathrm{m}\mathrm{o}\mathrm{I}\mathrm{p}\mathrm{l}\dot{\mathrm{u}}\mathrm{S}\mathrm{m}$: Polymorphic type assigmnent and CPS conversion, LISP
[HL93b] R.Harper aIld
and Symbolic Computation 6, pp.361. 380, 1993.
$\mathrm{M}.\mathrm{L}\mathrm{i}\mathrm{l}\mathrm{l}\mathrm{i}\mathrm{b}_{\mathrm{I}}\cdot \mathrm{i}\mathrm{d}\mathrm{g}\mathrm{e}$[HM93] R.Harper and J.C.Mitchell: On The Type Structure of Standard ML, ACM Transactions on Programming Languages and System8, Vol. 15, No.2, pp.210-252, 1993.
[Hof95] M.HofinaIm: Sound and complete axiomatisations of call-by-value control operators,
Math. Struct. in Comp. Science 5,’ 1995.
$\mathrm{p}\mathrm{p}.461-482\backslash$[How80] W.Howard: The $Formulae- aS-\tau ypes$ Notion of Constructions, To H.B. Curry: Essays
on combinatory logic, lambda-calculus, and formalism, Academic Pre8S, pp.479-490, 1980.
[HS97] M.Hofmann and T.Streicher: Continuation models are umiversal for12th Annual IEEE Symposium on Logic in Computer Science, 1997.

-calculus, Proc.

$\lambda\mu$[Koba97] S.Kobayashi: Monads as modality, Theor. Comput.Sci. 175, pp.29-74, 1997.

, and P.Urzyczyn: An Analysis of ML Typability, Joumal of the[KTU94] A.J.Kfoury,
Association for Computing Machinery, Vol.41, No.2, pp.368-398, 1994.
$\mathrm{J}.\mathrm{T}\mathrm{i}_{\mathrm{U}\mathrm{r}}\mathrm{y}11$

luations, Proc. 20th Annual[Lero93] X.Leroy: Polymorphism by name for references and
ACM Symposium ofof Programming Languages, pp.220-231, 1993.
$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{t}\dot{\mathrm{u}}$$P_{\mathit{7}\dot{\eta}}nciples$[Mit88] J.C.Mitchell: Polylnorphic Type Inference alzd Containment, Information and Computation 76, pp.211-249, 1988.
[Mi178] R.Milner: A Theory of Type Polymorphism in Progralmning, Journal of Computer and
System ScienCe817, pp.348-375, 1978.
[Murt91] C.R.Murthy: An Evaluation Semantics for Classical Proofs, Proc. 6th Annual IEEE
Symposium on Logic in Computer Science, pp.96-107, 1991.

[MW85] A.Meyer and M.Wand: Continuation Semantics in Typed Lambda-Calculi, Lecture
Notes ill Computer Sciellce 193, pp.219-224, 1985.
[Ong96] C.-H.L.Ong: A Semantic View of Classical Proofs: Type-Theoretic. Categorical, andDenotational Characterizations, Linear Logic ’96 Tokyo Meeting, 1996.
Computation-Howard Foundation for[OS97] C.-H.L.Ong and C.A.Stewart: A$Pr?nciples$
Languages,
Programming
SympoSiu7n
ACMwith Control, Proc. 24th Annualofof$\mathrm{F}_{\mathrm{U}1}1\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{a}1$$\mathrm{C}\mathrm{u}\mathrm{I}\iota \mathrm{y}$1997.

-Calculus: An Algorithrnic Interpretation of Classical Natural Deduc[Pari92] M.Parigot:
tion, Lecture Notes in Computer Science 624, pp.190-201, 1992.
$\lambda\mu$[Pari93] M.Parigot: Classical Prooffi as
pp.263-276, 1993.

$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{g}\mathrm{r}\mathrm{a}\mathrm{m}\mathrm{S}_{4}$Lecture Notes$\mathrm{i}_{1}\mathrm{u}$Computer Sciellce 713,

[Pari97] M.Parigot: Proofs of Strong Nonnalization for Second Order Classical Natural Deduction, J.Symbolic Logic 62 (4), pp.1461-1479, 1997.

49[Plot75]
125-159, 1975.

$\mathrm{G}.\mathrm{P}\mathrm{l}\mathrm{o}\mathrm{t}\mathrm{k}\mathrm{i}_{11:}\mathrm{C}\mathrm{a}\mathrm{u}_{-}\mathrm{b}\mathrm{y}$-Name,-Value alld the -Calculus, Theor. Comput.Sci. 1, pp.
$\lambda$$\mathrm{C}\mathrm{a}\mathrm{l}1_{-}\mathrm{b}\mathrm{y}$[Praw71] D.Prawitz: Ideas and Results in Proof Theory, Proc. 2nd Scandinavian Logic Symposium, edited by N.E.Fenstad, North-Holland, pp.235-307, 1971.
[RS94] N.J.Rehof and789, pp.516-542, 1994.

$\mathrm{M}.\mathrm{H}.\mathrm{S}\emptyset \mathrm{r}\mathrm{e}\mathrm{n}\mathrm{s}\mathrm{e}\mathrm{n}$: The$\lambda_{\Delta}$-Calculus, Lecture Notes in Computer Sciellcc[SR96] T.Streicher and B.Reus: Continuation semantics: abstract machines and control operators. to appear in J.Functional Programming.
[Taka89]
123, 1989.

: Parallel Reductions in -Calculus, J.Symbolic Computation 7, pp.113-$\mathrm{M}.\mathrm{T}\mathrm{a}\mathrm{k}\mathrm{a}\mathrm{h}\mathrm{a}\mathrm{S}\mathrm{l}\dot{\mathrm{u}}$$\lambda$