Mem. Fac. Sci. Eng. Shimane Univ.
Series B: Mathematical Science
36 (2003), pp. 39–48

AN INJECTIVE CPS-TRANSLATION FOR THE EXTENSIONAL
λ-CALCULUS
KEN-ETSU FUJITA(Received: January 31, 2003)
Abstract. We give a syntactical proof to the statement that a novel CPStranslation with surjective pairing is injective for the extensional λ-calculus. The
result itself might be preliminary, since the source language (the extensional λcalculus) of the translation is a sublanguage of the target language (λ-calculus
with surjective pairing). However this paper shows that there exists a nontrivial
injection from the extensional λ-calculus into the λ-calculus with surjective pairing. In this sense our result can be regarded as an extension of Plotkin, i.e., acall-by-value simulation of call-by-name λ-calculus with η-rule (extensionality).
Moreover, the method presented here can be naturally extended to the case of theextensional λµ-calculus which is defined from the extensional λ-calculus together
with control operators.

1. Introduction
Parigot [13, 14] introduced the λµ-calculus from the viewpoint of classical logic,
and established an extension of the Curry-Howard isomorphism [10, 7, 12]. Fromthe motivation of a universally computational point of view, we investigate typefree λµ-calculus [2, 5].
In terms of a category of continuations, it is proved that for any λµ-theory acontinuation semantics of λµ-calculus is sound and complete by Hofmann and Streicher [9]. Selinger [16] proposed the control category to establish an isomorphism
between call-by-name and call-by-value λµ-calculi with conjunction and disjunction types. In Streicher and Reus [17], the category of negated domains is applied
for a model of type free λµ-calculus. They remarked that the traditional CPStranslation1 naı̈vely based on Plotkin [15] cannot validate η-rule. All of the work
[9, 16, 17] introduced a novel CPS-translation which requires, at least, products asa primitive notion, so that η-rule can be validated by the use of surjective pairing,as observed in [4].
2000 Mathematics Subject Classification. 68N18, 68Q05, 68Q55.
Key words and phrases. extensional λ-calculus, surjective pairing, Church-Rosser property,
continuation-passing-style translation, call-by-name, call-by-value.
1CPS stands for continuation-passing style.
39

40

K. FUJITA

Towards a model theoretical investigation of type free λµ-calculus, as a preliminary step we show that the novel CPS-translation with surjective pairing is injective. It is syntactically proved that the CPS-translation is sound and complete forthe extensional λ-calculus. Here the extensionality means that the λ-calculus has
not only β-rule but also η-rule.
As a corollary the injective CPS-translation reveals a Church-Rosser fragmentof the λ-calculus with surjective pairing, which is not Church-Rosser as provedby Klop [1]. Along the line of Plotkin [15], this work can also be regarded as acall-by-value simulation of call-by-name λ-calculus with η-rule (extensionality). It
is remarked that the completeness in [15] has been proved by the essential useof the Church-Rosser property of the target calculus (call-by-value λ-calculus).
However our target calculus is not Church-Rosser as stated above. In order todefine an inverse translation and prove the completeness, we introduce a contextfree grammar which describes the image of the CPS-translation.
Although this paper handles only type free λ-calculus, our main theorem is stillvalid under typed λ-calculus. Moreover, the syntactical method presented in thispaper can be naturally extended to the case of the extensional λµ-calculus [13, 14]
which is defined from the extensional λ-calculus together with control operators.
2. CPS-Translation of λ-calculus into λ-calculus with surjective
pairing
We show a preliminary result that the novel CPS-translation is sound and complete for the extensional λ-calculus. The definitions of terms and reduction rules arerespectively given to the extensional λ-calculus denoted by Λ and the extensional
λ-calculus with surjective pairing denoted by Λhi .
Definition 1 (λ-calculus Λ).
Λ 3 M ::= x | λx.M | M M(β): (λx.M1 )M2 → M1 [x := M2 ](η): λx.M x → M if x 6∈ F V (M )Definition 2 (λ-calculus with surjective pairing Λhi ).
Λhi 3 M ::= x | λx.M | M M | hM, M i | π1 (M ) | π2 (M )(β): (λx.M1 )M2 → M1 [x := M2 ](η): λx.M x → M if x 6∈ F V (M )(π): πi hM1 , M2 i → Mi (i = 1, 2)(sp): hπ1 (M ), π2 (M )i → M
The term M1 [x := M2 ] denotes the result of substituting M2 for the free occurrences of x in M1 . F V (M ) stands for the set of free variables in M . The one
step reduction relation is denoted by →R where R consists of (β), (η), (β) + (η),∗λhi (= (β) + (η) + (π) + (sp)), etc. We write →+R and →R to denote the transitive
closure and the reflexive and transitive closure of →R , respectively. We employ thenotation =R to indicate the symmetric, reflexive and transitive closure of →R . The
binary relation ≡ denotes the syntactic identity under renaming of bound variables.

