Emmanuel Beffara

Proofs as executions

1 Introduction

The extension of the familiar Curry-Howard correspondence to interactive models of computation has been an active research topic for several decades. Several systems were proposed based on linear logic [START_REF] Girard | Linear logic[END_REF], following the fundamental observation that it is a logic of interaction. Interpretations of proofs as processes, first formalized by Abramsky [START_REF] Abramsky | Proofs as processes[END_REF], later refined by various people including the first author [START_REF] Beffara | A concurrent model for linear logic[END_REF], stressed that proof nets [START_REF] Girard | Proof-nets : the parallel syntax for proof theory[END_REF] and process calculi have significant similarities in dynamics. At the same time, type systems for concurrency [START_REF] Yoshida | Strong normalisation in the π-calculus[END_REF] revealed to be equivalent to variants of linear logic [START_REF] Honda | An exact correspondence between a typed π-calculus and polarised proof-nets[END_REF][START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]. These approaches successfully stress the fact that concurrent calculi are very expressive and versatile models of interactive behaviour, however they are not satisfactory yet as a prooftheoretical account of concurrency, because they tend to impose determinism in execution, effectively constraining processes to functional behaviour. Several approaches to the question of non-determinism in logic have been proposed. The use of the additive connectives of linear logic as a proof-theoretic representation of it was for instance explored by Mairson and Terui [START_REF] Mairson | On the computational complexity of cut-elimination in linear logic[END_REF] to provide a notion of non-deterministic cut-elimination, or by Maurel [START_REF] Maurel | Nondeterministic light logics and NP time[END_REF] or the second author [START_REF] Mogbil | Non-deterministic boolean proof nets[END_REF] who used it to represent the kind of non-determinism familiar in complexity theory. In a different style, differential logic was recently developed by Ehrhard and Regnier [START_REF] Ehrhard | Differential interaction nets[END_REF] and its untyped proof formalism was shown expressive enough to represent the π-calculus [START_REF] Ehrhard | Interpreting a finitary π-calculus in differential interaction nets[END_REF].

The present work proposes a different approach to the topic, by questioning the "proofs-as-programs" paradigm. Proof theory wants cut elimination to be confluent, because the meaning of proofs lies in their normal forms. On the other hand, reduction in process calculi is execution: the meaning of a term is not its final irreducible form but what happens to get there, as interaction with other processes. Hence we propose to match proofs with executions rather than terms. But this raises the new question of what is the logical meaning of an execution.

Here we must remember that cut elimination is a process of explicitation and cut-free proofs are explicit, direct reasonings justifying some fact. In our case, the fact is the interaction, which is a scheduling of a set of events in a system. The justification, then, is the control flow through the system, specifying when actions happen and when execution jumps from one process to another.

Technically, we illustrate this idea in the very simple setting of finitary CCS with no choice operator, in order to focus on the novel ideas of our approach, but ways to extend these techniques to a larger class of processes are sketched in the perspectives. The corresponding logic is multiplicative linear logic, with a family of modalities à la Hennessy-Milner [START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF] representing actions.

In our type system, multiplicatives represent causality and independence between parts of a run, using connectedness/acyclicity arguments to describe avoidance of deadlocks. Modalities represent observable transitions, with explicit scheduling constraints using the well-known stratifying effect of boxes in proof nets. Axiom rules have an unusual interpretation: they are void of interactive content (no forwarding or copycat behaviour), but they logically implement the transfer of control flow between different parts of a running process.

This handling of control flow using the symmetries of linear logic is reminiscent of the work of Mazurak and Zdancewicz [START_REF] Mazurak | Lolliproc: to concurrency from classical linear logic via curry-howard and control[END_REF] who use linear negation as an explicit scheduling operation. Our work differs from theirs and other works on typing for concurrency, in that we proceed "backwards": while Curry-Howard systems for concurrency embed logical systems into concurrent calculi, we embed executions of processes into a logical system. Outline The paper is organized as follows: Section 2 introduces a logic of schedulings based on linear logic and illustrates our interpretation. Section 3 defines a simple fragment of CCS and a notion of determinisation, used to represent executions as terms. Section 4 presents the proof nets for the logic of schedulings and its cut-elimination. Section 5 shows the typing of executions and the associated subject reduction property, and Section 6 establishes the completeness property that all lock-avoiding executions are typable.

A logic of schedulings

We first present the logic we use to describe interactions and schedulings. It corresponds to the multiplicative fragment of linear logic [START_REF] Girard | Linear logic[END_REF], augmented with a family of modalities that describe actions.

P Γ, A, B P Γ, A `B (`) P Γ, A Q B, ∆ P | Q Γ, A B, ∆ (⊗) P Γ, A Q A ⊥ , ∆ P | Q Γ, ∆ (cut) 1 A, A ⊥ (ax) P Γ, A a.P Γ, a A (act) P Γ a / ∈ Γ (νa)P Γ (new)
Derived rules:

         P : Γ, A B P : Γ A B ( R) P : Γ A Q : ∆, B C P | Q : Γ, ∆, A B C ( L) P : Γ A B Q : ∆ A P | Q : Γ, ∆ B (mp) P : Γ, A B a.P : Γ, ā A B (act)
= α | α ⊥ | A B | A `B | a A | a A
where the α are literals and the a are CCS names. The negation A ⊥ of a nonliteral formula A is defined by de Morgan duality as

(A B) ⊥ = A ⊥ `B⊥ and ( a A) ⊥ = a A ⊥ . A type (Γ, ∆ . . .)
is a finite multiset of formulas. Derivations are built from the rules of table 1, where the left side of is a CCS term up to structural congruence (as of section 3). The same rule (act) applies for names of both polarities. In (new), a ∈ Γ means that neither a nor a occurs in Γ .

Although it is formulated as a type system for processes, this logic should be interpreted as a calculus for building schedulings. To explain this interpretation, we adopt a few notations that stress the functional aspect of the system: P : A 1 , . . . , A n B represents the judgement P A ⊥ 1 , . . . , A ⊥ n , B and the binary connective A B stands for A ⊥ `B. We easily get the derived rules of table 1: ( R) and ( L) are respectively a reformulation of (`) and (⊗), and (mp) is modus ponens for linear implication, obtained with (ax), (⊗) and (cut). This is an intuitionistic or implicative formulation, but we do need the full expressiveness of the MLL a for the developments of the following sections.

A formula specifies a way for a process to interact with its environment and a proof provides a way to justify this interaction. A judgement P : A 1 , . . . , A n B then denotes a function that combines n interactions of types A i for independent processes Q i into an interaction of type B of the process

Q 1 | • • • | Q n | P .
-A modality a A means doing the action a and then acting according to A.

To lighten notations, we will represent successive modalities as a single one:

abc α means a b c α. -Implication A
B is an interaction that provides a behaviour B expecting A from the environment, as made explicit by the rule (mp). The rule ( R) means that some context may actually be provided by the environment.

