PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 92(106) (2012), 79–95 DOI: 10.2298/PIM1206079L

ON SEMANTICS OF A TERM CALCULUS FOR CLASSICAL LOGIC

Silvia Likavec and Pierre Lescanne

Communicated by Žarko Mijajlović

Abstract. The calculus of Curien and Herbelin was introduced to provide the Curry–Howard correspondence for classical logic. The terms of this calculus represent derivations in the sequent calculus proof system and reduction reflects the process of cut-elimination. We investigate some properties of two well-behaved subcalculi of untyped calculus of Curien and Herbelin, closed under the call-by-name and the call-by-value reduction, respectively. Continuation semantics is given using the category of negated domains and Moggi’s Kleisli category over predomains for the continuation monad. Soundness theorems are given for both versions thus relating operational and denotational semantics. A thorough overview of the work on continuation semantics is given.

1. Introduction

It is well known that simply typed lambda calculus corresponds to intuitionistic logic through Curry–Howard correspondence [15]. Extending lambda calculus with control operators brings this correspondence to the realm of classical logic, as first showed by Griffin in [13]. Next cornerstone in the study of theories of control in programming languages was Parigot’s λμ calculus [27].

\overline{λ}μμ̃ calculus of Curien and Herbelin [6] is a system with a more fine-grained analysis of calculations within languages with control operators. Since it was introduced in [6], \overline{λ}μμ̃ calculus has had a strong influence on further understanding between calculi with control operators and classical logic (see [2, 3, 39, 40]).

This work contributes to the better understanding of \overline{λ}μμ̃ calculus in two ways. We prove confluence and build denotational semantics for the untyped version of the calculus. Untyped \overline{λ}μμ̃ calculus is Turing-complete, hence a naive set-theoretic approach would not be enough. Since the calculus is not confluent, it is necessary to

2010 Mathematics Subject Classification: Primary 03B40, 03B70, 18C50; Secondary 68N18. Key words and phrases: logic, lambda calculus, call-by-value, call-by-name, confluence, continuation semantics, control, monad, category theory. Partially supported by the Ministry of Education and Science of Serbia, project ON174026.

consider separately the call-by-name and call-by-value disciplines. The semantics is defined using category of negated domains [35] and Kleisli category [18]. Soundness theorems are given for both, call-by-value and call-by-name subcalculi, thus relating operational and denotational semantics.

The paper is organized as follows. In Section 2 we recall the syntax and the reduction rules of \overline{λ}μμ̃ calculus, and its two well-behaved subcalculi \overline{λ}μμ̃_{T} and \overline{λ}μμ̃_{Q}. In Section 3 we prove the confluence for \overline{λ}μμ̃_{T} (the proof of confluence for \overline{λ}μμ̃_{Q} being analogous). Section 4 presents an overview of the work done on continuation semantics, gives an account of negated domains and presents the basic notions of Kleisli triple and Kleisli category. We give the semantic interpretations of \overline{λ}μμ̃_{Q} and \overline{λ}μμ̃_{T} calculi in Subections 5.1 and 5.2. We conclude in Section 6.

2. Overview of \overline{λ}μμ̃ calculus

2.1. Intuition and syntax. The \overline{λ}μμ̃ calculus was introduced by Curien and Herbelin in [6], giving a Curry–Howard correspondence for classical logic. The terms of \overline{λ}μμ̃ represent derivations in the implicational fragment (hence without conjunction or disjunction) of the sequent calculus proof system LK and reduction reflects the process of cut-elimination.^{1} The untyped version of the calculus can be seen as the foundation of a functional programming language with explicit notion of control and was further studied by Ghilezan and Lescanne in [12].

The syntax of \overline{λ}μμ̃ is given by the following, where v ranges over the set Caller of callers, e ranges over the set Calleeof callees and c ranges over the set Capsule of capsules:

v ::= x | λx.v | μα.c  e ::= α | v • e | μ̃x.c  c ::= ⟨v ∥ e⟩

There are two kinds of variables in the calculus: the set Var_{v}, consisting of caller variables (denoted by Latin variables x, y, …) and the set Var_{e}, consisting of callee variables (denoted by Greek variables α, β, …). The caller variables can be bound by λ abstraction or by μ abstraction, whereas the callee variables can be bound by μ̃ abstraction. The sets of free caller and callee variables, Fv_{v} and Fv_{e}, are defined as usual, respecting Barendregt’s convention [4] that no variable can be both, bound and free, in the expression.

In [6], the basic constructs are called commands, terms, and contexts. In our opinion, meta-concepts like “terms" and “contexts" are going to be used naturally as in any other language, so it would be inappropriate to use them as concepts inside the language. In order to avoid confusion, in this work we use the following basic syntactic entities: the set Caller of callers, the set Callee of callees and the set Capsule of capsules, chosen by Ghilezan and Lescanne in [12].

Capsules are the place where callers and callees interact. A caller can either get the data from the callee, or it can ask the callee to replace one of its internal callee variables. A callee can ask a caller to replace one of its internal caller variables. The components can be nested and more processes can be active at the same time.

1Although, some cuts build normal forms in \overline{λ}μ_{μ}, as opposed to Lengrand’s λξ calculus [20 ], which is exactly LK (with implicit structural rules).

2.2. Reduction rules. There are only three rules that characterize the reduction in \overline{λ}μμ̃:

\begin{matrix}(→ ′) & ⟨λx.v_{1} ∥ v_{2} • e⟩ → ⟨v_{2} ∥ μ̃x.⟨v_{1} ∥ e⟩⟩ \\ (μ) & ⟨μα.c ∥ e⟩ → c[α ← e] \\ (μ̃) & ⟨v ∥ μ̃x.c⟩ → c[x ← v] \end{matrix}

The above substitutions are defined as to avoid variable capture [4].

The calculus has a critical pair ⟨μα.c_{1} ∥ μ̃x.c_{2}⟩ where both (μ) and (μ̃) rule can be applied non-deterministically, producing two different results. For example,

⟨μα.⟨y ∥ β⟩ ∥ μ̃x.⟨z ∥ γ⟩⟩ →_{μ} ⟨y ∥ β⟩ and ⟨μα.⟨y ∥ β⟩ ∥ μ̃x.⟨z ∥ γ⟩⟩ →_{μ} ⟨z ∥ γ⟩,

where α and β denote syntactically different callee variables.

Hence, the calculus is not confluent. But if the priority is given either to (μ) or to (μ̃) rule, we obtain two confluent subcalculi \overline{λ}μμ̃_{T} and \overline{λ}μμ̃_{Q} (we retain the original notation from [6]). We give the details in the next subsection.

2.3. Two confluent subcalculi. There are two possible reduction strategies in the calculus that depend on the orientation of the critical pair. If the priority is given to (μ) redexes, call-by-value reduction is obtained (\overline{λ}μμ̃_{Q} calculus), whereas giving the priority to (μ̃) redexes, simulates call-by-name reduction (\overline{λ}μμ̃_{T} calculus).