AN INJECTIVE CPS-TRANSLATION FOR THE EXTENSIONAL λ-CALCULUS

41

It is noted that the rule of (η) implies the extensional equality of functions, i.e.,f =βη g if f M =βη gM for any M ∈ Λ. Suppse f M =βη gM for any M ∈ Λ.
Then we have f x =βη gx for a fresh variable x, and we also have λx.f x =βη λx.gx.
Hence, an application of (η) gives f =βη g.
For a CPS-translation, we assume that Λhi has two kinds of variables denotedby x and a.
Definition 3 (CPS-translation : Λ → Λhi ).
(i): [[x]] = x(ii): [[λx.M ]] = λa.(λx.[[M ]])(π1 a)(π2 a)(iii): [[M1 M2 ]] = λa.[[M1 ]]h[[M2 ]], ai
Example 1. It is instructive to calculate the following where m, n ≥ 0:[[λx1 . . . xm .xM1 · · · Mn ]] →+λa.xh[[M1 ]], . . . , h[[Mn ]], π2m ai . . .i
β[x1 := π1 a, x2 := π1 (π2 a), . . . , xm := π1 (π2m−1 a)]
Proposition 1 (Soundness). Let M1 , M2 ∈ Λ. If we have M1 →βη M2 then[[M1 ]] →+[[M2 ]].
λhi
Proof. By induction on the derivation of M1 →βη M2 . We show some of the basecases.
Case of: (β)[[(λx.M1 )M2 ]]

=
=
→β
→+
π
→β
→η

λa.[[λx.M1 ]]h[[M2 ]], ai
λa.(λa0 .(λx.[[M1 ]])(π1 a0 )(π2 a0 ))h[[M2 ]], ai
λa.(λx.[[M1 ]])(π1 h[[M2 ]], ai)(π2 h[[M2 ]], ai)
λa.(λx.[[M1 ]])[[M2 ]]aλa.[[M1 ]][x := [[M2 ]]]a = λa.[[M1 [x := M2 ]]]a[[M1 [x := M2 ]]]Case of: (η) where x 6∈ F V (M )[[λx.M x]]= λa.(λx.[[M x]])(π1 a)(π2 a)= λa.(λx.λa0 .[[M ]]hx, a0 i)(π1 a)(π2 a)λa.[[M ]]hπ1 a, π2 ai→+β→sp λa.[[M ]]a→η [[M ]]¤It is remarked that Proposition 1 holds true even under the restricted form V ,i.e., the call-by-value computation as follows:V::= x | λx.M | hV, V i | π1 (V ) | π2 (V )(βv ): (λx.M )V → M [x := V ]42

K. FUJITA(ηv ): λx.V x → V(πv ): πi hV1 , V2 i → Vi (i = 1, 2)(spv ): hπ1 V, π2 V i → V
Hence this work can be regarded as a call-by-value simulation of call-by-name λcalculus with η-rule.
2.1. Universe of the translation. We will give a definition of the inverse translation to each element of the universe of the CPS-translation:
def