-An variable α is a behaviour not known from the considered term. An interaction of type α means jumping to a continuation of type α, necessarily provided by the context: indeed, since a scheduling of this type may not provide any behaviour, it effectively gives control to some other process.

As we will formalize later on, the term P on the left side of a judgement is guaranteed to be able to provide the behaviour computed by the proof, and this behaviour will consume all the actions of P . Reciprocally, all the behaviours that consume all actions of P correspond to some proof.

Let us illustrate this by examining the possible ways of typing a term like a.b.1 | c.1. This term has three possible ways of interacting: each interleaving of the sequence (a, b) with the sequence (c) is a valid trace. A simple interleaving is the sequential execution of one part followed by the other, as (a, b, c). E.g. The other crucial point is the introduction of a in front of b.1, as the succession of rules (ax), ( L), (act), ( R). The conclusion type reads as "if using b α the environment can do C, then, by combining with it, a.b.1 can do a then C". Operationally, a.b.1 starts by doing a, then jumps to C (the behaviour of the environment), and at some point the environment will give control back from C (that is the negative occurrence of C) and b.1 will then perform b α. This part is generic in C: we could use the same reasoning for any type C, including a type variable γ. In a more concise way, (B γ) a γ is an interruptible version of the modality a B. Similarly, the typing of c.1 is generic in B. We only need to choose B and C appropriately for the (mp) rule, so that types unify properly.

Another aspect is when parallel composition is typed by a cut which means that a synchronisation (send/receive) happens between the composed processes:

with δ = α ε = α
Here the conclusion type is a simple interaction with the environment. This term has different proofs providing the same type, e.g. using a intermediate trace for e.1|d.ē.1 instead of d.ē.1| d.1 as in the proof above. Such variants are irrelevant in scheduling and will be removed by switching to proof nets in the next sections.

CCS runs as pairings

We consider processes of the standard language CCS [START_REF] Milner | Communication and concurrency[END_REF]. The general language is defined by the following grammar. Note that we use 1 for the inactive process instead of the usual 0 because it is the neutral element of | which is a multiplicative operation. Moreover, actions a are decorated by locations :

P, Q ::= a .P | ā .P | 1 | (P | Q) | P + Q | * P | (νa)P
where a is taken from an infinite set N of names and is taken from an infinite set L of locations. Each location is used at most once in any term. The main source of non-determinism is the fact that a given action name may occur several times in a given term, and locations are used to name the different occurrences.

For the purpose of the present study, we actually restrict to the following fragment. The reason for this will be explained in the following development.

Definition 2 (MCCS).

Multiplicative CCS is the fragment of CCS using neither choice (+) nor replication ( * ). Structural congruence is the smallest congruence ≡ that makes parallel composition associative commutative and 1 neutral.

The set of locations occurring in P is written L(P ). Given ∈ L(P ), the subject of is the name tagged by , written subj P . The polarity of is that of the action tagged by its subject, written pol P , element of {±1}. Intuitively, a negative action ā represents the sending of a signal on a channel a, and a positive action a represents the reception of such a signal. Definition 3 (execution). Execution is the relation over structural congruence classes, labelled by partial involutions over L, defined by the rule

ā .P | a m .Q | R → {( ,m)} ex P | Q | R
Let → ex * be the reflexive transitive closure of → ex , with the annotations defined as P → ∅ ex * P and if P → c ex * Q → d ex * R then P → c∪d ex * R. The annotation c in P → c ex Q describes which occurrences interact in the execution step, we write P → ex Q if c is unimportant. Similarly, we keep locations implicit when they do not matter. Remark that, for a given P and c, there is at most one Q such that P → c ex Q, since c describes the interaction completely.

Definition 4 (pairing). A pairing of a term P is a partial involution c over L(P ) such that for all ∈ dom c, subj c( ) = subj and pol c( ) =pol . Let ∼ c be the smallest equivalence that contains c. Let ≤ P be the partial order over L(P ) such that < P m for every subterm x .Q of P with m ∈ L(Q). c is consistent if dom c is downward closed for ≤ P and ∼ c < P ∼ c is acyclic. [START_REF] Beffara | A concurrent model for linear logic[END_REF][START_REF] De Naurois | Correctness of linear logic proof structures is NL-complete[END_REF], [START_REF] Beffara | Concurrent nets: a study of prefixing in process calculi[END_REF][START_REF] Ehrhard | Differential interaction nets[END_REF], (4, 7)}, c 2 = {(3, 5), [START_REF] Abramsky | Proofs as processes[END_REF][START_REF] Caires | Session types as intuitionistic linear propositions[END_REF], [START_REF] Beffara | A concurrent model for linear logic[END_REF][START_REF] De Naurois | Correctness of linear logic proof structures is NL-complete[END_REF], (7, 0), (9, 8)}, c 3 = {(1, 4), [START_REF] Beffara | Concurrent nets: a study of prefixing in process calculi[END_REF][START_REF] Ehrhard | Differential interaction nets[END_REF], (7, 0), [START_REF] Girard | Linear logic[END_REF][START_REF] Danos | The structure of multiplicatives[END_REF], [START_REF] Beffara | A concurrent model for linear logic[END_REF][START_REF] De Naurois | Correctness of linear logic proof structures is NL-complete[END_REF]}, c 4 = {(1, 0), [START_REF] Beffara | Concurrent nets: a study of prefixing in process calculi[END_REF][START_REF] Danos | The structure of multiplicatives[END_REF], [START_REF] Ehrhard | Interpreting a finitary π-calculus in differential interaction nets[END_REF][START_REF] Caires | Session types as intuitionistic linear propositions[END_REF], [START_REF] Girard | Linear logic[END_REF][START_REF] Ehrhard | Differential interaction nets[END_REF], [START_REF] Beffara | A concurrent model for linear logic[END_REF][START_REF] De Naurois | Correctness of linear logic proof structures is NL-complete[END_REF]}. Only c 1 is inconsistent as there is a cycle induced by {(3, 8), (4, 7)}. The maximal consistent pairing included in c 1 is {(9, 5), (1, 0), (2, 6)}.

Observe that pairings and consistency are preserved by structural congruence, as a direct consequence of the fact that subjects, polarities and prefixing are preserved by structural congruence. Proposition 1. A pairing c of a term P is consistent if and only if there is a term Q such that P → c ex * Q. Proof (sketch). In an execution P 0 → c1 ex P 1 → c2 ex • • • → cn ex P n , the c i are disjoint, so their union is a pairing, and consistency is ensured by the fact that executions respect prefixing. Conversely, write c = c 1 • • • c n with the c i atomic. By definition, if c is consistent then ≤ P induces a partial order over the domains of the c i . Assume that the considered enumeration respects this order, then we can prove by recurrence that there is an execution sequence