We first give the syntactic constructs of \overline{λ}μμ̃_{T} and \overline{λ}μμ̃_{Q}, respectively:

\underline{\overline{λ}μμ̃_{T}}  \underline{\overline{λ}μμ̃_{Q}}
c ::= ⟨v ∥ e⟩  c ::= ⟨v ∥ e⟩
v ::= x | λx.v| μα.c  V ::= x | λx.v
E ::= α | v • E  v ::= μα.c | V
e ::= μ̃x.c | E  e ::= α | μ̃x.c | V • e

In \overline{λ}μμ̃_{T} the new syntactic subcategory E of callees, called applicative contexts, is introduced in order to model call-by-name reduction. In \overline{λ}μμ̃_{Q}, notice the presence of the new syntactic construct V that models the values.

The reduction rules for \overline{λ}μμ̃_{T} and \overline{λ}μμ̃_{Q} are the following:

\underline{\overline{λ}μμ̃_{T}}
(→ ) ⟨λx.v_{1} ∥ v_{2} • E⟩ → ⟨v_{1}[x ← v_{2}] ∥ E⟩
(μ) ⟨μα.c ∥ E⟩ → c[α ← E]
(μ̃) ⟨v ∥ μ̃x.c⟩ → c[x ← v]
\underline{\overline{λ}μμ̃_{Q}}
(→ ′) ⟨λx.v_{1} ∥ V_{2} • e⟩ → ⟨V_{2} ∥ μ̃x.⟨v_{1} ∥ e⟩⟩
(μ) ⟨μα.c ∥ e⟩ → c[α ← e]
(μ̃) ⟨V ∥ μ̃x.c⟩ → c[x ← V]

Notice that our choice of rules does not violate the symmetry of Curien– Herbelin rules. In [6] only the rule (→ ′) is considered for both subcalculi. In this paper we use (→ ) reduction rather than (→ ′) reduction in the case of \overline{λ}μμ̃_{T}, since the application of the (→ ′) rule will always be immediately followed by the application of the (μ̃) rule and that is exactly the rule (→ ). We think that our choice makes explicit the priorities of the rules in each subcalculus.

3. Confluence

Since in the next sections we work with two confluent subcalculi of \overline{λ}μμ̃ calculus, and confluence was never spelled out so far, we think it is in place to prove the confluence for each of them. We adopt the technique of parallel reduction given by Takahashi in [38]. This approach consists of simultaneously reducing all the redexes existing in a term.

We give the proof only for \overline{λ}μμ̃_{T}, since the proof for \overline{λ}μμ̃_{Q} is obtained by a straightforward modification of the proof for \overline{λ}μμ̃_{T}. The complete proofs can be found in [21]. We denote the reduction defined by the three reduction rules for \overline{λ}μμ̃_{T} by →_{n} and its reflexive, transitive and closure by congruence by → →_{n} .

First, we define the notion of parallel reduction ⇒_{n} for \overline{λ}μμ̃_{T}. We prove that → →_{n} is reflexive and transitive closure of ⇒_{n} (Lemma 3.3), so in order to prove the confluence of → →_{n} , it is enough to prove the diamond property for ⇒_{n} (Theorem 3.2). The diamond property for ⇒_{n} , follows from the stronger “Star property” for ⇒_{n} that we prove (Theorem 3.1).

3.1. Parallel reduction for \overline{λ}μμ̃_{T} calculus. Definition 3.1 (Parallel reduction for \overline{λ}μμ̃_{T} calculus). The parallel reduction, denoted by ⇒_{n} is defined inductively, as follows:

x ⇒_{n} x (g1^{n}) {v ⇒_{n} v′ \atop λx.v ⇒_{n} λx.v′} (g2_{n}) {c ⇒_{n} c′ \atop μα.c ⇒_{n} μα.c′} (g3_{n})
α ⇒_{n} α (g4^{n}) {v ⇒_{n} v′, E ⇒_{n} E′ \atop v • E ⇒_{n} v′• E′} (g5_{n}) {c ⇒_{n} c′ \atop μ̃x.c ⇒_{n} μ̃x.c′} (g6_{n})

{v ⇒_{n} v′, e ⇒_{n} e′ \atop ⟨v ∥ e⟩ ⇒_{n} ⟨v′ ∥ e′⟩}(g7_{n}) {v_{1} ⇒_{n} v′_{1}, v_{2} ⇒_{n} v′_{2}, E ⇒_{n} E′ \atop ⟨λx.v_{1} ∥ v_{2} • E⟩ ⇒_{n} ⟨v′_{1}[x ← v′_{2}] ∥ E′⟩}(g8_{n})
{c ⇒_{n} c′, E ⇒_{n} E′ \atop ⟨μα.c ∥ E⟩ ⇒_{n} c′[α ← E′]} (g9_{n}) {v ⇒_{n} v′, c ⇒_{n} c′ \atop ⟨v ∥ μ̃x.c⟩ ⇒_{n} c′[x ← v′]}(g10_{n})

Lemma 3.1. For every term G, G ⇒_{n} G.

Proof. Induction on the structure of G. The base cases are the rules (g1_{n}) and (g4_{n}) from Definition 3.1. For any other term of the calculus, we apply the induction hypothesis to the immediate subterms of G (rules (g2_{n}), (g3_{n}), (g5_{n})– (g7_{n})). □

Lemma 3.2 (Substitution lemma).

1. G[x ← v_{1}][y ← v_{2}] = G[y ← v_{2}][x ← v_{1}[y ← v_{2}]], for x ≠ y, x ∉ Fv_{v}(v_{2}).

2. G[x ← v][α ← e] = G[α ← e][x ← v[α ← e]], for x ∉ Fv_{v}(e).

3. G[α ← e][x ← v] = G[x ← v][α ← e[x ← v]], for α ∉ Fv_{e}(v).

4. G[α ← e_{1}][β ← e_{2}] = G[β ← e_{2}][α ← e_{1}[β ← e_{2}]], for α ≠ β, α ∉ Fv_{e}(e_{2}).

Proof. Induction on the structure of G. It is enough to prove the first two statements for the caller variables, and the last two statements for the callee variables only, since all the other cases are either trivial or follow directly from the induction hypothesis. □

Next, we give the definition of contexts, which are terms with the “hole" and are used in the proof of Lemma 3.3.

Definition 3.2 (Contexts).

C ::= [ ] | λx.C | μα.C | v • C | C • E | μ̃x.C | ⟨v ∥ C⟩ | ⟨C ∥ e⟩

With C[G] we denote “filling the hole” of the context C with the term G (with possible variable capture).

Lemma 3.3. 1. If G →_{n} G′ then G ⇒_{n} G′; 2. If G ⇒_{n} G′ then G → →_{n} G′;

3. If G ⇒_{n} G′ and H ⇒_{n} H′, then

G[x ← H] ⇒_{n} G′[x ← H′] and G[α ← H] ⇒_{n} G′[α ← H′].