Univλ = {P ∈ Λhi | [[M ]] →∗λhi P for some M ∈ Λ}
Every element in the universe will be generated by the following context-free grammar:
R ::= x | π1 K | (λx.R)R | λa.RK
K ::= a | π2 K | hR, Ki
Lemma 1 (Subject reduction property). The categories R and K are closed under
the following reductions:(βx ): (λx.R1 )R2 → R1 [x := R2 ](βa ): (λa.RK1 )K2 → RK1 [a := K2 ](ηa ): λa.Ra → R if a 6∈ F V (R)(πR,K ): π1 hR, Ki → R and π2 hR, Ki → K(spK ): hπ1 (K), π2 (K)i → K
Proof. Because we have that R1 [x := R2 ] ∈ R, K[x := R] ∈ K by simultaneous
induction on the structures of R1 and K; and that R[a := K] ∈ R, K1 [a := K2 ] ∈ K
similarly.
¤
Proposition 2. Univλ ⊆ R, i.e., Univλ is generated by R.
Proof. From definition 3, we have [[M ]] ∈ R for any M ∈ Λ. Moreover, from Lemma
1, R and K are closed under the reductions, and hence Univλ ⊆ R is obtained. ¤There uniquely exists a projection normal form by the sole use of (πR,K ), andthe projection normal form of K is in the following form Knf :Knf ::= π2n a | hRnf , Knf i
where n ≥ 0. For a technical reason, an occurrence of a single variable a ∈ K, i.e.,
π2n a where n = 0 is handled as an (spK )-expansion form; hπ1 a, π2 ai. Under thisconsideration, K can be supposed to be in the form of hR1 , . . . , hRm , π2n ai . . .i withm ≥ 0, n ≥ 1.
Lemma 2 (π-normal form). Let m ≥ 0 and n ≥ 1. Then every element in theuniverse Univλ is one of the following forms up to (πR,K )-reductions and (spK )expansions:(1): x(2): π1 (π2i a) for some i ≥ 0(3): (λx.R)R1

AN INJECTIVE CPS-TRANSLATION FOR THE EXTENSIONAL λ-CALCULUS

43(4): λa.RhR1 , . . . , hRm , π2n ai . . .i for some m ≥ 0 and n ≥ 1
where R and Ri (1 ≤ i ≤ m) are in the form of (1), (2), (3), or (4) above.
We call the occurrence of (π2n a) in the case of (4) above a tail with the variable a.
Moreover, the following property is satisfied under renaming of bound variables:(i): For each λa, there exists a unique occurrence of the corresponding tailπ2n a for some n ≥ 1;(ii): If we have π1 (π2i a) as a proper subterm where i ≥ 0, then there exists theleast n ≥ 1 such that the condition i + 1 ≤ n holds for the tail π2n a with thevariable a.
Proof. First obtain a projection normal form only by the use of (πR,K )-reductions,and then check whether the form has the condition (ii). The application of (spK )expansion guarantees that (ii) holds true.
¤
2.2. Inverse translation. π-normal forms above play a role of representatives of
the image Univλ under the translation [[−]]. We give the definition of the inverse
translation \ to every element indef

π-nf(Univλ ) = {π-normal(P ) ∈ Λhi | [[M ]] →∗λhi P for some M ∈ Λ}.
That is, P \ = (π-normal(P ))\ for any P ∈ Univλ .
Definition 4 (Inverse translation \ : π-nf(Univλ ) → Λ).
(1): x\ = x(2): (π1 (π2i a))\ = ai+1 (i ≥ 0)(3): ((λx.R)R1 )\ = (λx.R\ )R1\\
(4): (λa.RhR1 , . . . hRm , π2n ai . . .i)\ = λa1 . . . an .R\ R1\ · · · Rm(m ≥ 0, n ≥ 1)
Lemma 3. For any M ∈ Λ, we have [[M ]]\ →∗η M .
Proof. By induction on the structure of M ∈ Λ. We show some of the base cases.
(i):[[λx.M ]]\=(λa.(λx.[[M ]])(π1 a)(π2 a))\=λa1 .(λx.[[M ]]\ )a1→η λx.[[M ]]\→∗η λx.M by the induction hypothesis.
(ii):[[M1 M2 ]]\=(λa.[[M1 ]]h[[M2 ]], ai)\=