P = P 0 → c1 ex P 1 • • • → cn ex
P n , since each c i joins two actions of P i-1 that are minimal for ≤ Pi-1 .

We easily get the following (for proof see appendix B.1).

Proposition 2. Let P be a term. Any two executions P → c ex * Q and P → c ex * R with the same pairing are permutations of each other, and in this case Q ≡ R.

We will thus consider consistent pairings as the proper notion of execution for CCS terms. Maximal consistent pairings represent executions of processes until a state where no more execution is possible.

A useful tool in the study of pairings is the following notion of determinisation, by which we can turn a pairing of a term into a term that has no other pairing. In other words, determinisation is a way to represent a run of a term in the language of MCCS itself.

Definition 5 (deterministic term). A term P is deterministic if it has at most one occurrence of each action.

The pairings of a deterministic term form a lattice, consistent pairings too, so there is a unique maximal consistent pairing for any deterministic term.

The restriction operator (νa) serves two purposes: it limits the scope of a name, and it makes it possible to have names local to each copy of a subterm in the presence of replication; both these features are useless in the deterministic case, hence we leave it out on determinisation. We abide by Barendregt's convention that each bound channel is named distinctly from each other channel. Definition 6 (determinisation). Assume an injective map δ : N × {±1} × L → N . Given a partial involution c, determinisation along c is the operator ∂ c which commutes with parallel composition such that ∂ c ((νa)P ) = ∂ c (P ) and

∂ c a .P = δ(a, +1, ) .∂ c (P ) , ∂ c ā .P = δ(a, +1, ) .∂ c (P ) if ∈ dom c, δ(a, -1, ) .∂ c (P ) otherwise.
By construction, ∂ c (P ) is deterministic, the pairings of ∂ c (P ) are the restrictions of c, consistency preserved, so c is the unique maximal pairing of ∂ c (P ).

Example 2. For the term P and the pairings of example 1, we obtain the following determinisations (with δ(a, +1, 7) = d and δ(b, +1, 9) = e):

c 3 = {(1, 4), (3, 8), (7, 0), (9, 5), (2, 6)} induces ∂ c3 (P ) = a.c | b.ā | ē.c | d. b | e | d, c 4 = {(1, 0), (3, 5), (7, 4), (9, 8), (2, 6)} induces ∂ c4 (P ) = a.c | b. d | b.c | d.ē | e | ā.
If we extended our study to the whole of CCS, determinisations would still be in MCCS, but the theory of pairings would have to be refined: external choice requires a notion of conflict in the space of locations (as in event structures [START_REF] Winskel | Event structures[END_REF]), replications requires the introduction of indices to distinguish copies.

Proof nets for MLL with action modalities

Proofs in sequent calculus are well suited to inductive reasoning, however their use in proof theory is uneasy because their rigid structure obscures many arguments, like those below in particular. For this reason, we will turn to proof nets, using the standard machinery of linear logic [START_REF] Girard | Proof-nets : the parallel syntax for proof theory[END_REF][START_REF] Danos | The structure of multiplicatives[END_REF]. Modality rules are represented using boxes (like promotions in standard linear logic, but with different typing rules). The only extra information we add to standard proof structures is the location of each box, to reflect the use of locations in CCS terms in the sequel. For readers not familiar with the standard definitions of proof structures and proof nets, these are put in appendix. We detail here specificities of MLL a .

Definition 7 (proof structure). A proof structure consists of an ordered forest of nodes labelled by formulas, denoted x A , with a set Ax of axiom links (pairs of leaves), a set Cut of cuts (pairs of roots) and a set Box of modality boxes, labelled by action modalities, such that each box β has a unique location (β). The roots that are not part of a cut are called the conclusion nodes. The conclusion type is the multiset of the labels of the conclusion nodes.

A modality box β is a set of nodes (the ports) associated to a proof structure S whose conclusions are in bijection with the ports. If the modality of β is a , then the principal port is labelled a A and matches a conclusion of S labelled A, while auxiliary ports have the same label as their matching conclusion in S.