Proof. 1. Induction on the context of the redex. If G →_{n} G′ then G = C[H], G′ = C[H′] and H →_{n} H′. We just show two illustrative cases:

* C = [ ]. We proceed by induction on the definition of H →_{n} H′. We have the

following cases:

- H = ⟨μα.c ∥ E⟩ and H′ = c[α ← E]. Then H ⇒_{n} H′ by (g9_{n}), because c ⇒_{n} c and E ⇒_{n} E by Lemma 3.1.

- Cases H = ⟨λx.v_{1} ∥ v_{2} • E⟩ and H = ⟨v ∥ μ̃x.c⟩ are treated similarly.

* C = μ̃x.C′. Then G = μ̃x.C′[H] and G′ = μ̃x.C′[H′]. By the induction hypothesis, C′[H] ⇒_{n} C′[H′], so by (g3_{n}) of the Definition 3.1 we get G ⇒_{n} G′.

2. Induction on the definition of G ⇒_{n} G′. Since the proofs follow the same pattern in all the cases, we show just the case when

G = ⟨λx.v_{1} ∥ v_{2} • E⟩ ⇒_{n} ⟨v′_{1}[x ← v′_{2}] ∥ E′⟩ = G′.

This follows directly from v_{1} ⇒_{n} v′_{1}, v_{2} ⇒_{n} v′_{2} and E ⇒_{n} E′. By the induction hypothesis, v_{i} → →_{n} v′_{i}, i = 1, 2 and E → →_{n} E′ so it follows that

G = ⟨λx.v_{1} ∥ v_{2} • E⟩ →_{n} ⟨v_{1}[x ← v_{2}] ∥ E⟩ → →_{n} ⟨v′_{1}[x ← v′_{2}] ∥ E′⟩ = G′.

3. Induction on the definition of G ⇒_{n} G′. We only illustrate the proof of G[x ← H] ⇒_{n} G′[x ← H′], since the proof of G[α ← H] ⇒_{n} G′[α ← H′] follows the same pattern (using cases 3 and 4 of the Substitution lemma 3.2).

Let G = ⟨λy.v_{1} ∥ v_{2}•E⟩ ⇒_{n} ⟨v′_{1}[y ← v′_{2}] ∥ E′⟩ = G′. This is a direct consequence of v_{1} ⇒_{n} v′_{1}, v_{2} ⇒_{n} v′_{2}, and E ⇒_{n} E′. By the induction hypothesis it follows that v_{1}[x ← H] ⇒_{n} v′_{1}[x ← H′], v_{2}[x ← H] ⇒_{n} v′_{2}[x ← H′], and E[x ← H] ⇒_{n} E′[x ← H′]. Then, using Lemma 3.2(1) and (g8_{n}) we derive

G[x ← H]= ⟨λy.v_{1} ∥ v_{2} • E⟩[x ← H]
= ⟨λy.v_{1}[x ← H] ∥ v_{2}[x ← H] • E[x ← H]⟩
⇒_{n} ⟨v′_{1}[x ← H′][y ← v′_{2}[x ← H′]] ∥ E′[x ← H′]⟩
= ⟨v′_{1}[y ← v′_{2}][x ← H′] ∥ E′[x ← H′]⟩ = G′[x ← H′].  □

From 1 and 2 we conclude that → →_{n} is the reflexive and transitive closure of ⇒_{n} .

3.2. Confluence of \overline{λ}μμ̃_{T} calculus. Next, we define the term G^{∗} which is obtained from G by simultaneously reducing all the existing redexes of the term G.

Definition 3.3. Let G be an arbitrary term of \overline{λ}μμ̃_{T}. The term G^{∗} is defined inductively as follows:

\begin{matrix}(∗1_{n}) & x^{∗} ≡ x & (∗2_{n}) & (λx.v)^{∗} ≡ λx.v^{∗} & (∗3_{n}) & (μα.c)^{∗} ≡ μα.c^{∗} \\ (∗4_{n}) & α^{∗} ≡ α & (∗5_{n}) & (v • E)^{∗} ≡ v^{∗} • E^{∗} & (∗6_{n}) & (μ̃x.c)^{∗} ≡ μ̃x.c^{∗} \end{matrix} ; \begin{aligned}(∗7_{n}) & (⟨v ∥ e⟩)^{∗} ≡ ⟨v^{∗} ∥ e^{∗}⟩ if ⟨v ∥ e⟩ ≠ ⟨λx.v_{1} ∥ v_{2} • E⟩, \\ & ⟨v ∥ e⟩ ≠ ⟨μα.c ∥ E⟩ and ⟨v ∥ e⟩ ≠ ⟨v ∥ μ̃x.c⟩ \\ (∗8_{n}) & (⟨λx.v_{1} ∥ v_{2} • E⟩)^{∗} ≡ ⟨v_{1}^{∗}[x ← v_{2}^{∗}] ∥ E^{∗}⟩ \\ (∗9_{n}) & (⟨μα.c ∥ E⟩)^{∗} ≡ c^{∗}[α ← E^{∗}] \\ (∗10_{n}) & (⟨v ∥ μ̃x.c⟩)^{∗} ≡ c^{∗}[x ← v^{∗}] \end{aligned}

Theorem 3.1 (Star property for ⇒_{n} ). If G ⇒_{n} G′ then G′⇒_{n} G^{∗}.

Proof. Induction on the structure of G. We show only one illustrative case when G = ⟨λx.v_{1} ∥ v_{2} • E⟩.

If ⟨λx.v_{1} ∥ v_{2} • E⟩ ⇒_{n} G′ then we distinguish two subcases:

1. G′ = ⟨λx.v′_{1} ∥ v′_{2}•E′⟩ for some v′_{1}, v′_{2}, and E′ such that v_{i} ⇒_{n} v′_{i}, i = 1, 2 and E ⇒_{n} E′. By the induction hypothesis, v′_{i}⇒_{n} v_{i}^{∗}, i = 1, 2 and E′⇒_{n} E^{∗}. Then, G′ = ⟨λx.v′_{1} ∥ v′_{2} • E′⟩ ⇒_{n} ⟨v_{1}^{∗}[x ← v_{2}^{∗}] ∥ E^{∗}⟩ = G^{∗} by (g8_{n}).

2. G′ = ⟨v′_{1}[x ← v′_{2}] ∥ E′⟩ for some v′_{1}, v′_{2}, and E′ such that v_{i} ⇒_{n} v′_{i}, i = 1, 2 and E ⇒_{n} E′. By the induction hypothesis, v′_{i}⇒_{n} v_{i}^{∗}, i = 1, 2 and E′⇒_{n} E^{∗}. Then, G′ = ⟨v′_{1}[x ← v′_{2}] ∥ E′⟩ ⇒_{n} ⟨v_{1}^{∗}[x ← v_{2}^{∗}] ∥ E^{∗}⟩ by Lemma 3.3(3) and (g7_{n}). □

Now it is easy to deduce the diamond property for ⇒_{n} .

