Ugo Dal Lago
email: ugo.dallago@unibo.it

Damiano Mazza
email: damiano.mazza@lipn.univ-paris13.fr

Intersection Types and Runtime Errors in the Pi-Calculus

Keywords: CCS Concepts:, Theory of computation → Process calculi, Linear logic, Type structures, intersection types, π -calculus, runtime error analysis, linear logic

We introduce a type system for the π -calculus which is designed to guarantee that typable processes are well-behaved, namely they never produce a run-time error and, even if they may diverge, there is always a chance for them to łfinish their workž, i.e., to reduce to an idle process. The introduced type system is based on non-idempotent intersections, and is thus very powerful as for the class of processes it can capture. Indeed, despite the fact that the underlying property is Π 0 2 -complete, there is a way to show that the system is complete, i.e., that any well-behaved process is typable, although for obvious reasons infinitely many derivations need to be considered.

INTRODUCTION

The concept of a type system has been a useful abstraction in the theory and practice of programming languages, since the very early days [START_REF] Backus | Revised report on the algorithmic languageAlgol 60[END_REF]. Types are assigned to code fragments including variables, subroutines, and dynamic allocated objects, and their purpose is to guarantee a form of safety, i.e., that łwell-typed programs cannot go wrongž [START_REF] Milner | A theory of type polymorphism in programming[END_REF]], or even more complex properties, e.g., that well-typed program terminate without going wrong [START_REF] Hughes | Proving the Correctness of Reactive Systems Using Sized Types[END_REF]. Noticeably, the converse is not necessarily true: there can well be programs satisfying the prescribed property which are not typable. But the guarantee provided by types is anyway very valuable, particularly when the behavior of subprograms within programs turns out to be complex, like for so-called higher-order functions: in those scenarios, keeping track of who does what is even more crucial to prevent run-time errors. Indeed, type systems for higher-order programming languages are among the best studied topics in the programming language and logic in computer science communities. A host of different type systems exist, and forms of polymorphic [START_REF] Girard | Une extension de l'interpretation de Gödel a l'analyse, et son application a l'élimination des coupures dans l'analyse et la théorie des types[END_REF][START_REF] Reynolds | Towards a Theory of Type Structure[END_REF], refinement [START_REF] Freeman | Refinement Types for ML[END_REF], sized [START_REF] Hughes | Proving the Correctness of Reactive Systems Using Sized Types[END_REF], or dependent types (to mention only a few) have been applied to a variety of programming languages. There is always a tension between expressiveness and tractability here: the more expressive the type system is, the more computationally expensive type checking and type inference are bound to be, because the underlying program properties are invariably undecidable. From simple types, where type inference has polytime complexity, one can go all the way to System F, for which the same problem is well-known to be undecidable [START_REF] Wells | Typability and Type-Checking in the Second-Order lambda-Calculus are Equivalent and Undecidable[END_REF]], through ML-style type systems, in which inference is EXPTIME-complete [Kanellakis et al. 1994].

Logic and programming language semantics can help in studying the intrinsic limits of the type-based approach, by providing some guidelines as for how to design elegant type systems, or by exploring the intrinsic limits of the approach. A particularly relevant example is given by intersection types [START_REF] Coppo | A new type assignment for λ-terms[END_REF], in which various normalization properties of λ-terms can be precisely characterized by typability (see for instance [START_REF] Krivine | Lambda-calculus, types and models[END_REF]] for the standard examples: head normalization, weak normalization, strong normalization).

But what happens if one switches to concurrent calculi and process algebras? Type systems guaranteeing safety properties of processes have been studied for a long time now, with remarkable results coming out in the last twenty years. For example, quite robust and expressive type systems guaranteeing deadlock freedom of π -processes can be given [START_REF] Suenaga | Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts[END_REF]. As another example, session types [START_REF] Honda | Language Primitives and Type Discipline for Structured Communication-Based Programming[END_REF]] have had quite an impact in the way concurrent programs and processes can be structured. Finally, termination of processes is another area in which much progress can be observed in the last fifteen years [Demangeon et al. 2010a,b;[START_REF] Yoshida | Strong normalisation in the pi-calculus[END_REF]]. More information on related work can be found in Section 1.1.

Despite the very strong expressive power of the obtained type methodologies, not much is known about the limits of the type-based approach in a concurrency scenario, contrarily to what one observes in the realm of sequential languages. Is there any type system able not only to guarantee but also to characterize some relevant property of concurrent processes, like deadlock-freedom, liveness, or termination? In the literature, some attempts in this direction can be found, but none of them gives a definite answer. Giving a satisfactory answer to the question above is, we believe, a key step in understanding the deep nature of the aforementioned properties, which are universally accepted to be desirable in concurrent systems.

In this paper, we show that, indeed, an intersection type discipline may be given for a fragment of the π -calculus, and proved sound and complete for checking, in essence, a form of deadlock-freedom and termination for processes, which we dub good behavior. This is the first such result, as far as the authors know.

The route to the result is full of caveats, however. First of all, one needs to clarify that the intrinsic non-determinism of π -calculus processes prevents us from hoping to have such a type system, at least if one sticks to the usual scheme in which one type derivation is sufficient as a certificate for the given property. Indeed, the class of well-behaved processes turns out to be a Π 0 2 -complete set, which by definition cannot be characterized by a finitary, recursively checkable, type system. This admittedly not surprising result will be proved formally in Sect. 2.4 below.

Related Work

Intersection types have been introduced by Coppo and Dezani [START_REF] Coppo | A new type assignment for λ-terms[END_REF] as a generalization of simple types for ordinary λ-terms inspired by semantics. After their introduction, it became clear quite soon that intersection types could be used to characterize notions like that of a weakly normalizing [START_REF] Coppo | Functional Characters of Solvable Terms[END_REF] or that of strongly normalizing λ-terms [START_REF] Coppo | An extension of the basic functionality theory for the λ-calculus[END_REF]. By changing the properties satisfied by the intersection type operator, one can also turn intersection types into a way to read the complexity of normalization of a λ-term (i.e. the number of β-steps to normal form along a strategy) from one of its type derivations [START_REF] Accattoli | Tight typings and split bounds[END_REF][START_REF] Daniel De | Execution time of λ-terms via denotational semantics and intersection types[END_REF]. The same paradigm has been recently shown to be applicable to other kinds of λ-calculi, like probabilistic λ-calculi [START_REF] Breuvart | On Intersection Types and Probabilistic Lambda Calculi[END_REF].

Intersection type systems for π -calculus processes have already been proposed in the literature, e.g., by [START_REF] Castagna | Encoding CDuce in the Cpi-Calculus[END_REF]] and by Piccolo [START_REF] Piccolo | Strong Normalization in the π -calculus with Intersection and Union Types[END_REF]]. In both of the cited papers, intersections are mixed with unions. But neither in one nor in the other, one can hope to have any completeness result. Moreover, intersection is used in an unusual way, namely for typing non-deterministic choices. In our work, intersections deal with the exponentials rather than the additives.

As already mentioned, many type systems for process algebras have been introduced in the last two decades. A cornerstone in the normalization theory for π -calculus is the work by Berger, Honda and Yoshida [START_REF] Yoshida | Strong normalisation in the pi-calculus[END_REF], in which a combination of logical and process-theoretical ideas led to a robust approach, capable of guaranteeing strong normalization for all typable processes.

Another rather prolific research line is centered around linearity in the sense of Girard's linear logic [START_REF] Girard | Linear Logic[END_REF]], and has been initiated by the seminal work of Kobayashi, Pierce and Turner [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF]]. This has been followed by many type systems, based or not on linearity, guaranteeing forms of deadlock-freedom [START_REF] Kobayashi | A New Type System for Deadlock-Free Processes[END_REF][START_REF] Padovani | Deadlock and lock freedom in the linear π -calculus[END_REF], livelockfreedom [START_REF] Kobayashi | Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness[END_REF]], termination [Demangeon et al. 2010b;[START_REF] Deng | Towards an Algebraic Theory of Typed Mobile Processes[END_REF], or combinations thereof. Again, none of them aim at the kind of completeness property we are interested at here.

A very successful typing paradigm for concurrent processes is certainly the one of session types [START_REF] Honda | Language Primitives and Type Discipline for Structured Communication-Based Programming[END_REF]]. There, the inherently chaotic nature of concurrent interaction is tamed by way of the notion of a session, which is a tree-like description of the possible interactions happening between the (possibly multiple [START_REF] Honda | Multiparty asynchronous session types[END_REF]) involved parties. Here, even more than in other type disciplines for processes, communication is constrained to follow a prescribed protocol, and so there is even less hope to get a completeness result. This is particularly visible in certainly formulations of session types (e.g. [START_REF] Caires | Session Types as Intuitionistic Linear Propositions[END_REF]), in which the only way to type a parallel composition is to find one and only one channel that the two components share, and restrict it immediately after forming the parallel composition.