The graphical notation of proof structures is presented in figure 1. By definition there are arcs only to multiplicative nodes, moreover proof structures can be drawn considering the top-bottom orientation of arcs, so we keep arc orientation implicit by this convention. Arcs to a `node are joint by a circle on the side of this node. By construction, the conclusion labels suffice to deduce all labels, so we keep most of this information implicit.

Definition 8 (proof net).

A proof net is a proof structure built following MLL a sequent calculus rules. An immediate subnet of a proof net π is an induced subgraph of π that is itself a proof net. A subnet of π is either an immediate subnet of π or (inductively) a subnet of a box of π.

Well known correctness criteria [START_REF] Danos | The structure of multiplicatives[END_REF][START_REF] Girard | Proof-nets : the parallel syntax for proof theory[END_REF][START_REF] De Naurois | Correctness of linear logic proof structures is NL-complete[END_REF] apply to characterise proof nets among proof structures by combinatorial means like acyclicity and connectedness.

Definition 9 (cut elimination). Annotated cut elimination is the relation → c

ce over proof structures, labelled by partial involutions c over L, that is the reflexive transitive closure of the rules below (such that if π → c ce π → d ce π then π → c∪d ce π ). We have π → c ce π if π contains a cut κ = {x, y} either at top level or inside a box and one of the following cases occurs:

-Multiplicative step and Axiom step: standard definition, with c = ∅. -Modality step: If x and y are principal ports of two boxes β, β , then c permutes (β) and (β ) and π is obtained by replacing each box with its associated proof structure. -Commutation step: If x is the auxiliary port of a box β, then c = ∅, and the cut and a subnet of π that contains y are moved inside β.

Our proof system enjoys a standard cut-elimination theorem using this definition: if π → c ce π and π is a proof net, then π is a proof net with the same conclusion (this is proved by standard arguments using correctness criteria, hence we will not develop this point); if a proof π is irreducible by → ce , then it has no cut link (this is an immediate case analysis). Note however that → ce is not confluent, because of commutation steps.

Definition 10 (head reduction). Head reduction is the annotated relation → c

h over proof structures defined as the restriction of → c ce that only applies at top level and does not use the commutation step of cut elimination. This particular strategy is relevant because it does not reduce inside boxes, that is under prefixes, it only affects cuts in active position (from the point of view of processes). However, this strategy does not eliminate all cuts in general.

In the analysis of proofs, the following notion of path will be useful. It describes a way to traverse arcs and axioms/cuts in a proof structure while respecting the logical meaning of formulas.

Definition 11 (path).

A path in a proof structure S is an alternating path in the underlying graph of S, such that alternations occur only at axioms, cuts and boxes. Each move between ports x and y of a box β must be associated with a path between the corresponding conclusions in β. We further require a typing constraint: a path can only move up a left (resp. right) branch if has moved down a left (resp. right) branch before, with a natural well-bracketing condition.

For instance, a path starting from an axiom with type α may move down the tree of nodes, reach a cut, move up the other side of the cut, always in the branches that contain α, reach an axiom, and so on.

Typing executions of MCCS terms

Proofs in MLL a will serve as a type system. Although this can be formulated in usual sequent style (as in table 1), the natural notion rather relates proof nets and structural congruence classes of terms.

Definition 12 (term assignment). Let S be a proof structure. The MCCS term S assigned to π is the parallel composition of the β for each box β in S. In turn, for a box β with location and associated structure S β , the term β is a . S β if the principal port of β has modality a and ā . S β if the principal port of β has modality a . A term P is said to have type Γ if there is a proof net π of conclusion Γ such that π ≡ P . In this case we write π : P Γ .

A proof net is a proof structure that is built using the rules of table 1, ignoring the terms on the left of the symbols. It is obvious that these terms do reflect the definition of term assignment: A term P has type Γ if and only if there is a type derivation with conclusion P Γ using the rules of table 1.

We now establish the correspondence between cut elimination in a proof and execution steps in the assigned terms. The first result justifies head reduction: Proposition 3. Let π be a proof structure. For every head reduction π → c h π there is an execution π → c ex * π . Proof (sketch). Axiom and multiplicative cut elimination steps do not affect the assigned terms, besides their annotation is empty, so the result holds immediately for them. When a modality step applies, it reduces a cut between boxes with dual modalities (because of typing), hence the associated terms are ready to interact; the reduct is easily seen to be the assigned term of the reduct proof. Subject reduction does not hold in general. Indeed, a given proof may hold several occurrences of a given modality, corresponding to different occurrences of an action in the term, and the structure of cuts may not match a given execution step. This is not a defect, since we actually intend to type pairings rather than processes: we do get subject reduction if we restrict to proofs that describe deterministic terms.

Definition 13 (linear proof ). A proof structure S is called linear if -S contains at most one box for each modality, for each a, all occurrences of a A in the labels in S have the same immediate subformula A, and if a A and a B occur then A and B are dual, if S contains a box for both a A and a A ⊥ , then neither formula occurs in the conclusion type of S.

The essence of the linearity condition is the first constraint. Intuitively, the second and third constraints serve to guarantee that the property is preserved by composition. Indeed, if a formula a A occurs in the conclusion of a proof π, then the proof may be cut against a proof that contains a modality box for a A ⊥ , which breaks linearity if π already contains a box for some a B. Note that the fact of being a linear proof is preserved by cut elimination.

Theorem 1 (subject reduction). Let π be a linear proof of conclusion P Γ . For every execution P → c ex * P there is a linear proof π : P Γ .

Proof (sketch). An execution step π → ( ,m) ex P involves immediate subterms a .Q and ām .R for a ∈ N . Then π contains two top level boxes with respective principal ports x a A and y a A ⊥ , for A ∈ M LL a . Since π is linear, x and y are elimination boxes for each other, ending a path ρ (as of definition 11) whose axioms contain modalities of x and y in their types. Let π be the rewriting of π where such modalities are removed (boxes are replaced by their contents, axioms on a A by axioms on A). Clearly π is a linear proof of conclusion P Γ .

This theorem states that types are preserved by execution in deterministic terms. However, the proof uses a rewriting of the typing proofs that does not correspond to cut elimination in general. Indeed, consider the following example of typing, call π the l.h.s.: We can get a precise correspondence between execution and head cut elimination by imposing an additional constraint on the shape of proofs. In the statement below, an axiom is immediately contained in a box if it is an immediate subnet of the structure associated with this box. Definition 14 (regular proof ). An axiom link immediately contained in a box β is anchored if there is a path from one of its conclusions to an auxiliary port of β and a path from its other conclusion to the principal port. A proof structure π is regular if all its axioms are anchored and for every pair of boxes with dual modalities, one of the boxes does not immediately contain any axiom.

Theorem 2 (strong subject reduction). Let π be a regular linear proof net. For every execution π → c ex * P there is a regular linear proof π such that π → c h π and π = P .

Proof (sketch). Consider an execution step π → ( ,m) ex P . As in the proof of theorem 1, linearity implies that there are boxes at top level and a path ρ between their principal ports x a A and y a A ⊥ for immediate subterms a .Q and ām .R of π . Since x is cut at top level, ρ traverses no box, otherwise linearity or regularity would be contradicted. Then ρ is a multiplicative cut path whose cut elimination → ∅ h until x and y preserves π as well as regularity and linearity.

Anti-execution and completeness

In this section we establish our correspondence theorem relating typings and executions. To achieve this goal we first provide a kind of reciprocal statement for subject reduction: if a term T can reduce into a typed term T , then we can type T with a proof that reduces to the typing of T . Because we want logically correct proof structures, this operation requires some care. We now describe a general method for deducing a typing by "anti-execution" of a proof. We stay at a partly informal level for clarity, all formal statements are detailed in appendix B.3.

Consider a generic execution step

P | a.Q | ā.R → ex P | Q | R.
Assume the reduct is typed by some proof π. We want to put the parts of π that correspond to Q and R into boxes, with a cut between them, while rewriting the proof to avoid cycles. For this purpose, we proceed in four steps:

Selection consists in moving each box belonging to Q or R away from the main proof, by means of an axiom/cut pair, so that Q and R are represented by simple sets of boxes, cut with the main proof (which corresponds to P ), with no multiplicative connectives:

→

Chaining consists in introducing an extra axiom/cut pair in the middle of each cut between P and R, so that there are cuts only between P and Q or Q and R, and not between P and R directly:

R Q P → P Q R
Simplification consists in making sure that there is actually exactly one cut between P and Q and one between Q and R, by multiplexing multiple cuts through multiplicatives:

→

Correctness criteria guarantee that we can always find two cuts for which there is one connected component on one side, two on the other. Boxing consists in putting Q and R into boxes, cut together, so that Q has one auxiliary port to P and R has no auxiliary port:

→

Following this method, we prove the following statement:

Proposition 4 (anti-execution). Let T 1 → c ex T 2 be an execution step and let π 2 : T 2 Γ be a typing. There exists a typing π 1 : Lemma 1 (preserved regularity). In the construction of proposition 4, if π 2 is regular, then so is π 1 . If π 2 is linear and T 2 is deterministic, then π 1 is linear.

T 1 Γ such that π 1 → c h π 2 .
Proof (sketch). Let T 2 = P | Q | R.
If an axiom is introduced by anti-execution rewrite steps, used in proposition 4 then: i) it is added to P by selection and it will not be boxed, or ii) it is added to Q by chaining and becomes anchored by simplification and boxing. No axiom is introduced on the side of R, Q only contains chaining axioms, so regularity is satisfied for the new axioms. Besides, regularity is not broken for axioms previously present in the proof. Example 6. In the previous example 5, one can also start execution by (b, b)(a, ā) as seen in the typing. All execution permutation of ∂ c4 (P ) in the pairing c 4 is allowed by the typing proof synthesized from the execution e.

We now summarize the previous results, about subject reduction and the reverse operation, into a precise statement relating typings and execution.

Lemma 2 (initial typing). Every linear MCCS term where no name occurs with both modalities is typable by a cut-free regular proof.

Proof. We simply build a proof of T A T , B T with A T non-modal by induction on T . For T = 1, use the axiom rule to get 1 α ⊥ , α. For T = P | Q, deduce T A P `AQ , B P B Q by the tensor rule. For T = a.P , deduce T A P , a B P by the action rule, similarly for ā.P . The proof thus built is obviously regular since every axiom is at top level or anchored, and there are no pairs of boxes with dual modalities. Theorem 3 (completeness). For every execution P → c ex * Q there are typings π P : P Γ and π Q : Q Γ such that π P → c h π Q . Moreover, for every execution sequence