Theorem 3.2 (Diamond property for ⇒_{n} ). If G_{1} _{n}⇐ G ⇒_{n} G_{2} then G_{1} ⇒_{n} G′_{n}⇐ G_{2} for some G′.

Finally, from Theorem 3.2, it follows that \overline{λ}μμ̃_{T} is confluent.

Theorem 3.3 (Confluence of \overline{λ}μμ̃_{T}). If G_{1} _{n}← ← G → →_{n} G_{2} then G_{1} → →_{n} G′_{n}← ← G_{2} for some G′.

4. Continuation semantics

4.1. Introduction. When interpreting the calculi that embody a notion of control, it is convenient to start from continuation semantics that enables to explicitly refer to continuations, the semantic constructs that represent evaluation contexts.

The method of continuations was first introduced in [37] in order to formalize a flow control in programming languages. Continuations can be seen as analogues of the evaluation contexts, used to evaluate terms. Hence, the term is evaluated in the context representing the rest of the computation. A subterm is evaluated in a new context where the rest of the term is evaluated, and then handed to the old context. The value obtained by evaluation of the term is passed to the context.

Continuation-passing-style (cps) translations were introduced by Fischer and Reynolds in [9] and [31] for the call-by-value lambda calculus, whereas a call-by-name variant was introduced by Plotkin in [28]. Moggi gave a semantic version of a call-by-value cps translation in his study of notions of computation in [25]. Lafont [19] introduced a cps translation of the call-by-name λC calculus [7,8] to a fragment of lambda calculus that corresponds to the ¬, ∧-fragment of the intuitionistic logic. Hence, continuation semantics can be seen as a generalization of the double negation rule from logic, in a sense that cps translation is a transformation on terms which, when observed on types, corresponds to a double negation translation.

In Selinger in [34], categorical semantics for both, call-by-name and call-by-value versions of Parigot’s λμ calculus [27] with disjunction types was given. In this work the notion of control category is formally introduced. It is shown that the call-by-name λμ calculus forms an internal language for control categories, whereas the call-by-value λμ calculus forms an internal language for co-control categories. The opposite of the call-by-name model is shown to be equivalent to the cbv model in the presence of product and disjunction types. Hofmann and Streicher presented categorical continuation models for the call-by-name λμ calculus in [17] and showed the completeness.

In their original work on the \overline{λ}μμ̃ calculus [6], Curien and Herbelin defined a call-by-name and a call-by-value cps-translations of the complete typed \overline{λ}μμ̃ calculus into simply typed lambda calculus. The important point to notice is that they also interpret the types of the form A − B, which are dual to the arrow types A → B. The translations validate call-by-name and call-by-value discipline, respectively.

Lengrand gave categorical semantics of the typed \overline{λ}μμ̃ calculus and the λξ calculus (implicational fragment of the classical sequent calculus LK) in [20].

Ong [26] defined a class of categorical models for the call-by-name λμ calculus based on fibrations. This model was later extended for two forms of disjunction by Pym and Ritter in [30].

4.2. Category of continuations. Categories of continuations were introduced by Hofmann and Streicher in [16]. They can be seen as special instances of control categories, which were introduced and formally described by Selinger in [34]. In simple words, control categories are cartesian closed categories enriched with premonoidal structure of [29].

Let C be a category with distributive finite products and sums. We also assume that there is a fixed object R ∈ C such that exponentials of the form R^{A} exist for all objects A. If C also satisfies the mono requirement (i.e., the morphism ∂_{A} : A → R^{R^{A}} is monic^{2} for all A ∈ C) then such a category C is called a response category and R is called an object of responses.

For a given response category C, the full subcategory of C that consists of the objects of the form R^{A} is called a category of continuations and is denoted by R^{C}. This category is cartesian closed [22] and has a canonical premonoidal structure [34]. This can be summarized as follows:

2A morphism f : A → B in a category C is called monic if for any object C and any two morphisms g_{1}, g_{2} : C → A, if f ∘ g_{1} = f ∘ g_{2}, then g_{1} = g_{2}.

• 1 ≅ R^{0} (terminal object in R^{C} is 1)

• R^{A} × R^{B} ≅ R^{A+B} (R^{C} has cartesian products)

• (R^{B})^{(R^{A} )} ≅ R^{R^{A} ×B} (R^{C} has exponentials)

• ⊥ := R^{1} ≅ R (bottom exists in R^{C})

• R^{A}⅋R^{B} := R^{A×B} (⅋ is a binoidal functor in R^{C}, see [34] for details).

In fact, it is proved in [34] that every control category is equivalent to a category of continuations (see also [11]).

4.3. Category of negated domains. As a further specialization of categories of continuations, we describe the category of negated domains N_{R} which was introduced by Lafont in [19], where he investigated the translation of classical propositional logic to the ¬, ∧-fragment of the intuitionistic propositional logic.

Before giving the formal definition, let us first of all, fix some basic terminology that will be used.

• A predomain is a partial order where all directed subsets have a supremum. It does not necessarily have a least element.

• A domain is a predomain with a least element called bottom, denoted by ⊥.

• A Scott continuous function is a monotone function that preserves suprema of directed sets.

• A strict continuous function is a function that preserves bottom elements. The category of predomains and Scott continuous functions is denoted by P. The category of domains and Scott continuous (resp. strict Scott continuous) functions is denoted by D (resp. D_{⊥} ).

Let R be some fixed domain with the bottom ⊥_{R} for a category D. We call R a domain of responses. For each predomain A ∈ P we can form the exponential R^{A} ∈ D. Then we define the category N_{R} equivalent to a full subcategory of D, where the morphisms operate on exponentials of the form R^{A}. Hence, the category N_{R} is an instance of the category of continuations where the category P of predomains is a basic category, since it has finite products and sums, and exponentials of the form R^{A} exist. Let us give the formal definition.

Definition 4.1. The category of negated domains N_{R} over the category P of predomains is defined as follows:

• the objects of N_{R} are objects of P (predomains),

• N_{R}(A, B) = P(R^{A}, R^{B}),

• composition of morphisms in N_{R} is inherited from P.

As already mentioned, (R^{B})^{(R^{A} )} ≅ R^{R^{A} ×B} , so we will denote the function space operator in N_{R} as (see [36]): A ⇒ B := R^{A} × B.

Since by the assumption, R has a bottom element, all the exponentials have bottom elements. The bottom element for R^{A} is given by ⊥_{R^{A}} = λx : A.⊥_{R} for any predomain A ∈ P. Hence, N_{R} is equivalent to a full subcategory of D. The least fixpoint for f ∈ N_{R}(A, A) is given by ⨆ _{n∈ℕ} f^{n}(⊥_{R^{A}} ). The following theorem (proved in [35]) states that the category N_{R} has enough structure to interpret functional calculi, especially the calculi with control operators.

Theorem 4.1. The category N_{R} is cartesian closed and has the least fixpoint operator, for any domain R.