(λa.[[M1 ]]h[[M2 ]], hπ1 a, π2 aii)\=

λa1 .[[M ]]\ [[M2 ]]\ a1→η [[M1 ]]\ [[M2 ]]\→∗η M1 M2 by the induction hypotheses.
¤

44

K. FUJITAFor the variables ai (i ≥ 1), the CPS-translation is naturally extended as follows:
Definition 5.
[[ai ]] = ai (i ≥ 1)[[λai .M ]] = λa.(λai .[[M ]])(π1 a)(π2 a)Lemma 4. For any P ∈ Univλ , we have that [[P \ ]]θ →∗λhi P where θ = [a1 :=π1 a, a2 := π1 (π2 a), . . . , ai+1 := π1 (π2i a), . . .].
Proof. By induction on the structure of P ∈ Univλ . We show some of the cases.
Case: P of (λx.R)R1[[((λx.R)R1 )\ ]]=λa.(λa0 .(λx.[[R\ ]])(π1 a0 )(π2 a0 ))h[[R1\ ]], ai→+(λx.[[R\ ]])[[R1\ ]]λhiThen from the induction hypotheses we have the desired property:[[((λx.R)R1 )\ ]]θ →+(λx.([[R\ ]]θ))([[R1\ ]]θ)λhi→∗λhi (λx.R)R1
Case: P of λa.RhR1 , . . . , hRm , π2n ai . . .i[[λa.RhR1 , . . . , hRm , π2n ai . . .i]]=\[[λa1 . . . an .R\ R1\ . . . Rm]]\→+
λa.[[R\ ]]h[[R1\ ]], . . . , h[[Rm]], π2n ai . . .i
β[a1 := π1 a, a2 := π1 (π2 a), . . . , an := π1 (π2n−1 a)]
Now the use of the induction hypotheses gives what we need:[[λa.RhR1 , . . . , hRm , π2n ai . . .i]]θ

→+β\λa.([[R\ ]]θ)h([[R1\ ]]θ), . . . , h([[Rm]]θ), π2n ai . . .i→∗λhi λa.RhR1 , . . . , hRm , π2n ai . . .i¤
Lemma 5. Let R, R1 , . . . , Rn ∈ R.
(1): R\ [x := R1\ ] = (R[x := R1 ])\(2): (R[b := hR1 , . . . , hRm , π2n ai . . .i])\\= R\ [b1 := R1\ , . . . , bm := Rm, bm+1 := an+1 , bm+2 := an+2 , · · · ]under the simultaneous substitution where m ≥ 0 and n ≥ 1.
Proof. By straightforward induction on the structure of R. We show the base casefor (2).
Case of: i + 1 ≤ m(π1 (π2i b)[b := hR1 , . . . , hRm , π2n ai . . .i])\ = (π1 (π2i hR1 , . . . , hRm , π2n ai . . .i))\\\= Ri+1= (π1 (π2i b))\ [bi+1 := Ri+1]

AN INJECTIVE CPS-TRANSLATION FOR THE EXTENSIONAL λ-CALCULUS

45