Summing up, our work lies more or less at the meeting point of a broad spectrum of type-based techniques: the hope of ensuring properties of processes by looking at just one derivation is traded for completeness which, as we prove in this work, makes the set of łwell-typedž processes not recursively enumerable. It is thus hard to precisely contextualize this work, at least in the realm of concurrency theory. The comparison, e.g., with the work on termination [Demangeon et al. 2010b;[START_REF] Deng | Towards an Algebraic Theory of Typed Mobile Processes[END_REF] is a good example: their typability implies strong normalization, while we characterize a weak form of normalization (plus error-freedom), but guaranteeing completeness, which in their work is by construction impossible.

Contributions

This paper's contributions can be summarized as follows:

• We introduce a notion of asynchronous hyperlocalized π -process, study its expressive power by way of some examples, and define some basic behavioral properties for them. This is in Sect. 2. łHyperlocalizedž means that our π -calculus is in fact a fragment of the localized calculus, i.e., we have further constraints on the presence of input names under input prefixes. These constraints do not hinder in a significant way the expressiveness of the calculus, as we show in Sect. 2.3. • We prove that verifying the good behavior of an AHL π -term is a very hard problem, namely it is Π 0 2 -complete. This is proved by reducing the universal termination problem for Turing machines to it. Although not surprising, this is the first result of this kind in the literature, and shows that good behavior of π -processes is fundamentally different from termination in purely sequential languages like the λ-calculus, in which the property of being terminating (in any reasonable sense) can be proved by finitary, recursively checkable, certificates. • We introduce our intersection type system and prove its main property: a novel notion of complete typability characterizes good behavior (Sect. 3). Furthermore, we provide examples to show how our type system works with some familiar concepts (Sect. 3.4).

We conclude by discussing our work and its perspectives (Sect. 4).

THE CALCULUS

In this section, we present the process calculus at the center of our paper. We give its syntax and reduction semantics (Section 2.1) and define well-behaved processes (Section 2.2), a class of processes that we will then characterize in the next section. The calculus we consider is based on the polyadic asynchronous localized π -calculus [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF], on which we impose a further, non-standard constraint that we call hyperlocalization. Despite being a non-trivial restriction, hyperlocalization does not significantly hinder the expressiveness of the calculus, as we show in Section 2.3. As announced, the property of being well-behaved is of an essentially different nature with respect to, say, termination in sequential programming languages like the λ-calculus: the latter is typically Σ 0 1 -complete, while here we are strictly higher in the arithmetical hierarchy, as shown in Section 2.4.

Processes and Reduction

We fix a countably infinite set of names, ranged over by x, y, z, w. We write x for an arbitrary finite sequence of names, the length of which is denoted by | x |. Later, the notation • will also be used for sequences of other objects (types, etc.).

We start by considering the following variant of the polyadic asynchronous π -calculus:

P, Q ::= 0 P | Q νxP terminated process, parallel composition, name restriction x⟨ y⟩ x ( y).P !x ( y).P output particle, input prefix, replicated input prefix (server)

In an output particle x⟨ y⟩ or input prefix x ( y) or !x ( y), the name x is said to occur as subject; in the case of the output particle, the names y are said to occur as objects. The set fn(P ) of free names of P is defined as usual: the names y are bound in x ( y).P and !x ( y).P, and x is bound in νxP; free names are those that are not bound. We write out(P ) for the subset of fn(P ) of those names appearing as subjects of output prefixes. As usual, we write x, x .P and !x .P as short-hands for x⟨⟩, x ().P and !x ().P, respectively. Structural congruence is the contextual, symmetric-transitive closure of the following equations:

(P | Q ) | R ≡ P | (Q | R) 0 | P ≡ P P | Q ≡ Q | P νxνyP ≡ νyνxP νxP | Q ≡ νx (P | Q ) provided that x fn(Q ).
As usual, we write ν (x 1 , . . . , x n )P for an arbitrary sequence of restrictions, the order of which is irrelevant by the fourth equation. As customary in process algebras, structural congruence has no computational value and is meant to capture the fact that some processes, although syntactically different, should in fact be considered as identical.

Intersection Types and Runtime Errors in the Pi-Calculus

7:5

Reduction between processes is defined as follows. First, we have the basic rules

x⟨ y⟩ | x ( z).P -→ P { y/ z} provided that | y| = | z|, x⟨ y⟩ | !x ( z).P -→ P { y/ z} | !x ( z).P provided that | y| = | z|, νx (!x ( z 1 ).P 1 | • • • | !x ( z n ).P n ) -→ 0.
The first rule is standard: it corresponds to the basic intuition that R := x ( z).P is a process waiting to receive a number of names via channel x, and that x⟨ y⟩ represents a message consisting of a number of names y sent on x; when such an output particle meets R, the names y are received by R and the process continues as P { y/ z}, which denotes the substitution of each name in y to the corresponding formal parameter in z. For such a substitution to be well-defined, the sequences y and z must have equal length, which explains the side condition.

The second rule is derivable from the first rule and the standard equation !P ≡ P | !P, which we prefer to avoid in order to keep structural congruence simpler. This rule corresponds to the intuition that !x ( z).P acts as a server capable of behaving like x ( z).P an indefinite number of times, i.e., capable of accepting an indefinite number of requests.

The third rule is not strictly necessary but makes the presentation of our results cleaner. It is sensible under the server intuition described above: once it becomes clear that no-one will ever make any request on x, a łserver poolž on x may be shut down. Note that the case n = 0 is νx0 -→ 0, whose equational form is usually one of the axioms of structural congruence.

The first two steps are called communication steps, the third clean-up step. The reduction relation between processes, denoted by -→, is the closure of the above basic rules under evaluation contexts

C ::= {•} C | P νxC
and under structural congruence:

S ≡ P -→ Q ≡ R implies S -→ R.
We write -→ * for the reflexive-transitive closure of -→.

Definition 2.1 (hyperlocalized process). A process of the above calculus is hyperlocalized if, in any subprocess of the form x ( y).P or !x ( y).P, no z ∈ fn(P ) occurs as the subject of an input prefix. The set of hyperlocalized processes forms the polyadic asynchronous hyperlocalized π -calculus, or AHLπ for short.

In the more standard localized π -calculus [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF]), the restriction to x ( y).P and !x ( y).P is that only the names in y are forbidden to appear as subjects of input prefixes, so our constraint is strictly stronger, hence the terminology. Let us give a few simple examples:

x (y).(y | y.0 | w⟨y⟩) not localized;

x (y).(y | z.0 | w⟨y⟩) localized, not hyperlocalized;

x (y).νz(y | z.0 | w⟨y⟩) hyperlocalized.

The main property of the localized π -calculus is that, in a process of the form νxP, every possible input via x is statically determined by the syntax of P. As [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF] put it, łevery process that receives via a name is local to the process that created that namež. This locality property is useful in several applications, such as distributed programming (where processes run at different sites) and object-oriented programming (where names represent object names). Our additional restriction is of logical nature; we defer a discussion to Sect. 4.

The following lemma, which shows that AHLπ is a well-defined subcalculus of the asynchronous π -calculus, is straightforward: Lemma 2.2. Let P be a hyperlocalized process.

(1)

If P ≡ Q, then Q is hyperlocalized. (2) If P -→ Q, then Q is hyperlocalized.

Behavioral Properties of Processes

We now define the properties of processes that we will be interested in. The first concept we need is the one of runtime error, which arguably encompasses those situations which we would like to avoid in the execution of a process.

Definition 2.3 (Runtime Error).

A runtime error is one of the following configurations: Arity Mismatch: a process of the form x⟨ y⟩ | x ( z).P or x⟨ y⟩ | !x ( z).P such that | y| | z|; such configurations are stuck because two processes are trying to communicate but the number of actual parameters sent does not match the number of formal parameters expected on the receiving side. Failed Send: a process of the form νx (x⟨ y⟩ | R), where R contains no input prefix whose subject is x; this is a process in which data has been sent on channel x but will never be consumed. Endless Wait: a process of the form νx (x ( z).Q | R), where x out(R), i.e., R contains no output particle whose subject is x; dual to a Failed Send, this is a situation in which a process waits for an input on channel x which will never arrive. Dependency Cycle: an i/o cycle on x 1 , . . . , x n , with n ≥ 1, is a process of the form †x 1 ( y

1 ).Q 1 | • • • | †x n ( y n ).Q n ,
where †x ( y).Q stands for either x ( y).Q or !x ( y).Q, such that x i+1 ∈ out(Q i ) for all 1 ≤ i < n and x 1 ∈ out(Q n ) (remember that out(P ) is the set of free names of P occurring as subjects of output particles). A dependency cycle is a process of the form

ν (x 1 , . . . , x n )(C | R)
where C is an i/o cycle on x 1 , . . . , x n and R is arbitrary; this is a classic form of deadlock, in which the dependency graph between processes is indeed cyclic.

Dependency cycles are perhaps the hardest to grasp, so let us give an example:

ν (x, y)(x .y | y.x | x ),
which fits the above definition once we take x 1 = x, x 2 = y, C = x .y | y.x and R = x. There is obviously a sort of a vicious circle here: the first subprocess of C waits for the second subprocess to send over x, but the second subprocess cannot proceed because it is waiting for the first subprocess to send over y. Of course, a configuration containing a łself-cyclež such as νx (x .x | x ) is also a dependency cycle (here, adding x in parallel makes the example more conspicuous because νx x .x is an endless wait as well as a dependency cycle).

The reader may object here that the vicious circles of our dependency cycles are not so łviciousž because that may be broken: for instance, in the first example above, the particle x may be used to łunblockž the first subprocess, yielding

ν (x, y)(x .y | y.x | x ) -→ ν (x, y)(y | y.x ) -→ * νx x .
Note, however, that the resulting process is a failed send, i.e., a runtime error. This is not a coincidence; we will come back to this point momentarily.

Now that the notion of a runtime error has been precisely formalized, defining well-behaved processes is relatively easy: we only need to remember that for a process to be error-free it is necessary that it does not produce a runtime error at top-level.

Intersection Types and Runtime Errors in the Pi-Calculus 7:7 Definition 2.4 (Well-Behaved Process). A process P contains a top-level runtime error if

P ≡ ν z(E | Q )
where E is a runtime error. It is error-free if it contains no top-level runtime error. A process is idle if it is error-free and cannot reduce (i.e., it is in normal form with respect to the rewriting rules of Sect. 2.1). A process P is well-behaved if, whenever P -→ * Q:

(1) Q is error-free;

(2) there exists an idle process I such that Q -→ * I .

Note that the only closed idle process is 0. Therefore, in the closed case, a well-behaved process is one that never generates top-level runtime errors and always has a way of evolving to 0. This is a typical property that one would ask of an operating system: it may run forever, but it must never produce errors and may always be shut down.

Of course, our notion of good behavior is only as convincing as the notion of runtime error it is based upon. For what concerns arity mismatches, failed sends and endless waits, we hope that the reader will not have trouble recognizing these as unwanted configurations. Dependency cycles are a bit more subtle because, as observed above, we allow them to be broken. A less controversial notion would be the following:

Definition 2.5 (Deadlock). A dependency cycle ν (x 1 , . . . , x n )(C | R) is breakable if R -→ * x i ⟨ y⟩ | R ′ for some 1 ≤ i ≤ n. A deadlock is an unbreakable dependency cycle.
The simplest examples of deadlocks are dependency cycles in which R = 0, e.g. ν (x, y)(x .y | y.x ), but of course more complex examples may be imagined, such as ν (x, y)(x .y | y.x | z.x ). These are clearly łbadž configurations because not only are they vicious circles but they are also persistent, i.e., their presence cannot be removed by reduction. We therefore hope that the reader will be fully convinced by the following notion of łbadž behavior: Definition 2.6 (Ill-Behaved Process). A process P is ill-behaved if there exists Q such that P -→ * Q and one of the following holds:

(1) Q contains a top-level arity mismatch, failed send, endless wait or deadlock;

(2) Q cannot reduce to an idle process.

It turns out that, in AHLπ , the ill-behaved processes are exactly those that are not well-behaved. That is, for behavioral purposes, our looser notion of dependency cycle is equivalent to the less controversial notion of deadlock. More precisely, assuming hyperlocality, one may show (as we do below) that the presence of a dependency cycle, even breakable, implies the possibility of the appearance of an łuncontroversially badž configuration (namely, a deadlock, a failed send or a process with no idle form). Since dependency cycles admit a simpler definition than deadlocks, this explains why we chose to ground our łofficialž definition of good behavior on the former rather than the latter.

In the following, we call a process that cannot reduce to an idle form restless.

Lemma 2.7.

Let P := ν (x, w )( †x ( z).Q | x⟨ y⟩ | R) be hyperlocalized, with †x ( z).Q standing for either x ( z).Q or !x ( z).Q. Then:
• if Q { y/ z} is restless, then P reduces to a restless process;

• if, on the contrary, Q { y/ z} reduces to an idle form, then

P -→ * ν (x, w ′ )(s 1 ⟨ r 1 ⟩ | • • • | s m ⟨ r m ⟩ | R)
and, for all p ∈ out(Q ), there exists i such that s i = p.

Proof. Assume that Q ′ := Q { y/ z} is restless. We have

P -→ ν (x, w )(Q ′ | R ′ ) =: S, where R ′ = R or R ′ = !x ( z).Q | R
depending on the form of †x ( z).Q. By hyperlocality, no free name of Q ′ is the subject of an input prefix in Q ′ , which means that every communication that Q ′ may perform with R ′ concerns an output particle a⟨ b⟩ produced by Q ′ and consumed by R ′ . Furthermore, such an output particle cannot interact within Q ′ , for otherwise there would be an input on a in Q ′ , contradicting locality. Therefore, neither these output particles nor R ′ itself may bear any impact on the reductions causing Q ′ to be restless, so the process S is restless.

On the contrary, if Q ′ -→ * I with I idle, then a straightforward case analysis shows that

I = ν r (s 1 ⟨ r 1 ⟩ | • • • | s m ⟨ r m ⟩) (
there may be no inputs because of hyperlocality). Furthermore, if p ∈ out(Q ), i.e., p is free in Q and there is an output particle p⟨ q⟩ in Q, then there must be some s i ⟨ r i ⟩ which is equal to p⟨ q⟩, because by hyperlocality there cannot be any input on p in Q ′ and so no reduction of Q ′ may consume p⟨ q⟩. □ Proposition 2.8. A hyperlocalized process is ill-behaved iff it is not well-behaved.

Proof. Ill-behaved processes are obviously not well-behaved, so let us turn to the converse. For this, it is enough to show that if a hyperlocalized process P contains a top-level breakable dependency cycle, then P is ill-behaved. So let