4.4. From ordinary models to continuation models. For the extensional lambda calculus, a model is given by an object C in a cartesian closed category, such that C is isomorphic to its function space, i.e., C ≅ C^{C} [32,33]. We call such an object a reflexive object. (For solutions of recursive domain equations, we refer the reader to [1, 10, 14].)

In order to obtain a model of lambda calculus and its extensions in N_{R}, we have the same requirement in the category N_{R} of negated domains, which means that we are looking for an object K such that K ≅ K ⇒ K. This requires solving the domain equation K ≅ R^{K} × K in P. For K which is the initial solution of this domain equation, we have that R^{K} ≅ R^{R^{K} ×K} ≅ (R^{K})^{(R^{K} )} , so we conclude that C = R^{K} is a solution of domain equation C ≅ C^{C} in P and is called a continuation model of the untyped lambda calculus. In [35] it is proved that C = R^{K} is isomorphic to Scott’s C_{∞} model of extensional lambda calculus [32, 33] by taking C = R.

We can interpret the untyped lambda calculus in N_{R}. The meaning of a lambda term is a morphism R^{K} mapping continuations (the elements of K) to responses (the elements of R). The continuation for the function f : R^{A} → R^{B} is a pair ⟨s, k⟩, where the argument for the function f is s ∈ R^{A} and k ∈ B is the continuation for f(s).

This interpretation can be extended to Felleisen’s call-by-name λC calculus [7] and to the untyped version of Parigot’s λμ calculus [27], given in Streicher and Reus [35]. In the same work it is also proved that the semantic equations defining the interpretations in the continuation model of the untyped lambda calculus are in 1-1 correspondence with the transition rules of Krivine’s abstract machine.

4.5. Kleisli category. Kleisli categories introduced by Kleisli in [18] (see also [5, 23]) provide the categorical semantics of computations based on monads. Since every monad corresponds to Kleisli triple, the semantics can be given using Kleisli triples that are easier to justify computationally.

When interpreting a programming language in the call-by-value setting in a category C, we need to distinguish the objects A that represent the values of type A from the objects T A that represent the computations of type A. The computations of type A are obtained by applying a functor T to A, which is called the notion of computation [25]. There are certain conditions that T has to satisfy and it turns out that T needs to give rise to a Kleisli triple, whereas programs form the Kleisli category for such a triple.

The following definitions are taken from Moggi’s paper on notions of computations [25], which are in turn taken from [24].

Definition 4.2. A Kleisli triple over a category C is a triple (T, η, _^{∗}), such that T : Obj(C) → Obj(C), η_{A} : A → T A for A ∈ Obj(C), f^{∗} : T A → T B for f : A → T B and the following equations hold:

η_{A}^{∗} = id_{T A}; f^{∗} ∘ η_{A} = f for f : A → T B;
g^{∗} ∘ f^{∗} = (g^{∗} ∘ f)^{∗} for f : A → T B and g : B → T K.

Next we give the definition of the Kleisli category.

Definition 4.3. The Kleisli category C_{T} over a category C for a given Kleisli triple (T, η, _^{∗}) is defined as follows:

• the objects of C_{T} are the objects of C;

• C_{T}(A, B) = C(A, T B);

• id_{C_{T}} = η_{A} : A → T A;

• g ∘_{C_{T}} f = g^{∗} ∘ f : A → T D for f ∈ C_{T}(A, B) and g ∈ C_{T}(B, D).

4.6. Kleisli triple of continuations. Depending on the specific computation that we want to model, different computational monads or Kleisli triples can be chosen. In this analysis we will consider Kleisli triple of continuations given by

• T A = R^{R^{A}} , where R is the fixed object of responses, together with

• a family of morphisms η_{A}(a) = λk : R^{A}.k(a) and

• an operation on morphisms f^{∗}(s) = λk : R^{B}.s(λa : A.f(a)(k)) for f : A → T B and s ∈ T A.

We will denote by K_{R} the Kleisli category over the category P of predomains for a given Kleisli triple of continuations (T, η, _^{∗}).

Then, the intuitive meaning of η_{A} is the inclusion of values into computations, whereas f^{∗} can be seen as an extension of a function f mapping values to computations into a function mapping computations into computations.

As noticed in [36], the Kleisli category K_{R} for a continuation Kleisli triple and the dual of the category of negated domains N_{R}^{op} are isomorphic and the isomorphism is given by H : K_{R} → N_{R}^{op} and K : N_{R}^{op} → K_{R}, where

H(f) = λk : R^{B}.λv : A.f(v)(k) ∈ (R^{A})^{(R^{B} )} for f ∈ (T B)^{A},
K(g) = λv : A.λk : R^{B}.g(k)(v) ∈ (T B)^{(A)} for g ∈ (R^{A})^{R^{B}} .

5. Semantics

As we have seen, the categories N_{R} and C_{T} are very convenient for defining the semantics of the various calculi with control operators, since they allow to explicitly deal with continuations. Therefore, we think they are a good starting point for giving the semantics of \overline{λ}μμ̃ calculus, although the results of this section apply to any categorical model in which it is possible to solve the domain equations.

As mentioned previously, \overline{λ}μμ̃ is not confluent due to the presence of the critical pair ⟨μα.c ∥ μ̃x.c⟩. Hence, we consider separately two well-behaved subsyntaxes closed either under call-by-value (\overline{λ}μμ̃_{Q}) or under call-by-name reduction (\overline{λ}μμ̃_{T}).

5.1. Semantics of \overline{λ}μμ̃_{Q} calculus. In this subection we will consider \overline{λ}μμ̃_{Q},

which is a variant of untyped \overline{λ}μμ̃ calculus closed under the call-by-value reduction.

We give the definition of the interpretation functions for all four syntactic categories of the calculus. Having an interpretation function also for the values prevents the values and the computations to be confused. Lambda abstractions are values, but can also have arguments that are values, producing computations as the result, so it is necessary to have W ≅ C^{W}.

Definition 5.1. Let us consider the initial solution of the system of domain equations W ≅ C^{W}, K ≅ R^{W}, C ≅ R^{K}. Let Envbe the set of the environments that map the caller variables to the elements of W and the callee variables to the elements of K, i.e., for ρ ∈ Env: ∀x ∈ Var_{v}, ρ(x) ∈ W and ∀α ∈ Var_{e}, ρ(α) ∈ K. The interpretation functions

[[−]]_{V} : Value→ Env→ W = C^{W}  [[−]]_{D} : Caller→ Env→ C = R^{K}
[[−]]_{C} : Callee→ Env→ K = R^{W}  [[−]]_{R} : Capsule→ Env→ R

are defined as follows:

Value:  Caller:
[[x]]_{V}ρ= ρ(x)  [[x]]_{D}ρ= λk.k[[x]]_{V}ρ
[[λx.v]]_{V}ρ= λw.[[v]]_{D}ρ[x := w]  [[λx.v]]_{D}ρ= λk.k[[λx.v]]_{V}ρ
[[μα.c]]_{D}ρ= λk.[[c]]_{R}ρ[α := k]

