Federico Aschieri

Francesco A Genco

Par Means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs

Along the lines of Abramsky's "Proofs-as-Processes" program, we present an interpretation of multiplicative linear logic as typing system for concurrent functional programming. In particular, we study a linear multipleconclusion natural deduction system and show it is isomorphic to a simple and natural extension of λ-calculus with parallelism and communication primitives, called λ `. We shall prove that λ `satisfies all the desirable properties for a typed programming language: subject reduction, progress, strong normalization and confluence.

Introduction

The Proofs-as-Processes Program Introduced by Girard in 1987, linear logic was announced right off the bat as the logic of parallelism. According to [START_REF] Girard | Linear logic[END_REF], the "connectives of linear logic have an obvious meaning in terms of parallel computation (...) In particular, the multiplicative fragment can be seen as a system of communication without problems of synchronization." Stimulated by this remark and the further observation that "cut elimination is parallel communication between processes" ( [START_REF] Girard | Proofs and Types[END_REF], pp. 155), Abramsky [START_REF] Abramsky | Proofs as processes[END_REF] launched the "Proofs-as-Processes" program, whose goal was to support with computational evidence Girard's claims. Namely, the goal was "to show how a process calculus, sufficiently expressive to allow a reasonable range of concurrent programming examples to be handled, could be exhibited as the computational correlate of a proof system" [START_REF] Abramsky | Proofs as processes[END_REF]. A candidate process calculus was Milner's π-calculus [START_REF] Milner | A calculus of mobile processes[END_REF]; a possible proof system, the linear sequent calculus. The hope was that linear logic could provide a canonical and firm foundation to concurrent computation, serving as a tool for typing and reasoning about communicating processes.

Early Successes and Limitations

After early works of [START_REF] Bellin | On the pi-calculus and linear logic[END_REF] and [START_REF] Beffara | A concurrent model for linear logic[END_REF], the turning point was the discovery by Caires and Pfenning [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] of a tight correspondence between intuitionistic linear logic and a session typed π-calculus, the motto being: linear propositions as session types, proofs as processes, cut-elimination as communication. This was yet another instance of the famous Curry-Howard correspondence [START_REF] Wadler | Propositions as types[END_REF], linking proofs to programs, propositions to types, proof normalization to computation. Soon after, Wadler [START_REF] Wadler | Propositions as sessions[END_REF] introduced the session typed π-calculus CP, shown to tightly correspond to classical linear logic.

This important research notwithstanding, it appears that there is still ground to cover toward canonical and firm foundations for concurrent computation. First of all, asynchronous communication does not appear to rest on solid foundations. Yet this communication style is easier to implement and more practical than the purely synchronous paradigm, so it is widespread and asynchronous typed process calculi have been already investigated (see [START_REF] Gay | Linear type theory for asynchronous session types[END_REF]). Unfortunately, linear logic has not so far provided via Curry-Howard a logical account of asynchronous communication. The reason is that there is a glaring discrepancy between full cut-elimination in sequent calculus and π-calculus reduction which has not so far been addressed. On one hand, as we shall see, linear logic does support asynchronous communication, but only through the full process of cutelimination, which indeed makes essential use of asynchronous communication. On the other hand, the π-calculus of [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] only mimics a partial cut-elimination process that only eliminates top-level cuts. Indeed, by comparison with its type system, the π-calculus lacks some necessary computational reduction rules. Some of the missing reductions, corresponding to commuting conversions, were provided in Wadler's CP. The congruence rules that allow the extra reductions to mirror full cut-elimination, however, were rejected: in Wadler's [START_REF] Wadler | Propositions as sessions[END_REF] own words, "such rules do not correspond well to our notion of computation on processes, so we omit them". A set of reductions similar to that rejected by Wadler is regarded in [START_REF] Pérez | Linear logical relations for session-based concurrency[END_REF] as sound relatively to a notion of "typed context bisimilarity". The notion, however, only ensures that two "bisimilar" processes have the same input/output behaviour along their main communication channel; the internal synchronization among the parallel components of the two processes is not captured and may differ significantly. Thus, the extensional flavor of the bisimilarity notion prevents it from detecting the intensionally different behaviour of the related processes, that is, how differently they communicate and compute.

Attempts to model asynchronous communication by mirroring full cut-elimination with Milner's π-calculus are indeed bound to fail. An example will clarify the matter. In the process νz(x(y).z(w).P | z[a].Q), the second process z[a].Q wishes to transmit the message a along the channel z to the first process. However, the first process is not ready to receive on z yet: it is designed to first receive a message on the channel x. In Milner's π-calculus, this is a deadlock, because input and output actions are rigidly ordered and blocking, for the sake of synchronization. Indeed, as the heir of CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF], π-calculus was born as formalism for representing synchronization: a communication happens when two processes synchronize by consuming two dual constructs, as for instance x m and x(y). However, when a process is seen as a proof in the logical system, the order between prefixes becomes less relevant, thus in CP there is an extra commuting conversion νz(x(y).z(w).P | z[a].Q) → x(y).νz(z(w).P | z[a].Q)

In CP, there is no further reduction allowed, and rightly so: otherwise the blocking nature of the prefix x(y) would be violated, making the very construct pointless for synchronization. On the other hand, for cut-elimination the now possible reduction

x(y).νz(z(w).P | z[a].Q) → x(y).νz(P [a/w] | Q) is needed. In this case, however, as we have seen the very existence of a construct for input becomes misleading and it would be more coherent to drop it altogether, so that the first process would be directly re-written and reduced as follows

νz(P | w[a].Q) → νz(P [a/w] | Q)
This is indeed the approach of the present paper. Sensitive to similar concerns, [START_REF] Kokke | Better late than never: a fully-abstract semantics for classical processes[END_REF] introduced HCP, which features delayed input-output actions, modeling a form of asynchrony. However, the change in the transitions with respect to CP undermines the synchronous nature of Milner's π-calculus, as we have seen, making HCP quite a different calculus and questioning its canonicality. Moreover, HCP comes at the cost of adding more structure, in the form of the hypersequent separator [START_REF] Arnon Avron | Hypersequents, logical consequence and intermediate logics for concurrency[END_REF], to the linear sequent calculus. In HCP this structure is logically redundant, whereas Avron employed it to increase the logical power of sequents. On the other hand, the added structure enables HCP to enjoy a nice isomorphism with proofs.

There are other limitations in the current linear logic foundations of concurrent computation. The linear sequent calculus fails to combine seamlessly functional and concurrent computation. Indeed, according to Abramsky et al. [START_REF] Abramsky | Interaction categories and the foundations of typed concurrent programming[END_REF] it is a "major open problem (...) to combine our understanding of the functional and concurrent paradigms, with their associated mathematical underpinnings, in a single unified theory". The sequent calculus falls short in several other respects: it prevents deadlocks, but by excessively restricting possible communication patterns, for instance by forbidding cyclic configurations; it does not permit in any simple way code mobility, that is, the ability to communicate code, like in higher-order π-calculus [START_REF] Sangiorgi | Expressing mobility in process algebras: first-order and higher-order paradigms[END_REF]; it does not represent multi-party communication sessions; its syntax does not match exactly the syntax of processes. In order to address some of these pitfalls, much work has been done, by either considering non-standard proof systems for linear logic or by extending the logic itself; unfortunately for the canonical-foundation enterprise and practical usability, these systems tends to be proof-theoretically artificial. A system adding a functional language on top of linear-logic-based typed π-calculus was studied in [START_REF] Toninho | Higher-order processes, functions, and sessions: A monadic integration[END_REF]. A solution for allowing, also in the context of the session typed π-calculus, cyclic communication patterns, was given in [START_REF] Dardha | A new linear logic for deadlock-free session-typed processes[END_REF] by coming up with a new variant of linear logic; this makes it possible, for example, to implement Milner's scheduler process. Multi-party session types have been treated for example in [START_REF] Carbone | Multiparty session types as coherence proofs[END_REF]. A hypersequent proof system for linear logic whose syntax perfectly matches the syntax of π-calculus has been introduced in [START_REF] Kokke | Better late than never: a fully-abstract semantics for classical processes[END_REF]. A logic for typing asynchronous communication in a non-standard process calculus has been proposed in [START_REF] Pruiksma | A message-passing interpretation of adjoint logic[END_REF].

λ `: A Concurrent Extension of λ-Calculus Arising from Linear Logic

We shall illustrate a new approach in the study of linear logic as typing system for concurrent programs. Our framework does not suffer any of the mentioned limitations of linear sequent calculus. Inspired by [START_REF] Eades | Multiple conclusion linear logic: Cut elimination and more[END_REF][START_REF] Parigot | Free deduction: An analysis of "computations" in classical logic[END_REF], we move away from sequent calculus and adopt a multiple-conclusion natural deduction for multiplicative linear logic, which we show to be isomorphic to a concurrent extension of λ-calculus, called λ `. As a result, λ `is typed by linear multiple-conclusion natural deduction; it is naturally asynchronous, yet it can model synchronous communication as well; it allows arbitrary communication patterns, like cyclic ones, but prevents deadlocks; it allows higher-order communication and code mobility; it mirrors perfectly a full normalization procedure resulting in analytic proofs; its types can be read as program specifications in the traditional way, although they do not describe communication protocols as session types do.

The typing system of λ `, in its non-linear variant, has been very well studied: computationally, it was famously interpreted by Parigot [START_REF] Parigot | Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction[END_REF] as λµ-calculus; proof-theoretically, it was thoroughly investigated by [START_REF] Cellucci | Existential instantiation and normalization in sequent natural deduction[END_REF]. Although proof-nets have sometimes been dubbed "the natural deduction of linear logic", our typing system is closer to a natural deduction. It is not exactly natural deduction [START_REF] Prawitz | Ideas and results in proof theory[END_REF], since it is multiple-conclusion, hence it is natural for building and typing parallel programs, but not much so for modeling human deduction. However, our system is based on natural-deduction normalization rather than sequentcalculus cut-elimination and linear implication is a primitive connective, with the standard introduction and elimination rules. Like proof-nets (see [START_REF] Girard | Linear logic[END_REF], [START_REF] Honda | An exact correspondence between a typed pi-calculus and polarised proof-nets[END_REF]), λ `abstracts away from those inessential permutations in the order of rules that plague multiple-conclusion logical systems. As a result, λ `avoids commuting conversions, which have never been convincing from the computational point of view. Actually, λ `is not only a concurrent λ-calculus, it also looks like a natural deduction version of proof nets. Finally, it enjoys all the good properties that a well-behaved functional programming language should have: subject reduction, progress, strong normalization, and confluence. It is a step forward in the direction of that elusive concurrent λ-calculus which Milner attempted to find, before creating CCS out of the failure1 .

The Insight

The main insight behind the typing system of λ `is to break into two rules the linear implication introduction. One rule is intuitionistic and yields functional abstraction, the second is classical and yields communication. Namely, the first rule, taken from [START_REF] Eades | Multiple conclusion linear logic: Cut elimination and more[END_REF], introduces the λ-operator, the second a communication channel with continuation:

Γ, x : A ⇒ t : B, ∆ Γ ⇒ λx t : A B, ∆ I ( if x occurs in t) Γ, x : A ⇒ t : B, ∆ Γ ⇒ x. t : A B, ∆ I ( if x occurs in ∆)
Indeed, a communication channel x. t is supposed to take as argument a term u : A, transmit it along the channel x and then continue with t : B. We shall indeed denote the application of x. t to u as xu.t, as in π-calculus: a promising sign! The parallel operator | is introduced by the `introduction rule:

Γ ⇒ s : A, t : B, ∆ Γ ⇒ s | t : A `B, ∆ `I
finally doing justice to the `connective, called par since the beginning.

Multiplicative Linear Logic as a Concurrent Functional Calculus

In this section, we present the syntax, the typing system NMLL (Natural deduction for Multiplicative Linear Logic) and the reduction rules of the concurrent functional calculus λ `. The calculus λ `is nothing but a linear lambda calculus extended with communication primitives. When x occurs in u, the operator x. u is denoted and behaves exactly as λx u. When x does not occur in u, the term x. u behaves as an output channel x followed by a continuation u. Channels in λ `are thus firstclass citizens that can be transmitted, shared, moved and applied to messages just like functions to arguments. When the channel x. u is applied to an argument v, it will be denoted as xv.u, because it behaves exactly as its π-calculus counterpart: it transmits the message v and continues with u. The term x y u transmits the two messages contained in u along the channels x and y and then terminates. Indeed, as it will be clear from the type system, the term u inside x y u must be of type A `B and must contain two messages: the term of type A and the term of type B.

The Calculus λ

If we omit parentheses, each term of λ `can be rewritten, not uniquely, as a parallel composition of several terms: t 1 | t 2 | . . . | t n . We will adopt this notation throughout the paper since it is irrelevant how the parallel operator | associates.

Remark 2.1. An alternative choice for the syntax of λ `may have been:

u, v ::= x | u v | λx u | xv.u | u | v | x y u | • | close(u)
Then the operator xv.u would have been typed by a cut-rule and the construct x. u would have been defined as: λy xy.u. This approach would have raised some technical complications: when transmitting a message v, one would have to deal with the free variables of v which are bound by λ operators occurring outside v. A similar issue is solved in [START_REF] Aschieri | Classical proofs as parallel programs[END_REF], and a simpler solution could be adopted here. Nevertheless, we adopt the present approach, as it is the smoother.

The Typing System NMLL

Definition 2.2 (Types). The types of NMLL are built in the usual way from propositional variables, ⊥ and the connectives and `.

Since the typing system of λ `is classical linear logic, the ⊗ connective can be defined in terms of the others. Indeed, its computational interpretation seems less primitive, as it defines no computational construct that is not already captured by and `. Hence, we leave it out of the system.

Definition 2.3 (Sequents). The judgments of the typing system NMLL for λ àre sequents Γ ⇒ ∆, where: 1. Γ = x 1 : A 1 , . . . , x n : A n is a sequence of distinct variable declarations, each x i being a variable, A i a type and x i = x j for i = j.

2. ∆ = t 1 : B 1 , . . . , t n : B n , t n+1 , . . . , t m , each t i being a term of λ `and B i a type.

The typing system of λ `is a linear version of the multiple-conclusion classical natural deduction of [START_REF] Cellucci | Existential instantiation and normalization in sequent natural deduction[END_REF]. It is presented in Table 1 and discussed in detail below. As usual, we interpret a derivable sequent Γ ⇒ ∆ as a judgement typing a sequence of terms ∆, provided their variables are used with types declared in Γ. The terms in ∆ that have no type are processes that return no value, and always have the form close(u), with u : ⊥. These terms cannot be ignored, as they may be involved in some communication; thus they are evaluated and then terminated. The close( ) construct is introduced by the ⊥E rule and is essential to keep a tight correspondence between logic and calculus, as explained at the beginning of Section 5.

Linearity of Variables

The only condition that the typing rules must satisfy in order to be applied is that their premises share no variable. This amounts to requiring the linearity of variables and to making sure that there is no clash among the names of the output channels. As we shall see in Proposition 7.1, the result of this implicit renaming is that a typed term cannot contain two distinct occurrences of the same output channel x nor of the same input channel x. This property has two consequences. First, in λ `we do not need, and actually do not use, any renaming during reductions. Secondly, communication channels cannot be used twice: once a message is transmitted along a channel, the channel is consumed and disappears forever, both from the sender and from the receiver of the message. These two processes can of course keep communicating with each other or with other processes, but they must use different channels for further communications.

Γ ⇒ s : A, t : B, ∆ Γ ⇒ s | t : A `B, ∆ `I Γ ⇒ s : A `B, ∆ Σ1, x : A ⇒ Θ1 Σ2, y : B ⇒ Θ2 Γ, Σ1, Σ2 ⇒ x y s : ⊥, ∆, Θ1, Θ2 `E
Each rule in this table can only be applied if its premises share no variable Table 1: The type assignment rules of NMLL.

`as a Parallel Operator

The typing system of λ `is tailored to parallel computation. It is based on the view that the different processes of a parallel program are not independent enti-ties, but make sense only as components of a larger and more complex system: they share resources through communication and they exploit the computational power of one another. Hence, one cannot build and type one process, without building at the same time all the interconnected processes. Coherently, a derivation of a sequent Γ ⇒ t 1 : A 1 , . . . , t n : A n , t n+1 , . . . t m builds in parallel the terms t 1 , . . . , t m , following the logical structure of the intended communication pattern. The commas in the conclusion of a sequent, indeed, mean exactly parallel composition. Since the comma, in the final analysis, is the `connective, we obtain the following typing rule:

Γ ⇒ s : A, t : B, ∆ Γ ⇒ s | t : A `B, ∆ `I
As the `is commutative and associative, so is the comma. Our reduction rules, indeed, treat parallel composition as commutative and associative, since they bypass the order and association of processes. Technically, however, the term s | t : A `B is different from the term t | s : B `A, since A `B and B `A are logically equivalent, but not the same type. It would be possible to add explicit commutation and association congruences on the outermost parallel operators |, provided Subject Reduction is restated modulo logical equivalence. Since there is no computational gain in adding such congruences, we do not consider them.

Linear λ-Calculus

λ `contains the linear λ-calculus as a subsystem. On one hand, function application and variable declaration are respectively given by the rule E and the axiom:

Γ ⇒ s : A B, ∆ Σ ⇒ t : A, Θ Γ, Σ ⇒ st : B, ∆, Θ E x : A ⇒ x : A
as usual. On the other hand, the treatment of linear implication is the main novelty of the type system of λ `. Namely, the linear implication introduction rule is broken in two rules. The first is intuitionistic and yields functional abstraction, the second is classical and yields communication. Functional abstraction λ is obtained by the rule:

Γ, x : A ⇒ t : B, ∆ Γ ⇒ λx t : A B, ∆ I ( if x occurs in t)
Such a rule has been studied by [START_REF] Eades | Multiple conclusion linear logic: Cut elimination and more[END_REF] in the context of multiple-conclusion intuitionistic linear logic. Indeed, when x occurs in t, the term λx t is a standard linear λ-term. The application of a function to an argument generates in λ the standard λ-calculus reduction

(λx u)t → u[t/x]
where u[t/x] is the term obtained from u by replacing the occurrence of x with t.

Communication

The other rule for linear implication introduction is:

Γ, x : A ⇒ t : B, ∆ Γ ⇒ x. t : A B, ∆ I ( if x occurs in ∆)
In this case, the variable x does not occur in t, therefore the term x. t is no more a λ-term and behaves like an output channel with continuation t. Namely, when x. t is applied to an argument u, a communication is triggered: the term u is transmitted along the channel x to another process inside ∆ and will replace x inside that process. We thus have in λ `the reduction rules:

C[xu.s] | D[x] → C[s] | D[u] C[x] | D[xu.s] → C[u] | D[s]
where C[ ] and D[ ] are arbitrary contexts, as usual defined as follows.

Definition 2.4 (Contexts). A context C[

] is a term containing a variable [ ] occurring exactly once. For any term t we denote by

C[t] the result of replacing [ ] by t in C[ ]. C[ ] is simple if it does not contain subterms of the form D[ ] | u or u | D[ ] .
In the reduction above, by definition of context, only one occurrence of x is replaced by u. Therefore, if the context

D[ ] is not simple, then the term D[x]
is a parallel composition of several processes and only one of them will actually receive u. For instance, we have

xu.• | (λy y | z x) → • | (λy y | z u).
Unlike in pure π-calculus, the output operator xu.s may transmit its message even if it is surrounded by a potentially non-empty context. This is necessary for fully normalizing the proofs: the alternative is to give up on a full correspondence with the normalization/cut-elimination process, as done in Wadler's typed π-calculus CP [START_REF] Wadler | Propositions as sessions[END_REF]. In our case, it might happen that some variable y of the message u lies under the scope of an operator λy occurring in the context. There is no problem, though: the operator λy is just a notation which automatically becomes y, if the need arises -namely, if y changes location. For instance, let us consider the natural reduction strategy that avoids to reduce under λ:

(λy x(y w).•)v | x → x(v w).• | x → • | v w
If we instead first fire the communication reduction along the channel x, we obtain the very same result, but by a different mechanism:

(λy x(y w).•)v | x = (y. x(y w).•)v | x → (y. •)v | y w = yv.• | y w → • | v w
What happens in this second reduction is that the value of y, still not known during the first communication, is automatically redirected and communicated to the new location of y by the second communication. Therefore, the code mobility issues created by closures, solved in [START_REF] Aschieri | Classical proofs as parallel programs[END_REF] in a more complicated way, literally disappear in λ `.