Case of: i + 1 > m(π1 (π2i b)[b := hR1 , . . . , hRm , π2n ai . . .i])\ = (π1 (π2i hR1 , . . . , hRm , π2n ai . . .i))\= (π1 (π2n+i−m a))\ = an+i−m+1= (π1 (π2i b))\ [bm+1 := an+1 , . . .]= bi+1 [bm+1 := an+1 , . . .] = ai+1−m+n¤
Proposition 3 (Completeness). Let P, Q ∈ Univλ .
(1): If P →βx Q then P \ →β Q\ .
\(2): If P →βa Q then P \ →+β Q .
(3): If P →ηa Q then P \ →η Q\ .
(4): If P →πR,K Q then P \ ≡ Q\ .
(5): If P →spK Q then P \ →∗η Q\ .
Proof. By induction on the derivations. We show one case for (2), and other cases
are straightforward.
Let K be hS1 , . . . , hSq , π2p bi . . .i with q ≥ 0, p ≥ 1, and K 0 be hR1 , . . . , hRm ,π2n ai . . .i with m ≥ 0, n ≥ 1. Let θ be [b := K 0 ]. Now we prove the case P ofλa.(λb.RK)K 0 :\(λa.(λb.RK)K 0 )\ = λa1 . . . an .(λb1 . . . bp .R\ S1\ · · · Sq\ )R1\ · · · Rm