Callee:

[[α]]_{C}ρ= ρ(α)  Capsule:
[[V • e]]_{C}ρ= λw.(w([[V]]_{V}ρ))([[e]]_{C}ρ) [[⟨v ∥ e⟩]]_{R}ρ= [[v]]_{D}ρ([[e]]_{C}ρ)

[[μ̃x.c]]_{C}ρ= λw.[[c]]_{R}ρ[x := w]

We will omit the subscripts in various interpretations, (since they can be deduced from the term being interpreted), a part from [[−]]_{V} where we leave the subscript to avoid the ambiguity.

One important difference when interpreting the call-by-value calculus (with respect to the interpretation of the call-by-name variant) is that variables are interpreted as values, i.e., ρ(x) ∈ W, whereas in the call-by-name case variables are interpreted as computations, i.e., ρ(x) ∈ C.

The different syntactic constructs of \overline{λ}μμ̃_{Q} can be seen as elements of the following semantical objects:

• values are the elements of W,

• callers as computations are the elements of C = R^{R^{W}} ,

• callees as continuations are the elements of K = R^{W},

• capsules as responses are the elements of R. In the case of callees, V • e and μ̃x.c can be seen as call-by-value evaluation

contexts. For V • e, the computation (seen as a value) is applied to V and then evaluated in the evaluation context e. For μ̃x.c, the caller is just fed into the capsule c. In the case of capsules, the meaning of the term v (element of C) is applied to the continuation bound to e (element of K) and produces an element of R.

Also, notice that the interpretation of values in C is obtained by applying η_{A}(a) = λk : R^{A}.k(a) from the Kleisli triple, to the interpretation of values in W. Hence, we include values into denotations. On the other hand, μα.c is not a value, so its interpretation is given only in C. Its meaning is the functional abstraction over the continuation variable α.

Next we give some lemmas that are used to prove that the semantics is preserved under the reduction rules.

Lemma 5.1 (Substitution lemma). Let G be the term of \overline{λ}μμ̃_{Q} (caller, callee, or capsule). Then

1. [[G[x ← V]]]ρ = [[G]]ρ[x := [[V]]_{V}ρ], for all four interpretation functions.

2. [[G[α ← e]]]ρ = [[G]]ρ[α := [[e]]ρ].

Proof. 1. Induction on the structure of V, followed by induction on the structure of G. 1.1. [[G[x ← y]]]ρ = [[G]]ρ[x := ρ(y)] We prove the statement only for [[−]]_{D}.

* G = z trivial

* G = x [[x[x ← y]]]ρ = [[y]]ρ = λk.kρ(y) = λk.kρ[x := ρ(y)](x)

= [[x]]ρ[x := ρ(y)]

* G = λz.r [[λz.r[x ← y]]]ρ = λk.k(λw.[[r[x ← y]]]ρ[z := w])

= λk.k(λw.[[r]]ρ[x := ρ(y), z := w]) = [[λz.r]]ρ[x := ρ(y)]

* G = μα.c [[μα.c[x ← y]]]ρ = λk.[[c[x ← y]]]ρ[α := k] = λk.[[c]]ρ[x := ρ(y), α := k] = [[μα.c]]ρ[x := ρ(y)]

* The cases G = β, G = V • e, G = μ̃y.c, and G = ⟨v ∥ e⟩ are either trivial or

follow from the induction hypothesis. 1.2. [[G[x ← λy.v]]]ρ = [[G]]ρ[x := [[λy.v]]_{V}ρ] Again, we prove the statement for [[−]]_{D}.

* G = z trivial

* G = x [[x[x ← λy.v]]]ρ = [[λy.v]]ρ = λk.k([[λy.v]]_{V}ρ)

= λk.k(ρ[x := [[λy.v]]_{V}ρ](x)) = [[x]]ρ[x := [[λy.v]]_{V}ρ]

* G = λz.r [[λz.r[x ← λy.v]]]ρ = λk.k([[λz.r[x ← λy.v]]]_{V}ρ)

= λk.k(λw.[[r[x ← λy.v]]]ρ[z := w])

= λk.k(λw.[[r]]ρ[x := [[λy.v]]_{V}ρ, z := w]) = [[λz.r]]ρ[x := [[λy.v]]_{V}ρ]

* G = μα.c [[μα.c[x ← λy.v]]]ρ = λk.[[c[x ← λy.v]]]ρ[α := k] = λk.[[c]]ρ[x := [[λy.v]]_{V}ρ][α := k] = [[μα.c]]ρ[x := [[λy.v]]_{V}ρ]

* The cases G = β, G = V • e, G = μ̃y.c, and G = ⟨v ∥ e⟩ again follow trivially.

2. Induction on the structure of G, followed by induction on the structure of e. It is enough to prove the lemma for G = α because all the other cases follow either trivially (G = γ, G = x) or by the induction hypothesis.

* e = β [[α[α ← β]]]ρ = [[β]]ρ = [[α]]ρ[α := Aiβρ]

* e = μ̃x.c [[α[α ← μ̃x.c]]]ρ = [[μ̃x.c]]ρ = [[α]]ρ[α := [[μ̃x.c]]ρ]

* e = V • e [[α[α ← V • e]]]ρ = [[V • e]]ρ = [[α]]ρ[α := [[V • e]]ρ]. □

Theorem 5.1 (Preservation of the semantics under reduction).

If G_{1} → G_{2}, then [[G_{1}]] = [[G_{2}]].

Proof. 1. ⟨μα.c ∥ e⟩ → c[α ← e] [[⟨μα.c ∥ e⟩]]ρ = [[μα.c]]ρ([[e]]ρ) = (λk.[[c]]ρ[α := k])([[e]]ρ) = [[c]]ρ[α := [[e]]ρ] = [[c[α ← e]]]ρ

2. ⟨V ∥ μ̃x.c⟩ → c[x ← V] Induction on the structure of V.

* V = y [[⟨y ∥ μ̃x.c⟩]]ρ = [[y]]ρ([[μ̃x.c]]ρ) = (λk.kρ(y))(λw.[[c]]ρ[x := w])

= (λw.[[c]]ρ[x := w])ρ(y) = [[c]]ρ[x := ρ(y)] = [[c[x ← y]]]ρ

* V = λy.v [[⟨λy.v ∥ μ̃x.c⟩]]ρ = [[λy.v]]ρ([[μ̃x.c]]ρ)

= (λk.k(λw.[[v]]ρ[y := w]))(λw_{1}.[[c]]ρ[x := w_{1}])
= (λw_{1}.[[c]]ρ[x := w_{1}])(λw.[[v]]ρ[y := w])
= [[c]]ρ[x := λw.[[v]]ρ[y := w]] = [[c[x ← λy.v]]]ρ

Hence [[⟨V ∥ μ̃x.c⟩]]ρ = [[c[x ← V]]]ρ.