Similarly, the "capture" of variables during communications by output operators x creates no issue. For instance, the result of the reduction above communicating first along x, then along y:

xv.y | yx.• → y | yv.• → v | •
can also be obtained by communicating first along y, then along x, thus allowing the variable x to be captured by the x operator, which then automatically becomes λx:

xv.y | yx.• → xv.x | • = (λx x)v | • → v | •

Output Channels without Continuation

The elimination rule for the connective `types binary output channels with no associated continuation, a kind of operator also found in the asynchronous π-calculus [START_REF] Boudol | Asynchrony and the Pi-calculus[END_REF]:

Γ ⇒ s : A `B, ∆ Σ 1 , x : A ⇒ Θ 1 Σ 2 , y : B ⇒ Θ 2 Γ, Σ 1 , Σ 2 ⇒ x y s : ⊥, ∆, Θ 1 , Θ 2 `E
When s is a parallel composition u | v, the term x y s transmits u and v respectively along the channel x and y and then terminates with no value, as reflected by its type ⊥. As a result, exactly one occurrence of x will be replaced by u and exactly one occurrence of y will be replaced by v, in two different processes or in the same. The correspondent reduction rules of λ `are:

C[x y (s | t)] | D[x][y] → C[•] | D[s][t] D[x][y] | C[x y (s | t)] → D[s][t] | C[•] D[x] | C[x y (s | t)] | E[y] → D[s] | C[•] | E[t] D[y] | C[x y (s | t)] | E[x] → D[t] | C[•] | E[s]
The first two reduction rules concern the case in which the variables x and y occur in the same context. The last two address the case in which the variables x and y occur in two different contexts.

Process Termination

Classical logic is obtained by a combination of the classical linear implication introduction rule and the ⊥-introduction rule, which introduces the terminated process •, which, in turn, does nothing:

Γ ⇒ ∆ Γ ⇒ ∆, • : ⊥ ⊥I
We can derive the linear excluded middle as shown below on the left. Since terms of type ⊥ return no value, we have the typing rule below on the right.

x : A ⇒ x : A x : A ⇒ x : A, • : ⊥ ⇒ x : A, x. • : A ⊥ ⇒ x | x. • : A `(A ⊥) Γ ⇒ t : ⊥, ∆ Γ ⇒ close(t), ∆ ⊥E
which introduces the construct close(t), whose intended meaning is to execute t and then terminate the computation with no return value, hence it has no type. One could also add the reduction rule close(•) →.

The Reduction Rules of λ

The complete list of reduction rules of λ `is presented in Table 2 for the reader's convenience.

(λx u)t → u[t/x] C[xu.s] | D[x] → C[s] | D[u] C[x] | D[xu.s] → C[u] | D[s] C[x y (s | t)] | D[x][y] → C[•] | D[s][t] D[x][y] | C[x y (s | t)] → D[s][t] | C[•] D[x] | C[x y (s | t)] | E[y] → D[s] | C[•] | E[t] D[y] | C[x y (s | t)] | E[x] → D[t] | C[•] | E[s]
Table 2: Reduction rules for NMLL terms.

As usual, for any context C[ ], we adopt the reduction scheme C[t] → C[u]

whenever t → u. We denote by → * the reflexive and transitive closure of the one-step reduction →. As usual, we shall employ the λ-calculus concepts of normal form and strong normalization.

Definition 2.5 (Normal Forms and Strongly Normalizable Terms).

• A redex is a term u such that u → v for some v and reduction in Table 2.

A term t is called a normal form or, simply, normal, if there is no u such that t → u.

• A finite or infinite sequence of terms u 1 , u 2 , . . . , u n , . . . is said to be a reduction of t, if t = u 1 , and for all i, u i → u i+1 . A term u of λ `is normalizable if there is a finite reduction of u whose last term is normal and is strong normalizable if every reduction of u is finite.

Programming with λ

Ìn order to acquire familiarity with the main features of λ, we discuss now some programming examples. Namely, we shall see how to implement client-server communication, synchronization, cyclic communication patterns and channel sharing.

Example 3.1 (Client-Server: Request/Answer). In this example, we discuss how to represent in λ `a simple communication protocol, consisting in a request/answer message exchange. A server hosts an online catalogue, mapping product names to prices. A client transmits a string prod : String to the server, representing a product name whose price the client wishes to know. The server answers the client request by sending back the price of the product prod, computed by the function cost : String N. A naive way to implement client and server would be

CLIEN T xprod.y | SERV ER y(cost x).• Although, as expected xprod.y | y(cost x).• → y | y(cost prod).• → y | y(price).• → price | •
we observe that, this way, synchronization is implemented poorly. As we see below, the server may send to the client the message (cost x) before it receives any request whatsoever!

xprod.y | y(cost x).• → xprod.cost x | • = (λx cost x)prod | • → * price | •
What we expect, instead, is that only the request of the client can trigger computation and transmission of the answer by the server. In order to force that, the trick is to encapsulate the message prod into the λ-term λaλb a (b prod), whose task is to take as input a server channel a, a continuation b and apply the channel a to b prod. We thus implement client and server as shown below on the left. Since the server output channel y. • is not applied to any argument, the server has no choice but to wait for the client request, as shown below on the right.

CLIEN T

x(λaλb a (b prod)).y