C := †x 1 ( z 1 ).Q 1 | • • • | †x n ( z n ).Q n be an i/o cycle on x = x 1 , . . . , x n and suppose that P = ν ( x, w )(C | R) such that R -→ * x i ⟨ y⟩ | R ′ .
We may assume without loss of generality that i = 1 (a cycle being perfectly symmetric). Let

P ′ := ν ( x, w )(C | x 1 ⟨ y⟩ | R ′ ).
We have two possibilities:

• either Q 1 { y/ z 1 } is restless, in which case, by Lemma 2.7, P ′ (and hence P) reduces to a restless process and is therefore ill-behaved by definition; • or Q 1 { y/ z 1 } is not restless, i.e., it reduces to an idle form which, again by Lemma 2.7, is of the form ν r 1 (x 2 ⟨ y 2 ⟩ | I 1 ) with I 1 consisting only of output particles (remember that x 2 ∈ out(Q 1 ) by hypothesis), and therefore

P -→ P ′ -→ * ν ( x, w, r 1 )(Q ′ 1 | †x 2 ( z 2 ).Q 2 | • • • | †x n ( z n ).Q n | x 2 ⟨ y 2 ⟩ | R ′ | I 1 ), where Q ′ 1 is !x 1 ( y 1 ).Q 1 or 0, depending on whether the input †x 1 ( y 1 ).Q 1 in C is replicated or not.
In the second case, we are in position of iterating the same reasoning, which leads us (by induction on n, if we want to be fully formal) to the conclusion that either P reduces to a restless process or

P -→ * ν ( x, w ′ )(C ′ | x 1 ⟨ y 1 ⟩ | R ′ | I ),
where C ′ consists of the replicated inputs from the original cycle C and I consists of a number of output particles deriving from the idle forms of the various

Q i { y i / z i }.
Now, if the process on the right hand side has no input on x 1 , we have a failed send and we may conclude. Otherwise, observe that, by hyperlocality, such an input must be at top-level in either C ′ or R ′ . Let us start by supposing that it is in R ′ . In that case, the output particle x 1 ⟨ y⟩ in P ′ may interact directly with R ′ , preventing the cycle to break. We have two possibilities:

Intersection Types and Runtime Errors in the Pi-Calculus 7:9

• R is able to produce only finitely many output particles interacting with C: in this case, we have shown that these lead either to a restless process, or they may actually be consumed łinternallyž to R itself; therefore, either we find a restless process or, after finitely many steps, the dependency cycle loses every chance of being broken and becomes a true deadlock; • R produces infinitely many output particles interacting with C: in this case, the reasoning may be iterated again and again, showing that P is restless. Suppose now that the input on x 1 is in C ′ , which means that it is equal to !x 1 ( z 1 ).Q 1 . We have two subcases:

• every input of the cycle C is replicated, i.e., C ′ = C. Then, P ′ is restless: indeed, we have arrived here from P ′ by avoiding reductions to restless processes, i.e., all other possibilities lead to restless processes; in spite of this, we still obtained a process essentially identical to P ′ , so we are bound to loop forever. • There is at least one input of C which is not replicated. Let us suppose for simplicity that this is x 2 ( y 2 ).Q 2 (the other possibilities are not different in an essential way). In this case, we let the output x 1 ⟨ y 1 ⟩ be consumed by !x 1 ( z 1 ).Q 1 in C ′ , we apply the same reasoning as above and obtain ν (

x, w ′ )(C ′ | x 2 ⟨ y ′ 2 ⟩ | R ′ | I ′ )
, except that now in C ′ there is no input on x 2 , so we are brought to the case already considered above in which an input on x 2 , if present at all, is in R ′ , and we conclude.

□

Expressiveness

The aim of this section is to give some convincing arguments on the expressiveness of AHLπ . More specifically, we show that three different forms of processes, the first one sequential and the other two truly concurrent, can all be written as AHLπ processes.

2.3.1 Functional Programming. We will start by considering a parallel and non-deterministic λcalculus, denoted by Λ [•], | . This is a nontrivial extension of the pure, untyped λ-calculus endowed with a form of parallel composition, and in which a function can be applied to more than one term at the same time. Terms of Λ [•], | are the expressions generated by the following grammar:

M, N ::= x λx .M M[N 1 , . . . , N k ] 0 M | N
As usual, the parallel operator is assumed to be associative, commutative and with neutral element 0. Reduction is defined from the following rules (we write ⃗

N for [N 1 , . . . , N k ]) (λx .M ) ⃗ N -→ M {N i /x }, 0 ⃗ N -→ 0, (M | N ) ⃗ P -→ M ⃗ P | N ⃗ P, closed under weak head evaluation contexts E ::= {•} EM E | M.
Observe how the first rule non-deterministically picks one N i and substitutes it to x. Because of this rule, the calculus is not confluent. This extension of the λ-calculus may be encoded in our fragment of ALπ as follows:

x u := x⟨u⟩ λx .M u := νa(u⟨a⟩ | a(x, v). M v) M[N 1 , . . . , N k ] u := νv ( M v | v (a).νz(a⟨z, u⟩ | !z(w ). N 1 w ) | • • • | v (a).νz(a⟨z, u⟩ | !z(w ). N k w )) 0 u := 0 M | N u := M u | N u
where u is a fresh name. The fact that the encoding lands in AHLπ is immediate once we observe the following invariant, easily proved by induction: fn( M u) = fv(M ) ∪ {u} (where fv(M ) denotes the set of free variables of M) and, moreover, every name in fn( M u) occurs in M u itself in output position (as subject or object). The above encoding is very similar to (the asynchronous variant of) Sangiorgi's encoding of the call-by-name λ-calculus given in [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF]] (Milner's original encoding [START_REF] Milner | Functions as Processes[END_REF]] is slightly more succinct but is not localized). Indeed, one may look at the above calculus as a łreverse engineeringž of a parallel liberalization of Sangiorgi's encoding: one takes the image of that encoding, closes it under parallel composition and adds the possibility of having an arbitrary number of concurrent arguments in the encoding of an application (which is quite natural from the π -calculus point of view). From this, one may łread backž a λ-calculus (the one presented above) which maps to such processes, treating parallel composition homomorphically.

The main property of the encoding, which follows from the corresponding property of Sangiorgi's encoding via the above discussion, is the following (we use ≃ c to denote barbed congruence on AHLπ , which is defined as customary [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF]): Proposition 2.9. Let M be a term of

Λ [•], | . (1) M -→ M ′ implies M u -→ * ≃ c M ′ u; (2) M u -→ * P implies that M -→ M ′ for some M ′ such that P -→ * ≃ c M ′ u.
Although we will never use them here, it is straightforward to endow Λ [•], | with control operators (like those corresponding to classical logic proofs in the sense of the Curry-Howard correspondence), obtaining a non-deterministic and parallel extension of the λµ-calculus:

• one adds the construct µa.[b]M to the grammar, where a, b range over continuation variables;

• one adds the rule

(µa.[b]C{[a]M 1 , . . . , [a]M n }) ⃗ N -→ µa.[b]C{[a]M 1 N i 1 , . . . , [a]M n N i n },
where C is a n-hole context and i 1 , . . . , i n ∈ {1, . . . , k} are arbitrary and not necessarily distinct, i.e., the rule picks n terms among N 1 , . . . , N k , possibly using the same term more than once and discarding some terms; • the encoding • is extended by setting µa.[b]M u := M b{u/a}.

Locks.

A lock is one of the most basic concurrent primitives, being a way to model the safe access to resources which can only be accessed sequentially, like critical regions. A particularly economic way of implementing a lock in the π -calculus is to see it as a buffer containing at most one value: in νl

(P 1 | • • • | P n | l )
, each P i competes to read from l, and puts back a value once it has done. Unfortunately, this simple solution is not acceptable from our point of view: P i will typically be of the form l .Q i {l }, i.e., Q i contains l, inducing a dependency cycle. Consider instead

L := !a(z).νv (p⟨v⟩ | v.z⟨z⟩) Lock := νa(a⟨a⟩ | L).
A process using the above lock will be of the form

P i := p(v).Q i with Q i -→ * R i | v, i.
e., P i waits for the signal from the lock, then performs some operations, upon completion of which sends a release signal via the channel received from the lock process. The process

P 1 | • • • | P i | • • • | P n | Lock reduces to νv (P 1 | • • • | Q i | • • • | P n | νa(v.a⟨a⟩ | L))
Intersection Types and Runtime Errors in the Pi-Calculus 7:11 in which a non-deterministically chosen process is ready to execute, while the others are waiting for it to release the lock. We will later analyze the behavior of this process via types. For the moment, it suffices to observe that this is an AHLπ process which does not exhibit a top-level run-time error.

A Toy

Operating System. Consider the following definitions:

Serv i := !r i (a).a OpSys := Serv 1 | • • • | Serv n R i (z) := νa(r i ⟨a⟩ | a.z⟨z⟩) U (z) := νs (s | !s.R 1 (z) | • • • | !s.R n (z) | !s.0) User := νu (u⟨u⟩ | !u (z).U (z))
OpSys is the abstraction of a multi-user, concurrent operating system offering services Serv i for 1 ≤ i ≤ n. Each subprocess Serv i is the abstraction of a system call, which is invoked by sending a request on channel r i , together with a channel where the answer has to be sent. User is the abstraction of a user who is logged into the system. The real definition is in U , the rest is needed to encode recursion: the user requests an indefinite number of services, in random order, and may eventually decide to logout (this is represented by the subprocess !s.0).

The operating system with an arbitrary number of logged-in users may then be modeled by the process

User | • • • | User | OpSys.
Again, below we will perform a behavioral analysis via types also for this process.

Hardness of Checking Good Behavior

By resorting to some computable encoding of processes as integers (i.e., Gödelization), the problem of checking whether a process is well-behaved may be formalized as a subset of N. More precisely, let us define W := {n ∈ N | n is the code of a well-behaved AHLπ process}.

We will now show that W is Π 0 2 -complete. For simplicity, we will use the Gödelization transparently, i.e., we will say ła process Pž instead of łthe code n of a process Pž.

That W is a Π 0 2 set is fairly clear: runtime errors are finite configurations, so there is a ∆ 0 0 formula (i.e., using only bounded quantifiers) ErrorFree(P ) which holds iff P is an error-free process; moreover, there is a ∆ 0 0 formula Red(P, Q, r ) (similar to Kleene's T predicate) holding iff r is the code of a reduction P -→ * Q; finally, there is a ∆ 0 0 formula Idle(P ) holding iff P is idle. So W is defined by the formula ∀r .∀Q.∃q.∃I .Red(P, Q, r ) ⇒ ErrorFree(Q ) ∧ Red(Q, I, q) ∧ Idle(I ), which contains P as only free variable and is Π 0 2 by definition. For what concerns the completeness of W , we decompose the reduction from a Π 0 2 -complete problem in two steps. Call a term M of Λ [•], | safe if, whenever M -→ * M ′ , there exists N normal such that M ′ -→ * N . Let S be the set of (codes of) safe terms. Now, one may check that:

• thanks to the functional nature of the λ-calculus, the encoding M u of a λ-term M never produces runtime errors, i.e., for all M u -→ * Q, Q is error-free;

• if N is normal, then N u is idle.
Therefore, by the correctness of the encoding (Proposition 2.9), M is safe iff M u is well-behaved. Since • is clearly computable, we just proved that S reduces to W . It is thus enough to show that S is Π 0 2 -hard, which we will do by reducing to S the archetypal Π 0 2 -complete set, namely H := {n ∈ N | n is the code of a Turing machine halting on all inputs}.

It is of course enough to restrict to Turing machines working on the binary alphabet {0, 1}. The following are completely standard results [START_REF] Henk | The Lambda Calculus[END_REF]]:

• a binary string w ∈ {0, 1} * may be encoded as a λ-term w such that there are λ-terms cons i , with i ∈ {0, 1}, satisfying cons i w -→ * iw by means of head reduction; • for every Turing machine M one may explicitly construct a λ-term M such that, for every w ∈ {0, 1} * , the head reduction of Mw terminates on I (the identity λ-term I = λx .x) iff M terminates on input w. By applying terms to a suitable number of identities, the above results transfer to weak call-by-name (remember that our λ-calculus of Sect. 2.3.1 does not reduce under abstraction).

Consider now the following terms of the λ-calculus of Sect. 2.3.1:

proj i := λz 1 .λz 2 .λz 3 .z i , i ∈ {1, 2, 3}, X := λx .λw.λm.(λp.p(mw )(xx (cons 0 w )m)(xx (cons 1 w )m))[proj 1 , proj 2 , proj 3 ], G m := XXεm,
where m is a variable. The intuition behind G m is that it is a (recursively-defined) łrandomž string generator: we start from the empty string and, at each step, firing the redex involving multiapplication in X non-deterministically chooses whether we add a 0, a 1 or whether we stop and apply m to the string generated so far. One may easily check that:

(1) for all

w 1 • • • w n ∈ {0, 1} n , we have G m -→ * m(cons w 1 (. . . cons w n ε . . .));
(2) for all G m -→ * N , there exists

w 1 • • • w n ∈ {0, 1} n s.t. N -→ * m(cons w 1 (. . . cons w n ε . . .)).
We now contend that a Turing machine M terminates on all inputs iff G M is safe, which is enough to prove that H reduces to S. Suppose that M terminates on all inputs, and let G M -→ * M ′ . Now, there are two cases: either M reached the head position at some point during the reduction, in which case by property (2) above we have G M -→ * M (cons w 1 (. . . cons w n ε . . .)) -→ * M ′ for some w 1 • • • w n ∈ {0, 1} n ; or M has not reached the head yet, in which case M ′ is like the term N of property (2) above, and we have M ′ -→ * M (cons w 1 (. . . cons w n ε . . .)) for some

w 1 • • • w n ∈ {0, 1} n .
In both cases, we are essentially computing M w for some w ∈ {0, 1} * , which head-normalizes by hypothesis, so G M is safe.

Suppose now that there exists w = w 1 • • • w n ∈ {0, 1} n on which M does not terminate. Then by property (1) above G M -→ * M (cons w 1 (. . . cons w n ε . . .)), which behaves like M w, whose head reduction does not terminate by hypothesis, showing that G M is not safe.

INTERSECTION TYPES

This section is devoted to presenting our type discipline for processes, also proving that it captures good behavior as we defined it in Section 2.2 above. We will also instantiate our type discipline to some example processes (Section 3.4). From here on, all processes are tacitly taken to be in AHLπ .

Types and Derivations

Types cannot be defined directly here, and will be introduced as those pre-types satisfying a coherence condition. Pre-types are defined by mutual induction with type sequences:

A, B, C ::= Θ 1 ∧ • • • ∧ Θ k pre-types Θ, Ξ ::= * (A 1 , . . . , A n ) type sequences
The nullary case (i.e., k = 0) of intersection is written ⊤. Pre-types are considered up to commutativity of intersection, e.g. () ∧ ( * ) = ( * ) ∧ (). Note that the constant * is not the same as the empty sequence, denoted by (). Also observe that intersection is not idempotent: Θ ∧ Θ ∧ Ξ is not the same as Θ ∧ Ξ.

If A = Θ 1 ∧ • • • ∧ Θ k and B = Ξ 1 ∧ • • • ∧ Ξ p are pre-types, then A ∧ B is naturally defined as Θ 1 ∧ • • • ∧ Θ k ∧ Ξ 1 ∧ • • • ∧ Ξ p .
In particular, A ∧ ⊤ = ⊤ ∧ A = A. There are no base types (except * , which however is not really a base type but a constant); including them would change nothing to our results. We define the binary relation ⌢ on pre-types and type sequences, called coherence, as the smallest symmetric relation satisfying

∀ Θ * ⌢ Θ A i ⌢ B i ∀i ∈ {1, . . . , n} (A 1 , . . . , A n ) ⌢ (B 1 , . . . , B n ) Θ i ⌢ Ξ j ∀i ∈ {1, . . . , k }, ∀j ∈ {1, . . . , p} Θ 1 ∧ • • • ∧ Θ k ⌢ Ξ 1 ∧ • • • ∧ Ξ p
A type is a pre-type A such that A ⌢ A. An obvious example of type is * . By applying the rightmost rule when k = 0, we see that ⊤ ⌢ A for any A, so ⊤ is also a type. A more complex example is given by the family A 0 := ⊤, A i+1 := (A i ) ∧ A i . Checking that A n is a type for all n ∈ N may be done by proving, by induction on m + n, the stronger statement that A m ⌢ A n and (A m ) ⌢ A n for all m, n ∈ N.

The idea behind the definition of pre-type is the following. Type sequences are needed to type input/output prefixes/particles: intuitively (and approximately), in x (y 1 , . . . , y n ).P or x⟨y 1 , . . . , y n ⟩, if each y i has type A i , then x will be typed with (A 1 , . . . , A n ). Since a name may appear more than once as subject of an input/output prefix/particle, intersection is used to collect all the corresponding type sequences: for instance, if a process contains two output particles x⟨ y⟩ and x⟨ z⟩, and if the types of y and z are A and B, respectively, then x will receive the type ( A) ∧ ( B). This also explains why intersection is non-idempotent. If x is never used, then it will get type ⊤. Of course, this means that we may read back usage information from types: for instance, if x : (()) ∧ (⊤) types x as input, we know that there is a reduction sequence in which x will be used twice, once receiving a name which will in turn be used once for a nullary output (the type ()) and once receiving a name which will not be used at all (the type ⊤).

There is a subtlety concerning inputs: when an input is never used, we must distinguish the replicated and non-replicated case. Indeed, while !x ( z).P and x ( z).P are both innocuous processes which must be typable, we have that νx !x ( y).P -→ 0, which must still be typable, whereas νx x ( y).P is a runtime error (an endless wait, Definition 2.3) and must not be typable. This is the reason behind the presence of the constant * : it is used to type the subject of an unused non-replicated input prefix, whereas for unused replicated inputs we use ⊤.

While the input/output distinction does not appear at the level of types (they are, in a sense, łself-dualž), it will appear in the type system: a type on the left (resp. right) of a judgment will be an input (resp. output) type. A key property then will be for a name to appear with identical types on both sides of a typing judgment: indeed, x : A on the left means łchannel x is used by input prefixes expecting specification Až, so x : A on the right means that such a specification is met by the outputs on x. This information is crucial for typing name restrictions (res rule, Fig. 1).

We have thus far explained the shape of pre-types but said nothing as to why these have to be restricted. The reason is that we want our type system to ensure at least absence of arity mismatches (the first kind of runtime error in Definition 2.3): recall that these arise when an output particle sending n names on a channel meets an input prefix on the same channel expecting m names, with m n. The obvious solution is to force intersections to be łuniformž: if Θ 1 ∧ • • • ∧ Θ k is the pre-type of a channel, we want the length of each Θ i to be equal. But of course this is too naive: the length must be the same łhereditarilyž, i.e., the pre-types in each Θ i must also be uniform, and so on. This łhereditary uniformityž is captured by the above coherence relation.

Let us now get to the type system. We consider typing judgments of the form Γ ⊢ P :: ∆ where • P is a process of AHLπ ;

• ∆ is a finite sequence (permutable at will) of declarations of the form

y : B
where B is a type and y is a name. Such a declaration corresponds to the possible presence in P of free occurrences of y as subjects or objects of an output particle. • Γ is a finite sequence (permutable at will) of declarations of the form

(x; X ) : A
where A is a type, x a name and X a finite set of names. Such a declaration corresponds to the possible presence in P of free occurrences of x as subjects of input prefixes and X contains all those names, declared in ∆, which may depend on x, in the sense that, if y ∈ X , then there may be an output particle mentioning y whose emission ultimately depends on a reception on x (a trivial example would be x .y). We write (x; y 1 , . . . , y k ) for (x; {y 1 , . . . , y k }). Please observe once again how ∆ provides type information for channels involved in output actions, while Γ does the same for input actions. A name x may be declared both in Γ and in ∆, meaning that x is possibly used both as input and output in P.

The typing rules are given in Fig. 1. Let us explain the notations used therein:

• the notation x : A stands for x 1 : A 1 , . . . , x n : A n , with n arbitrary (including null).

• The notation z : ⊤ on the right is short for an arbitrary sequence z 1 : ⊤, . . . , z n : ⊤; on the left, w : ⊤ is short for (w 1 ; ) : ⊤, . . . , (w n ; ) : ⊤; in both cases, the names declared do not appear free in the subject process. • In the !in rule, k ∈ N is arbitrary and is said to be the arity of the instance of the rule. The intersections k j=1 C j are defined pointwise. For instance, the unary case is identical to the in rule (except for the subject process), whereas a typical binary instance may look like ⊢ P :: y : A 1 , z : C 1 ⊢ P :: y : A 2 , z : C 2 (x; z) : (A 1 ) ∧ (A 2 ) ⊢ !x (y).P :: z : C 1 ∧ C 2 !in (we assumed that fn(P ) = {y, z}). The nullary case has the following general shape, which is very similar to that of the in * rule, the difference being that here x gets type ⊤ instead of * : w : ⊤, (x; fn(P ) \ y) : ⊤ ⊢ !x ( y).P :: z : ⊤ !in and of course we demand that z contains at least fn(P ) \ y.

• in the par rule, the operation ∧ on sequences of type declarations is pointwise. For instance, the following is an instance of the rule:

(x; v, z) : A, (y; ) : C ⊢ P :: v : D 1 , w : E 1 , z : F 1 (x; w, z) : B, (y; v) : ⊤ ⊢ Q :: v : D 2 , w : E 2 , z : F 2 (x; v, w, z) : A ∧ B, (y; v) : C ⊢ P | Q :: v : D 1 ∧ D 2 , w : E 1 ∧ E 2 , z : F 1 ∧ F 2 par
The pre-condition of the out rule looks a bit complicated, so let us explain it. If we are typing an output particle x⟨z 1 , . . . , z n ⟩, then the output context must declare at least x, z 1 , . . . , z n . The complication comes from the fact that some of the z j may be equal to each other and, furthermore, Intersection Types and Runtime Errors in the Pi-Calculus 7:15 equal to x itself. In other words, the various z j are not names but occurrences of names. So we consider the names declared to be x, y, with y a sequence of names (without repetitions and pairwise distinct from x) such that there is a function f : {1, . . . , n} → {x, y} such that, for all 1 ≤ j ≤ n, f (j) = z j . The types A 1 , . . . , A n mentioned in the rule are the types of the occurrences z 1 , . . . , z n ; then, if e.g. z 3 = z 7 = y 2 (i.e., f -1 (y 2 ) = {3, 7}), the context will contain the declaration y 2 : A 3 ∧ A 7 . If no z j equals y i (i.e., f -1 (y i ) = ∅), then y i gets type ⊤ (the empty intersection). This is where the seemingly complicated shape of the types of x, y comes from. The type of x further reflects the fact that it is the subject of the output, so it must contain at least the type sequence (A 1 , . . . , A n ). To give a couple of concrete examples, we have that x⟨y, z, z⟩ may be typed in context x :