P → c1 ex P 1 • • • → cn ex P n = Q with c 1 ∪ • • • ∪ c n = c, there is a cut elimination sequence π P → c1 h π 1 • • • → cn h π n = π Q
, with π i = P i for all i. Proof. By definition, the term ∂ c (Q) is linear and has no dual actions, so by lemma 2 we can find a cut-free regular proof π Q : ∂ c (Q)

Γ . If we apply proposition 4 repeatedly to π Q with the steps of the considered execution ∂ c (P ) → c ex * ∂ c (Q), we get a proof π P : ∂ c (P ) Γ that reduces to π Q by a head reduction sequence labelled c. Let π P and π Q be the relabellings of π P and π Q by the inverse of ∂ c , then we have π P : P Γ , π Q : Q Γ and π P → c h π Q . Every execution sequence of P with label c is an execution sequence of ∂ c (P ) with the same label. By lemma 1, π P enjoys strong subject reduction as of theorem 2, hence every run of ∂ c (P ) labelled by c corresponds to a head reduction sequence in π P labelled by c. By relabelling with ∂ -1 c , every run of P labelled by c corresponds to a head reduction sequence π P → c h π Q . In other words, every execution of a term can be exactly characterized up to permutation by typing, in the sense that the execution sequences of the term within the same pairing will be exactly the head reduction sequences of the associated typing proof. By combining determinisation (definition 6) and strong subject reduction (theorem 2) we get that, conversely, each regular typing of a term defines a set of executions stable by permutation.

In this work we have developed, in the simple framework of multiplicative CCS, a precise logical description of executions of processes. A key technical tool is the use of pairings, by which we separate non-determinism in communication from the multiplicity of equivalent schedulings; this technique extends well to more expressive frameworks (full CCS, π-calculus, etc.). The logical interpretation we propose moves beyond the traditional Curry-Howard for concurrency by accepting non-deterministic terms, albeit with a change of interpretation in the correspondence. Indeed, the logic we use is well studied and has a wide range of existing tools (efficient correctness criteria, proof search, etc.) but its interpretation in our paradigm of proof-as-executions is new.

Logical expressiveness

The restriction to purely multiplicative objects, in MCCS and MLL, lets us concentrate on the precise role of multiplicatives and axioms as descriptions of how a process interacts with its environment, but it hides the complexity inherent to the other defining features of concurrent systems like choice, recursion, name passing, etc. It should be stressed that extending the calculus or the logic are two different things.

On the one hand, extending the calculus enriches the set of possible executions, by introducing more subtle synchronization possibilities: choice allows for conflict between actions, replication allows for arbitrarily large runs with some uniformity, value passing allows for communication of ground values, name passing allows the set of synchronizable pairs to evolve along execution. After determinisation, all these features essentially disappear and deterministic runs can still be formulated in MCCS. On the other hand, enriching the logic leads to richer descriptions of the control flow in processes, for instance using a first order language with predicates to describe properties of continuations. Furthermore, new connectives allow a given type to correspond to more distinct executions.

These two kinds of extensions are not independent, however, since each feature of the calculus can be usefully described using a feature of the logic. Let us illustrate this in the case of choice and additives. The technique of pairings still works, consistency simply needs to take into account a notion of conflict as in event structures [START_REF] Winskel | Event structures[END_REF]. The type system is naturally extended by additive rules:

P Γ, A Q Γ, B P + Q Γ, A & B P Γ, A P Γ, A B
possibly with the restriction that A and B are modal. A type A&B for a behavior means either behaving as A or as B, according to what the environment provides, while A B means behaving as A or B depending on one's own choice.

With this we can type useful processes that use choice. For instance, describe a boolean on names t, f as some process that will send a signal on one of the channels t, f . This can be materialized by the type B(t, f ) := α ⊥ , t α f α which reads like "give me control (using α), I will terminate by a signal on t or f ". Then consider a negation function: N := t. f + f. t . By studying its interactions with the environments E 1 := t | f and E 2 := f | t , we see that both the N | E i have complete consistent pairings, hence we can type them as α ⊥ , α. Extracting the types of N we get t α ⊥ , f α and f α ⊥ , t α, which we combine by additives into a unique type t α ⊥ & f α ⊥ , t α f α. This way we get a possible specification for N .

Causality A crucial feature of our work is the interpretation of axioms as a way to transfer causality. An effect is that, most of the time, the type of a term will contain modalities for actions that it does not contain by itself. For instance, a.

b may have type a c α ⊥ , b c α, which can be read "give me a signal on a with the promise of a signal on c, and I will answer with a signal on b and the promise of a signal c". This makes it explicit that this part of interaction will be involved in the triggering of interaction on c, but only indirectly by allowing bearers of c to get active. This idea suggests new ways of analyzing causality in interactive systems, and the fact that the flow of causality is often as complicated as the flow of information. Besides, a similar fact is illustrated by the expressiveness of solos [START_REF] Laneve | Solos in concert[END_REF][START_REF] Beffara | Concurrent nets: a study of prefixing in process calculi[END_REF], where communication is used to carry all prefixing information in processes. Our interpretation may provide a logical insight on this matter.

A MLL a and restricted type system

A.1 MLL with action modalities Proof structures of MLL a are formally defined as follows:

-The forest is seen as an acyclic graph (V S , E S ) oriented from leaves to roots, with a total order on the ingoing arcs of each node. -We write v A to signify that vertex v has label A. We impose that if a vertex v A is not a leaf, then it has two children x B and y C (in this order) and either A = B C or A = B `C; the main connective of A is the sort of v. -Axioms are pairwise disjoint pairs of leaves labelled by dual formulas.

-Cuts are disjoint pairs of roots labelled by dual formulas.

-Boxes are disjoint non-empty sets of leaves, -Ax ∪ Box forms a partition of the set of leaves.

-Each box β has a distinguished element called its principal port, the others are auxiliary ports. Each box is associated (inductively) to a proof structure S β with a bijection φ from the elements of β to the conclusions of S β .

• For the principal port x A of β we have A = a B or A = a B where B is the label of φ(x); • for each other element y of β, the labels of y and φ(y) are the same.

To each box β we also associate a location (β), with the constraint that each location is used at most once in any given structure.

The roots that are not part of a cut are called the conclusion nodes of S. The conclusion type of S is the multiset of the labels of its conclusion nodes.

Proof nets (PN) are formally defined as follows:

(ax):

({u A ax , v A ⊥ ax }, {uv}, ∅, ∅, {u, v}) is a PN. (`): If G = (V, E, A, P, C) is a PN and u A , v B are two conclusions of G, then (V {w A`B `}, E, A ∪ {uw, vw}, P ∪ {{uw, vw}}, C \ {u, v} ∪ {w}) is a PN. (⊗): If G = (V, E, A, P, C) and G = (V , E , A , P , C ) are disjoint PNs, u A is a conclusion of G and v B is a conclusion of G , then (V V {w A B }, E E , A A {uw, vw}, P P , (C \ {u}) (C \ {v}) {w}) is a PN. (act): If G = (V, E, A, P, C) is a PN with conclusions set C = {u A , v B1 1 , . . . , v B k k }, then ({x a A a (G), y B1 1 , . . . , y B k k }, {uv 1 , . . . , uv k }, ∅, ∅, {u, v 1 , . . . , v k }) is a PN. Also when changing a A by a A. (cut): If G = (V, E, A, P, C) and G = (V , E , A , P , C ) are disjoint PNs, u A is a conclusion of G and v A ⊥ is a conclusion of G , then (V V , E E ∪ {uv}, A A , P P , (C \ {u}) (C \ {v})) is a PN.
Cut elimination in MLL a is formally defined as follows. Let π and π be a proof structure and c be a partial involution on L. Annotated cut elimination is the relation → c ce over proof structures, labelled by partial involutions c over L, that is the reflexive transitive closure of the rules below (such that if π → c ce π → d ce π then π → c∪d ce π ). We have π → c ce π if π contains a cut κ = {x, y} either at top level or inside a box and one of the following cases occurs (note that x and y may be freely exchanged):

Axiom and cut rules (A is a literal α or a MLLaformula):

1 A o , A ⊥ (ax) P Γ, A o Q A ⊥ , ∆ P | Q Γ, ∆ (cut)
Multiplicative rules:

P Γ, A p , B p P Γ, (A `B) p (`) P Γ, A p Q B p , ∆ P | Q Γ, (A B) p , ∆ (⊗)
Modality and New rules: The restriction to anchored proofs may be designed with a restriction of our type system as in Table 2. The idea is to enforce in each box an orientation from auxiliary ports to principal port, for axioms on modalities. We simply use a decoration on formulas when needed. The letters p, q, . . . indicate the o decoration (output) or no decoration. The sequence of formulas Γ γ is a sequence of formulas decorated with letters. Proof. First remark that, by definition of execution, we have L(P ) = L(Q) dom c, besides dom d ⊂ L(Q) so the domains of c and d are disjoint. We can thus define the involution c = c ∪ d, and check that it is indeed a pairing of P .

P Γ, A o a .P Γ γ , ( a A) p (act) P Γ a / ∈ Γ (νa)P Γ (new)

B Detailed proofs

Let ∈ dom c . If ∈ dom c then is the location of an action involved in the execution step, so subj P c( ) = subj P and pol P c( ) =pol P by definition of execution, and subsequently the property holds for c . Otherwise is in the domain of d, then the same property holds for d in Q since d is a pairing of Q, and again we get it for c in P . Hence c is a pairing of P . Now suppose d that is consistent but c is not. Write ≺ c P m if there is a location n such that < P n ∼ c m. Then there exists a cycle 0 ≺ c P 1

≺ c P • • • ≺ c P k = 0 .
If all the i are in Q then this cycle exists in ≺ d Q , which cannot be since d is consistent. Since c annotates a reduction of P , all elements of dom c are minimal for ≤ P , so the cycle cannot consist only of elements of dom c. So we may assume 0 ∈ L(Q) and 1 ∈ dom c. This means either 0 < P 1 or 0 < P c( 1 ), in each case this implies that some location in dom c is prefixed in P , which is impossible. Hence c is consistent.

Proof (proposition 1). By iterating lemma 3, from an execution

P 0 → c1 ex P 1 → c2 ex • • • → cn ex P n we can deduce a pairing c = c 1 ∪ • • • ∪ c n of P 0 .
This pairing represents the execution above, because it contains all the choices made during this execution. Indeed we can prove that executions that yield the same pairing are equivalent. The converse is detailed in the main text.

P 1 • • • → c σ(n) ex
P n . We now prove that the final terms P n and P n are equal up to structural congruence. Call d(σ) the number of pairs (i, j) such that i < j and σ(i) > σ(j). We proceed by induction on d(σ). If this number is 0, then σ is the identity function and the sequences match, so obviously we have P n ≡ P n . Otherwise, consider a minimal i such that σ(i) = i, hence σ -1 (i) = i and σ -1 (i) > i, and let j = σ -1 (i) -1. The reduction sequences match in their first i -1 steps, then one has a reduction labelled c i while the other has a reduction labelled c σ(i) . By repeated applications of lemma 4, we can deduce that for each k ≥ i there is a term

Q k such that P k → ci ex Q k and Q k-1 → c σ(k) ex Q k if k > i: P i c σ(i) ci+1 / / • • • P i-1 ci < < c σ(i) ! ! Q i c σ(i+1) / / • • • c σ(j-1) / / Q j-1 c σ(j) / / Q j P i ci ? ? c σ(i+1) / / • • • ci = = c σ(j-1)
/ / P j-1 ci ; ;

c σ(j) / / P j ci ; ;

c σ(j+1)
/ / P j+1 Moreover, by construction c σ(j+1) = c i , so P j+1 ≡ Q j , because there is at most one possible reduction for a given annotation. Hence we can deduce a pair of reduction steps

P j-1 → c σ(j+1) ex Q j-1 → c σ(j) ex P j+1
. This yields a new reduction sequence from P 0 to P n that corresponds to a new permutation σ of the sequence (c i ), and σ is σ where σ(j) and σ(j + 1) are swapped. By definition of j we have σ(j) > σ(j + 1) so σ (j) < σ (j + 1). For any a ∈ {j, j + 1} we have σ(a) < σ(j) if and only if σ (a) < σ (j + 1), and the same exchanging j and j + 1, so we have d(σ ) = d(σ) -1, and we can conclude by induction hypothesis.

B.2 Typing