Case of: p + 1 ≤ m(λa.(λb.RK)K 0 )\\\→+λa1 . . . an .(R\ S1\ · · · Sq\ )[b1 := R1\ , . . . , bp := Rp\ ]Rp+1· · · Rmβ=λa1 . . . an .(R\ S1\ · · · Sq\ )\\\· · · Rm
, bm+1 := am+1 , bm+2 := am+2 , . . .]Rp+1[b1 := R1\ , . . . , bm := Rm

since none of bp+1 , bp+2 , . . . appears in R\ , S1\ , . . . , Sq\=\\
λa1 . . . an .((Rθ)\ (S1 θ)\ · · · (Sq θ)\ )Rp+1· · · Rmby Lemma 5=(λa.RθhS1 θ, . . . , hSq θ, hRp+1 , . . . , hRm , π2n ai . . .ii . . .i)\=(λa.RθhS1 θ, . . . , hSq θ, π2p hR1 , . . . , hRm , π2n ai . . .ii . . .i)\=(λa.RK[b := K 0 ])\Case of: p + 1 > m(λa.(λb.RK)K 0 )\\λa1 . . . an .λbm+1 . . . bp .(R\ S1\ · · · Sq\ )[b1 := R1\ , . . . , bm := Rm
]
→+
β

=

λa1 . . . an an+1 . . . ap−m+n .R\ S1\ · · · Sq\\[b1 := R1\ , . . . , bm := Rm, bm+1 := an+1 , bm+2 := an+2 , . . .]=λa1 . . . an+p−m .(Rθ)\ (S1 θ)\ · · · (Sq θ)\ by Lemma 5=(λa.RθhS1 θ, . . . , hSq θ, π2n+p−m (a)i . . .i)\=(λa.RθhS1 θ, . . . , hSq θ, π2p hR1 , . . . , hRm , π2n ai . . .ii . . .i)\=(λa.RK[b := K 0 ])\46

K. FUJITA¤
Now we can establish our main theorem (equational correspondence between Λ
and Univλ ⊆ Λhi ).
Theorem 1.
(i): Let M1 , M2 ∈ Λ. M1 =βη M2 if and only if [[M1 ]] =λhi [[M2 ]].
(ii): Let P1 , P2 ∈ Univλ . P1 =λhi P2 if and only if P1\ =βη P2\ .
Proof.
(i): From Propositions 1 and 3 and Lemma 3.
(ii): From Propositions 1 and 3 and Lemma 4.
¤
def

Let [M ] = {N ∈ Λ | [[M ]] =λhi [[N ]]} for M ∈ Λ. The theorem above means that
we have N1 =βη N2 for any N1 , N2 ∈ [M ].
defCorollary 1. Let [[Λ]] = {[[M ]] ∈ Λhi | M ∈ Λ}. [[Λ]] is a Church-Rosser subset, inthe sense that if P →∗λhi P1 and P →∗λhi P2 where P, P1 , P2 ∈ [[Λ]] then there exists
some Q ∈ [[Λ]] such that P1 →∗λhi Q and P2 →∗λhi Q.
3. Concluding Remarks(1): Λhi is not Church-Rosser by Klop [1].
As stated in Corollary 1, Theorem 1 reveals thatdef[[Λ]] = {[[M ]] ∈ Λhi | M ∈ Λ}
is a confluent fragment, in the sense that if P1 =λhi P2 for P1 , P2 ∈ [[Λ]] thenthere exists some P ∈ [[Λ]] such that P1 →∗λhi P and P2 →∗λhi P .
(2): There exists a one-to-one correspondence between Λhi and C-monoids2
by Lambek and Scott [11] and by Curien [3]:(CAss ): (x ◦ y) ◦ z = x ◦ (y ◦ z)
(CIdl ): 1 ◦ x = x(CIdr ): x ◦ 1 = x(CFst ): π1 ◦ hx, yi = x(CSnd ): π2 ◦ hx, yi = y(CSP ): hπ1 ◦ x, π2 ◦ xi = x(CApp ): App ◦ hCur(x) ◦ π1 , π2 i = x(CSΛ ): Cur(App ◦ hx ◦ π1 , π2 i) = x
Theorem 1 implies that there also exists a nontrivial injection from Λ into
C-monoids.
(3): Even in the case of typed λ-calculus, the novel CPS-translation works
well as a negative translation from proofs of intuitionistic logic consistingof ⇒ (implication) into those of that consisting of ⇒ and ∧ (conjunction).
¬A (negation of A) is defined by A ⇒ ⊥ where ⊥ is treated as an arbitrary
proposition letter. From the Curry-Howard isomorphism [10], formulae are
regarded as types and proofs are as terms or programs. Here the judgementΓ ` M : A says that M is a proof of the formula A under the set of
2According to [11], C stands for Curry, Church, combinatory or cartesian.

AN INJECTIVE CPS-TRANSLATION FOR THE EXTENSIONAL λ-CALCULUS

47

assumptions Γ. The inference rules of typed Λhi is given as follows, andthose of typed Λ is defined by typed Λhi without (∧I) nor (∧E):
x:A ∈ ΓΓ`x:A
Γ, x : A1 ` M : A2(⇒ I)
Γ ` λx.M : A1 ⇒ A2

Γ ` M1 : A1 ⇒ A2 Γ ` M2 : A1(⇒ E)
Γ ` M1 M2 : A2

Γ ` M1 : A1 Γ ` M2 : A2(∧I)
Γ ` hM1 , M2 i : A1 ∧ A2

Γ ` M : A1 ∧ A2(∧E)
Γ ` πi (M ) : Ai

Proposition 4. Γ ` M : A in typed Λ if and only if Γk ` [[M ]] : Ak in typed
Λhi , where
formulae (types) are embedded as follows: (A1 ⇒ A2 )k = ¬(Ak1 ∧ A∗2 );Ak = ¬¬A if A is atomic; andA∗ = B where ¬B ≡ Ak .
We remark that the embedding Ak is essentially equivalent to the GödelGentzen negative translation, since we have ¬(Ak1 ∧ A∗2 ) ⇔ (Ak1 ⇒ Ak2 ) in
the so-called minimal logic. This observation can be applied to prove theonly-if part of the proposition above.
(4): A recursive domain safisfyingU∼=U ×U ∼= [U → U ]gives a model of the λ-calculus with surjective pairing [8]. The domainU∼= U ×U ∼= [U → U ] can provide continuation denotational semantics ofthe extensional λµ-calculus as well. From a natural extension of Theorem
1 the completeness of the continuation denotational semantics of the λµcalculus depends on that of the direct denotational semantics of Λhi . See
also [6] for a formal relation, via continuous functions f and g, between
the continuation denotational semantics C(−) of the λµ-calculus and the
CPS-translation followed by the direct denotational semantics D(−) of Λhi :injective CP SM∈ Λµ−−−−−−−→
Λhi 3 [[M
 ]]



continuationy
ydirectfg
0
C(M ) ∈ U ←−−−−−−−−−−−−−−→ U 3 D[[M ]]where U 0 = [U × U → U ].
Acknowledgments . I am grateful to Horai-Takahashi Masako and Yokouchi Hirofumi for helpful discussions. This work has been partially supported by Grantsin-Aid for Scientific Research (C)(2)14540119, Japan Society for the Promotion of

48

K. FUJITA

Science. This research has been supported by the Kayamori Foundation of Informational Science Advancement.
References[1] H. P. Barendregt: The Lambda Calculus, Its Syntax and Semantics (revised edition), NorthHolland, 1984.
[2] K. Baba, S. Hirokawa, and K. Fujita: Parallel Reduction in Type-Free λµ-Calculus, Electronic Notes in Theoretical Computer Science, Vol. 42, pp. 52–66, 2001.
[3] P. -L. Curien: Categorical Combinators, Sequential Algorithms and Functional Programming, Pitman, London/John Wiley&Sons, 1986.
[4] K. Fujita: A Simple Model of Type Free λµ-Calculus, The 18th Conference Proceedings
Japan Society for Software Science and Technology, 2001.
[5] K. Fujita: An interpretation of λµ-calculus in λ-calculus, Information Processing Letters,Vol. 84-5, pp. 261–264, 2002.
[6] K. Fujita: Continuation Semantics and CPS-translation of λµ-Calculus, Scientiae Mathematicae Japonicae, Vol. 57, No. 1, pp. 73–82, 2003.
[7] T. G. Griffin: A Formulae-as-Types Notion of Control, Proc. the 17th Annual ACM Symposium on Principles of Programming Languages, pp. 47–58, 1990.
[8] C. A. Gunter and D. S. Scott: Semantic Domains, in: Handbook of Theoretical Computer
Science Vol. B : Formal Models and Semantics, Elsevier Science Publishers B. V., 1990.
[9] M. Hofmann and T. Streicher: Continuation models are universal for λµ-calculus, Proc. the12th Annual IEEE Symposium on Logic in Computer Science, pp. 387–395, 1997.
[10] W. Howard: The Formulae-as-Types Notion of Constructions, in: To H.B.Curry: Essays
on combinatory logic, lambda-calculus, and formalism, Academic Press, pp. 479–490, 1980.
[11] J. Lambek and P. J. Scott: Introduction to higher order categorical logic, Cambridge University Press, 1986.
[12] C. R. Murthy: An Evaluation Semantics for Classical Proofs, Proc. the 6th Annual IEEE
Symposium on Logic in Computer Science, pp. 96–107, 1991.
[13] M. Parigot: λµ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction,
Lecture Notes in Computer Science 624, pp. 190–201, 1992.
[14] M. Parigot: Proofs of Strong Normalization for Second Order Classical Natural Deduction,
J. Symbolic Logic 62 (4), pp. 1461–1479, 1997.
[15] G. Plotkin: Call-by-Name, Call-by-Value and the λ-Calculus, Theoretical Computer Science
1, pp. 125–159, 1975.
[16] P. Selinger: Control Categories and Duality: on the Categorical Semantics of the LambdaMu Calculus, Mathematical Structures in Computer Science 11, pp. 207–260, 2001.
[17] T. Streicher and B. Reus: Classical Logic, Continuation Semantics and Abstract Machines,
J. Functional Programming 8, No. 6, pp. 543–572, 1998.
Department of Mathematics and Computer Science, Shimane University, Matsue
690-8504, Japan.
E-mail address: fujiken@cis.shimane-u.ac.jp