w : ⊤ ⊢ 0 :: z : ⊤ zero A 1 , . . . , A n types f : {1, . . . , n} → {x, y} C i = j ∈f -1 (y i ) A j , 1 ≤ i ≤ | y| w : ⊤ ⊢ x⟨f (1), . . . , f (n)⟩ :: x : (A 1 , . . . , A n ) ∧ j ∈f -1 (x ) A j
( A 1 ) ∧ • • • ∧ ( A k ) ⊢ !x ( y).P :: z : k j=1 C j !in (x, X ) : A ⊢ P :: y : C (x, Y ) : B ⊢ Q :: y : D (x; X ∪ Y ) : A ∧ B ⊢ P | Q :: y : C ∧ D par Γ, (x; X ) : A, (w 1 ; Y 1 , x ) : B 1 , . . . , (w n ; Y n , x ) : B n ⊢ P :: ∆, x : A x X , Γ Γ, (w 1 ; Y 1 ∪ X ) : B 1 , . . . , (w n ; Y n ∪ X ) : B n ⊢ νxP :: ∆ res
(A 1 , A 2 , A 3 ), y : A 1 , z : A 2 ∧ A 3 , w : ⊤, whereas x⟨x, z, z⟩ may be typed in context x : (A 1 , A 2 , A 3 ) ∧ A 1 , z : A 2 ∧ A 3 , w : ⊤.
We have not yet commented on input declarations, and why they are of the form (x; X ) : A rather than just x : A. The reason is that we want to avoid dependency cycles: the pair (x; X ) indicates, as mentioned above, that there are outputs whose subjects are in X which are guarded by an input prefix whose subject is x. The idea then is to maintain such information so that x ∈ X implies that we have an i/o cycle, which explains the side condition of the res rule. At the same time, the res rule updates the dependency information by stating that, if in P the names X depend on x and x depends on w, then in νxP the names X depend on w. The par rule also updates the information by joining dependencies.

Typability and Complete Typability

As stressed in the Introduction, a process P being typable in our type system does not imply that P cannot exhibit any bad behavior, i.e., that P is well-behaved. This section is devoted to introducing the notion of complete typability, which will be the one characterizing good behavior. As such, because of the result of Sect. 2.4, it cannot be turned into a recursively enumerable predicate on processes, but relies instead on the existence of (potentially) infinitely many type derivations for the process under consideration, say P. Each of these derivations is a łwitnessž of the good behavior of a possible execution of P. If all possible executions have a witness, we say that P is completely typable. In order to formalize this idea, we need to say what it means for a type derivation to match a reduction sequence, which in turn requires us to recall a few standard concepts of rewriting theory (essentially, the notion of ancestor). Definition 3.1 (Typability). A process P is typable if there exists a derivation of Γ ⊢ P :: ∆ using the rules of Fig. 1, such that, for all x : A in ∆ and (x; X ) : B in Γ, it holds that B = A ∧ C for some C.

It is not hard to show that typability is stable under structural congruence: P typable and P ≡ Q implies Q typable, in the same context. This fact will be tacitly used in the sequel.

We will now define the concept of ancestor, a standard notion in rewriting theory. In what follows, we will use σ , ρ to range over reduction sequences, and we will write ρ : P -→ * Q, or P ρ -→ * Q to mean that ρ is a reduction sequence from P to Q.

Definition 3.2 (Prefix Occurrence

). An output prefix, denoted by o, is of the form x⟨ y⟩; an input prefix, denoted by ι, is of the form x ( y) or !x ( y). Input and output prefixes are generically denoted by π . A prefix context is defined as follows:

C ::= {•} {•}.P x ( y).C !x ( y).C C | P P | C νxC.
Note that a prefix context C contains exactly one occurrence of {•}, the hole; we say that C is an input context if the hole occurs as {•}.P inside C, otherwise it is an output context. A prefix occurrence is a pair (π , C) such that π is an input (resp. output) prefix and C an input (resp. output) prefix context. We denote by C{π } the process obtained by substituting π for the hole {•} in C. Given a process P, the set of prefix occurrences of P is

pref(P ) := {(π , C) | C{π } = P }.
Note that P ≡ Q implies pref(P ) pref(Q ), i.e., the sets of prefix occurrences of the two processes are in bijection and such a bijection is uniquely determined. In what follows, for simplicity we will identify a prefix occurrence (π , C) with the prefix π , unless this generates confusion.

Consider now the basic reduction rules of AHLπ :

x⟨ y⟩ | x ( z).P -→ P { y/ z}, x⟨ y⟩ | !x ( z).P -→ P { y/ z} | !x ( z).P, νx (!x ( z 1 ).P 1 | • • • | !x ( z n ).P n ) -→ 0.
Call L and R the left and right hand sides of the rules, respectively. It is clear that every prefix appearing in R is a renaming of a unique prefix appearing in L. More formally, we may define a function Anc : pref(R) → pref(L) such that: if π ∈ pref(P { y/ z}), then Anc(π ) = σ where σ is the unique prefix in pref(P ) (as a subprocess of L) such that π = σ { y/ z}; if π ∈ pref(!x ( z).P ), then Anc(π ) = π as a prefix of L, i.e., π is mapped to łitselfž. The function Anc above may be extended to a function Anc ρ : pref(Q ) → pref(P ) for every one-step reduction ρ : P -→ Q, by simply setting it to be the łidentityž on prefixes not directly Intersection Types and Runtime Errors in the Pi-Calculus 7:17 involved in the communication. (This is well-defined because, as observed above, pref(•) is stable under structural equivalence, modulo a unique bijection). Furthermore, if we have a reduction sequence of length n ρ :

P ρ 1 -→ • • • ρ n -→ Q, we may define Anc ρ : pref(Q ) → pref(P ) by setting Anc ρ := Anc ρ 1 • • • • • Anc ρ n . Note that, if we denote composition of reductions ρ : P -→ * Q, σ : Q -→ * R by ρ; σ , then Anc ρ;σ = Anc ρ • Anc σ .
Definition 3.3 (Ancestor). Let ρ : P -→ * Q be a reduction sequence, and let π ∈ pref(Q ). The prefix Anc ρ (π ) ∈ pref(P ) is called the ancestor of π along ρ.

Note that, because of duplication, the ancestor function need not be injective: for instance, in

ρ : νx (x⟨a⟩ | x⟨b⟩ | !x (z).z) -→ * a | b,
the output particles a and b on the right have the same ancestor z. It is interesting to observe that our type system has a very precise way of accounting for such duplications. For instance, the left hand side above may be typed with the following derivation, which we call δ : Observe that the output particle z (the common ancestor of a and b) is typed twice in δ , once for each branch of the binary !in rule in δ ′ . This is because δ is somehow anticipating on the fact that z will be used twice during the reduction of the process it types.

Another very important remark is that δ contains precise information about the reduction ρ itself. This is composed of two communication steps, one concerning x⟨a⟩ and the other x⟨b⟩, plus a clean-up step. Disregarding the latter (which has no computational value), the two communication steps of ρ are visible in δ by the fact that x receives twice the type (()) as output, once as the subject of x⟨a⟩ and once as the subject of x⟨b⟩, and it receives the type (()) ∧ (()) as input, as the subject of !x (z). The fact that output types and input types match is not a chance but is a crucial phenomenon which is at the heart of our type system, and which we now proceed to make formal.

In what follows, we write δ :: P to mean that δ is a type derivation concluding with a judgment typing P. Definition 3.4 (Matching). Let ρ : P -→ * Q and let σ : Q -→ Q ′ be a communication step concerning an output prefix o and an input prefix ι. Let δ :: P. We say that δ matches σ if there exists a type A such that:

(1) if x is the subject of o ′ := Anc ρ;σ (o), δ contains a rule out whose conclusion is Γ ⊢ o ′ :: ∆, x : A;

(2) if y is the subject of ι ′ := Anc ρ;σ (ι), δ contains a rule in or !in whose conclusion is Γ, (y; Y ) : A ∧ B ⊢ ι ′ .Q :: ∆ for some type B (which may be ⊤). Let δ :: P and ρ : P -→ * Q. We say that δ matches ρ, and we write δ ▷◁ ρ, if δ matches every communication step fired along ρ.

Note that any derivation for P matches the identity reduction on P. Also observe that if δ ▷◁ (ρ; σ ) then δ ▷◁ ρ. We are now ready to give the most important definition of the whole paper:

⊢ x⟨ z⟩ :: x : ( D), s : D out γ ′ . . . . ⊢ R :: Σ ′ , z : D (x; out(R) \ z) : ( D) ⊢ x ( z).R :: Σ ′ in (x; out(R) \ z) : E ⊢ x⟨ y⟩.R | x ( z).R :: Σ ′ , x : ( D), s : D par
By replacing δ ′ in the original derivation δ by the derivation above, we obtain a derivation for P. Note that this derivation, say ε, satisfies ε ▷◁ P. • Similarly, if the reduction is by the rule x⟨ y⟩ | !x ( z).P -→ P { y/ z} | !x ( z).P, we can replace the subderivation for P { y/ z} | !x ( z).P by the one for x⟨ y⟩ | !x ( z).P: the only difference is that now we do not newly put !in rule to the subderivation, but add one premise to the existing application of !in rule.

• If the reduction is by the rule νx (!x ( z 1 ).P 1 | • • • | !x ( z n ).P n ) -→ 0, the process νx (!x ( z 1 ).P 1 | • • • | !x ( z n ).P n
) can be typed by the following derivation and it can be inserted by par rule to the place where the redex is in P:

(x; out(P 1 ) \ z 1 ) : ⊤ ⊢ !x ( z 1 ).P 1 :: x : ⊤ !in • • • (x; out(P n ) \ z n ) : ⊤ ⊢ !x ( z n ).P n :: !in (x; i out(P i ) \ i z i ) : ⊤ ⊢ !x ( z 1 ).P 1 | • • • | !x ( z n ).P n :: x : ⊤ par * ⊢ νx (!x ( z 1 ).P 1 | • • • | !x ( z n ).P n ) :: res .
Since this derivation has empty contexts, inserting it in the original derivation does not have any effect on validity of the derivation. Quantitative, Existential Subject Reduction. First we need a sub-lemma (proof is by structural induction).

Lemma 3.7. Let δ :: P. Then δ { x/ y} :: P { x/ y}, where δ { x/ y} is defined by renaming y by x in each processes and contexts in the derivation (if both z and v are renamed by w and z : A, v : B in a context, replace them by w : A ∧ B).

Existence of ρ : P -→ Q matching δ is a consequence of the typability condition (Definition 3.1) and the side condition on the res rule, which ensure that every output type is matched by an input type. Consider then such a ρ.

• Suppose that the reduction is by the rule x⟨ y⟩ | x ( z).R -→ R{ y/ z}. Since δ ▷◁ ρ, the derivation δ must contain a subderivation δ ′ in the following shape:

⊢ x⟨ y⟩ :: x : ( A), w : A ′ out γ . . . . ⊢ R :: z : A, Σ (x; out(R) \ z) : ( A) ⊢ x ( z).R :: Σ in (x; out(R) \ z) : ( A) ⊢ x⟨ y⟩ | x ( z).R :: x : ( A), w : A ′ , Σ par
where w is the set of names obtained by removing duplicates in y, the type ( A) of x is shared in the two contexts because δ ▷◁ ρ. By replacing δ ′ in the whole derivation δ by the derivation γ { y/ z}, we obtain a valid derivation with two less applications of rules. The derivation γ { y/ z}, and the derivation obtained by replacing δ ′ in δ by γ { y/ z} satisfies that: every contexts below γ { y/ z} except x are the same as δ , and the type of x (if any) is B where x is typed by ( A) ∧ B in δ . Especially, when applying res rule, the condition that the types of the same name match is satisfied as long as it is in the original derivation δ .

• Similarly, if the reduction ρ :

P -→ Q is by the rule x⟨ y⟩ | !x ( z).R -→ R{ y/ z} | !x ( z).R, the derivation δ must contain ⊢ x⟨ y⟩ :: x : ( A j ), w : A ′j out γ 1 . . . . ⊢ R :: z : A 1 , Σ 1 • • • γ n . . . . ⊢ R :: z : A n , Σ n (x; p) : i ( A i ) ⊢ !x ( z).R :: i Σ i !in (x; p) : i ( A i ) ⊢ x⟨ y⟩ | !x ( z).R :: x : ( A j ), w : A ′j , i Σ i par
and replacing it in δ by the following derivation γ ′ yields a valid derivation for Q with exactly one less applications of rules. As in the former case, contexts are preserved except the name x loses one intersection in its type, hence all the other applications of rules present in δ remain valid.