Proof (proposition 3). Clearly we can deduce the general result from the case of each individual rule. Cut elimination steps for multiplicatives and axioms do not affect the nesting of boxes, which is the only part of proofs used in term assignment, so for each such step π → ∅ h π we have π = π , hence π → ∅ ex * π by reflexivity. For an elimination step for modalities, we have π → ( ,m) h π where and m are the locations of two boxes β and β . By definition there is a cut between their principal ports x and y, so these ports must have dual types a A and a A ⊥ . Call π 1 and π 2 the proofs associated to β and β , then we have β = a . π 1 and β = ām . π 2 . Moreover, there is a term P such that π = β | β | P so we have π → ( ,m) ex π 1 | π 2 | P , and the latter is equal to π by definition of the cut elimination step for modalities.

Proof (subject reduction theorem 1). Consider an execution step π → ( ,m) ex P . This step involves immediate subterms a .Q and ām .R for some name a, hence π must contain a box at top level with principal port x a A and one with principal port y a A ⊥ , for some formula A. Since π is linear, a A and a A ⊥ do not occur in the conclusion type, so they are cut. Since π is linear, no other boxes introducing these modalities can be in π. So x and y are elimination boxes for each other, and there is a path (as of definition 11) ρ from x to y in π. Remark that ends of ρ are modality rules on a A and a A ⊥ whereas all axioms along ρ contain these modalities in their types. Let π be the rewriting of π where such modalities are removed by rewriting axioms on a A/ a A ⊥ in axioms on A/A ⊥ , and by rewriting the end boxes by their contents. Clearly π is a linear proof that infers P .

Proof (strong subject reduction theorem 2). Consider an execution step π → ( ,m) ex P . This step involves immediate subterms a .Q and ām .R for some name a, hence π must contain a box at top level with principal port x a A and one with principal port y a A ⊥ , for some formula A. Since π is linear, a A and a A ⊥ do not occur in the conclusion type, so they are cut. Since π is linear, no other boxes introducing these modalities can be in π. So x and y are elimination boxes for each other, and there is a path (as of definition 11) ρ from x to y in π. For simplification we consider that boxes are replaced by their associated proof net keeping the information of auxiliary and principal ports (this is more like sequent calculus derivations).

Since x is at top level and cut, suppose that along ρ we get through a box β from x. By duality it is only with axioms on modality formulas a A/ a A ⊥ . Moreover by typing rules going inside β can only be done through an auxiliary port. Since π is regular, ρ go out from β through its principal port. By typing rules it is not possible to reach y without encountering before a principal port of a box eliminating β. Moreover this is only possible using an axiom on modality formulas a A/ a A ⊥ in this box. Remark that since π is regular and β has axioms on modalities, corresponding elimination box is simple. Then to use an axiom on modalities contradict that π is regular. Then there is no box traversal along ρ. Then by typing ρ is a multiplicative cut path whose cut elimination → ∅ h until x and y preserves π as well as regularity and linearity of proof.

B.3 Anti-execution by division of proof nets

Definition 15. A 3-partition of a set X is a triple (P, Q, R) of pairwise disjoint, possibly empty subsets of X such that P ∪ Q ∪ R = X. Definition 16. A division of a proof net π is a 3-partition (P, Q, R) of the set of nodes of π such that the subgraph π P of π induced by P (resp. Q, R) is a disjoint union of immediate subnets of π. The division is called proper if P, Q, R are not empty. It is called simple if π P , π Q , π R are immediate subnets of π.

Remark that, because each component must be a proof net, each node in a component must have its ancestors in the same component, so the only edges of π that are not part π P ∪ π Q ∪ π R must be cut edges.

Let (P, Q, R) be a division of a proof net π, let π be a reduct of π by some cut elimination step. Call P , Q , R the restrictions of P, Q, R to the node set of π . If (P , Q , R ) is a division of π , then we say that (P, Q, R) reduces to (P , Q , R ).

Lemma 5 (selection). Let (B P , B Q , B R ) be a 3-partition of the set of boxes of a proof net π. There is a division (P, Q, R) of a proof net π that reduces to π by axiom steps such that Q (resp. R ) contains exactly the boxes B Q (resp. B R ).

Proof. For each box β ∈ B Q ∪ B R , for each auxiliary port x A ∈ β, we introduce two new leaves y A ⊥ , z A , a cut {x, y} and an axiom {y, z}, and we turn any outgoing edge of x into an outgoing edge of z. Call π the resulting proof net.

→

Let Q be the set of auxiliary ports of boxes in B Q , R be the set of auxiliary ports of boxes in B R , and let P be the set of all other nodes. Each box in B Q ∪ B R is obviously a subnet of π , moreover P induces a subnet of π , so (P, Q, R) is a division of π with the expected properties.

Lemma 6 (chaining). Let (P, Q, R) be a division of a proof net π. There exists a proper division (P , Q , R ) of a proof net π , with no cut between π P and π R , that reduces to (P, Q, R) by axiom steps.

Proof. Since π is a proof net, it must have at least one conclusion node x A . If some set among P, Q, R is empty (say Q), extend π by adding an axiom on two fresh nodes {y A ⊥ , z A } and a cut {x, y}, and put y and z into Q. This way we get a proper division. Now, for each cut {x A , y A ⊥ } with x ∈ P and y ∈ R, introduce a fresh axiom {u A ⊥ , v A }, put u and v in Q, then remove the cut {x, y} and introduce two new cuts {x, u} and {v, y}. This way we make sure there is no cut between P and R.

R Q

P → P Q R
The only operation we have done here is introducing axiom/cut pairs on existing cut links or conclusions, so the resulting structure is a proof net that reduces to the original one by axiom steps, only removing the newly created nodes.

Lemma 7 (simplification). Let (P, Q, R) be a proper division of a proof net π with no cut between π P and π R . There is a simple division (P , Q , R ) of a proof net π that reduces to (P, Q, R) by multiplicative steps.