3. ⟨λx.v ∥ V • e⟩ → ⟨V ∥ μ̃x.⟨v ∥ e⟩⟩ [[⟨λx.v ∥ V • e⟩]]ρ = [[λx.v]]ρ([[V • e]]ρ) = (λk.k(λw.[[v]]ρ[x := w]))(λw_{1}.(w_{1}([[V]]_{V}ρ))([[e]]ρ)) = (λw_{1}.(w_{1}([[V]]_{V}ρ))([[e]]ρ))(λw.[[v]]ρ[x := w]) = (λw.[[v]]ρ[x := w])([[V]]_{V}ρ)([[e]]ρ) = [[v]]ρ[x := [[V]]_{V}ρ]([[e]]ρ) = [[v[x ← V]]]ρ([[e]]ρ)

[[⟨V ∥ μ̃x.⟨v ∥ e⟩⟩]]ρ = [[V]]ρ([[μ̃x.⟨v ∥ e⟩]]ρ)

= [[⟨v ∥ e⟩[x ← V]]]ρ as in 2.

= [[v[x ← V]]]ρ([[e]]ρ) since x ∉ e. □

For the complete proofs see [21].

5.2. Semantics of \overline{λ}μμ̃_{T} calculus. In Subection 5.1, we considered two different types of computations, namely the values as the elements of W and the computations as the elements of C. With the help of η_{A}(a) = λk : R^{A}.k(a) from the Kleisli triple, we had a way of including the values into the computations. So we will apply the same technique at the level of continuations. In the set of callees we will distinguish basic continuations that we call co-values (called applicative contexts in [6]), from the rest of continuations.

Next, we give the interpretation functions for all the four syntactic constructs of \overline{λ}μμ̃_{T}. Giving the interpretation function also for co-values, makes a clear difference between co-values and the rest of callees.

Definition 5.2. Let K be the initial solution of the domain equation K ≅ R^{K} × K and let C = R^{K} and F = R^{C}. With Envwe denote the set of the environments that map the caller variables to the elements of C and the callee variables to the elements of K, i.e., for ρ ∈ Env:

∀x ∈ Var_{v}, ρ(x) ∈ C and ∀α ∈ Var_{e}, ρ(α) ∈ K.

Then the interpretation functions are defined as follows:

[[−]]_{C} : Co-value→ Env→ K  [[−]]_{E} : Callee→ Env→ F = R^{C}
[[−]]_{D} : Caller→ Env→ C = R^{K}  [[−]]_{R} : Capsule→ Env→ R
Co-value:  Callee:
[[α]]_{C}ρ= ρ(α)  [[α]]_{E}ρ= λs.s([[α]]_{C}ρ)
[[v • E]]_{C}ρ= ⟨[[v]]_{D}ρ, [[E]]_{C}ρ⟩  [[v • E]]_{E}ρ= λs.s([[v • E]]_{C}ρ)
[[μ̃x.c]]_{E}ρ= λs.[[c]]_{R}ρ[x := s]

Caller:

[[x]]_{D}ρ= ρ(x)  Capsule:
[[λx.v]]_{D}ρ= λ⟨s, k⟩.[[v]]_{D}ρ[x := s]k [[⟨v ∥ e⟩]]_{R}ρ= [[e]]_{E}ρ([[v]]_{D}ρ)
[[μα.c]]_{D}ρ= λk.[[c]]_{R}ρ[α := k]

We will omit the subscripts in various interpretations, as they can be deduced from the terms being interpreted, apart from [[−]]_{E} where we leave the subscript to avoid the ambiguity.

Now, we can see the different syntactic constructs of \overline{λ}μμ̃_{T} as the elements of the following semantical objects:

• callers as computations are the elements of C = R^{K},

• co-values as basic continuations are the elements of K ≅ R^{K} × K,

• callees as continuations are the elements of F = R^{C},

• capsules as responses are the elements of R.

Since K ≅ R^{K} ×K, continuations are of the form ⟨s, k⟩, where s ∈ C and k ∈ K. Therefore we can see continuations as infinite lists of denotations which correspond to the denotational versions of the call-by-name evaluation contexts. Callers are interpreted as functions that map continuations to responses. This reflects the fact that a caller can either get the data from a callee or ask it to replace one of its internal callee variables. Hence, callers expect callees as arguments. Since a callee can ask a caller to replace one of its internal caller variables, it has to have a functional part that could be applied to a caller. Finally, in the case of capsules, the interpretation of the callee is applied to the interpretation of the caller, thus producing an element in R.

Also, notice that the interpretation of the co-values in F is obtained by applying η_{K} (k) = λs : R^{R^{K}} .s(k) from the Kleisli triple, to the interpretation of the co-values in K. Hence, we include the co-values into the continuations. On the other hand, μ̃x.c is not a co-value, hence its interpretation is given only in F.

As in the previous section, we first give some lemmas that are used later to prove that the semantics is preserved under the reduction rules.

Lemma 5.2 (Substitution lemma). Let G be the term of \overline{λ}μμ̃_{T} (caller, callee, or capsule). Then

1. [[G[x ← v]]]ρ = [[G]]ρ[x := [[v]]ρ];

2. [[G[α ← E]]]_{(K)} ρ = [[G]]_{(K)} ρ[x := [[E]]_{C}ρ]

where [[−]]_{(K)} means that in the case of co-values, the lemma holds for both interpretations, namely [[−]]_{E} and [[−]]_{C}.

Theorem 5.2 (Preservation of the semantics under reduction).

If G_{1} → G_{2} then [[G_{1}]] = [[G_{2}]]

6. Conclusions

This work investigates some properties of \overline{λ}μμ̃_{T} and \overline{λ}μμ̃_{Q}, the two subcalculi of untyped \overline{λ}μμ̃ calculus of Curien and Herbelin [6], closed under the call-by-name and the call-by-value reduction, respectively.

First of all, the proof of confluence for both versions of the \overline{λ}μμ̃ calculus is given, adopting the method of parallel reduction given in [38]. As a step towards a better understanding of denotational semantics of \overline{λ}μμ̃ calculus, its untyped callby-value (\overline{λ}μμ̃_{Q}) and call-by-name (\overline{λ}μμ̃_{T}) versions are interpreted. Continuation semantics of \overline{λ}μμ̃_{Q} and \overline{λ}μμ̃_{T} is given using the category of negated domains of [35], and Moggi’s Kleisli category over predomains for the continuation monad [25]. In both cases the reduction preserves the denotations.

The first future step to take is to explore completeness and show that these semantics are computationally adequate. We would also like to extend the present work to the complete symmetric calculus of [6] and find the interpretation for all the constructs of that calculus, including e•v and βλ.e. Still in the realm of categorical semantics, we intend to interprete the typed \overline{λ}μμ̃ calculus using fibrations, as done for the λμ calculus in [26] and [30].

Acknowledgements. The authors would like to thank the two anonymous referees for their valuable remarks which helped us improve the final version of the paper.

References