⊢ R{ y/ z} ::

w : A ′j out ε (x; p) : i j ( A i ) ⊢ R{ y/ z} | !x ( z).R :: x : ( A j ), w : A ′j , i j Σ i par where ε is γ 1 . . . . ⊢ R :: z : A 1 , Σ 1 • • • γ j-1 . . . . ⊢ R :: z : A j-1 , Σ j-1 γ j+1 . . . . ⊢ R :: z : A j+1 , Σ j+1 • • • γ n . . . . ⊢ R :: z : A n , Σ n (x; p) : i j ( A i ) ⊢ !x ( z).R :: i j Σ i !in

□

Corollary 3.8. A process P is typable iff there exists an idle process I such that P -→ * I .

Proof.

(if) Suppose there exists an idle process I such that P -→ * I . Then, since I is typable by Proposition 3.6, P is itself typable by subject expansion in Proposition 3.6. (only if) Suppose P is typable by a derivation δ . By quantitative, existential subject reduction in Proposition 3.6, there exists a reduction sequence

P -→ Q 1 -→ • • • Q k where each Q i is
typable for 1 ≤ k, the last process Q k does not reduce, and k ≤ |δ |. Since a typable process is error-free by Proposition 3.6, Q k is a error-free irreducible process, i.e., idle. □ Lemma 3.9. Let P be completely typable and let P -→ Q. Then, Q is completely typable.

Proof. Let ρ : P -→ Q and σ : Q -→ * R. Then we have a sequence of reductions ρ; σ starting from P. Since P is completely typable, there exists a derivation δ that satisfies δ :: P and δ ▷◁ ρ. As in the proof of the existential subject reduction in Proposition 3.6, we can modify the derivation δ to another derivation δ ′ for Q. Since the modification only renames the rest of derivation, the prefixes appearing in redexes in σ still satisfy the condition in Definition 3.4, and hence δ ′ ▷◁ σ for any σ : Q -→ * R. □

Note that subject expansion of Proposition 3.6 is constructive: given ρ : P -→ * Q, every derivation ε :: Q induces a derivation ρ * (ε) :: P, which we call the pullback of ε along ρ.

Lemma 3.10 (pullback). Let ρ : P -→ * Q. Then, for all ε :: Q, ρ * (ε ) ▷◁ ρ.

Proof. Let ρ = σ ; σ ′ where σ : P -→ * Q ′ and σ ′ : Q ′ -→ Q, and let ε :: Q. The derivation for Q ′ we constructed from ε in the proof of subject expansion indeed matches σ ′ ; by induction on the length of ρ we obtain a derivation that matches the whole ρ that we take as ρ * (ε). □ Theorem 3.11. A process is completely typable iff it is well-behaved.

Proof.

(if) Let P be a well-behaved process and ρ : P -→ * Q be an arbitrary sequence of reductions. Since P is well-behaved, there must be an idle process I satisfying σ : Q -→ * I . By Proposition 3.6, I is typable by some derivation δ ; by Lemma 3.10, there exists a derivation σ * (δ ) that matches σ . By repeatedly applying Lemma 3.10 we obtain ρ * (σ * (δ )) that matches ρ; σ , and hence ρ. (only if) Let P be completely typable. Then for any sequence of reductions ρ : P -→ * Q, Q is also completely typable by Lemma 3.9, and thus Q is typable. By Proposition 3.6 Q is error-free, and there exists another sequence of reductions σ : Q -→ * R where R is irreducible; since σ ; ρ is also a sequence of reductions starting from P, R is also typable and hence error-free, i.e., idle. □

Examples

We now go back to the examples from Sect. 2.3 and look at them from the point of view of typing.

3.4.1 Functional Programming. In the case of functional programming, there is not much to be said: the encoding of a non-deterministic λ-term (or λµ-term) is such that no runtime error may ever arise, so good behavior reduces to termination of weak head reduction. Let us say that a term M may converge if M -→ * N for some (weak head) normal form N ; let us say that it may diverge if M -→ * Ω for some term Ω having no normal form. Our type system gives us the standard result expected from intersection types: a functional process is typable (resp. completely typable) iff its evaluation under weak head reduction may converge (resp. may not diverge, i.e., it is safe, in the terminology of Sect. 2.4).

Locks.

Consider the final process of Sect. 2.3.2, i.e., the lock together with the processes competing for it. We will now give a complete analysis of its possible type derivations. Let A 0 := ⊤, A i+1 := (A i ) ∧ A i . We saw above (just after the definition of type) that these are all types. We start by observing that we have for all m ∈ N.

Suppose now that we have, for all 1 ≤ i ≤ n,

⊢ Q i :: v : (), p : ⊤
that is, v is used as the subject of a nullary output in Q i (the lock release signal), p is not used in Q i and, for simplicity, we assume that Q i has no other free name (for instance, we may simply take Q i := v, i.e., Q i releases the lock as soon as it obtains it). We then have Note that, by syntax directedness and the type constraints on rules, these are all the type derivations for the lock with n processes. The derivations in which m = n are the most interesting: they match a full reduction to idle form, in which every P i has acquired the lock at some point and released it. The order in which the lock is acquired is given by the types A n , . . . , A 1 , A 0 . Indeed, channel p (the lock channel) has input type (()) in each P i (this is visible in the last derivation); note that, in the derivation typing L, there are n + 1 copies of Q in which p gets output type (()), and each of these copies of Q has some z : A j in its context, 0 ≤ j ≤ n. The possible lock-acquisition orderings correspond to the possible matchings of the i-th input type (()) typing P i with the j-th output type (()) typing the j-th copy of Q. The 0-th copy of Q, in which p : ( * ), corresponds to the last reduction Lock -→ νv (p⟨v⟩ | v.z⟨z⟩ | L) leading to the idle form after all P i 's have terminated.

⊢ Q i :: v : ()
3.4.3 Toy Operating System. Let us give another example of how very precise information about the behavior of processes may be extracted from typing derivations. To make things more understandable, we first consider a (drastically) simplified version of the toy operating system of Sect. 2.3.3:

SimpOpSys := !r .0 V (z) := νs (s | !s.(r | z⟨z⟩) | !s.0) SimpUser := νu (u⟨u⟩ | !u (z).V (z))
SimpOpSys offers just one service: receiving a łpingž on channel r . SimpUser pings the operating system indefinitely, and may decide at any time to log out. As we did for the lock process, we will now give a complete analysis of the behavior of the SimpOpSys/SimpUser system by means of a complete analysis of its type derivations.

First, for all m ∈ N, we have

⊢ 0 :: zero (r ; ) : () m ⊢ SimpOpSys :: !in
where, as in the previous section, () m stands for () ∧ • • • ∧ () m times. In fact, by syntax directedness, these are all the possible type derivations for SimpOpSys.

Before analyzing the simplified user, let us make a notational simplification: in par rules, we will discard unnecessary declarations of the form (x; ) : ⊤ or x : ⊤, writing which exhausts all possibilities for V (z). Besides syntax-directedness, the key point here is the final res rule, which forces the input and output type of s to match. Because of the presence of a single output particle s, the output type cannot be but (), hence the total arity of the two !in rules for !s.(r | z⟨z⟩) and !s.0 must add up to 1. This corresponds to the fact that the output s is matched to exactly one of the two inputs, and the other input is discarded (which is possible because it is a server).

For SimpUser, we get

⊢ u⟨u⟩ :: u : A n+1 out . . . . ⊢ V (z) :: z : A n , r : () . . . . . . . ⊢ V (z) :: z : A 1 , r : () . . . . ⊢ V (z) :: z : A 0 , r : ⊤ (u; r ) : A n+1 ⊢ !u (z).V (z) :: r : () n !in (u; r ) : A n+1 ⊢ u⟨u⟩ | !u (z).V (z) :: r : () n , u : A n+1 par ⊢ SimpUser :: r : () n
res which exhausts all possibilities because of the above discussion and because, again due to the last res rule, the input and output type of u must match and the only ways to type u⟨u⟩ are with u : A n+1 for n ∈ N, where A n is the same family of types considered in the above section, defined by

A 0 = ⊤, A i+1 = (A i ) ∧ A i and thus satisfying A n+1 = (A n ) ∧ • • • ∧ (A 1 ) ∧ (A 0 ).
Let us consider the simple case in which there is only one user. Thanks to the above, we have for all m, n ∈ N. Each of these derivations describes a possible behavior of the user/system process. The integer m corresponds to the number of times the user pings the system. The cases m < n match reductions in which the user has not yet logged out; when m ≥ n, the user has logged out and the idle form SimpOpSys has been reached. Similarly to the lock example, each typing of V (z) in a derivation of SimpUser is labelled by an integer 0 ≤ i ≤ n. The positive i's correspond to pings by the user: i = n is the first, i = n -1 the second and so on. The case i = 0 corresponds to the log out. Therefore, each derivation of the user/system process corresponds to an evolution in which eventually the user logs out; however, when m < n, such a log out operation is still in the future and the derivation only matches the first m pings.

A similar analysis may be performed for the toy operating system of Sect. 2.3.3. Without giving the details, we get (r 1 ; ) : (()) k 1 , . . . , (r n ; ) : (()) k n ⊢ OpSys :: and ⊢ User :: r 1 : B 1 , . . . , r n : B n where each B i is of the form (()) l i and at most one of them may have the form (()) l i ∧ ( * ). If there are m users, ranged over by j, we may write B j i for the above types. In analogy with the simplified case, we have:

• the number k i corresponds to the number of times the i-th service is invoked;

• for a given user j, the number l j i corresponds to the number of times the user invokes the i-th service;

• the presence of the type ( * ) in one of the B j i 's corresponds to the fact that user j has not yet logged out and that the user's last request was for the i-th service;

• as in the lock example, the order in which requests from the different users are met by the operating system may be inferred by the presence of types of the form A i in the derivation. The details are slightly more complex (the derivations are bigger) but the essence is identical, which is why we do not give them as they would not add much to the understanding of the type system. The point is that, in certain cases, it is possible to perform a complete analysis of the type derivations of a process, a task which is facilitated by the syntax-directedness of the type system. From such an analysis, a complete description of the behavior of a process may be inferred.

DISCUSSION

Where does our type system come from? The type system presented here was not łpulled out of a hatž but obtained from a recently introduced construction [START_REF] Mazza | Polyadic approximations, fibrations and intersection types[END_REF], which is based on the idea that intersection types come from approximations in linear logic. In a nutshell, one of the main consequences of the construction is that a programming language has an łintersection-flavoredž type discipline as soon as it may be meaningfully translated in linear logic. For instance, Mazza et al. show how every major system of intersection types for the λ-calculus arises from applying their construction to Girard's translation of intuitionistic logic (and hence the λ-calculus) in linear logic.

It is known that the π -calculus may be translated in linear logic: several encodings and correspondences were proposed in the past decade or so [START_REF] Caires | Session Types as Intuitionistic Linear Propositions[END_REF][START_REF] Ehrhard | Interpreting a Finitary Pi-Calculus in Differential Interaction Nets[END_REF][START_REF] Honda | An exact correspondence between a typed pi-calculus and polarised proof-nets[END_REF][START_REF] Wadler | Propositions as sessions[END_REF]]. For our work, we turned to Honda and Laurent's correspondence, but amended it in the light of Ehrhard and Laurent's encoding, which is more liberal (for instance, Honda and Laurent consider the private π -calculus and restrict to replicated input only, while no such restrictions are present in our case). The resulting encoding of the π -calculus in linear logic (using proof nets) is described in [de Visme and Mazza 2017]. Our type system results by applying, in a nearly automatic way, the construction of [START_REF] Mazza | Polyadic approximations, fibrations and intersection types[END_REF] to this latter encoding. Albeit that work also contains a general theorem for inferring dynamic properties from the type systems built by the construction, the assumptions of the theorem do not cover concurrent languages like the π -calculus, so we had to prove our results łby handž (in light of Sect. 2.4, it was impossible to be otherwise). Nevertheless, we think that this is a nice application of the methodology brought forth by that work: we would not have been capable of coming up with our type system without the help of the above-mentioned construction.