| SERV ER x (y. •) cost x(λaλb a (b prod)).y | x (y. •) cost → y | (λaλb a (b prod)) (y. •) cost → * y | (y(cost prod).• → * y | yprice.• → price | • By defining X := (N ⊥) (String N)
⊥, we can type the process above as follows:

x : X ⇒ x : X ⇒ y : N, y. • : N ⊥ x : X ⇒ y : N, x (y. •) : (String N) ⊥ ⇒ cost : String N x : X ⇒ y : N, x (y. •) cost : ⊥ ⇒ x. y : X N, x (y. •) cost : ⊥ ⇒ (λaλb a (b prod)) : X ⇒ x(λaλb a (b prod)).y : N, x (y. •) cost : ⊥ ⇒ x(λaλb a (b prod)).y | x (y. •) cost : N `⊥
Example 3.2 (Client-Server: Dialogue). We present now a continuation of the previous example which models a longer interaction. We want to represent the following transaction of an online sale. As before, a buyer transmits to a seller a product name prod : String, the seller computes by the function cost the monetary cost price : N of prod and communicates it to the buyer. Then the buyer applies a function pay : N → String to price, that will transmit to the server the credit card number card : String if the client wishes to buy the product, the empty string otherwise. By comparison with the previous example, we must add a new communication channel z for the third communication, because in λ èach communication requires a fresh channel. As before, in order to implement synchronization, messages M will be always transmitted as (λaλb a (b M )):

CLIEN T x(λaλb a (b prod)).y (z. •) pay | SERV ER x (y. z) (λcλa λb a (b cost c))
We can observe the following interaction:

x(λaλb a (b prod)).y (z. •) pay | x (y. z) (λcλa λb a (b cost c)) → y (z. •) pay | (λaλb a (b prod)) (y. z) (λcλa λb a (b cost c)) → * y (z. •) pay | y((λcλa λb a (b cost c))prod).z → * y (z. •) pay | y(λa λb a (b price)).z → (λa λb a (b price)) (z. •) pay | z → * z(pay price).• | z → zcard.• | z → • | card By defining X := (Y String) (String Y ) String, Y := (String ⊥) (N String)
⊥, we can type the process above as follows:

x . Unlike in the session typed π-calculi of [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] and [START_REF] Wadler | Propositions as sessions[END_REF], in λ `one can type in a natural way cyclic communication patterns, as shown in the following example. A client has some secret information M : String, which it wishes to encrypt. For added security, the client desires two encryptions of the message. A couple of servers, by joining forces, offer this kind of double-encryption service. Therefore, the client sends M to the first server, which encrypts M by applying the function enc 1 : String String and then transmits the result to the second server, which in turn encrypts it by applying the function enc 2 : String String and finally transmits the result to the client. The implementation is shown below on the left, and we observe the interaction shown below on the right.

: X ⇒ x : X ⇒ z : String, z. • : String ⊥ y : Y ⇒ y : Y y : Y ⇒ y (z. •) : (N String) ⊥, z : String ⇒ y (z. •) : (N String) ⊥, y. z : Y String ⇒ pay : N String ⇒ y (z. •) pay : ⊥, y. z : Y String x : X ⇒ y (z. •) pay : ⊥, x (y. z) : (String Y ) String ⇒ λcλa λb a (b cost c) : String Y x : X ⇒ y (z. •) pay : ⊥, x (y. z)(λcλa λb a (b cost c)) : String ⇒ x. y (z. •) pay : X ⊥, x (y. z)(λcλa λb a (b cost c)) : String ⇒ λaλb a (b prod) : X ⇒ x(
CLIEN T xM.z | SERV ER 1 y(enc 1 x).• | SERV ER 2 z(enc 2 y).• xM.z | y(enc 1 x).• | z(enc 2 y).• → z | y(enc 1 M ).• | z(enc 2 y).• → z | yM .• | z(enc 2 y).• → z | • | z(enc 2 M ).• → z | • | zM .• → M | • | •
We can type the process above as follows: Example 3.4 (Channel Transmission). Just like π-calculus, λ `supports communication of channel names and thus dynamic communication patterns, as we see in the following example. A server offers a printing service, which is hosted on another machine, connected to the server. In order to exploit the service an access code is required. A consumer, which wants to print the string M , sends its access code access : String to the server, which checks it by the function check. Upon success, the server transmits to the consumer the channel z along which the printer offers its services, so that finally the consumer can send M to the printer. We model printer, server and client as follows:

P RIN T ER z print | SERV ER (check x)(y. •)(z. •) | CON SU M ER xaccess.y (λa a M )
We observe the following interaction:

z print | (check x)(y. •)(z. •) | xaccess.y (λa a M ) → z print | (check access)(y. •)(z. •) | y (λa a M ) → z print | y(z. •).• | y (λa a M ) → z print | • | z(λa a M ).• → (λa a M ) print | • | • → print M | • | • By defining C := ((String ⊥) ⊥)
⊥, we can type the above process as follows:

x :

String ⇒ check x : C C ⊥ y : C ⇒ • : ⊥, y (λa a M ) : ⊥ ⇒ y. • : C, y (λa a M ) : ⊥ x : String ⇒ (check x)(y. •) : C ⊥, y (λa a M ) : ⊥ ⇒ (check x)(y. •) : C ⊥, x. y (λa a M ) : String ⊥ ⇒ access : String ⇒ (check x)(y. •) : C ⊥, xaccess.y (λa a M ) : ⊥ ⇒ z print : ⊥, z. • : C ⇒ z print : ⊥, (check x)(y. •)(z. •) : ⊥, xaccess.y (λa a M ) : ⊥ ⇒ z print | (check x)(y. •)(z. •) : ⊥ `⊥, xaccess.y (λa a M ) : ⊥ ⇒ z print | (check x)(y. •)(z. •) | xaccess.y (λa a M ) : (⊥ `⊥) `⊥ 4

Intermezzo: Synchronous Communication in λ

Ìn π-calculus the actions of both sending and receiving messages are synchronous and blocking. They are synchronous, because they require that the sender and the receiver synchronize; they are blocking, because the execution of both the sender and the receiver is blocked until the message is actually transmitted. Therefore, on one hand, if there is no receiver listening to the channel, a process can neither transmit its message along the channel nor proceed with its execution. On the other hand, a process which does listen cannot proceed with its execution until it receives the message it is waiting for. In π-calculus, synchronicity is implemented by a construct for sending xm. and a construct for receiving x(y). which need to be outermost in the connected processes in order to activate the reduction:

xm.P | x(y).Q → P | Q[m/y].
The blocking nature of the actions is implemented by forbidding reductions inside P and Q before the actions are executed, that is, by forcing a reduction strategy.

Non-blocking actions have been advocated by various authors (e.g. [START_REF] Merro | On asynchrony in name-passing calculi[END_REF], [START_REF] Kokke | Better late than never: a fully-abstract semantics for classical processes[END_REF]) and are necessary for a full correspondence between cut-elimination and process execution. In λ `, the fact that sending and receiving are non-blocking is implemented by just removing the input construct x(y). Hence, provided that x occurs in Q, in λ `we have:

xm.P | Q → P | Q[m/x]
E := [ ] | E u | V E | x y E | close(E)
where V is any value.

To obtain a call-by-value version of λ `, we rewrite the main reduction rules of λ `as follows:

. . . | E[(λx u)V ] | . . . → cbv . . . | E[u[V /x]] | . . . . . . | E[xV.s] | . . . | E [x] | . . . → cbv . . . | E[s] | . . . | E [V ] | . . . . . . | E [x] | . . . | E[xV.s] | . . . → cbv . . . | E [V ] | . . . | E[s] | . . .
where V is a value and E, E call-by-value evaluation contexts. The reduction for x y V are analogous. The idea is that call-by-value contexts bring back a notion of order among operations, which can be used to represent the sequential facet of computation. Thus a term E [x] represents a process whose next operation is a read operation on the channel x, followed by the operations contained in E [ ]. Similarly to Wadler's principal-cut-elimination strategy for CP, → cbv only allows communication on the top level parallel operators.

We can now define in λ `the synchronous input-construct as follows:

x(y).u := (λy u) x Indeed, the term x(y).u is always stuck: since u is located under a λ, no reduction can be performed inside u; since x is not a value, the redex (λy u) x cannot be contracted either. For similar reasons, the term xV.u = (x. u)V is stuck as well: since V is a value, no reduction can be performed inside V ; since u is located under an output operator, no reduction can be performed inside u either. Thus, the only reduction that could be fired is the transmission of V along the channel x, which however requires a suitable receiver, namely a process whose call-by-value evaluation cannot further proceed: the process requires an input value and waits for it. Indeed, in the following configuration, we can reduce

xV.u | x(y).w = xV.u | (λy w)x → cbv u | (λy w)V → cbv u | w[V /y]
In the configuration xV.u | (λz z x(y).w)(λk k) however, the process xV.u cannot transmit its message V until (λz z x(y).w)(λk k) is ready to receive, which will happen as soon as its head redex will be contracted and the value of x(y).w will be really needed. Thus, after one reduction step, we have

xV.u | (λk k) x(y).w → cbv u | (λk k)((λy w) V ) → cbv u | (λk k) w[V /y] → cbv u | w[V /y]

Soundness and Completeness

We show now that the typing system NMLL of λ `captures exactly classical multiplicative linear logic. Namely, we show that NMLL is equivalent to the sequent calculus MLL for classical multiplicative linear logic. The cut rule and the logical rules of MLL -namely, the rules introducing the logical connectives of linear logic on the left or on the right -are the standard double-sided sequent rules for classical linear logic. The initial sequent ⊥ ⇒ corresponds to the initial sequent ⇒ 1. We use the former since we do not use an explicit duality operator.

The only non-standard rule of NMLL is ⊥E. It is clearly sound since it captures the neutrality of ⊥ with respect to `, and hence to the comma on the right-hand side of sequents.

Γ ⇒ ∆ Γ ⇒ ∆, ⊥ ⊥ ⊥ ⇒ Γ ⇒ A, ∆ Σ, B ⇒ Θ Γ, Σ, A B ⇒ ∆, Θ l Γ, A ⇒ B, ∆ Γ ⇒ A B, ∆ r Γ, A ⇒ ∆ Σ, B ⇒ Θ Γ, Σ, A `B ⇒ ∆, Θ `l Γ ⇒ A, B, ∆ Γ ⇒ A `B, ∆ `r Γ ⇒ A, ∆ Σ, A ⇒ Θ Γ, Σ ⇒ ∆, Θ cut
Table 3: The sequent calculus MLL.

Proposition 5.1 (Soundness). If Γ ⇒ ∆ is derivable in NMLL, then Γ ⇒ ∆ is derivable in MLL.
Proof. By induction on the number of rule applications in the NMLL derivation of S = Γ ⇒ ∆.

The natural deduction calculus NMLL corresponds very neatly to the sequent calculus MLL. Hence, a completeness proof of NMLL with respect to MLL is quite straightforward. The proof deviates from standard reasoning only insofar as we need to handle the occurrences of ⊥ introduced by `E. Indeed, whenever we apply `E, we introduce an occurrence of ⊥ to type a term of the form x y m containing output channels x and y and a message m. But, in order to obtain a derivation of a specific target sequent Γ ⇒ ∆, we might need to remove those extra occurrences of ⊥. To do so, we use the ⊥E rule.

Proposition 5.2 (Completeness). If Γ ⇒ ∆ is derivable in MLL, then Γ ⇒ ∆ is derivable in NMLL.
Proof. By induction on the number of rule applications in the MLL derivation of S = Γ ⇒ ∆.

Subject Reduction

We are now going to prove that the reductions of λ `preserve the typing of terms, a property well-known under the name of Subject Reduction. We first need the concept of substitution, which in λ `is just a replacement of some variables, with no renaming involved. Definition 6.1 (Substitution). For any multiset of typed terms ∆ and terms v 1 , . . . , v n , we denote by ∆[v 1 /x 1 . . . v n /x n ] the simultaneous replacement, for any i ∈ {1, . . . , n}, of all occurrences of x i in all terms of ∆ by v i . Given a substitution [t/x], we refer to t as the substituting term and to x as the substituted variable.

In order to prove Subject Reduction, we first prove that if we have a variable x : A in the context of a derivable sequent Γ, x : A ⇒ ∆ and we can type a term t : A by deriving a sequent Σ ⇒ t : A, Θ, then we can derive the sequent Γ, Σ ⇒ ∆[t/x], Θ effectively replacing the variable x : A with the term t : A. The proof-theoretical intuition is the following: if A is among the assumptions of a proof, and we have a derivation t of A, then we can use t to derive A directly inside the proof. Lemma 6.1 (Substitution). If Σ ⇒ t : A, Θ and Γ, x : A ⇒ ∆ are derivable in NMLL and share no variable, then Γ, Σ ⇒ ∆[t/x], Θ is derivable in NMLL as well.

Proof. We proceed by induction on the number of rule applications in the derivation of Γ, x : A ⇒ ∆.

If no rule is applied in the derivation, then Γ, x : A ⇒ ∆ is of the form x : A ⇒ x : A. Therefore, Γ, Σ ⇒ ∆[t/x], Θ is just Σ ⇒ t : A, Θ and the claim trivially holds.

Suppose now that the statement holds for any sequent which is derivable with n or less rule applications, we show the result for any sequent Γ, x : A ⇒ ∆ which is derivable using n + 1 rule applications. We reason by cases on the last rule applied in this derivation of Γ, x : A ⇒ ∆.

• Γ, x : A ⇒ ∆ Γ, x : A ⇒ ∆ , • : ⊥ ⊥I where ∆ = ∆ , • : ⊥. By inductive hypothesis Γ, Σ ⇒ ∆ [t/x], Θ is derivable. By applying Γ, Σ ⇒ ∆ [t/x], Θ Γ, Σ ⇒ ∆ [t/x], Θ, • : ⊥ ⊥I
we obtain a derivation of Γ, Σ ⇒ ∆[t/x], Θ, which verifies the claim. The rule ⊥E is similar.

• Γ 1 ⇒ v : B C, ∆ 1 Γ 2 ⇒ w : B, ∆ 2 Γ 1 , Γ 2 ⇒ vw : C, ∆ 1 , ∆ 2 E where ∆ = vw : C, ∆ 1 , ∆ 2 .
Suppose that x : A is contained in Γ 1 and hence that Γ 1 = Γ 1 , x : A and that Γ = Γ 1 , Γ 2 . The case in which

x : A is contained in Γ 2 is analogous. By inductive hypothesis Γ 1 , Σ ⇒ v[t/x] : B C, ∆ 1 [t/
x], Θ is derivable. Now, due to the type assignment rules of NMLL and since x : A is contained in Γ 1 , we have that x cannot occur in w. By hypothesis, t and Θ share no variable with Γ 2 , w, ∆ 2 . Hence, by applying Proof. We prove the statement by induction on the number of rule applications in the derivation of Π ⇒ t 1 : F 1 , . . . , t n : F n , t n+1 , . . . , t m .

Γ 1 , Σ ⇒ v[t/x] : B C, ∆ 1 [t/x], Θ Γ 2 ⇒ w : B, ∆ 2 Γ 1 , Σ, Γ 2 ⇒ (v[t/x])w : C, ∆ 1 [t/x],
If no rule is applied in the derivation, then Π ⇒ t 1 : F 1 , . . . , t n : F n , t n+1 , . . . , t m is of the form x : A ⇒ x : A. Since no reduction applies to any term in the right-hand side of the sequents, the claim trivially holds.

Suppose now that the statement holds for any NMLL derivation containing m or less rule applications, we show the result for a generic NMLL derivation of Π ⇒ t 1 : F 1 , . . . , t n : F n , t n+1 , . . . , t m containing m + 1 rule applications. We reason by cases on the last rule applied in this NMLL derivation.

• Γ ⇒ x. v : A B, ∆ Σ ⇒ w : A, Θ Γ, Σ ⇒ xw.v : B, ∆, Θ E where t 1 | . . . | t m = t 1 | . . . | xw.v | . . . | t m and t 1 | . . . | t m = (t 1 | . . . | v | . . . | t m )[w/x]
since x occurs only once.

-If the last rule applied above Γ ⇒

x. v : A B, ∆ is Γ, x : A ⇒ v : B, ∆ Γ ⇒ x. v : A B, ∆ I
then, by the restriction on NMLL rule applications, x occurs either in v or in ∆, and by Lemma 6.1 applied to the sequents Σ ⇒ w : A, Θ and Γ, x :

A ⇒ v : B, ∆ we obtain that Γ, Σ ⇒ v[w/x] : B, ∆[w/x],
Θ is derivable and hence that we have a derivation of Π ⇒ t 1 : F 1 , . . . , t n : F n , t n+1 , . . . , t m . -Otherwise, we have

Φ1 ⇒ x. v : A B, Ψ1 . . . Φp ⇒ Ψp Γ ⇒ x. v : A B, ∆ ρ Σ ⇒ w : A, Θ Γ, Σ ⇒ xw.v : B, ∆, Θ E
where x. v : A B only occurs in one of the premises of ρ -we display it in the first premise without loss of generality. If we construct the following derivation

Φ1 ⇒ x. v : A B, Ψ1 Σ ⇒ w : A, Θ Φ1, Σ ⇒ xw.v : B, Ψ1, Θ E . . . Φp ⇒ Ψp Γ, Σ ⇒ xw.v : B, ∆,
= Φ 1 , Σ ⇒ v[w/x] : B, Ψ 1 [w/x], Θ
By assumption we have

Γ, Σ ⇒ xw.v : B, ∆, Θ = Π ⇒ t 1 : F 1 , . . . , t n : F n , t n+1 , . . . , t m
Therefore, by inspection of the rules of NMLL, it is easy to see that by the rule application

Φ 1 , Σ ⇒ v[w/x] : B, Ψ 1 [w/x], Θ . . . Φ p ⇒ Ψ p Γ, Σ ⇒ v[w/x] : B, ∆[w/x], Θ ρ
we obtain a derivation of the sequent

Γ, Σ ⇒ v[w/x] : B, ∆[w/x], Θ = Γ, Σ ⇒ t 1 : F 1 , . . . , t n : F n , t n+1 , . . . , t m • Γ ⇒ v | w : A `B, ∆ Σ 1 , x : A ⇒ Θ 1 Σ 2 , y : B ⇒ Θ 2 Γ, Σ 1 , Σ 2 ⇒ x y (v | w) : ⊥, ∆, Θ 1 , Θ 2 `E where t 1 | . . . | t m = t 1 | . . . | x y (v | w) | . . . | t m and t 1 | . . . | t m = (t 1 | . . . | • | . . . | t m )[v/x w/y] -If the last rule applied above Γ ⇒ v | w : A `B, ∆ is Γ ⇒ v : A, w : B, ∆ Γ ⇒ v | w : A `B, ∆ `I
By the application of Lemma 6.1 to the sequents Γ ⇒ v : A, w : B, ∆ and Σ 1 , x :

A ⇒ Θ 1 we obtain that Γ, Σ 1 ⇒ w : B, ∆, Θ 1 [v/x
Φ1 ⇒ v | w : A `B, Ψ1 . . . Φp ⇒ Ψp Γ ⇒ v | w : A `B, ∆ ρ Σ1, x : A ⇒ Θ1 Σ2, y : B ⇒ Θ2 Γ, Σ ⇒ x y (v | w) : ⊥, ∆, Θ1, Θ2 `E
where v | w : A `B only occurs in one of the premises of ρ -we display it in the first premise without loss of generality.

If we construct the following derivation

Φ1 ⇒ v | w : A `B, Ψ1 Σ1, x : A ⇒ Θ1 Σ2, y : B ⇒ Θ2 Φ1, Σ ⇒ x y (v | w) : ⊥, Ψ1, Θ1, Θ2 `E . . . Φp ⇒ Ψp Γ, Σ ⇒ x y (v | w) : ⊥, ∆, Θ1, Θ2 ρ
we know without loss of generality that

x y (v | w) : ⊥, Ψ 1 , Θ 1 , Θ 2 = t 1 : F 1 , .
. . , t j : F j , t n+1 , . . . , t i and that

t 1 | . . . | t j | t n+1 | . . . | t i → t 1 | . . . | t j | t n+1 | . . . | t i
because x and y occur in Θ 1 and Θ 2 respectively. By inductive hypothesis, there is a derivation of

Φ 1 , Σ ⇒ t 1 : F 1 , . . . , t j : F j , t n+1 , . . . , t i = Φ 1 , Σ ⇒ • : ⊥, Ψ 1 , Θ 1 [v/x], Θ 2 [w/y] By assumption Γ, Σ ⇒ x y (v | w) : ⊥, ∆, Θ 1 , Θ 2 = Π ⇒ t 1 : F 1 , . . . , t n : F n , t n+1 , . . . , t m 21
Therefore, by the rule application

Φ1, Σ ⇒ • : ⊥, Ψ1, Θ1[v/x], Θ2[w/y] . . . Φp ⇒ Ψp Γ, Σ ⇒ • : ⊥, ∆, Θ1[v/x], Θ2[w/y] ρ
we have a derivation of the sequent According to the typing rules, no variable can occur in different premises of the same rule application. Therefore, both the term xw.v (respectively y z v) and the variable x (respectively y and z) occur inside the same premise of the last rule application

Γ, Σ ⇒ • : ⊥, ∆, Θ 1 [v/x], Θ 2 [w/y] = Γ, Σ ⇒ t 1 : F 1 , . . . ,
Γ ⇒ u 1 : G 1 , . . . , u p : G p . . . Φ ⇒ Ψ Σ ⇒ ∆, C 1 [u 1 ] : F j , . . . , C p [u p ] : F n ρ in the derivation of Σ ⇒ ∆, C 1 [u 1 ] : F j , . . . , C p [u p ] : F n = Π ⇒ t 1 : F 1 , . . . ,
| . . . | t m is of the form D[ C 1 [u 1 ] | . . . | C p [u p ]
] and by assumption

t 1 | . . . | t m = D[ C 1 [u 1 ] | . . . | C p [u p ] ]
Therefore, by inspection of the rules of NMLL, it is easy to see that by the application of ρ

Γ ⇒ u 1 : G 1 , . . . , u p : G p . . . Φ ⇒ Ψ Σ ⇒ ∆, C 1 [u 1 ] : F j , . . . , C p [u p ] : F n ρ
to the root of the derivation of Γ ⇒ u 1 : G 1 , . . . , u p : G p , we obtain a derivation of

Σ ⇒ ∆, C 1 [u 1 ] : F j , . . . , C p [u p ] : F n = Π ⇒ t 1 : F 1 , . . . , t n : F n , t n+1 , . . . , t m

Progress

We show now that λ `is deadlock-free: if a process contains a potential communication, then the term is not normal and the communication will be carried out. In λ `, potential communications are represented by subterms of the form xv.w or x y v. Indeed, the presence of those subterms in a process means that the process can use a communication channel x -or a pair of channels x and y -to transmit a message v. Thus we need to show that if such a subterm occurs in a term, there is also a receiver and the term is not normal. We start by showing some properties of the distribution of variables inside NMLL sequents and inside typed λ `-terms. The crucial property is that an output communication channel x can only occur if there is a corresponding input channel x.

Proposition 7.1 (Linearity of Channels). Assume Γ ⇒ ∆ is derivable in NMLL and let x be any variable. Then:

• if x occurs in Γ, x occurs exactly once in ∆ and x does not occur in ∆;

• if x does not occur in Γ but occurs in ∆, x occurs exactly once as x and exactly once as x in ∆.

Proof. By straightforward induction on the length of the derivation of Γ ⇒ ∆.

We recall that by Definition 2.4 a simple context C[ ] is a process which is not a direct parallel composition of simpler processes. A crucial property of simple contexts that we are going to obtain now is the following: if C[zu.v] is typable and C[ ] is simple, then the variable z cannot occur in C[ ]. If such a configuration were possible, we might type λ `-terms like z(zu.v) and we would have to choose between allowing components of the same process reduction to communicate z(zu.v) → uv or tolerating a deadlock. Fortunately, the next proposition rules out this scenery.

Proposition 7.2. Suppose Φ ⇒ C[u] : F, Π or Φ ⇒ C[u], Π is derivable in NMLL. Then, if C[ ] is simple and the variable z occurs in u, then z does not occur in C[ ]. • Γ ⇒ ∆ Γ ⇒ ∆, • : ⊥ ⊥I. Since C[u]
occurs in ∆, this case is ruled out by our assumption that C[u] does not occur in Γ ⇒ ∆. It is now easy to show that if a communication is possible, it will be carried out: if a typable λ `-term contains output channels ready to transmit messages, then it can always perform the communication, because there is always a suitable receiver.

• Γ ⇒ ∆, t : ⊥ Γ ⇒ ∆, close (t
• Γ ⇒ t : A `B, ∆ Σ 1 , x : A ⇒ Θ 1 Σ 2 , y : B ⇒ Θ 2 Γ, Σ 1 , Σ 2 ⇒ x y t : ⊥, ∆, Θ 1 , Θ 2 `E.
Theorem 7.3 (Progress). and so do y and y. By inspection of the inference rules of NMLL it is easy to see that x, y cannot occur in u, therefore they occur in some t i . Thus, a reduction is possible.

1. Suppose Γ ⇒ C[xv.u] : F, t 1 : F 1 , . . . , t n : F n , t n+1 , . . . ,

The Subformula Property

We show in this section that each normal λ `-term corresponds to an analytic derivation: the type of each subterm of any normal λ `-term t is either a subformula of the type of t or a subformula of the types of the variables of t. This property guarantees that, proof-theoretically, the reduction rules of λ `give rise to a complete detour removal procedure, hence we can conclude they are also satisfactory from a logical point of view. Indeed, without this property it is not possible to relate normalization and cut-elimination, as a normal proof without the subformula property cannot be translated in to a cut-free proof. NMLL can then be considered as a well-behaved alternative to sequent calculus and proof-nets for multiplicative linear logic.

We start by defining what it means for a derivation to be in normal form. We then recall the notion of stack [START_REF] Krivine | Classical realizability. Interactive models of computation and program behavior[END_REF]. A stack represents, from a logical perspective, a series of elimination rules, from a computational perspective, a series of tasks to be carried out.

Strong Normalization

It is quite immediate to see that all terms of the calculus strongly normalize. Indeed, each reduction step strictly decreases the size of the term. This is due to the linear nature of terms (Proposition 7.1): each communication or λ-reduction moves one or two terms from one location to another. Therefore, no duplication is involved in the reductions. Since, moreover, each reduction removes one binder from the term, we have that the size of the term strictly decreases. We formally show this in the following theorem. Definition 9.1 (Communication-size of a term). For any term t, its communication size cs(t) is the number of occurrences of x. and x y in t.

Theorem 9.1 (Strong normalization). For any term t such that Γ ⇒ t : F is derivable in NMLL, all sequences of terms t 1 , t 2 . . . such that t 1 = t and t i → t i+1 are finite and contain exactly cs(t) terms.

Proof. The proof is by induction on the communication-size cs(t) of t.

Confluence

We show now that each λ `-term has a unique normal form. Since all λ `-terms have a normal form, this implies that the calculus λ `is confluent: for any term t, if t → t and t → t , then there is a term t such that both t → t and t → t .

In order to simplify the proof of confluence, we define the concept of activator. Intuitively, the activator of a reduction is the term which is responsible for the reduction. For instance, to trigger a communication we only need a subterm which is ready to send a message, such as xw.v. If we do trigger this communication of w through x, the term xw.v is going to be its activator. Definition 10.1 (Activator). Given any reduction s → t, we say that the activator of s → t is the subterm of s of the form (λx v)w, xw.v, y z v, which is displayed in the corresponding reduction.

Theorem 10.1 (Uniqueness of the normal form). For any term t such that the sequent Γ ⇒ t : F is derivable in NMLL, t has only one normal form.

Proof. The proof is by induction on the length of the normalization of t.

If cs(t) = 0, the claim trivially holds. We show the claim for a generic term t such that cs(t) = m + 1, under the assumption that the claim holds for all terms with communication-size m or less.

Suppose that the term t reduces to two different terms t and t if we reduce two different redexes in t. We show that both t and t can reduce to the same term t . Since, by inductive hypothesis, t has a unique normal form and t has a unique normal form as well, this is enough to show that t has a unique normal form. Since the argument for the `-reductions is everywhere close to identical λ `and Linear Session Typed π-Calculi. An established way to interpret linear logic proofs into concurrent programs is by interpreting sequent calculi for linear logic into π-calculi with session types, see [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF][START_REF] Wadler | Propositions as sessions[END_REF][START_REF] Kokke | Better late than never: a fully-abstract semantics for classical processes[END_REF]. In those calculi, a session type is a logical expression containing information about the whole sequence of exchanges that occur between two processes along one channel. Session types are attached only to communication channels, therefore they only describe the channels' input/output behaviour, not the processes using them. In λ `, as in the tradition of the Curry-Howard correspondence, types are instead attached to processes, are read as process specifications and are employed to formally guarantee that processes will behave according to the specifications expressed by their type. In other words, while the goal of session types is to formally describe process interactions, hence the dynamics of communication, the types of λ `formally describe the result of the computation. Session types focus on how computation proceeds, the types of λ `focus on what computation accomplishes. Nevertheless, since the nature of π-calculus processes is determined by their channels' behaviour, specifying channels means also specifying processes, hence the difference with λ `is not as significant as it may appear.

A channel typed by a session type will occur in general more than once and will support several transmissions. By contrast, in λ `each output channel can only occur once and thus be used once. As our examples show, two processes of λ `can nevertheless be connected by several different channels. Therefore, in λ `there is no restriction on the number and direction of the communications between any two processes: information can be exchanged back and forth with no limitation.

Unlike in π-calculus, there is no need in λ `of a construct νx for declaring a communication channel private. Since any given channel connects exactly two processes, it already is a private link between the processes, simply because there is no other process sharing the same channel.

The typing system of λ `supports also cyclically interconnected processes, therefore λ `cannot be faithfully translated in the linearly session typed πcalculi [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF][START_REF] Wadler | Propositions as sessions[END_REF][START_REF] Kokke | Better late than never: a fully-abstract semantics for classical processes[END_REF]. At the time of this writing, we do not know any translation of the multiplicative fragments of those calculi in λ `, but also we are aware of no reason a translation should not be possible. Indeed, a referee asked whether the equivalence between the natural deduction NMLL and the sequent calculus MLL induces a translation of CP into λ `. In order to derive in λ `the CP cut-rule, based on the axiom A `A⊥ , where A ⊥ is the involutive negation of A, one needs to prove A `A⊥ in NMLL. The resulting proof requires several instances of the exclude middle B `(B ⊥), with different subformulas B of A, and thus introduces several different communication channels. This indicates that the behavior of a session type introduced in CP by the cut-rule might be simulated by several individual channels of λ `-a technique known in the literature [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF] as linearization. A practical implementation of this idea is not trivial though, because in order to express the dual A of A we need ⊗, which is not a primitive connective in λ `. It may be better to build a direct translation of CP into λ `, drawing inspiration from the translation of session types into linear types formally studied in [START_REF] Dardha | Session types revisited[END_REF].

The work in [START_REF] Paykin | A List of Successes That Can Change the World -Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday[END_REF] may help out in this direction, because it presents a translation between a version of CP (CP ± ) and a linear version of the calculus λ µ typed by classical logic. A translation between CP ± and λ `is not straightforward; obstacles like circular communication patterns generate non-trivial technical problems. Such a translation might be obtained if a linear version of λ µ could simulate λ `. But even considering the result in [START_REF] Paykin | A List of Successes That Can Change the World -Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday[END_REF], it is not obvious how to translate λ `into linear λ µ .

To summarize, the main advantages of λ `with respect to session typed πcalculi are: λ-calculus offers natively all the power of functional programming; process networks are more flexible, as processes need not always come in pairs; code mobility offers the possibility of transmitting directly code, which is sometimes less expensive than transmitting a reference and letting the receiver and the referenced code exchange information back and forth. Some disadvantages: one single channel cannot represent a logically uniform sequence of message exchanges and types do not specify communication protocols, unlike session types; the sequentiality of input-output actions must be coded in CPS style, unlike in π-calculus, where it is represented by a more linear syntax.

λ `and Typed Concurrent λ-Calculi. As consequence of adopting linear sequent calculus, the calculi of [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF][START_REF] Wadler | Propositions as sessions[END_REF][START_REF] Kokke | Better late than never: a fully-abstract semantics for classical processes[END_REF] do not directly support functional computation. Some approaches have been developed to overcome this intrinsic limitation.

The system in [START_REF] Toninho | Higher-order processes, functions, and sessions: A monadic integration[END_REF] provides some combination of session typed processes and functional programs. However, the typing system for the functional part is just added on top of the linear logic system. Therefore, there is no seamless account of both functional and concurrent computation by a single system for linear logic, which is the main accomplishment of our work.

The linear concurrent functional calculus GV in [START_REF] Wadler | Propositions as sessions[END_REF] is more similar in spirit to λ `. However, when it comes to linear logic, it displays no connection between computation and the full normalization process leading to analytic proofs. No direct reduction rules for GV are provided either. [START_REF] Lindley | A semantics for propositions as sessions[END_REF] introduce a new version GV of GV, endow it with an operational semantics and relate it to linear logic through CP. There are several differences between λ `and GV . First, GV is not based on a direct isomorphism with a logical system: several constants, like send and receive, are not typed by logical tautologies, and parallel compositions have no type. Second, each process is just a parallel composition of simply typed λ-terms, while in λ `any two processes can be composed. Hence, in GV only terms of λ-calculus, and not complex processes, can be transmitted as messages, unlike in λ `. Nevertheless, the typed λ-calculus of GV includes the fork operation, and thus it is possible to transmit terms that will eventually become parallel compositions of processes in the context of the receiver. Third, GV is limited to a call-by-value strategy while λ `reduction is not restricted to any particular strategy and reflects full cut-elimination.

The concurrent λ-calculi in [START_REF] Aschieri | Gödel logic: from natural deduction to parallel computation[END_REF][START_REF] Aschieri | Classical proofs as parallel programs[END_REF] are typed by Gödel and classical logic. They are based on extensions of intuitionistic natural deduction, thus feature full typed λ-calculus. The reduction rules are significantly more complex than those of λ `, due to the treatment that code mobility requires; strong normalization and confluence do not hold. The concurrent λ-calculus of [START_REF] Aschieri | On natural deduction in classical first-order logic: Curry-howard correspondence, strong normalization and herbrand's theorem[END_REF] is typed by first-order classical logic. It resembles a session-typed calculus, but supports only data transmission. It is strongly normalizing, but non-confluent and does not enjoy any subformula property. The calculus Lolliproc in [START_REF] Mazurak | Lolliproc: to concurrency from classical linear logic via curry-howard and control[END_REF] is a parallel interpretation of control operators, rather than a calculus for communication. The completeness of the typing system with respect to linear logic and the subformula property are not shown, which makes unclear if it actually is a legitimate proof system for the logic.

λ `and Proof-Nets. Proof-nets for multiplicative linear logic [START_REF] Girard | Linear logic[END_REF] can encode several programming languages, among them linear λ-calculus [START_REF] Girard | Proofs and Types[END_REF] and typed π-calculus [START_REF] Honda | An exact correspondence between a typed pi-calculus and polarised proof-nets[END_REF]. We believe λ `can be encoded in proof-nets as well and hence offers a new way of using proof-nets for representing functional concurrent computation. However, λ `is based on the connectives , `and normalization, while proof-nets are based on the connectives ⊗, `and cut-elimination, which makes λ `more suitable as syntax for functional concurrent programming. Indeed, λ `is a full-blown programming language right off the bat, while proof-nets were created as an elegant and economical proof system for linear logic.

λ `and Exponentials. As type system of λ `, multiplicative linear logic already features all the important characters of functional concurrent computation, and because of both its expressiveness and simplicity, it deserves to be treated as a type system on its own, as traditional in linear logic. One nontrivial problem is to extend the type system of λ `with exponentials. We do not see any real obstacles to doing that, but we leave the problem as future work. As a result, λ `may gain more duplication and replication abilities, as those of CP [START_REF] Wadler | Propositions as sessions[END_REF].

λµ and λ `: Sequentiality vs Parallelism. As far as the logical rules for implication are concerned, the type system of the original version of λµ [START_REF] Parigot | Free deduction: An analysis of "computations" in classical logic[END_REF] is exactly the non-linear version of the type system of λ `. However, λµ and λ `strongly diverge if we consider their computational behaviour. The crucial difference between λ `and λµ is that while in λµ a whole list of formulas is used to type a single term: t : A 1 , . . . , A n , in λ `each element of the list of formulas types a different term: t 1 : A 1 , . . . , t n : A n . Indeed, although the type system of λµ actually builds several terms, it does it sequentially, so the result is a unique term; instead, the type system of λ `builds several terms in parallel and let them communicate. The reason is that in λµ only one distinguished "active" formula of each list can be directly involved in an inference. Labels α, β . . . -called µ-variables -are introduced to explicitly activate a formula by the rule t : Γ ⇒ A β , ∆ µβ t : Γ ⇒ A, ∆ or deactivate it by the rule

t : Γ ⇒ A, ∆ [β]t : Γ ⇒ A β , ∆
, where Γ is a context containing declaration of λ-variables x, y, . . . and ∆ is a multiset containing formulae labeled by µ-variables α, β . . . . As we can see from the condition on the context ∆, at most one formula in each sequent can be without a label.

The history of activations and deactivations occurring in the derivation is recorded inside the corresponding λµ-term, as we can see in the following example Here the construction of w has been paused for a while and resumed with the last inference rule. Hence, v can be considered as the "real" argument of w, rather than of (µβ.u)v. As consequence, there is the reduction (µβ.u)v → µβ.u[[β](wv)/[β]w], where the argument v of µβ.u is transmitted as argument to all subterms of t with label [β].

Intuitionistic Linear Logic with `. The λ-calculus in [START_REF] Eades | Multiple conclusion linear logic: Cut elimination and more[END_REF] provides a computational interpretation of an intuitionistic linear logic with `. The typing system is a linear sequent calculus, so the corresponding λ-calculus is rather obtained by translation than by a Curry-Howard isomorphism between proofs and λ-terms. To obtain such an isomorphism, our move to natural deduction was necessary. Also, in [START_REF] Eades | Multiple conclusion linear logic: Cut elimination and more[END_REF] cut-elimination is not interpreted as communication, so the system does not support concurrency. A radical change in the treatment of linear implication was needed to recover communication and an interpretation of `as parallel operator was needed to recover parallelism, which is what we did. It is also instructive to compare `E rule to the corresponding rule in [START_REF] Eades | Multiple conclusion linear logic: Cut elimination and more[END_REF]: This rule duplicates s, compromising linearity of variables. But computation linearity is safe if we consider that s virtually occurs twice, but it will only be used once: one half of it in v, the other half in w; the two spare halves will be discarded. Since λ `is built around communication, we re-interpreted disjunction redexes as communications in order to avoid unnecessary duplication. Indeed, in the `E rule with premises Γ ⇒ s : A `B, ∆, Σ 1 , x : A ⇒ v : C, Θ 1 and Σ 2 , y : B ⇒ w : D, Θ 2 , we just let s be an autonomous term -living in parallel with all other terms in our multiple-conclusion -and establish a communication channel from s to both v and w. When s assumes the right form, we trigger a communication transmitting one half of s to v and the other half to w, as required.

Definition 2 . 1 (|

 21 Terms of λ `). The untyped terms of λ `are defined by the following grammar: u, v ::= • (terminated process) | x. u (output channel x with continuation) | x y u (output channels x, y without continuation) λx u := x. u (function definition (provided x occurs in u)) | xv.u := (x. u)v generalization of the lambda calculus, to admit concurrent computation."

  λaλb a (b prod)).y (z. •) pay : ⊥, x (y. z)(λcλa λb a (b cost c)) : String ⇒ x(λaλb a (b prod)).y (z. •) pay | x (y. z)(λcλa λb a (b cost c)) : ⊥ `String Example 3.3 (Cyclic Communication)

⇒

  z : String, z. • : String ⊥ y : String ⇒ • : ⊥, enc 2 y : String y : String ⇒ z : String, • : ⊥, z(enc 2 y).• : ⊥ ⇒ z : String, y. • : String ⊥, z(enc 2 y).• : ⊥ x : String ⇒ enc 1 x : String x : String ⇒ z : String, y(enc 1 x).• : ⊥, z(enc 2 y).• : ⊥ ⇒ x. z : String String, y(enc 1 x).• : ⊥, z(enc 2 y).• : ⊥ ⇒ M : String ⇒ xM.z : String, y(enc 1 x).• : ⊥, z(enc 2 y).• : ⊥ ⇒ xM.z | y(enc 1 x).• : String `⊥, z(enc 2 y).• : ⊥ ⇒ xM.z | y(enc 1 x).• | z(enc 2 y).• : (String `⊥) `⊥

  ) ⊥E. By our assumption, it must be the case that C[u] = close(t). If C[ ] = close([ ]), surely z does not occur in C[ ]. If C[ ] = close(D[ ]), with t = D[u], then by inductive hypothesis, z does not occur in D[ ], thus it does not occur in C[ ] = close(D[ ]) either. • Γ ⇒ t : A B, ∆ Σ ⇒ s : A, Θ Γ, Σ ⇒ ts : B, ∆, Θ E . By our assumption, it must be the case that C[u] = ts. Therefore, t = D[u] or s = D[u], with respectively C[ ] = D[ ] s and C[ ] = t D[ ]. By inductive hypothesis, z does not occur in D[ ]. Moreover, since the premises of the typing rule share no variable, z cannot occur respectively in s and t. Therefore, z does not occur in C[ ]. • Γ, x : A ⇒ t : B, ∆ Γ ⇒ x. t : A B, ∆ I . By our assumption, it must be the case that C[u] = x. t. Therefore, t = D[u] and C[ ] = x. D[ ]. By inductive hypothesis, z does not occur in D[ ]. Moreover, z = x, otherwise z would occur twice in x. t, contradicting Proposition 7.1. Therefore, z does not occur in C[ ] = x. D[ ].

  By our assumption, it must be the case that C[u] = x y t. Therefore, t = D[u] and C[ ] = x y D[ ]. By inductive hypothesis, z does not occur in D[ ]. Moreover, z = x, y, otherwise z would occur twice in x y t, contradicting Proposition 7.1. Therefore z does not occur in C[ ] = x y D[ ]. • Γ ⇒ t : A, s : B, ∆ Γ ⇒ t | s : A `B, ∆ `I. We claim that this case is not possible. Indeed, if it were, by our assumption we would have C[u] = t | s. Therefore t = D[u] or s = D[u], with respectively C[ ] = D[ ] | s and C[ ] = t | D[ ]. Since by Definition 2.4 the context C[ ] would not be simple, we would have a contradiction.

w

  : A → B, ∆ [β]w : (A → B) β , ∆ . . . . u : (A → B) β , ∆ µβ.u : A → B, ∆ v : A, Σ (µβ.u) v : B, ∆, Σ

Γ

  ⇒ s : A `B, ∆ Σ1, x : A ⇒ v : C, Θ1 Σ2, y : B ⇒ w : D, Θ2 Γ, Σ1, Σ2 ⇒ let s be(A `-)in v : C, let s be(-`B)in w : D, ∆, Θ1, Θ1 `E2

  4.1 The Call-by-Value λ Àlthoughλ `is naturally asynchronous, we can model synchronous and blocking actions also in λ `, by defining reduction to automatically follow a call-by-value discipline.Definition 4.2 (Call-by-value Contexts). We define a call-by-value evaluation context by the following grammar:

	Definition 4.1 (Value). A value is any term of one of the following forms:
	x. t	s | t

  The proof of the Subject Reduction is now quite standard. Theorem 6.2 (Subject Reduction). Assume there is a NMLL derivation of Π ⇒ t 1 : F 1 , . . . , t n : F n , t n+1 , . . . , t m . If t 1 | . . . | t m → t 1 | . . . | t m , then there is a derivation of Π ⇒ t 1 : F 1 , . . . , t n : F n , t n+1 , . . . , t m .

				Θ, ∆ 2	E
		we obtain a derivation of Γ, Σ ⇒ (vw)[t/x] : C, ∆[t/x], Θ, which verifies
		the claim.
	•	Γ, y : B ⇒ s : C, ∆ Γ ⇒ y. s : B C, ∆	I where ∆ = y. s : B	C, ∆ . Since x : A must

occur in Γ in the conclusion of the rule application, we know that x = y. By inductive hypothesis, Γ, y :

B, Σ ⇒ s[t/x] : C, ∆ [t/x],

Θ is derivable. Hence, since by hypothesis y does not occur in t, by applying Γ, y : B, Σ ⇒ s[t/x] : C, ∆ [t/x], Θ Γ, Σ ⇒ y. (s[t/x]) : B C, ∆ [t/x], Θ I we obtain a derivation of Γ, Σ ⇒ (y. s)[t/x] : B C, ∆ [t/x], Θ, which verifies the claim.

• The cases `E and `I are similar.

  t n : F n , t n+1 , . . . , t m • In all other cases, the term xw.v (or x y v) that triggered the reduction t 1 | . . . | t m → t 1 | . . . | t m already occurs in the premises of the last rule ρ applied in the NMLL derivation of Π ⇒ t 1 : F 1 , . . . , t n : F n , t n+1 , . . . , t m .

  t m is derivable in NMLL. Then the term C[xv.u] | t 1 | . . . | t m is not normal. 2. Suppose Γ ⇒ C[x y u] : F, t 1 : F 1 , . . . , t n : F n , t n+1 , . . . , t m is derivable in NMLL. Then the term C[x y u] | t 1 | . . . | t m is not normal. Proof. 1. By Proposition 7.1, x and x must occur exactly once in the term C[xv.u] | t 1 | . . . | t m . If x occurs in some t i , then a reduction is possible and we are done. We assume therefore that x occurs in C[xv.u]. We also assume C[ ] is empty, otherwise x occurs in u, hence xv.u = (λx u)v, which is not normal and we are done. We claim now that C[xv.u] has a subterm of the form E[xv.u] | D[x] or D[x] | E[xv.u], which implies a communication reduction is possible, allowing us to conclude the proof. We prove our claim by induction on C[xv.u]. If C[xv.u] = z. C [xv.u] or C[xv.u] = y z C [xv.u] or C[xv.u] = close(C [xv.u]), then we apply the induction hypothesis on C [xv.u], and we are done. If C[xv.u] = w C [xv.u] or C[xv.u] = C [xv.u] w, then by Proposition 7.2, x must occur in C [xv.u], hence we apply the induction hypothesis on C [xv.u], and we are done. If C[xv.u] = C [xv.u] | w or C[xv.u] = w | C [xv.u], then if x occurs in w, we are done. Otherwise, we apply the induction hypothesis on C [xv.u], and concluding the proof of the claim. 2. By Proposition 7.1, x and x must occur both exactly once in the term C[x y u] | t 1 | . . . | t m

  Definition 8.1 (Normal form). An NMLL derivation of a sequent Γ ⇒ t 1 : T 1 , . . . , t n : T n , t n+1 , . . . , t m is in normal form if the term t 1 | . . . | t m is in normal form.

According to Milner[START_REF] Milner | Lectures on a calculus for communicating systems[END_REF], "CCS is an attempt to provide a paradigm for concurrent computation. It arose after several unsuccessful attempts by the author to finds a satisfactory

x : A ⇒ x : A Γ, x : A ⇒ t : B, ∆ Γ ⇒ λx t : A B, ∆ I ( if x occurs in t) Γ, x : A ⇒ t : B, ∆ Γ ⇒ x. t : A B, ∆ I ( if x occurs in ∆) Γ ⇒ s : A B, ∆ Σ ⇒ t : A, Θ Γ, Σ ⇒ st : B, ∆, Θ E Γ ⇒ ∆ Γ ⇒ ∆, • : ⊥ ⊥I Γ ⇒ t : ⊥, ∆ Γ ⇒ close(t), ∆ ⊥E

Proof. We prove the statement by induction on the number of rule applications in the derivation of Φ⇒ C[u] : F, Π or Φ ⇒ C[u], Π. If C[ ] is empty, we are done. If no rule is applied in the derivation, then Φ ⇒ C[u] : F, Π or Φ ⇒ C[u], Π is of the form x : A ⇒ x : A, thus u = x and C[ ]is empty, therefore the claim trivially holds.Suppose now that the statement holds for any NMLL derivation containing m or less rule applications, we show the result for a generic NMLL derivation containing m + 1 rule applications. We reason by cases on the last rule applied in this NMLL derivation. We may assume that the term C[u] does not occur in any premise of this last rule, otherwise we just apply the inductive hypothesis to any premise containing C[u] and obtain the thesis.

* Funded by FWF project P32080-N31. † Funded by ANR JCJC project Intuitions Bolzaniennes.

 Definition 8.2 (Stack). A stack is a possibly empty sequence σ = ξ 1 ξ 2 . . . ξ n such that for every 1 ≤ i ≤ n, ξ i = t, with t term of NMLL. If t is a proof term, t σ denotes as usual the term (((t ξ 1 ) ξ 2 ) . . . ξ n ).

Before proving the Subformula Property, we need to establish two auxiliary results concerning the shape of terms. The first of these two results guarantees that the expected connection between the shape of a term with its type holds. Proposition 8.1 (Type coherence). If Γ ⇒ t : F, ∆ is derivable in NMLL and t is a value, then either t = x. t and F = A B or t = s | t and F = A `B, for some types A and B.

Proof. By induction on the number of rule applications in the derivation of Γ ⇒ t : F, ∆.

The second auxiliary result establishes that any normal λ `-term -the type of which is not ⊥ -is either a value or a sequence of operations that cannot be carried out.

Lemma 8.2 (The shape of normal terms). If there is a derivation in NMLL of Γ ⇒ u : F, Π, where u is in normal form, is not a value and F = ⊥, then u = yσ.

Proof. By induction on the number of rule applications in the derivation of Γ ⇒ u : F, Π.

We can now show that normal λ `-terms satisfy the Subformula Property. The proof is by induction on the size of the NMLL derivation and, as usual, the difficult case is the one involving implication elimination. Even though we handle this case by a standard argument on the type of sequences of eliminations, represented here by stacks, the multiple-conclusion setting forces us to integrate this argument in the main induction. We do so by using a stronger inductive statement that carries along the induction the required statement about the type of stacks. Theorem 8.3 (Subformula Property). Consider any normal NMLL derivation P of the sequent x 1 : X 1 , . . . , x m : X m ⇒ t 1 : T 1 , . . . , t n : T n , Π, where Π does not contain any type. Then every type S occurring in P is a subformula of some type T 1 , . . . , T n or X 1 , . . . , X m or ⊥.

Proof. We prove a stronger statement: Consider any normal NMLL derivation P of the sequent x 1 : X 1 , . . . , x m : X m ⇒ t 1 : T 1 , . . . , t n : T n , Π, where Π does not contain any type. Then every type S occurring in P is a subformula of some type T 1 , . . . , T n or X 1 , . . . , X m or ⊥. Moreover, if a term t i with i ∈ {1, . . . , n} is of the form yσ where σ is a stack, then T i is a subformula of some type T 1 , . . . , T i-1 , T i+1 , . . . , T n or X 1 , . . . , X m or ⊥.

The proof is by induction on the number of rule applications in P.

to the argument for -reductions, we only present the latter. Let us denote then the reduction t → t as

There are two main cases. 1. If one of the activators of t → t and t → t is a subterm of the other, we consider the outermost activator. Without loss of generality, we assume that the outermost is the activator of t → t . Now, the activator yr.s of t → t is either a subterm of v or of w.

• The activator of t → t is a subterm of v. The reduction t → t is then of the form

where v is obtained from v by replacing yr.s with s. Since, by Proposition 7.2, y does not occur in w, we have t → t , with

We just need to show that t → t , that is

By Proposition 7.1 we have that y = x. Now, if r contains x,

If r does not contain x and since y does not occur in w, we have

• The activator of t → t is a subterm of w. The reduction t → t is then of the form

where w is obtained from w by replacing yr.s with s. We have t → t , with

We just need to show that t → t , that is

We have the following reduction:

Now, r does not contain x, by Proposition 7.2 and because the activator of t → t occurs in w. Since, moreover, y = x, we also have

and therefore that t → t .

2. If neither of the activators of t → t and t → t is a subterm of the other, the reduction t → t is of the form

where u i and C [ ] are either equal to, respectively, u i and C[ ] or obtained from u i and C[ ], respectively, by replacing the activator yr.s of t → t with s. We have t → t , with

We just need to show that t → t , that is

Now, if s is the activator of a reduction, also s[w/x] has the suitable shape to be one; and the relative reductions substitute the same variable. By Definition 2.3, moreover, y = x and hence y occurs in the term (

and we can reduce it as follows:

We must now consider several cases, depending upon x and y occur in the messages w and r.

-If x occurs in r, but y does not occur in w, then, by Proposition 7. -Finally, we show it cannot be that both x occurs in r and y occurs in w. Indeed, suppose, for the sake of contradiction, that they do. By letting the term yr.s transmit its message r, we would have