1. R. M. Amadio and P-L. Curien, Domains and Lambda-Calculi, Cambridge University Press, Cambridge, 1998.

2. Z. M. Ariola and H. Herbelin, Minimal classical logic and control operators, in: Proc. Annual International Colloquium on Automata, Languages and Programming ICALP ’03, Lect. Notes Comput. Sci. 2719, Springer-Verlag, Berlin, 2003, 871–885.

3. Z. M. Ariola, H. Herbelin, and A. Sabry, A type-theoretic foundation of continuations and prompts, in: Proc. 9th Internat. Conf. on Funct. Prog. ICFP ’04, 40–53, 2004.

4. H. P. Barendregt, The Lambda Calculus: its Syntax and Semantics, North-Holland, Amsterdam, revised edition, 1984.

5. M. Barr and C. Wells, Category Theory for Computing Science, Les publications Centre de recherches mathématiques, 1999.

6. P.-L. Curien and H. Herbelin, The Duality of Computation, in: Proc. 5th Internat. Conf. on Functional Programming, ICFP’00, 233–243, Montreal, Canada, 2000; ACM Press.

7. M. Felleisen, D. P. Friedman, E. Kohlbecker and B. F. Duba, A syntactic theory of sequential control, Theor. Comput. Sci. 52(3):205–237, 1987.

8. M. Felleisen and R. Hieb, The revised report on the syntactic theories of sequential control and state, Theor. Comput. Sci. 103(2):235–271, 1992.

9. M. Fischer, Lambda calculus schemata, in: Proc. ACM Conf. on Proving Assertions About Programs ’72, 104–109 ACM Press, 1972.

10. P. Freyd, Remarks on algebraically compact categories, in: Notes of the London Mathematical Society, 177, 1992.

11. C. Führmann, The structure of call-by-value, PhD thesis, University of Edinburgh, 2000.

12. S. Ghilezan and P. Lescanne, Classical proofs, typed processes and intersection types, in: Proc. Workshop Types for Proofs and Programs TYPES ’03 (Selected Papers), Lect. Notes Comput. Sci. 3085, 226–241, Springer-Verlag, Berlin, 2004.

13. T. Griffin, A formulae-as-types notion of control, in: Proc. 19th Annual ACM Symp. on Principles Of Programming Languages, POPL ’90, 47–58, ACM Press, 1990.

14. C. A. Gunter and D. S. Scott, Semantic domains, In J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, volume B. Elsevier, Amsterdam, 1990.

15. W. Howard, The formulae-as-types notion of construction, in: J. P. Seldin and J. R. Hindley (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 479–490, Academic Press, 1980.

16. M. Hofmann and Th. Streicher, Continuation models are universal for lambda-mu-calculus, in: Proc. 11th IEEE Annual Symposium on Logic in Computer Science LICS ’97, 387–397. IEEE Computer Society Press, 1997.

17. M. Hofmann and Th. Streicher, Completeness of continuation models for λμ-calculus, Inf. Comput. 179(2):332–355, 2002.

18. H. Kleisli, Every standard construction is induced by a pair of adjoint functors, in: Proc. American Mathematical Society, volume 16, 544–546, 1965.

19. Y. Lafont, Negation versus implication, Draft, 1991.

20. S. Lengrand, Call-by-value, call-by-name, and strong normalization for the classical sequent calculus, Electr. Notes Theor. Comput. Sci. 86, Elsevier, 2003.

21. S. Likavec, Types for object-oriented and functional programming languages, PhD thesis, Università di Torino, Italy, ENS Lyon, France, 2005.

22. Y. Lafont, B. Reus, and Th. Streicher, Continuation semantics or expressing implication by negation, Technical Report 93-21. University of Munich, 1993.

23. J. Lambek and P. J. Scott, Introduction to higher order categorical logic, Cambridge University Press, Cambridge, 1986.

24. E. Manes, Algebraic theories, in: Graduate Texts in Mathematics. Springer Verlag, Berlin, 1976.

25. E. Moggi, Notions of computations and monads, Inf. Comput. 93(1), 1991.

26. C.-H. L. Ong, A semantic view of classical proofs: type-theoretic, categorical, denotational characterizations, in: Proc. 11th IEEE Annual Symposium on Logic in Computer Science LICS ’97, 230–241. IEEE Computer Society Press, 1997.

27. M. Parigot, λμ-calculus: An algorithmic interpretation of classical natural deduction, in: Proc. Internat. Conf. on Logic Programming and Automated Reasoning, LPAR ’92, Lect. Notes Comput. Sci. 624, 190–201, Springer-Verlag, Berlin, 1992.

28. G. D. Plotkin, Call-by-name, call-by-value and the λ-calculus, Theor. Comput. Sci. 1:125–159, 1975.

29. J. Power and E. Robinson, Premonoidal categories and notions of computation, Mathematical Structures in Computer Science, 7(87):453–468, 1997.

30. D. Pym and E. Ritter, On the semantics of classical disjunction, J. Pure Appl. Algebra 159:315–338, 2001.

31. J. C. Reynolds, Definitional interpreters for higher-order programming languages, in: Proc. ACM Annual Conference, 717–740, ACM Press, 1972.

32. D. S. Scott, Continuous lattices, in: F. W. Lawvere (ed.), Toposes, Algebraic Geometry and Logic, Lect. Notes Math. 274, 97–136, Springer-Verlag, Berlin, 1972.

33. D. S. Scott, Domains for denotational semantics, in: M. Nielsen and E. M. Schmidt (ed), Automata, Languages and Programming, Lect. Notes Comput. Sci. 140, Springer-Verlag, Berlin, 1982, 577–613.

34. P. Selinger, Control categories and duality: on the categorical semantics of the lambda-mu calculus, Math. Struct. Comput. Sci. 11(2):207–260, 2001.

35. Th. Streicher and B. Reus, Classical logic, continuation semantics and abstract machines, J. Funct. Program. 8(6):543–572, 1998.

36. Th. Streicher and B. Reus, Continuation semantics: Abstract machines and control operators, Unpublished manuscript, 1998.

37. C. Strachey and C. P. Wadsworth, Continuations: A mathematical semantics for handling full jumps, Oxford University Computing Laboratory Technical Monograph PRG-11, 1974.

38. M. Takahashi, Parallel reduction in λ-calculus, Inf. Comput. 118:120–127, 1995.

39. P. Wadler, Call-by-value is dual to call-by-name, in: Proc. 8th Internat. Conf. on Funct. Prog. ICFP ’03, 189–201, 2003.

40. P. Wadler, Call-by-value is dual to call-by-name-reloaded, in: Proc. Conf. on Rewriting Technics and Applications RTA ’05, Lect. Notes Comput. Sci. 3467, 185–203, 2005.

Dipartimento di Informatica (Received 05 10 2010) Università di Torino (Revised 19 07 2011) Italy

likavec@di.unito.it

University of Lyon École Normal Supérieure de Lyon France

pierre.lescanne@ens-lyon.fr