Why asynchronous hyperlocalized? The choice of π -calculus fragment in our work is dictated by its connection with polarized linear logic [START_REF] Honda | An exact correspondence between a typed pi-calculus and polarised proof-nets[END_REF]. Let us try and give as much intuition as possible about the two restrictions (asynchrony and hyperlocalization), knowing that a fully technical explanation is impossible without introducing proof nets.

When encoding the π -calculus in linear logic, π -calculus reduction is simulated by shallow proof net reduction (also known as surface reduction in linear λ-calculi [START_REF] Simpson | Reduction in a Linear Lambda-Calculus with Applications to Operational Semantics[END_REF]). The concept of łshallownessž comes from the syntax of proof nets, which includes certain constructs called łboxesž, associated with the exponential modality !(-) and marking sub-proof nets that may be duplicated or erased. Shallow reduction never reduces inside a box. This is reminiscent of weak reduction in the λ-calculus, which does not reduce under an abstraction. Boxes are therefore a natural way of encoding the blocking behavior of prefixes in the π -calculus, i.e., the fact that π .P does not reduce even if P may reduce. Recall however that a box is associated with the modality !(-); so, if one kind of prefix (input or output) is associated with the presence of a box, then it will be associated with !(-), which implies that the dual kind of prefix will be associated with ?(-), which does not come with a box. Therefore, matching input/output duality with linear logical duality forces one prefix to be blocking and the other to be non-blocking; since it makes little sense for input to be non-blocking, this leads straight to the asynchronous π -calculus.

Locality is a consequence of polarization. Like [START_REF] Honda | An exact correspondence between a typed pi-calculus and polarised proof-nets[END_REF], we are using an encoding of the π -calculus in the polarized fragment of linear logic. This forces all names of y in a prefix like x ( y) to be of the same polarity, opposite to that of x. Since polarities coincide with the input/output distinction, we have that y must be composed of output names.

Hyperlocalization is a bit more technical and is a sort of łcollateral damagež of the use of boxes in the encoding of input prefixes. Indeed, in the encoding of x ( y).P (or !x ( y).P), the encoding of P must be put łinside a boxž; however, not every proof net may be put łinside a boxž: its conclusions (corresponding to the free names of P) must all be of negative polarity, and this happens to be the output polarity, hence the restriction.

It is natural to ask whether these restrictions may be overcome, typically by changing the encoding of the π -calculus in proof nets. This is trickier than what it seems. For what concerns hyperlocalization, there appears to be no alternative to the use of a box in encoding !x ( y).P; for the reasons mentioned above, this inevitably leads to the restriction that no free name of P be used as subject of an input. The case of non-replicated input prefixes looks simpler to amend, but the fact that such prefixes are blocking still strongly suggests the use of boxes, leading to the same obstruction.

About lifting the asynchronous restriction, an obvious solution to encode synchronous communication would be to associate a combination of modalities with each prefix, something like !?(-) (and its dual ?!(-)), in such a way that a box is always present, so that both prefixes are blocking. Although possible in principle, this has the disadvantage of propagating the hyperlocality restriction to output prefixes, i.e., in x⟨ y⟩.P, the free names of P would be limited to output use only. Also, it is likely that, in such an encoding, the sequence y above would be forced to contain names used only as subjects of input prefixes. That this is not the case at present is precisely thanks to asynchrony. All these induced restrictions make it unclear whether we may meaningfully deal with a synchronous setting.

What have we achieved and where to go from here? To the best of our knowledge, this is the first application of intersection types to concurrency which is comparable, in terms of results, to the traditional applications of intersection types to functional programming, in the sense the we get a system which is both sound and complete for a given behavioral property. In particular, our type system characterizes łmay terminationž. Granted, this is not a very useful property in a concurrent setting, but no other type system that we are aware of achieves this (i.e., completeness).

The interesting property, good behavior, is hopelessly out of reach for a type system to capture, at least if we consider the usual meaning of łcapturingž (i.e., by means of existence of a type). In this respect, our type system is the best we can get: although no single, finite type derivation may ever capture good behavior, it does capture a fraction of it, and our type system is complete in the sense that it misses none of these fractions.

The theoretical limitation of Sect. 2.4 (Π 0 2 -completeness) and Theorem 3.11 together make our type system unsuitable for practical usage, which of course is not a problem in present context since we are interested in a theoretical exploration of the limits of intersection types for concurrent programming. However, it is important to observe that this does not prevent our work from having a potential impact on more practical investigations. Indeed, as Sect. 3.4 has hopefully shown, there are non-trivial cases in which it is possible to completely describe the type derivations for a process, which amounts to completely describing its behavior. Such a description could be a form of parametric derivation: in the examples of Sect. 3.4, the parameters were integers, but one may imagine more complex structures. This leads us towards a type discipline in the style of bounded linear logic [START_REF] Girard | Bounded linear logic: a modular approach to polynomial-time[END_REF], which is known to be related to intersection types (via the notion of approximation considered in [START_REF] Mazza | Polyadic approximations, fibrations and intersection types[END_REF]). More precisely, it seems that a similar application of (linear) dependent types as that given by [START_REF] Dal | Linear Dependent Types and Relative Completeness[END_REF] is possible here, which would yield more practical type systems, necessarily sacrificing completeness but hopefully still of remarkable expressiveness.

Another, perhaps more technical contribution of our work is that it clarifies the meaningfulness of encodings of π -calculi in linear logic. Indeed, it was shown that, for abstract reasons due to the absence of so-called confusion in differential proof nets (the target of both encodings of [START_REF] Ehrhard | Interpreting a Finitary Pi-Calculus in Differential Interaction Nets[END_REF][START_REF] Honda | An exact correspondence between a typed pi-calculus and polarised proof-nets[END_REF]), no encoding fully respecting the parallelism of the π -calculus could possibly be sound. Accordingly, the encoding at the basis of our work [de Visme and Mazza 2017] is syntactically unsound: if • denotes the encoding, there are processes P such that P may exhibit reductions having no match in P. However, thanks to the hyperlocalization restriction, it turns out that these łfaultyž reductions may only happen when P is already łfaultyž on its own, i.e., when it has no idle form. By Corollary 3.8, P is not typable, so the encoding is morally correct. This property is similar to that expressed by Proposition 2.8 and may be proved along the same lines.

One more thing worth noting is that the construction of [START_REF] Mazza | Polyadic approximations, fibrations and intersection types[END_REF], which is based on approximations, is in fact also related to the Taylor expansion of differential linear logic and its relational semantics. This is visible in our types, which are essentially the elements of the relational semantics of proof nets. From this perspective, another way of stating that the lack of correctness of the proof net encoding is harmless is that łfaultyž reductions only happen in proof nets/processes whose semantics is empty. More generally, the connection with denotational semantics, especially that with (linear) approximations, is another topic worth investigating further. Finally, connections between our type system and Girard's Geometry of Interaction [START_REF] Girard | Geometry of Interaction I: interpretation of System F[END_REF]] are worth being investigated, especially in view of some recent developments [START_REF] Dal Lago | The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens[END_REF]].

  , y : C out ⊢ P :: y : A, z : C w : ⊤, (x; out(P ) \ y) : ( A) ⊢ x ( y).P :: z : C in z contains at least fn(P ) \ y w : ⊤, (x; out(P ) \ y) : * ⊢ x ( y).P :: z : ⊤ in * ⊢ P :: y : A 1 , z : C 1 . . . ⊢ P :: y : A k , z : C k w : ⊤, (x; out(P ) \ y) :

Fig. 1 .

 1 Fig. 1. Typing rules.

  (x; ) : ⊤ ⊢ x⟨a⟩ :: a : (), b : ⊤, x : (()) out (x; ) : ⊤ ⊢ x⟨b⟩ :: a : ⊤, b : (), x : (()) out δ ′ (x; z) : (()) ∧ (()) ⊢ x⟨a⟩ | x⟨b⟩ | !x (z).z :: a : (), b : (), x : (()) ∧ (()) par ⊢ νx (x⟨a⟩ | x⟨b⟩ | !x (z).z) :: a : (), b : () res where the double bar indicates several applications of the par rule and δ ′ is the following derivation: ⊢ z :: z : (), a : ⊤, b : ⊤, x : ⊤ out ⊢ z :: z : (), a : ⊤, b : ⊤, x : ⊤ out (x; z) : (()) ∧ (()) ⊢ !x (z).z :: a : ⊤, b : ⊤, x : ⊤ !in

⊢

  a⟨a⟩ :: a : A n out for all n > 0. Let now Q := νv (p⟨v⟩ | v.z⟨z⟩), so that L = !a(z).Q. We have, for all n > 0(v; ) : ⊤ ⊢ p⟨v⟩ :: z : ⊤, p : (()), v : () out ⊢ z⟨z⟩ :: z : A n , p : ⊤, v : ⊤ out (v; z) : () ⊢ v.z⟨z⟩ :: z : A n , p : ⊤, v : ⊤ in (v; z) : () ⊢ p⟨v⟩ | v.z⟨z⟩ :: z : A n , p : (()), v : () par ⊢ Q :: z : A n , p : (())res and we also have (v; ) : ⊤ ⊢ p⟨v⟩ :: z : ⊤, p : ( * ), v : * out (v; z) : * ⊢ v.z⟨z⟩ :: z : ⊤, p : ⊤, v : ⊤ in * (v; z) : * ⊢ p⟨v⟩ | v.z⟨z⟩ :: z : ⊤, p : ( * ), v : * par ⊢ Q :: z : ⊤, p : ( * ) res Now, note that, for all m ∈ N, A m+1 = (A m ) ∧ • • • ∧ (A 1 ) ∧ (A 0 ), and recall that A 0 = ⊤. Thanks to this observation, we have ⊢ Q :: z : A m , p : (()) . . . ⊢ Q :: z : A 1 , p : (()) ⊢ Q :: z : A 0 , p : ( * ) (a; p) : A m+1 ⊢ L :: p : (()) m ∧ ( * ) !in Proc. ACM Program. Lang., Vol. 3, No. POPL, Article 7. Publication date: January 2019. Intersection Types and Runtime Errors in the Pi-Calculus 7:23 for all m ∈ N, where (()) m is short for (()) ∧ • • • ∧ (()) m times. Combining the above, we get ⊢ Lock :: p : (()) m ∧ ( * )

  , p : ⊤ (p; ) : (()) ⊢ P i :: p : ⊤ in so we finally obtain (p; ) : (()) ⊢ P 1 :: p : ⊤ . . . (p; ) : (()) ⊢ P n :: p : ⊤ (p; ) : ⊤ ⊢ Lock :: p : (()) m ∧ ( * ) (p; ) : (()) n ⊢ P 1 | • • • | P n | Lock :: p : (()) m ∧ ( * ) par

  (x; X ) : A ⊢ P :: z : C ⊢ Q :: y : B, z : D (x; X ) : A ⊢ P | Q :: y : B, z : C ∧ D par instead of (x; X ) : A ⊢ P :: y : ⊤, z : C (x; ) : ⊤ ⊢ Q :: y : B, z : D (x; X ) : A ⊢ P | Q :: y : B, z : C ∧ D par which is the łofficialž version of the rule given in Fig. 1. The łcompactž version of the rule is of course admissible because declarations of the form (x; ) : ⊤ or x : ⊤ may be added at will to derivable judgments, preserving derivability (this is a standard property provable by induction). So, for the simplified user, we have ⊢ s :: s : () out ⊢ r :: r : () out ⊢ z⟨z⟩ :: z : A n+1 out ⊢ r | z⟨s⟩ :: z : A n+1 , r : () par (s; z, u) : () ⊢ !s.(r | z⟨s⟩) :: z : A n+1 , r : () !in (s; ) : ⊤ ⊢ !s.0 :: !in (s; z, r ) : () ⊢ s | !s.(r | z⟨z⟩) | !s.0 :: z : A n+1 , r : (), s : () par ⊢ V (z) :: z : A n+1 , r : () res and we also have ⊢ s :: s : () out (s; z, u) : ⊤ ⊢ !s.(r | z⟨s⟩) :: z : A 0 , r : ⊤ z, r ) : () ⊢ s | !s.(r | z⟨z⟩) | !s.0 :: z : A 0 , r : ⊤, s : () par ⊢ V (z) :: z : A 0 , r : ⊤ res

  (r ; ) : () m ⊢ SimpUser | SimpOpSys :: r : () n