Proof. Since π is a proof net, it must be connected, so there are cuts between π P and π Q and between π Q and π R . We rewrite π to make sure that in each case there is exactly one cut. Suppose there are two cuts {x, x } and {y, y } between π P and π Q , with x, y ∈ P and x , y ∈ Q. If x and y are in the same connected component of π P , then x and y must be in two distinct components of π Q (because of acyclicity of π), so we can replace the two considered cuts by a cut on a new pair of nodes x `y and x y , which we put in P and Q respectively:

→

Otherwise x and y are not in the same connected component of π P , so x and y must be in the same component of π Q (because of connectedness of π), so this case is symmetric. By construction, the resulting proof net π reduces to π by multiplicative reduction and it has one less cut between π P and π Q . Iterating this method, we can make sure that there is exactly one cut between π P and π Q , and also between π Q and π R . Subsequently, π P , π Q , π R are immediate subnets of π , since they must be acyclic and connected.

Proof (proposition 4). Let { , m} be the domain of c. There is a name a such that T 1 ≡ (P |a .Q|ā m .R) → c ex (P |Q|R) ≡ T 2 , and by hypothesis π 2 = T 2 . Let (B P , B Q , B R ) be the 3-partition of the set of boxes of π 2 such that B P contains the boxes assigned to the actions in P , and similarly for Q and R.

By lemma 5 there is a division (p, q, r) a proof π that reduces to π 2 by axiom steps and such that q (resp. r) exactly contains the boxes B Q (resp. B R ). By lemma 6 there is a proper division (p , q , r ) of a proof π that reduces to (p, q, r) by axiom steps, and with no cut between π p and π r . By lemma 7 there is a simple division (p , q , r ) of a proof π that reduces to (p , q , r ) by multiplicative steps. Then (p , q , r ) reduces by multiplicative and axiom steps to π 2 and all the boxes contained in π p are the ones B P , and similarly for Q and R. Moreover there is no cut between π p and π r and one cut κ = {x A , y A ⊥ } between π q and π r .

We define π 1 as the proof net π as follows. The subnet π q is replaced by a box β q with location , with π q as contents, with x as its principal port and one auxiliary port for each conclusion of π q other than x. The subnet π r is replaced in the same way, with location m. The cut κ is retyped as {x a A , y a A ⊥ }. This is depicted as follows.

→

By construction there is a cut elimination step π 1 → c h π , besides we have π → ∅ h π 2 , so we get the expected reduction.

( 2 1

 2 rapport interne LIPN -Mai 2012) * Emmanuel Beffara 1 and Virgile Mogbil IML -FRE3529, CNRS -Université d'Aix-Marseille 2 LIPN -UMR7030, CNRS -Université Paris 13

  a.b.1 | c.d.1 : α abc α (cut) with C = c α. The important point is the choice of the axiom on C: it stands for the fact the a.b.1 finally hands control to c.1 for which we have type C.The interleaving (a, c, b) is more subtle: now c.1 will have to get control from a.b.1 after a and give back control to it after doing c. We can write this as 1 Again, the choice of the right types for the axioms is crucial because it depends on the continuation in interaction. Indeed, we have three steps (a, c, b) and as many types for continuations: cb α, b α and α.

e. 1 |

 1 d.ē.1 | d.1 : α α (cut)

Example 1 .

 1 The total pairings of P = a 1 .c 2 | b 3 .ā 4 | b5 .c 6 | a 7 . b8 | b 9 | ā0 are c 1 = {(9, 5), (1, 0),

Fig. 1 .

 1 Fig. 1. Representation of proof structures: axiom link, `node, node, boxes, cut.

Example 3 .

 3 Let π be the following proof net. have π = a.c | b.ā | ē.c | d. b | e | d. (It is ∂ c3 (P ) of previous examples). As it is deterministic term, we abusively identify locations with names. We consider the head reduction sequence π → z h π (where π is an axiom link) for z = {(d, d), (b, b), (a, ā), (e, ē), (c, c)}. We have π → z ex * π ≡ 1.

b

  Then the proof is linear, irreducible by head cut elimination, but the assigned term π = ā | b | a does execute into b. In π, this involves a cut on the axiom inside the middle box. As done in theorem 1 the rewriting of π in a linear proof π assigned to b is the r.h.s..

Example 4 .

 4 Consider the term P := a. b | b.c | ā.c. We cannot type each thread with a simple type like a α, b α ⊥ and then introduce a cut for each interaction, since we would get a cyclic proof structure, what is incorrect.

Example 5 .

 5 Consider the term of P of example 1. We consider the execution e = (a, ā)(b, b)(c, c)(d, d)(e, ē) of the determinized term ∂ c4 (P ) = a.c|b. d| b.c|d.ē|e| ā for the (total and consistent) pairing c 4 = {(1, 0),[START_REF] Beffara | Concurrent nets: a study of prefixing in process calculi[END_REF][START_REF] Danos | The structure of multiplicatives[END_REF],[START_REF] Ehrhard | Interpreting a finitary π-calculus in differential interaction nets[END_REF][START_REF] Caires | Session types as intuitionistic linear propositions[END_REF],[START_REF] Girard | Linear logic[END_REF][START_REF] Ehrhard | Differential interaction nets[END_REF], (2, 6)}. A typing synthesized by the construction of proposition 4 is the following.

⊥ 2 .

 2 Then c = ∅ and π is obtained by removing κ and the nodes x and y and adding the cuts {x 1 , y 1 } and {x 2 , y 2 }. -Axiom step: If y is a leaf node and it is part of an axiom α = {y, z} with x = z, then c = ∅ and π is obtained removing α, κ, y and z and rewriting any outgoing arc of z into an outgoing arc of x. -Modality step: If x and y are principal ports of two boxes β, β , then c permutes (β) and (β ) and π is obtained by replacing each box with its associated proof structure, identifying the conclusions of this structure with the ports of the box. -Commutation step: If x is the auxiliary port of a box β, call T the smallest subnet of π that contains y. Then c = ∅ and π is obtained by moving T and κ inside β, replacing the auxiliary port x by one auxiliary port for each conclusion of T .A.2 MLL a p , a restriction of MLL a

B. 1

 1 Runs and pairings Lemma 3. Let P → c ex Q be an execution and d be a pairing of Q, then dom c ∩ dom d = ∅ and c ∪ d is a pairing of P . If d is consistent, then so is c ∪ d.

Lemma 4 .

 4 Let P → c1 ex Q 1 and P → c2 ex Q 2 be two executions with dom c 1 ∩ dom c 2 = ∅. Then there is a unique R such thatQ 1 → c2 ex R and Q 2 → c1 ex R.Proof. By the existence of the execution step P → c1 ex Q 1 , we know that P can be written P ≡ ā .S |a m .T |P for some name a and with dom c 1 = { , m}. Similarly, the term P can be decomposed as P ≡ b .S | b m .T | P for some name b and with dom c 2 = { , m } to justify the execution step P → c2 ex Q 2 . By hypothesis the domains of c 1 and c 2 are disjoint, so and m are distinct from and m . As a consequence the term P can be decomposed as P ≡ ā .S |a m .T | b .S |b m .T |P and the terms Q 1 and Q 2 have execution steps with the expected annotations, with the common reduct R = S | T | S | T | P . Unicity of R up to structural congruence is a consequence of the fact the c 1 and c 2 completely describe which subterms of P, Q 1 , Q 2 interact and in which way. Proof (proposition 2). The pairing c is the disjoint union of the atomic involutions of each step, so clearly the execution sequences are permutations of each other. Write them as P = P 0 → c1 ex P 1 • • • → cn ex P n and P = P 0 → c σ(1) ex

Table 1 .

 1 Inference rules for MLL with action modalities (MLLa)

Definition 1 (MLL a ). The formulas of MLL a are built by the grammar A, B ::

Table 2 .

 2 Inference rules in MLLa p -Multiplicative step: If x and y have respective sorts and `, then each has two premises, call them respectively x A 1 , x B 2 , y A ⊥ 1 , y B

* Work partially supported by the french project Complice (ANR-08-BLANC-0211-01)