Proc. ACM Program. Lang., Vol. 3, No. POPL, Article 7. Publication date: January 2019.

ACKNOWLEDGMENTS

This work was partially supported by ANR grants Elica (ANR-14-CE25-0005) and Repas (ANR-16-CE25-0011), and INRIA/JSPS EA Crecogi.

Definition 3.5 (Complete Typability). A process P is completely typable if, for all ρ : P -→ * Q, there exists δ :: P such that δ ▷◁ ρ.

Note that complete typability implies typability: simply let ρ be the identity reduction on P.

Complete Typability Captures Good Behavior

This Section is technically the most relevant of the present paper, proving that complete typability is a necessary and sufficient condition for well-behaved processes. The first step towards our goal is to prove four key properties of our type systems. On the one hand, idle are typable, while typable processes are necessarily error-free. On the other hand, typability is preserved by anti-reduction, and (only existentially) by reduction. In what follows, we write |δ | for the size of a derivation (number of rules in it).

Proposition 3.6. The type system enjoys the following properties: Idle Typability: idle processes are typable; Error-Freedom: a typable process is error-free; Subject Expansion: if P is typable and Q -→ P, then Q is also typable; Quantitative, Existential Subject Reduction: given δ :: P with P reducible, there exists ρ : P -→ Q with δ ▷◁ ρ and there exists a derivation ε ::

Proof. We prove each of the four properties separately: Idle Typability.

be an arbitrary idle process (l, m, n may be 0). It suffices to give one derivation for P; we always have the following derivation. where par * is a repeated application of par rule, each γ i is

, and contexts in ε i 's are as in the explanation after Fig. 1. Error-Freedom. It suffices to show that any process with a runtime error (arity mismatch, dependency cycle, failed send, or endless wait) is untypable. Arity mismatch is untypable by the definition of types: the rules out, in, in * , and !in necessarily introduce pre-types with one or more tuples with the same arity as the input/output prefix. If arity mismatch is in a process, then a name in the context must be typed by a pre-type A that does not satisfy A ⌢ A since some sub-pre-types of A have different arity.

A dependency cycle at the top level is not typable. Because any such process contains a subprocess in the form

where †x i ( y i ) denotes either

, the rules in (or in * ) and !in that derive those input particles necessarily introduces (x 1 ; x n , p 1 ) and (x i ; x i-1 , p i ) for 1 < i ≤ n. It is easy to show that res rule on all x 1 , . . . , x n over such a subprocess †x 1 ( y

) is directly prohibited by the side-condition of res rule; when we have (x 1 ; x n , p 1 ) : A 1 , (x 2 ; x 1 , p 2 ) : A 2 , . . . , (x n ; x n-1 , p n ) : A n in a context, applying res rule on (without loss of generality) x n , we will obtain (x 1 ; x n-1 , p n , p 1 ) : A 1 , (x 2 ; x 1 , p 2 ) : A 2 , . . . , (x n-1 ; x n-2 , p n-1 ) : A n-1 that is impossible to apply res rule over x 1 , . . . , x n-1 by I.H. Failed send cannot be typed because a typing derivation for a failed-send process must contain a subderivation that types a process

Q n :: Σ, with the name x contained in the two contexts Γ and Σ.

Each application of in rule for x ( y i ).Q i necessarily types x by a non-⊤ type in the context Γ; however x in the context Σ can only be typed by ⊤, hence the types of x in Γ and that in Σ never match and res rule cannot be applied. Subject Expansion. Suppose Q is typable and ρ : P -→ Q.

• If the reduction is by the rule x⟨ y⟩ | x ( z).R -→ R{ y/ z}, by the syntax-directedness the derivation (call it δ ) for Q must contain a subderivation δ ′ in the following form:

Since R is inside an input particle in the redex, R does not have a free occurrence of input particle and thus Γ can only contain ⊤ types. Since the redex and the reduct are given by the reduction, we know every output prefixes v i ⟨ w i ⟩ that is renamed under the reduction ρ, and thus we can spot all the sub-derivations

where Γ i only contains ⊤ types and the subderivation is associated with a sequence of types B i and a function f : {1, . . . , |w i |} → {u i 1 , . . . , u i m } that designates the types A i , C i 1 , . . . , C i m . Some of the names v i , u i 1 , . . . , u i m have been renamed under ρ; consider the set X = {u ′i 1 , . . . , u ′i l } that is defined by

y and the occurrence of z j is renamed by y j in v i ⟨ w i ⟩ under ρ and define f ′ : {1, . . . , |w i |} → {u ′i 1 , . . . , u ′i l } by f ′ (j) = f (j) if the j-th occurrence of name in y is not renamed under ρ; f ′ (j) = z j if the j-th occurrence of name in z is renamed by y j under ρ.

Using f ′ and erasing Γ i , we obtain the following subderivation: ⊢ Anc(v i ⟨ w i ⟩) :: u ′i 1 : C ′ 1 , . . . , u ′i l : C ′ l out where C ′ j 's are as specified by B and f ′ . Here Γ i must be erased because we later apply a in rule; it can be safely erased since all the types in Γ i are ⊤, which means that Γ i is introduced by (co)weakening. Let γ ′ be a derivation obtained by replacing every such subderivation in δ ′ . Note that such a replacement makes z i 's appear in the contexts. Then we have


S Chaigne

A Maitre

B Arab-Chapelet

come

Oxydes d'actinides à façon pour la fabrication de combustibles nucléaires de Génération IV

Oxydes d'actinides à façon pour la fabrication de combustibles nucléaires de Génération IV

Nom, Prénom : Chaigne Séverin Contrat : CTBU Responsable CEA : Bénédicte Arab-Chapelet Organisme co-financeur : ANR Directeur universitaire : Alexandre Maître Université d'inscription : Limoges Laboratoire d'accueil : IRCER (Limoges) / LPCA Ecole doctorale : SIMME (n°522) Date de début de thèse :22/10/2015

Master : Sciences des matériaux

-----------------------------------------------------------------------------------------------------------------------------------------------

I. Contexte de l'étude

Contexte

Cette étude s'inscrit dans le cadre des recherches menées sur le traitement-recyclage des combustibles nucléaires du futur et, plus précisément, sur la fabrication de nouveaux combustibles sous forme de pastilles à partir de poudres d'oxydes à base d'actinides de différentes morphologies. Différents procédés de conversion sont envisagés pour la synthèse d'oxydes d'actinides à partir de l'uranium et du plutonium issus du traitement des combustibles usés. Plusieurs études menées au CEA sur le procédé de conversion par voie oxalique ont permis d'aboutir à des oxalates et à des oxydes d'actinides de morphologies très variées en fonction des paramètres de précipitation.

Objectifs

Dans ce contexte, l'objet de cette étude vise à évaluer l'aptitude à la mise en forme et au frittage de poudres d'oxydes d'actinides présentant différentes compositions chimiques, morphologies et textures poreuses. Dans un premier temps, il s'agit de travailler sur différents lots de poudres d'oxyde de cérium (CeO 2 ) généralement utilisés comme analogues non radioactifs des actinides d'après des propriétés physicochimiques assez similaires (e.g. rayon ionique, structure cristallographique, …). Une étude comparative du comportement de lots de poudre de différentes morphologies (i.e. forme, degré d'agglomération ou d'agrégation) a été menée lors des étapes de mise en forme et de frittage naturel. Afin de mettre plus facilement en exergue l'effet des paramètres morphologiques des matières premières, les travaux préliminaires se sont orientés vers l'utilisation d'une méthode de mise en forme conventionnelle, à savoir le pressage uniaxial, suivie par une étape de frittage naturel sous air. Les études suivantes vont se focaliser sur le développement d'un procédé innovant de mise en forme dans le domaine d'application nucléaire. Ce procédé devra permettre d'améliorer l'homogénéité de l'arrangement des particules au sein du combustible mais aussi de réduire le risque de propagation de poussières radioactives et de fabriquer des combustibles de géométrie annulaire.

II. Résultats et perspectives

Résultats

Une poudre commerciale et une poudre synthétisée par précipitation oxalique de CeO 2 ont été utilisées pour la mise au point du procédé de coulage-gélification. Des études préliminaires ont montré des aptitudes à la mise en forme et au frittage distinctes fonction de la morphologie initiale des poudres, de leur état d'agréation, de la densité à cru et de la distribution en taille de pores. Par exemple, l'agrégation des particules de CeO 2 résultant de la précipitation oxalique inhibe la capacité de compactage au cours du pressage et entraîne un frittage différentiel. Il serait pertinent d'améliorer les caractéristiques initiales de la poudre grâce à une étape de désagglomération afin d'obtenir un cru homogène en terme de taille de grains et de pores. C'est dans ce sens que le procédé de coulage-gélification a été choisi. Une suspension céramique est consolidée dans un moule non poreux de forme plus ou moins complexe suite à un processus de gélification induit par une réaction de polymérisation. Une pièce crue solide constituée de particules céramiques emprisonnées dans un réseau polymérique est ainsi obtenue. Ces additifs organiques sont ensuite éliminés lors d'une étape de déliantage à température modérée (i.e. T < 800°C). Ce procédé permet la fabrication de pièces de forme complexe et de microstructure (densité relative et taille de grains) contrôlée. Sur la base de formulations gélifiantes issues de la littérature, les étapes-clés du procédé ont été étudiées, notamment : (1) la stabilisation des suspensions, (2) l'initiation de la gélification et (3) l'évolution des caractéristiques microstructurales et dimensionnelles des pièces crues en fonction des traitements thermiques (séchage, déliantage, frittage). La mise en oeuvre du procédé s'est avérée concluante sur une poudre commerciale de CeO 2 . La suite du travail s'est focalisée sur une poudre de cérine synthétisée par précipitation oxalique. Après une phase d'adaptation des caractéristiques morphologiques des poudres synthétisées et du procédé de mise en forme, des pièces de forme complexe ont pu être élaborées. La transposition à une poudre d'oxydes mixtes (U,Ce)O 2 a ainsi pu être initiée et a permis de fabriquer les premières pastilles annulaires.

Perspectives

Les travaux actuels s'orientent sur l'optimisation du traitement de frittage de la poudre synthétisée par précipitation oxalique afin d'obtenir densité relative supérieure à 95%. Parallèlement, l'étude du comportement sous irradiation des différents réactifs mis en oeuvre dans ce procédé innovant a été effectuée à partir d'essais d'irradiation interne (incorporation de poudre à base de 238 Pu) et externe (irradiation par rayonnement alpha). Cette étude a permis de montrer que le rayonnement n'avait a priori pas d'effet néfaste sur le processus de gélification.

Document propriété du CEA -Reproduction et diffusion externes au CEA soumises à l'autorisation de l'émetteur