Franco Barbanera

Mariangiola Dezani-Ciancaglini

Ivan Lanese
email: ivan.lanese@gmail.com

Emilio Tuosto
email: emilio.tuosto@gssi.it

Composition and Decomposition of Multiparty Sessions

Multiparty sessions are systems of concurrent processes, which allow several participants to communicate by sending and receiving messages. Their overall behaviour can be described by means of global types. Typable multiparty sessions enjoy lock-freedom.

We look at multiparty sessions as open systems by allowing one to compose multiparty sessions by transforming two of their participants into a pair of coupled gateways, forwarding messages between the two sessions. Gateways need to be compatible. We show that the session resulting from the composition can be typed, and its type can be computed from the global types of the starting sessions. As a consequence, lock-freedom is preserved by composition. Compatibility between global types is necessary, since systems obtained by composing sessions with incompatible global types have locks (or they are not sessions). We also define direct composition, which allows one to connect two global types without using gateways. Finally, we propose a decomposition operator, to split a global type into two, which is the left inverse of direct composition. Direct composition and decomposition on global types prepare the ground for a novel framework allowing for the modular design and implementation of distributed systems.

Introduction

Distributed systems are seldom developed as independent entities. Indeed, in many cases they should be considered as open entities ready for interaction with an environment. Composition may be specified either statically, for a fixed environment, or dynamically, if the environment only becomes known upon deployment. In general, it is fairly natural to expect to connect open systems as if they were composable modules, and in doing that one should rely on "safe" methodologies and techniques, guaranteeing the composition not to "break" any relevant property of the single systems.

In [START_REF] Barbanera | Global Types for Open Systems[END_REF] a methodology has been proposed for the composition of systems, consisting in replacing any two participants (one per system) -if their behaviours are "compatible" -by a pair of coupled forwarders, dubbed gateways, enabling the two systems to exchange messages. In this approach, the behaviour of any participant can be looked at as an interface. In this setting, the notion of interface is interpreted not as the description of the interactions "offered" by a system but, dually, as those "required" by a possible environment (usually another system).

A convenient way to tackle the complexity of message-passing applications is by means of global specifications. The idea is to devise an abstract representation of the system, the so-called global view, that can be used as the blueprint for the realisation of each participant. A neat formalisation of this idea are MultiParty Session Types (MPSTs), introduced in [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF][START_REF] Honda | Multiparty Asynchronous Session Types[END_REF]. The global view is rendered in MPSTs as a global type meant to capture the interactions among the participants of the protocol. We illustrate, by means of a simple example, how the general idea of composition of systems by gateways can be exploited in the setting of MPTSs.

Let us assume to have System 1 formed by two participants, Alice and Bob, where Alice sends Bob a request for some advice and receives back either the advice asked for or an apology (sorry) for not being of any help. Let us also assume to have System 2, with participants Carol and Donald, where Carol sends a message req to Donald who surely replies with an advice, since, in case he does not know what to say, he provides one good for any occasion. Figure 1 shows the UML-like diagrams (following the intuitive notation introduced in [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF]) of Systems 1 and 2, where the curly bracket is used to group possible choices. These diagrams yield the global views of our systems. The representation in terms of global types of these views is as follows:

G 1 =Alice → Bob : req.Bob → Alice : {adv.End, sorry.End} G 2 =Carol → Donald : req.Donald → Carold : adv.End

Notice how G 1 and G 2 give a faithful textual representation of the diagrams in Figure 1. An advantage of global types is that they can be equipped with a precise semantics that allows one to verify if a realisation is correct with respect to the specification. For instance, the interaction behaviour of (a realisation of) Bob and of Carol can be specified respectively as:

Alice?req.Alice!{adv, sorry} and Donald!req.Donald?adv [START_REF] Barbanera | Global Types for Open Systems[END_REF] where ? means input, ! means output and between curly brackets we put possible input or output choices (those for input corresponding to external choices and those for output to internal choices).

Let us now think of System 1 and System 2 as open systems. Then, rather than looking at Bob and Carol as actual participants, we can consider them as interfaces. More precisely, the realisations in [START_REF] Barbanera | Global Types for Open Systems[END_REF] represent the behaviour of advice-providing and advice-requesting interfaces of systems to which System 2 and System 1, respectively, are willing to connect. Since any request can be satisfied 4 , System 1 and System 2 can be connected by simply replacing participants Bob and Carol, respectively, by the following "forwarding" processes (dubbed gateways): Notice that Bob's option of sending an apology is never used, since Donald never activates it, hence it will disappear from the global type describing the composition of G 1 and G 2 using Bob and Carol as gateways:

G 1 Bob↔Carol G 2 =
Alice → Bob : req.Bob → Carol : req.Carol → Donald : req. Donald → Carol : adv.Carol → Bob : adv.Bob → Alice : adv

Figure 2 shows the UML-like diagram corresponding to the above global type. In [START_REF] Barbanera | Global Types for Open Systems[END_REF] it is shown that, by connecting systems of Communicating Finite State Machines (CFSMs) [START_REF] Brand | On Communicating Finite-State Machines[END_REF] as shown above, many relevant properties of communication, such as deadlock freedom, are preserved. One of the contributions of the present paper is to provide a choreography formalism enabling the "lifting" of the composition-by-gateways approach in [START_REF] Barbanera | Global Types for Open Systems[END_REF] from systems to protocol descriptions, represented as MPSTs. More precisely, we define a function that, given two MPSTs and two participants (one per MPST) to be used as interfaces, computes the MPST of the composed system, as informally shown above in the G 1 Bob↔Carol G 2 example. This allows one to lift to the composed system all the guarantees on the soundness of communication provided by the chosen MPST formalism.

In our formalism, in particular, typable systems are guaranteed to be lockfree [START_REF] Kobayashi | A Type System for Lock-Free Processes[END_REF]. Hence, the systems obtained by composing typable systems are lockfree too. Beyond this, the global type of the composed system also provides a global view of the new system. Both the benefits are direct consequences of one of our main contributions: the function from the global types of the original systems to the global type of the system obtained by the composition outlined above.

We remark that our approach does not change the syntax of the chosen MPST approach, but allows one to look at it as a formalism to describe open systems (while MPSTs normally describe only closed systems).

While the idea of the approach is rather general, not all MPST formalisms in the literature are suitable for its application. For instance, the requirements imposed by the type system in [START_REF] Coppo | Global Progress for Dynamically Interleaved Multiparty Sessions[END_REF] are too strong for the gateway processes to be typed, thus we could not get any guarantee on the result of the composition.

In the present paper we apply the approach in a setting as simple as possible (inspired by [START_REF] Severi | Observational Equivalence for Multiparty Sessions[END_REF]), to highlight its features and avoid non intrinsic complexity. In particular, the simplicity of the calculus allows us to get rid of channels and local types. Moreover, as discussed in Section 11, our treatment of infinitary computations avoids the hindering issues caused by a syntactic description of recursion.

In order to ensure the correctness of composition, we appeal to interface compatibility, a condition on the two participants chosen as interfaces. We show that the compatibility relation used in [START_REF] Barbanera | Global Types for Open Systems[END_REF] can be relaxed to a relation closely connected to the observational preorder of [START_REF] Severi | Observational Equivalence for Multiparty Sessions[END_REF], in turn corresponding to the subtyping relation for session types of [START_REF] Gay | Subtyping for Session Types in the Pi Calculus[END_REF][START_REF] Demangeon | Full Abstraction in a Subtyped Pi-Calculus with Linear Types[END_REF]. In particular, in [START_REF] Barbanera | Global Types for Open Systems[END_REF] the interaction behaviour of Carol -in order to be compatible with Bob's one -should necessarily be Donald!req.Donald?{adv, sorry} (or Bob's should be Alice?req.Alice!adv). We show instead that the notion of compatibility can actually be relaxed so to allow our Bob and Carol in (1) to be compatible.

The notion of compatibility between global types is further investigated by showing it to be, not only a sufficient condition to get lock-freedom preservation under composition, but also a necessary condition.

The use of gateways enables a safe connection of systems by means of a minimal modification, corresponding to the transformation of interface participants into forwarders, while the other participants are unchanged. This property is quite important when composition happens dynamically. However this approach is less suitable when composition is performed statically, to support a modular design and development process. Indeed, in this case one would like to avoid the overhead due to gateways.

For instance, in our simple example, the composition of System 1 and System 2 could be obtained by "bypassing" the interface partecipants, so getting an MPST whose UML-like diagram is shown in Figure 3.

To formalise such an idea, we define a second function which performs direct composition (both at the level of global types and at the level of systems), that is composition not mediated by gateways. One can see direct composition as a simplification of composition by gateways, where the behaviour of gateways is internalised in the participants willing to communicate with the other system, hence gateways are no more needed. Of course, this approach requires some (limited) changes to the other participants of the systems to be composed. Moreover, we complement direct composition with an operation of decomposition, which is, on global types, its left inverse. Decomposition allows one to take a typed MPST and split its participants into two groups (to each group an interface participant is also added), thus creating two MPSTs. A MPST with the original global type can be recovered by direct composition. For example the decomposition of the system with the UML-diagram of Figure 3 In the standard subtyping for session types supertypes have less inputs and more outputs than their subtypes [START_REF] Demangeon | Full Abstraction in a Subtyped Pi-Calculus with Linear Types[END_REF]. In our type system we use a preorder on processes in which larger processes have less inputs than smaller ones, but the same outputs. This allows us to get: (i) a stronger notion of session fidelity, (ii) a better correspondence between composition by gate-ways at the level of multiparty sessions and the one at the level of global types, (iii) the necessity of compatibility between global types to ensure that lock-freedom is preserved under composition. Besides, we show that such a restriction does not change the class of multiparty sessions that can be typed (but may change the types assigned to them).

Outline. Sections 2, 3 and 4 respectively introduce our calculus of multiparty sessions, their global types, and prove the properties that well-typed sessions enjoy. Sections 5 and 6 define the compatibility relation and the composition via gateways for sessions and global types, respectively. The key result that sessions obtained from composition are typable (and hence lock free) is presented in Theorem 6.10. In Section 7 compatibility between global types is shown to be not only a sufficient, but also a necessary condition for lock-freedom of composition. Direct composition, allowing one to compose systems without the need for gateways, is defined in Section 8, where related properties are also discussed and proved. The decomposition operation, which complements the direct composition operation, is defined and investigated in Section 9. In Section 10 we discuss how all previous results change if we consider a preorder on processes mimicking the standard subtyping relation on session types, that allows larger processes to have more outputs than smaller ones. Section 11 concludes by a recap of the paper and by discussing related and future work.

Comparison with the workshop version. The present paper is a revised and extended version of [START_REF] Barbanera | Open Multiparty Sessions[END_REF]. The definition of the composition operation, first presented in [START_REF] Barbanera | Open Multiparty Sessions[END_REF], is considerably improved here, enabling us to simplify and make more readable also the proofs of most of the related results. This paper includes also a number of new contributions. First, we show that compatibility between global types is not only a sufficient, but also a necessary condition in order to get lock-freedom preservation for composition of typable multiparty sessions. Also, both the direct composition and the decomposition operations, and all the related results, are new. Lastly, in the workshop version we did not consider how the results change when the processes are compared using a preorder mimicking the standard subtyping.

Processes and Multiparty Sessions

We use the following base sets and notation: messages, ranged over by , , . . . ; session participants, ranged over by p, q, . . .; processes, ranged over by P, Q, . . . ; multiparty sessions, ranged over by M, M , . . . ; integers, ranged over by n, m, i, j, . . . . Processes implement the behaviour of participants. The input process p?{ i .P i | 1≤i≤n} waits for one of the messages i from participant p; the output process p!{ i .P i | 1≤i≤n} non-deterministically chooses one message i for some i, 1 ≤ i ≤ n, and sends it to participant p. We use Λ as shorthand for { i .P i | 1≤i≤n}. We define the multiset of messages in Λ as msg({ i .P i | 1≤i≤n}) = { i | 1≤i≤n}. After sending or receiving the message i for some i, the process reduces to P i . The set Λ acts as an external choice in p?Λ and as an internal choice in p!Λ. In a full-fledged calculus, messages would carry values, namely they would be of the form (v). For simplicity, we consider only pure messages. This agrees with the focus of session calculi, which is on process interactions that do not depend on actual transmitted values.

For the sake of abstraction, we do not take into account any explicit syntax for recursion. Rather, we consider processes as, possibly infinite, regular trees. Definition 2.1 (Processes). Let P range over the terms of the following grammar:

P ::= coinductive 0 | | p?Λ | | p!Λ Λ ::= { i .P i | 1≤i≤n}
where all messages in msg(Λ) are pairwise distinct. We call Λ a pre-choice and define the tree representation of P as the directed rooted tree such that (a) each internal node is labelled by p? or p! and has as many children as the number of messages (b) the edge from p? or p! to the child P i is labelled by i and (c) the leaves of the tree (if any) are labelled by 0.

The term P is a process if its tree representation is regular (namely, it has finitely many distinct sub-trees) and the pre-choice { i .P i | 1≤i≤n} is a choice of messages if P i is a process for all 1 ≤ i ≤ n.

The fact that the grammar for P has to be interpreted coinductively implies that infinite derivations are allowed. We identify processes with their tree representations and we shall sometimes refer to the trees as the processes themselves. The regularity condition implies that we only consider processes admitting a finite description. This is equivalent to writing processes with µ-notation and having an equality which allows for an infinite number of unfoldings. This is also called the equirecursive approach, since it views processes as the unique solutions of (guarded) recursive equations [START_REF] Pierce | Types and Programming Languages[END_REF]Section 20.2]. The existence and uniqueness of a solution follow from known results (see [START_REF] Courcelle | Fundamental Properties of Infinite Trees[END_REF] and [START_REF] Cardone | Recursive Types[END_REF]Theorem 7.5.34]). With such an approach, it is natural to use coinduction as the main logical tool, as we do in most of the proofs. In particular, we adopt the coinduction style advocated in [START_REF] Kozen | Practical Coinduction[END_REF] which, without compromising formal rigour, promotes readability and conciseness.

We define the set ptp(P ) of participants of process P by:

ptp(0) = ∅ ptp(p?{ i .P i | 1≤i≤n}) = ptp(p!{ i .P i | 1≤i≤n}) = {p}∪ptp(P 1 )∪ . . . ∪ptp(P n )
The regularity of processes assures that the set of participants is finite. We shall write .P Λ for { .P }∪Λ if ∈ msg(Λ), and Λ 1 Λ 2 for Λ 1 ∪Λ 2 if msg(Λ 1 )∩msg(Λ 2 ) = ∅. We shall also omit curly brackets in choices with only one branch, as well as trailing 0 processes. A multiparty session is the parallel composition of named processes, that is pairs participant/process. We define pts(p P ) = {p} and pts(M | M ) = pts(M) ∪ pts(M ).

Definition 2.2 (Multiparty Sessions

Operational Semantics. We assume to have a structural congruence ≡ on multiparty sessions, establishing that parallel composition is commutative, associative and has neutral elements p 0 for any fresh p.

The reduction for multiparty sessions allows participants to choose and communicate messages.

Definition 2.3 (LTS for Multiparty Sessions). The labelled transition system (LTS) for multiparty sessions is the closure under structural congruence of the reduction specified by the unique rule:

[comm] msg(Λ) ⊆ msg(Λ ) p q!( .P Λ) | q p?( .Q Λ ) | M p q --→ p P | q Q | M Rule [comm]
makes the communication possible: participant p sends message to participant q. This rule is non-deterministic in the choice of messages. The condition msg(Λ) ⊆ msg(Λ ) (borrowed from [START_REF] Barbanera | Compliance for Reversible Client/Server Interactions[END_REF][START_REF] Barbanera | Reversible Client/Server Interactions[END_REF]) assures that the sender can freely choose the message, since the receiver must offer all sender messages and possibly more. This allows us to distinguish in the operational semantics between internal and external choices. Note that this condition will always be true in well-typed sessions. For example, p q! | q p?{ , } p q --→ p 0 | q 0, while p q!{ , } | q p? is stuck, since participant p should be free of choosing to send message to participant q (p is making an internal choice), but q cannot receive this message.

We use M λ -→ M as shorthand for M p q --→ M for some p, q and . We sometimes omit the label, writing -→. As usual, -→ * denotes the reflexive and transitive closure of -→.

Example 2.4. Let us consider a system (inspired by a similar one in [START_REF] Barbanera | Global Types for Open Systems[END_REF]) with participants p, q, and h interacting according to the following protocol. Participant p keeps on sending text messages to q, which has to deliver them to h. After a message has been sent by p, the next one can be sent only if h has ascertained the propriety of language of the previous message, i.e if it does not contain, say, rude or offensive words. Participant h acknowledges to q the propriety of language of a received text by means of the message ack. In such a case q sends to p an ok message so that p can proceed by sending a further message. More precisely: 1. p sends a text message to q in order to be delivered to h, which accepts only texts possessing a good propriety of language;

p q h                text text nack notyet transf ack ok stop stop
2. then h either (a) sends an ack to q certifying the reception of the text and its propriety. In this case q sends back to p an ok message and the protocol goes back to step 1, so that p can proceed by sending a further text message;

(b) sends a nack message to inform q that the text has not the required propriety of language. In such a case q produces transf (a semantically invariant reformulation of the text), sends it back to h and the protocol goes to step 2 again. Before doing that, q informs p (through the notyet message) that the text has not been accepted yet and a reformulation has been requested;

(c) sends a stop message to inform q that no more text will be accepted. In such a case q informs p of that.

The above protocol can be described by the UML-like diagram of Figure 5. There, doubly-lined arrows denote iteration. The first communication of each branch in a choice is dotted, and the description of the branch ends where the vertical lines break. For graphical reasons the alternatives ack and nack appear in reverse order.

The multiparty session M = p P | q Q | h H where P = q!text.P 1 P 1 = q?{ok.P, notyet.P 1 , stop}

Q = p?text.h!text.Q 1 Q 1 = h?{ack.p!ok.Q, nack.p!notyet.h!transf.Q 1 , stop.p!stop} H = q?text.H 1 H 1 = q!{ack.H, nack.q?transf.H 1 , stop}
implements the protocol in Figure 5.

We end this section by defining the property of lock-freedom for multiparty sessions as in [START_REF] Kobayashi | A Type System for Lock-Free Processes[END_REF][START_REF] Padovani | Deadlock and Lock Freedom in the Linear πcalculus[END_REF]. Lock-freedom guarantees progress for each participant (and hence deadlock-freedom). In other words, each participant ready to communicate will eventually find her partner exposing a dual communication action. Recall that p 0 is a neutral element of | for the structural equivalence ≡ of multiparty sessions, and then p 0

| 1≤i≤n p i 0 ≡ p 0.
It can be easily proved that lock-freedom implies deadlock-freedom, but not vice versa.

Proposition 2.6. Lock-freedom implies deadlock-freedom, but not vice versa.

Proof. Let us first show that lock-freedom implies deadlock-freedom. Let M be lock-free. In order to show it to be also deadlock-free, let M -→ * M . We consider the two possible cases below:

M ≡ p 0
Deadlock-freedom descends hence immediately by Definition 2.5(i).

M ≡ p 0

In such a case we have necessarily that M ≡ p P | M (and hence M -→ * p P | M ) for some p, M and P = 0. By lock-freedom, it follows that p P | M -→ * M λ -→ with p occurring in λ. Then, trivially, M -→ M for some M , and we are done.

In order to show that the opposite implication does not hold, let us consider the following simple multiparty session:

M = p P | q Q | r s!
where P = q! .P and Q = p? .Q. It is not difficult to check that M is deadlock-free, whereas, since the process of r cannot communicate at all, M is not lock-free.

To get a stronger lock-freedom assuring that a communication involving p will occur in all reduction sequences starting from p P | M when P = 0 we need the following fairness assumption: in a session, any pair of participants ready to communicate will exchange a message after a finite number of steps.

In this way the multiparty session M = p P | q Q | r s! | s r? with P = q! .P and Q = p? .Q will not have the infinite reduction

M p q --→ M p q --→ • • •
where r and s never communicate. This assumption can be implemented, e.g., by a maximally parallel reduction in which at each step all possible communications are done [START_REF] Severi | Observational Equivalence for Multiparty Sessions[END_REF]. Notice that we do not require participants to choose outputs in a fair way, as exemplified below. This is not needed, since our type system will avoid starvation due to the choice of labels.

Example 2.7. The multiparty session

M = p P | q Q | r R with P = q!{ 1 .r? 3 , 2 .P }, Q = p?{ 1 , 2 .Q}, and R = p! 3 , has the infinite reduc- tion M p 2 q --→ M p 2 q --→ • • •
in which participant r can never send her message. This multiparty session will be rejected by our type system, see Remark 3.11.

Global Types and Typing System

The behaviour of multiparty sessions can be disciplined by means of types. Global types describe the whole conversation scenarios of multiparty sessions. As in [START_REF] Severi | Observational Equivalence for Multiparty Sessions[END_REF] we directly assign global types to multiparty sessions without the usual detour around session types and subtyping [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF][START_REF] Honda | Multiparty Asynchronous Session Types[END_REF].

The type p → q : { i .G i | 1≤i≤n} formalises a protocol where participant p must send to q a message i for some i, 1 ≤ i ≤ n, (and q must receive it) and then, depending on which i was chosen by p, the protocol continues as G i . We use Γ as shorthand for { i .G i | 1≤i≤n} and define the multiset

msg({ i .G i | 1≤i≤n}) = { i | 1 ≤ i ≤ n}.
Definition 3.1 (Global Types). Let G range over the terms of the following grammar:

G ::= coinductive End | | p → q : Γ Γ := { i .G i | 1≤i≤n}
where p = q and all messages in msg(Γ) are pairwise distinct. We call Γ a pre-choice of communications and define the tree representation of G as the directed rooted tree such that (a) each internal node is labelled by p → q and has as many children as the number of messages, (b) the edge from p → q to the child G i is labelled by i and (c) the leaves of the tree (if any) are labelled by End.

The term G is a global type if its tree representation is regular (namely, it has finitely many distinct sub-trees) and the pre-choice

{ i .G i | 1≤i≤n} is a choice of communications if G i is a global type for all i, 1 ≤ i ≤ n.
We identify global types with their tree representations and we shall sometimes refer to the tree representations as the global types themselves. As for processes, the regularity condition implies that we only consider global types admitting a finite representation.

The set ptg(G) of participants of global type G is defined similarly to those of processes and sessions. The regularity of global types assures that the set of participants is finite. We shall write .

G Γ for { .G} ∪ Γ if ∈ msg(Γ) and Γ 1 Γ 2 for Γ 1 ∪ Γ 2 if msg(Γ 1 ) ∩ msg(Γ 2 ) = ∅.
We assume that has the highest precedence, i.e. p → q : Γ 1 Γ 2 means p → q : (Γ 1 Γ 2 ). We shall omit curly brackets in choices with only one branch, as well as trailing End terms.

Since all messages in communication choices are pairwise distinct, the set of paths in the trees representing global types are determined by the labels of nodes and edges found on the way. Let ρ range over paths of global types. Formally the set of paths of a global type can be defined as a set of sequences ( is the empty sequence):

paths(End) = { } paths(p → q : { i .G i | 1≤i≤n}) = 1≤i≤n {(p → q) i ρ | ρ ∈ paths(G i )}
Note that every infinite path of a global type has infinitely many occurrences of '→'. We use "p ∈ ρ" as a shorthand for "p does not occur in ρ".

The function length returns the number of "interactions" in a path, and is defined as expected for finite paths:

length( ) = 0 length((p → q) i ρ) = 1 + length(ρ)
whereas we set length(ρ) = ∞ for infinite paths.

Example 3.2. A global type representing the protocol of Example 2.4 is:

G = p → q : text.q → h : text.G 1 G 1 = h → q : {ack.q → p : ok.G, nack.q → p : notyet.q → h : transf.G 1 , stop.q → p : stop}
Notice that G faithfully corresponds to the diagram in Figure 5.

Examples of paths in G are

ρ 1 =(p → q)text(q → h)text(h → q)stop(q → p)stop and ρ 2 =(p → q)text(q → h)text(h → q)ack(q → p)okρ 2
We get length(ρ 1 ) = 4 and length(ρ 2 ) = ∞.

Usually, as in [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF][START_REF] Honda | Multiparty Asynchronous Session Types[END_REF], projection of global types onto participants produces session types, and session types are assigned to processes by a type system. The simple shape of our messages, instead, allows us to define a projection of global types onto participants producing processes directly.

The projection of a global type onto a participant, if defined, returns the process that the participant should run to comply with the protocol specified by the global type. If the global type begins with a message from p to q, then the projection onto p should send one message to q, and the projection onto q should receive one message from p. The projection onto a third participant r skips the initial communication, that does not involve r. However, such a communication may be part of a choice, and since r is not part of it, she is not immediately aware of which branch is taken. Then, there are two possibilities: either r will behave in the same way in all the branches, hence she has no need to know which one has been taken, or she will discover later on which branch has been taken, by receiving distinct messages in each branch. In the first case, the projections on r of all the branches must be the same, and this projection defines her behaviour. In the second case, the projections yield input processes receiving from the same sender, and we can allow the process of r to combine all these processes, on the proviso the messages are all different. Definition 3.3 (Projection). Given a participant p, we coinductively define the partial function p on global types G as follows:

G p = 0 if p ∈ ptg(G) (p → q : { i .G i | 1≤i≤n}) p = q!{ i .G i p | 1≤i≤n} (q → p : { i .G i | 1≤i≤n}) p = q?{ i .G i p | 1≤i≤n} (q → r : { i .G i | 1≤i≤n}) p = = G 1 p if p ∈ {q, r} and G i p = G 1 p ∀ 1 ≤ i ≤ n s?(Λ 1 . . . Λ n ) if p ∈ {q, r} and G i p = s?Λ i ∀ 1 ≤ i ≤ n We say that G p is the projection of G onto p if G p is defined. We say that G is projectable if G p is defined for all participants p.
This projection is the coinductive version of the projection given in [START_REF] Dezani-Ciancaglini | Precise Subtyping for Synchronous Multiparty Sessions[END_REF][START_REF] Ghilezan | Precise Subtyping for Synchronous Multiparty Sessions[END_REF], where processes are replaced by local types.

As mentioned above, if p is not involved in the first communication of G, then in all branches the process of participant p must either behave in the same way or be an input from the same sender of different messages, so that p can understand which branch was chosen.

Example 3.4. The global type G of Example 3.2 is projectable, and by projecting it we obtain G p = P , G q = Q, G h = H, where P , Q, and H are as defined in Example 2.4. Also the global type G = p → q : { 1 .r → p : 3 , 2 .G } is projectable: G p = q!{ 1 .r? 3 , 2 .P }, G q = p?{ 1 , 2 .Q}, G r = p! 3 . These are the processes of the multiparty session shown in Example 2.7. Notice that G has two branches, the projection of the first branch onto r is p! 3 , the projection of the second branch onto r is just the projection of G onto r, so p! 3 is the (coinductive) projection of G onto r.

In order to assure lock-freedom by typing, we require each participant to occur in all the paths from the root, and that for each participant the first occurrences in the various paths are at bounded depth. This second constraint is formalised by requiring the depth of each participant in a global type -defined below in terms of the depth of a participant in a path -to be finite.

Definition 3.5 (Depth). Let depth(ρ, p) = length(ρ 1 ) if ρ = ρ 1 (q → r) ρ 2 , p ∈ ρ 1 and p ∈ {q, r} 0 if p ∈ ρ
We then define depth :

G × ptg(G) → N ∪ {∞} by depth(G, p) = sup{depth(ρ, p) | ρ ∈ paths(G)} Example 3.6.
Let G be as in Example 3.2; then depth(G, p) = depth(G, q) = 0, and The necessity of considering the depth of subterms in the definition of wellformedness is justified by the example

depth(G, h) = 1. Let G = p → q : { 1 .r → p : 3 , 2 .G } as in Example 3.4, then depth(G , r) = ∞.
G = p → r : 0 .p → q : { 1 .r → p : 3 , 2 .G }
where G is as above. In fact depth(G , r) = 0, while depth(G , r) = ∞. Therefore G is not well-formed, and this is important as we will show in Example 4.4.

In the following, we will only consider well-formed global types.

To type multiparty sessions we use the preorder on processes defined below and inspired by the subtyping of [START_REF] Castellani | Reversible Sessions with Flexible Choices[END_REF].

Definition 3.9 (Structural Preorder). We define the structural preorder on processes, P Q, by coinduction: Rule [sub-in] allows larger processes to offer fewer inputs than smaller ones, while Rule [sub-out] requires the output messages to be the same. The regularity condition on processes is crucial to guarantee the termination of algorithms for checking structural preorder. Usually, subtyping relations for output allow more branches in the supertype. We discuss this option in Section 10.

[sub-0] 0 0 [sub-out] P i Q i ∀1 ≤ i ≤ n p!{ i .P i | 1≤i≤n} p!{ i .Q i | 1≤i≤n} = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = [sub-in] P i Q i ∀1 ≤ i ≤ n p?({ i .P i | 1≤i≤n} Λ) p?{ i .Q i |
The typing judgments associate global types to sessions and are of the shape M : G. Definition 3.10 (Typing System). The only typing rule is:

[t-sess] p P ∈ M =⇒ P G p ptg(G) ⊆ pts(M) M : G A session M is well-typed if there exists G such that M : G.
The rule above requires that the processes in parallel can play as participants of a whole communication protocol or they are the terminated process, i.e. they are smaller or equal (according to the structural preorder) to the projections of a same global type. Note that [t-sess] is not coinductive since a multiparty session is a finite parallel composition of (possibly infinite) processes; hence coinduction is necessary only for the subtyping relation. In general, pts(M) ⊆ ptg(G) does not hold, for example p q! | q p? | r 0 : p → q : Remark 3.11. Since the projections of G = p → q : { 1 .r → p : 3 , 2 .G } as defined in Example 3.4 are exactly the processes P = q!{ 1 .r? 3 , 2 .P }, Q = p?{ 1 , 2 .Q}, and R = p! 3 of the multiparty session in Example 2.7 and G is not well-formed, our type system rejects the multiparty session in Example 2.7.

Properties of Well-Typed Sessions

We start with the standard lemmas of inversion and canonical form, easily following from Rule To formalise the properties of Subject Reduction and Session Fidelity [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF][START_REF] Honda | Multiparty Asynchronous Session Types[END_REF], we use the standard LTS for global types given below. Definition 4.3 (LTS for Global Types). The labelled transition system (LTS) for global types is specified by the rules:

[ecomm] p → q : .G Γ p q --→ G [icomm] G i p q --→ G i ∀1 ≤ i ≤ n {p, q} ∩ {r, s} = ∅ r → s : { i .G i | 1≤i≤n} p q --→ r → s : { i .G i | 1≤i≤n}
Rule [Icomm] makes sense since, in a projectable global type r → s : Γ, behaviours involving participants p and q ready to interact with each other uniformly in all branches can do so if they are both not involved in a previous interaction between r and s. In fact, the interaction between p and q is independent of the choice of r, and may be executed before it.

Example 4.4. Let G = p → r : 0 .p → q : { 1 .r → p : 3 , 2 .G } and G = p → q : { 1 .r → p : 3 , 2 .G } as in Example 3.8. We get G p r
-→ G . Notice that depth(G , r) = 0 and depth(G , r) = ∞. This shows that the finiteness of depth would not be preserved by reduction if we would not consider all subterms in condition (a) of Definition 3.7.

In the remainder of this section we show the main properties of our type system, i.e. Subject Reduction, Session Fidelity and Lock-Freedom. We start with three lemmas. The first lemma assures that well-formedness is preserved by the reduction of global types. The second lemma says that the depths of participants not occurring in the root of a global type decrease along the branches of the tree. The third lemma relates projections and reductions of global types. --→ G and G is well-formed, then G is well-formed too.

Proof. It is enough to observe that G is a subterm of G. Lemma 4.6. If G = p → q : Γ and depth(G, r) = 0, then depth(G, r) > depth(G , r) for all .G ∈ Γ.

Proof. All paths of G are of the shape (p → q) ρ, where ρ is a path of G . This gives depth(G, r) > depth(G , r), since depth(G, r) = 0 by hypothesis and it is finite since G is well-formed. Lemma 4.7 (Key Lemma). (i) If G p = q!Λ and G q = p?Λ , then

msg(Λ) = msg(Λ ). Moreover for all ∈ msg(Λ), G p q --→ G and .G p ∈ Λ and .G q ∈ Λ . (ii) If G p q
--→ G , then G p = q!Λ and G q = p?Λ and ∈ msg(Λ) = msg(Λ ).

Proof. (i). The proof is by induction on w = depth(G, p).

If w = 0, then G = p → q : Γ. Hence, by definition of projection (Definition 3.3), we have msg(Λ) = msg(Λ ) = msg(Γ) and, for all .G ∈ Γ, .G p ∈ Λ and .G q ∈ Λ . Moreover G p q --→ G using rule [ecomm]. If w > 0, then G = r → s : { i .G i | 1≤i≤n} and p ∈ {r, s}. From G q = p?Λ we get q ∈ {r, s}. Moreover G i p = q!Λ and G i q = p?Λ for all i, 1 ≤ i ≤ n, by definition of projection. By Lemma 4.6 w > depth(G i , p) for all i, 1 ≤ i ≤ n. By the induction hypothesis, msg(Λ) = msg(Λ ). Again by the induction hypothesis, G i p q --→ G i and .G i p ∈ Λ and .G i q ∈ Λ for all i, 1 ≤ i ≤ n, and all ∈ msg(Λ). We get

G p q --→ r → s : { i .G i | 1≤i≤n} using rule [icomm].
(ii). The proof is by induction on depth(G, p) and by cases on the reduction rules. The case of rule [ecomm] is easy. For rule [icomm], by the induction hypothesis, G i p = q!Λ i and G i q = p?Λ i and ∈ msg(Λ i ) = msg(Λ i ) for all i,

1 ≤ i ≤ n. By definition of projection G i p = G 1 p and G i q = G 1 q for all i, 1 ≤ i ≤ n. Again by definition of projection G p = G 1 p and G q = G 1 q .
Subject Reduction says that the transitions of well-typed sessions are mimicked by those of global types. Proof. First, we can deduce some structural information on M and M . Indeed, since M p q --→ M , then p q!( .P Λ) ∈ M, q p?( .Q Λ ) ∈ M and p P ∈ M , q Q ∈ M . Moreover r R ∈ M iff r R ∈ M for all r ∈ {p, q}. Thanks to typing, we can deduce similar information on G. Indeed, since M : G, we have that q!( .P Λ) G p , and p?( .Q Λ ) G q , and for all r R ∈ M such that r ∈ {p, q} we have R G r by Lemma 4.1. By definition of , from q!( .P Λ) G p we get G p = q!( .P 0 Λ 0 ) and P P 0 . Similarly from p?( .Q Λ ) G q we get G q = p?( .Q 0 Λ 0 ) and

Q Q 0 . Lemma 4.7(i) implies G p q
--→ G and G p = P 0 and G q = Q 0 . This proves the first part of the conclusion, we now move to the second one. We show G r G r for each r ∈ {p, q} and r R ∈ M by induction on depth(G, r) and by cases on the reduction rules. For rule [ecomm] we get G = p → q : ( .G Γ). By Definition 3.3 either G r = G r or G r G r . For rule [icomm] G i r G i r for all i, 1 ≤ i ≤ n, by the induction hypothesis. This implies G r G r . We conclude M : G . Session fidelity assures that the communications in a session typed by a global type proceed as prescribed by the global type. Theorem 4.9 (Session Fidelity). Let M : G.

(i) If M p q --→ M , then G p q --→ G and M : G . (ii) If G p q --→ G , then M p q
--→ M and M : G .

Proof. (i). It is the Subject Reduction Theorem. (ii). By Lemma 4.7(ii), G p = q!Λ and G q = p?Λ and ∈ msg(Λ) = msg(Λ ). By Lemma 4.7(i) .G p ∈ Λ and .G q ∈ Λ . By Lemma 4.2 p P ∈ M and q Q ∈ M and P G p and Q G q . By definition of we get

• P = q!( .P Λ 1 ) with { } ∪ msg(Λ 1 ) = msg(Λ) and P G p , • Q = p?( .Q Λ 2 ) with { } ∪ msg(Λ 2 ) ⊇ msg(Λ ) and Q G q .
Hence we have M p q

--→ M with p P ∈ M , q Q ∈ M and r R ∈ M iff r R ∈ M for all r ∈ {p, q}. We conclude M : G .

We end this section by showing that the type system assures lock-freedom. By Subject Reduction it is enough to prove that in well-typed sessions no active participant waits forever. It follows from Session Fidelity, using Lemma 4.6. It is easy to check that M : G, where M and G are the multiparty session and the global type of Examples 2.4 and 3.2, respectively. By the above result, M of Example 2.4 is hence provably lock-free.

Composition of Multiparty-Sessions via Gateways

Two multiparty sessions can be composed via gateways when they possess two compatible participants, i.e. participants that offer communications which can be paired. Hence, the two participants can be transformed into forwarders, that we dub "gateways".

We start by discussing the relation of compatibility between processes by elaborating on Examples 2.4 and 3.2. Consider the participant h in these examples as an interface; the messages sent by h have to be considered as those actually provided by an external environment, and the received messages as messages expected by such an environment. In a sense, this means that, if we abstract from participants' name in the process H = q?text.H 1 where H 1 = q!{ack.H, nack.q?transf.H 1 , stop}, we get an interface towards an external system rather than a description of an internal component of our system.

In order to better grasp the notion of compatibility hinted at above, let an( ) be an operation abstracting from the participants' name inside processes. So, in our example we would get an(H) = •?text.an(H 1 ) an(H 1 ) = •!{ack.an(H), nack.•?transf.an(H 1 ), stop} where • stands for an abstracted participant name.

The following example gives another system that could work as the environment of the system in Example 2.4.

Example 5.1. Consider a system formed by participants k, r and s interacting according to the following protocol:

Participant k sends text messages to r and s in an alternating way, starting with r.

Participants r and s inform k that a text has been accepted or refused by sending back, respectively, either ack or nack.

In the first case it is the other receiver's turn to receive the text: a message go is exchanged between r and s to signal this case;

In the second case, the sender has to resend the text until it is accepted. Meanwhile the involved participant between r and s informs the other one that she needs to wait, since the previous message is being resent in a transf ormed form. In order to better understand the above protocol, we can describe it in UML-like form as done in Figure 6.

This protocol can be implemented by the multiparty session

M = r R | s S | k K r where R = k?text.R 1 R 1 = k!{ack.s!go.R 2 , nack.s!wait.k?transf.R 1 } R 2 = s?{go.R, wait.R 2 } S = r?{go.k?text.S 1 , wait.S} S 1 = k!{ack.r!go.S, nack.r!wait.k?transf.S 1 } K r = r!text.K r K r = r?{ack.K s , nack.r!transf.K r } K s = s!text.K s K s = s?{ack.K r , nack.s!transf.K s }
The "behaviour as interface" of participant k in the previous system corresponds to an(K r ) = an(K s ) = •!text.an(K r ) an(K r ) = an(K s ) = •?{ack.an(K r ), nack.•!transf.an(K r )} Notice that the mapping an equates K r and K s , i.e. an(K r ) = an(K s ). The interactions "offered" and "requested" by an(H) and an(K r ) do not precisely match each other, that is an(H) = an(K r ) (where (•) is the standard syntactic duality function replacing '!' by '?' and vice versa [START_REF] Honda | Language Primitives and Type Discipline for Structured Communication-Based Programming[END_REF]). Nonetheless, it is easy to check that, even if the system p P | q Q of Example 2.4 can safely deal with a message stop coming from its environment, no problem arises in case such a message never arrives.

In the following definition, instead of explicitly introducing the an( ) function, we simply formalise the compatibility relation in such a way that two processes are compatible (as interfaces) whenever they offer dual communications to arbitrary participants, and, for each communication, the set of input labels is a subset of the set of output labels. This allows one gateway to send to the other each message received and to receive from the other each message she will send, see Definition 5.4.

Definition 5.2 (Compatible Processes).

The interface compatibility relation P ↔ Q on processes (compatibility for short), is the largest symmetric relation coinductively defined by: Notice that the relation ↔ is insensitive to the names of senders and receivers. Process compatibility is similar to, but simpler than, the subtyping relation defined in [START_REF] Gay | Subtyping for Session Types in the Pi Calculus[END_REF]. Therefore one can easily adapt the algorithm for subtyping in [START_REF] Gay | Subtyping for Session Types in the Pi Calculus[END_REF] so to check process compatibility. For what concerns our example, it is straightforward to verify that H ↔ K r .

[comp-0] 0 ↔ 0 [comp-o/i] P i ↔ Q i ∀1 ≤ i ≤ n p!({ i .P i | 1≤i≤n} Λ) ↔ q?{ i .Q i | 1≤i≤n}
Useful properties of compatibility are stated in the following proposition, whose proof is simple.

Proposition 5.3 (Compatibility Properties). (i) If P ↔ p?(Λ Λ ),

then P ↔ p?Λ.

(ii) If P ↔ p?Λ and P ↔ p?Λ with Λ ∩ Λ = ∅, then P ↔ p?(Λ Λ ).

(iii) If p!( .P Λ) ↔ q? .Q, then P ↔ Q. As done in [START_REF] Barbanera | Global Types for Open Systems[END_REF] for the setting of CFSMs [START_REF] Brand | On Communicating Finite-State Machines[END_REF], the presence of two compatible processes H and K in two multiparty sessions M and M enables their composition by transforming H and K into a pair of gateways. This means that each message received by H is immediately sent to K, each message sent by H needs to be first received from K, and the same holds also with H and K swapped. Hence, we define below a function gw(P, h) which transforms an arbitrary process P (representing the behaviour of K above) not containing a fixed participant h into a gateway towards h, namely a process which:

1. sends to h each message received in P ; 2. receives from h each message to be sent in P .

Considering the process of participant k chatting with participant p, this transformation can be represented by the UML-like diagrams of Figure 7.

Definition 5.4 (Gateway Process). Let h ∈ ptp(P ). We define the gateway process gw(P, h) coinductively as follows

gw(0, h) = 0 gw(p?{ i .P i | 1≤i≤n}, h) = p?{ i .h! i .gw(P i , h) | 1≤i≤n} gw(p!{ i .P i | 1≤i≤n}, h) = h?{ i .p! i .gw(P i , h) | 1≤i≤n}
A first lemma assures that gateway processes are well-defined. Lemma 5.5 (Gateway Processes are Well-Defined). If h ∈ ptp(P ), then gw(P, h) is defined and it is a process.

Proof. The proof is by coinduction on P and by cases on its shape. The case P = 0 is trivial.

If P = p?{ i .P i | 1≤i≤n} then gw(P, h) = p?{ i .h! i .gw(P i , h) | 1≤i≤n}
For each i, 1 ≤ i ≤ n, by coinduction gw(P i , h) is defined and it is a process, since h ∈ ptp(P i ). Hence, by definition also gw(p?{ i .P i | 1≤i≤n}, h) is a process. The proof for the case where P is an output process is similar.

The gateway process construction is monotone with respect to the structural preorder. This property is key to get Theorem 6.10 (ensuring that composition via gateways preserves typability) and it essentially relies on the fact that larger processes offer the same output messages than smaller ones.

Lemma 5.6 (Monotonicity of Gateway Construction).

Let h ∈ ptp(P ) ∪ ptp(Q). If P Q, then gw(P, h) gw(Q, h).

Proof. The proof is by coinduction on the derivation of P Q. We only consider the case of input processes, the proof for output processes is similar and simpler, the one for 0 is trivial.

If P = p?{ i .P i | 1≤i≤n} and Q = p?{ i .Q i | 1≤i≤m} with m ≤ n, then gw(P, h) =p?{ i .h! i .gw(P i , h) | 1≤i≤n} and gw(Q, h) =p?{ i .h! i .gw(Q i , h) | 1≤i≤m} From P Q we get P i Q i for all i, 1 ≤ i ≤ m.
We get by coinduction gw(P i , h) gw(Q i , h), which implies h! i .gw(P i , h) h! i .gw(Q i , h) for all i, 1 ≤ i ≤ m. Hence gw(P, h) gw(Q, h), by Definition 3.9.

The following relationship between compatibility and structural preorder of processes will be essential for proving one of our main results (Theorem 6.10).

Lemma 5.7 (Compatibility is Upward-Closed). If P ↔ Q, then P P and Q Q imply P ↔ Q .

Proof. By definition of process compatibility (Definition 5.2) and of process structural preorder (Definition 3.9)

P = p!{ i .P i | 1≤i≤n} P = p!{ i .P i | 1≤i≤n} Q = q?{ i .Q i | 1≤i≤m} Q = q?{ i .Q i | 1≤i≤m } with m ≤ m ≤ n
From P ↔ Q we get P i ↔ Q i for all i, 1 ≤ i ≤ m. From P P we get

P i P i for all i, 1 ≤ i ≤ n. From Q Q we get Q i Q i for all i, 1 ≤ i ≤ m . By coinduction we have P i ↔ Q i for all i, 1 ≤ i ≤ m .
We can then conclude P ↔ Q .

Essentially the result above shows that compatibility is upward-closed with respect to the structural preorder. However, it is not downward-closed. For example p! ↔ q? and q?{ , } q? , but p! ↔ q?{ , } is false.

The formal definition of composition of multiparty sessions via gateways is based on the notion of process compatibility (Definition 5.2) and on the transformation of a process into a gateway (Definition 5.4). We write (M, h) ↔ (M , k) when M, M are compatible via h and k.

Definition 5.9 (Composition Via Gateways of Multiparty Sessions).

Let M ≡ M 1 | h H, M ≡ M 1 | k K and (M, h) ↔ (M , k).
We define M h↔k M , the composition of M and M via gateways, through h and k, by Ĥ = gw(H, k) = q?text.k!text. Ĥ1 Ĥ1 = k?{ack.q!ack. Ĥ, nack.q!nack.q?transf.k!transf. Ĥ1 , stop.q!stop} Kr

M h↔k M = M 1 | M 1 | h gw(H, k) | k gw(K,
M h↔k M = p P | q Q | r R | s S | h Ĥ | k
                                   
= gw(K r , h) = h?text.r!text. K r K r = r?{ack.h!ack. Ks , nack.h!nack.h?transf.r!transf. K r } Ks = gw(K s , h) = h?text.s!text. K s K s = s?{ack.h!ack. Kr , nack.h!nack.h?transf.s!transf. K s }
The overall behaviour of the composed system is described in the UML-like diagram in Figure 8.

We have shown above how to compose two multiparty sessions, but we have not provided any guarantee on the behaviour of the resulting multiparty session. Composition via gateways preserves lock-freedom (cf. Section 6). To prove this, we define an operator taking the global types of two sessions and the name of a participant in each of them (the two participants need to be compatible) and building a type for the composed multiparty session. The composed global type will directly mimic the diagram in Figure 8.

Notice that preservation of lock-freedom cannot be inferred from the results of [2], where lock-freedom was not taken into account.

Composition of Global Types via Gateways

The composition defined in the previous section can be shown to be lockfreedom preserving by means of Theorem 4.10. In fact, it is possible to lift the composition via gateways of multiparty sessions in Definition 5.9 to the level of global types. We start by defining the compatibility of global types via two participants, which mimics the compatibility of multiparty sessions via two participants Definition 6.1 (Compatible Global Types). Two global types G, G are compatible via the participants h and

k if ptg(G)∩ptg(G ) = ∅ and G h ↔ G k . We write (G, h) ↔ (G , k) when G, G are compatible via h and k. It is easy to verify that (G, h) ↔ (G , k) implies h ∈ ptg(G) if, and only if, k ∈ ptg(G ).
The compatibility of typed sessions implies the compatibility of the corresponding global types.

M = p h? | h p! , M = q k! | k q?{ , }, G = h → p : , G = q → k : . Then G p = h? , G h = p! , G q = k
! , and G k = q? . We get p! ↔ q? , which implies (G, h) ↔ (G , k) according to Definition 6.1. Instead p! ↔ q?{ , } does not hold and therefore we do not have (M, h) ↔ (M , k) according to Definition 5.8. Intuitively, the typed sessions may have additional inputs due to structural preorder, and such additional inputs break compatibility at the level of sessions.

We are now ready to define the composition of global types via gateways. To avoid cumbersome parentheses, in the following we assume

→ : Γ h↔k → : Γ reads ( → : Γ) h↔k ( → : Γ ) → : Γ h↔k G reads ( → : Γ) h↔k G G h↔k → : Γ reads G h↔k ( → : Γ) . → : . → : .G h↔k G reads . → : . → : .(G h↔k G ) .G h↔k G reads .(G h↔k G )
where stands for arbitrary, possibly different participant names.

Definition 6.4 ( Global Type Composition via Gateways).

Let (G, h) ↔ (G , k). We define

G h↔k G
coinductively by the clauses of Figure 9, assuming {p, q, r, s} ∩ {h, k} = ∅. The clauses must be applied in the given order.

( The core rules of our construction are rules (2) and ( 3), where the communication received by one of the two gateways is sent to the other one, which in turns outputs it. The effect of the application of such rules can be roughly interpreted in terms of diagrams as described in Figure 10. Rules ( 4) and ( 5) allow a participant to take an interaction not involving the interface. In global types, the order of interactions between pairs of unrelated participants is irrelevant, since we would get the very same projections. In clauses ( 4) and ( 5), however, we swap roles h and k, as well as their corresponding global types in the "recursive call". We do that in order to spare the axiom G h↔k End = G. Moreover, this swapping avoids that in G k↔h G the interactions following a communication via gateway all belong to G (or G ) and that the communication is completed after the description of interactions all belonging to G (or G). In this way, the parallel nature of the interactions in G and G that are not affected by the communications via gateways is made visually more evident. Anyway the composition would be sound also without this swapping, just by adding the axiom G h↔k End = G.

) End h↔k G = G (2) p → h : { i .G i | 1≤i≤n} h↔k k → s : { i .G i | 1≤i≤n} Γ = p → h : { i .h → k : i .k → s : i .G i h↔k G i | 1≤i≤n} (3) h → p : { i .G i | 1≤i≤n} Γ h↔k s → k : { i .G i | 1≤i≤n} = s → k : { i .k → h : i .h → p : i .G i h↔k G i | 1≤i≤n} (4) p → q : { i .G i | 1≤i≤n} h↔k G = p → q : { i .G k↔h G i | 1≤i≤n} (5) G h↔k r → s : { i .G i | 1≤i≤n} = r → s : { i .G i k↔h G | 1≤i≤n} 1
G r = k → r : text.G r G r = r → k : {ack.r → s : go.G s , nack.r → s : wait.k → r : transf.G r } G s = k → s : text.G s G s = s → k : {ack.s → r : go.G r , nack.s → r : wait.k → s : transf.G s }
By composing, via h and k, the global type G of Example 3.2 and the above global type G r we obtain a global type directly corresponding to the diagram in Figure 8. In particular, we get:

G h↔k G r = p → q : text.q → h : text.h → k : text.k → r : text.G r k↔h G 1 G r k↔h G 1 = r → k : {ack.k → h : ack.h → q : ack.r → s : go.q → p : ok.G s k↔h G, nack.k → h : nack.h → q : nack.r → s : wait.q → p : notyet. q → h : transf.h → k : transf.k → r : transf.G r k↔h G 1 } G s k↔h G = p → q : text.q → h : text.h → k : text.k → s : text.G 1 h↔k G s G 1 h↔k G s = s → k : {ack.k → h : ack.h → q : ack.q → p : ok.s → r : go.G h↔k G r , nack.k → h : nack.h → q : nack.q → p : notyet.s → r : wait. q → h : transf.h → k : transf.k → s : transf.G 1 h↔k G s }
In G h↔k G r the text messages coming from p are delivered to q and, alternately, to r and s till they are accepted (ack). Participant p is informed when text messages are accepted (ok). During the cycle, q transforms a not yet accepted text into a more suitable form. The messages between q on one side and r and s on the other side are exchanged by passing through the coupled gateways h and k.

It is worth pointing out that in G h↔k G r , the stop branch of G disappeared. In fact, since any message coming from h in G does now come from k (which is now the gateway forwarding the messages coming in turn from either r or s), the function h↔k takes care of the fact that only ack or nack can be received by (the gateway) h. This fact is reflected in the following Theorem 6.9, where it is shown that gw(G h , k) and gw(G k , h) are less than or equal to the projections of G h↔k G on h and k, respectively.

We could look at both h and p as interfaces: h representing a socialnetwork system, which does not accept rude language, and p a social-network client sending text messages and requiring to be informed about their delivery status. From this point of view, the global type G of Example 3.2 actually describes a "delivery-guaranteed" service for text messages, assuring messages to be eventually delivered by means of a text-transformation policy.

In order to show that composition via gateways is well-defined, it is handy to express the condition G h ↔ G k by means of a relation, dubbed agreement, between the pairs (G, h) and (G, k). The agreement relation is used in the proof of Lemma 6.8. Definition 6.6 (Agreement Relation). The agreement relation

(G, h) (G, k)
is the largest symmetric relation coinductively defined by the rules:

[rel-End] (End, h) (G , k) if k ∈ ptg(G ) [rel-go] h ∈ {p, q} (G i , h) (G, k) ∀1 ≤ i ≤ n (p → q : { i .G i | 1≤i≤n}, h) (G,
(G i , h) (G i , k) ∀1 ≤ i ≤ n ≤ m (p → h : { i .G i | 1≤i≤n}, h) (k → q : { i .G i |
(G, h) (G , k) iff G h ↔ G k .
Proof. From (G, h) (G , k) we can show G h ↔ G k by coinduction and by cases on the rules of Definition 6.6. If the last applied rule is [rel-go] by coinduction G i h ↔ G k for all i, 1 ≤ i ≤ n. By Definition 3.3 we have two cases:

1. G h = G 1 h if G i h = G 1 h for all i, 1 ≤ i ≤ n; 2. G h = s?(Λ 1 . . . Λ n ) if G i p = s?Λ i for all i, 1 ≤ i ≤ n and msg(Λ i ) ∩ msg(Λ j ) = ∅ for all i,j, 1 ≤ i = j ≤ n.
In case 1 we are done. In case 2 we conclude by repeatedly applying Proposition 5.3(ii).

If the last applied rule is [rel-comm], then by coinduction

G i h ↔ G i k for all i, 1 ≤ i ≤ n. We get G h = p?{G i h |1≤i≤n} and G k = q!{G i k |1≤i≤m} by Definition 3.3. We can then derive G h ↔ G k using rule [comp-o/i] of Definition 5.2. Vice versa, if ¬ (G, h) (G , k
) there exists a "failing derivation" using rules of Definition 6.6 with conclusion (G, h) (G , k) and with at least one finite branch ending with a judgment having one of the following forms (or the symmetric ones):

1. (End, h) (Y, k) with k ∈ ptg(Y); 2. (p → h : Γ, h) (s → k : Γ , k); 3. (h → p : Γ, h) (k → s : Γ , k); 4. (p → h : Γ, h) (k → s : Γ , k
) and there exists ∈ msg(Γ) \ msg(Γ ).

In order to show ¬(G h ↔ G k ) it is enough to assume G h ↔ G k and to derive a contradiction by checking that the following statements hold:

a) If k ∈ ptg(Y), then ¬(End h ↔ Y k ); b) If Y = p → h : Γ and Y = s → k : Γ , then ¬(Y h ↔ Y k ); c) If Y = h → p : Γ and Y = k → s : Γ , then ¬(Y h ↔ Y k ); d) If Y = p → h : Γ, Y = k → s : Γ and there exists ∈ msg(Γ)\msg(Γ ), then ¬(Y h ↔ Y k ).
Statements a), b), c) and d) above descend easily from Definition 3.3 of projection and Definition 5.2 of compatibility between processes.

Using the previous lemma we can give the following definition of compatible global types, which is alternative to Definition 6.1:

The following theorem gives the key result concerning projections of types obtained by composing via gateways the global types G and G through participants h and k. It says that:

• the gateway processes are equal to or smaller than the corresponding projections of G h↔k G on h and k;

• the projections of G and G on all participants different from h and k are equal to or smaller than the corresponding projections of G h↔k G . Theorem 6.9 (Projection of Composition via Gateways).

If (G, h) ↔ (G , k), then G h↔k G is well-formed. Moreover (i) gw(G h , k) (G h↔k G ) h and gw(G k , h) (G h↔k G ) k ; (ii) G p (G h↔k G ) p and G q (G h↔k G ) q ,
for any p ∈ ptg(G) and q ∈ ptg(G ) such that p = h and q = k.

Proof. By Lemma 6.8 G h↔k G is a global type. We recall that by Definition 3.7 a global type is well-formed iff

• each participant has finite depth for all subterms of the global type;

• the global type is projectable on each participant.

It is easy to verify that if

w = max{depth(G 0 , p) | G 0 is a subterm of G and p ∈ ptg(G)} and w = max{depth(G 0 , p) | G 0 is a subterm of G and p ∈ ptg(G )} then depth( Ĝ, p) ≤ 2(w + w ) for all Ĝ subterm of G h↔k G and all p ∈ ptg(G) ∪ ptg(G ).
We show the projectability of the composition by proving (i) and (ii). (i). We consider only the case gw(G h , k)

(G h↔k G ) h as the proof of gw(G k , h) (G h↔k G ) k is specular. We prove gw(Y h , k) (Y h↔k Y ) h for any recursive call Y h↔k Y in G h↔k G
by coinduction and by cases on the last applied rule. Rules (1), ( 4) and ( 5) do not modify the communications of participant h, so coinduction easily applies. Rule (2):

Y h↔k Y = p → h : { i .h → k : i .k → s : i .Y i h↔k Y i | 1≤i≤n} where Y = p → h : { i .Y i | 1≤i≤n} and Y = k → s : { i .Y i | 1≤i≤n} Γ. Then Y h = p?{ i .Y i h | 1≤i≤n} by Definition 3.3. gw(Y h , k) = p?{ i .k! i .gw(Y i h , k) | 1≤i≤n} by Definition 5.4 p?{ i .k! i .(Y i h↔k Y i ) h | 1≤i≤n} by rules [sub-in] and [sub-out] of Definition 3.9 since by coinduction gw(Y i h , k) (Y i h↔k Y i ) h for all i, 1 ≤ i ≤ n = (Y h↔k Y ) h by Definition 3.3. Rule (3): Y h↔k Y = s → k : { i .k → h : i .h → p : i .Y i h↔k Y i | 1≤i≤n}, where Y = h → p : { i .Y i | 1≤i≤m} and Y = s → k : { i .Y i | 1≤i≤n} with m ≥ n. Then Y h = p!{ i .Y i h | 1≤i≤m} by Definition 3.3. gw(Y h , k) = k?{ i .p! i .gw(Y i h , k) | 1≤i≤m} by Definition 5.4 k?{ i .p! i .gw(Y i h , k) | 1≤i≤n} by rule [sub-in] k?{ i .p! i .(Y i h↔k Y i ) h | 1≤i≤n} by rules [sub-in] and [sub-out] of Definition 3.9 since by coinduction gw(Y i h , k) (Y i h↔k Y i ) h for all i, 1 ≤ i ≤ n = (Y h↔k Y ) h
by Definition 3.3. (ii). We only show G p (G h↔k G ) p for p ∈ ptg(G) and p = h. The proof of G q (G h↔k G ) q for q ∈ ptg(G ) and q = k is specular. Consider the recursive calls Y h↔k Y in G h↔k G . We prove Y p (Y h↔k Y ) p by coinduction on Y, Y and by cases on the last applied rule. The only rule which modifies the communications of p is rule (3):

Y h↔k Y = s → k : { i .k → h : i .h → p : i .Y i h↔k Y i | 1≤i≤n}, where Y = h → p : { i .Y i | 1≤i≤m} and Y = s → k : { i .Y i | 1≤i≤n} with m ≥ n. Y p = h?{ i .Y i p | 1≤i≤m} by Definition 3.3 h?{ i .Y i p | 1≤i≤n} by rule [sub-in] h?{ i .(Y i h↔k Y i ) p | 1≤i≤n} by rule [sub-in] since by coinduction Y i p (Y i h↔k Y i ) p for all i, 1 ≤ i ≤ n = (Y h↔k Y ) p by Definition 3.3.
We now show that by composing via gateways two well-typed sessions which are compatible, we get a session which is also well-typed. This is relevant, since well-typed sessions enjoy lock-freedom (Theorem 4.10).

M h↔k M = M 1 | M 1 | h gw(H, k) | k gw(K, h)
From M : G we get H G h and from M : G we get K G k , both thanks to the Inversion Lemma (Lemma 4.1). Lemma 5.6 gives gw(H, k) gw(G h , k) and gw(K, h) gw(G k , h). From (M, h) ↔ (M , k) by Lemma 6.2 we get (G, h) ↔ (G , k). We conclude M h↔k M : G h↔k G using the relations on the projections of G h↔k G given in Theorem 6.9.

As a general application of the previous results, let us suppose to have two systems that correspond to multiparty sessions that are compatible via some participants (according to Definition 5.8) and that are well-typed (according to Definition 3.10). At this point, we can "deploy" the composed system (following Definition 5.9) without any further verification step, since Theorem 6.10 ensures that under such conditions we have a well-typed and hence lockfree composed system. Besides, we are able to provide the documentation (the global type) of the resulting system.

Compatibility of Global Types is Necessary

We have shown that the composition of typeable multiparty sessions, via the transformation of two participants into gateways, does preserve lockfreedom in case the two participants are compatible. One could wonder whether session compatibility, besides being a sufficient condition for ensuring such a preservation property, is also necessary. Example 6.3 shows that this is not the case.

Example 7.1 (Session Compatibility is not Necessary). Let us take M = p h? | h p! and M = q k! | k q?{ , } from Example 6.3. Then (M, h) ↔ (M , k) does not hold, and therefore M h↔k M is undefined. Nonetheless, applying the gateway construction (cf. Definition 5.4), we can build p h? | h k? .p! | q k! | k q?{ .h! , .h! } which is lock-free, since its only reduction terminates with p 0. The reason is that even if potentially k could try to send to p (via h), creating a deadlock, in this session such a possibility is never taken, since q will never send to k. Notice that in the same example (G, h) ↔ (G , k) instead holds (recall that in Example 6.3 G = h → p : and G = q → k : ).

We will now show that compatibility of global types is instead necessary. Let ¬ (G, h) ↔ (G , k) and M : G and M : G . Lemma 6.2 gives

¬ (M, h) ↔ (M , k) . This implies that M h↔k M is undefined. Anyway, if M ≡ M 1 | h H and M ≡ M 1 | k K we can build M 1 | M 1 | h gw(H, k) | k gw(K, h).
Theorem 7.5 below shows that this parallel composition is not lock-free (or not even a session) when ¬ (G, h) ↔ (G , k) and M : G and M : G .

We proceed by providing an inductive characterisation of the relation of non-compatibility between processes. We first give the definition of a relation between processes (Definition 7.2), and then we show that this relation coincides with the negation of process compatibility (Lemma 7.3). Definition 7.2 (Non-Compatibility of Processes). The non-compatibility relation between processes, dubbed ↔, is the symmetric closure of the relation inductively defined as follows.

[nocomp-0]

P = 0 P ↔ 0 [nocomp-i] p?Λ ↔ q?Λ [nocomp-o] p!Λ ↔ q!Λ [nocomp-lab] msg(Λ ) ⊆ msg(Λ) p!Λ ↔ q?Λ [nocomp-hered] P ↔ Q p!( .P Λ) ↔ q?( .Q Λ ) Lemma 7.3 (Negation of Compatibility). P ↔ Q iff ¬(P ↔ Q).
Proof. If P ↔ Q, then we can show ¬(P ↔ Q) by induction on the derivation of P ↔ Q. We just develop the inductive case [nocomp-hered]. In this case, P = p!( .P Λ) and Q = q?( .Q Λ ); moreover, P ↔ Q and thus, by the induction hypothesis, ¬(P ↔ Q ). We now notice that P ↔ Q could only possibly hold by rule [comp-o/i] but, since ¬(P ↔ Q ), at least one of the coinductive premises of such a rule is not satisfied. Hence, we conclude

¬(P ↔ Q).
Vice versa, if ¬(P ↔ Q) we construct a derivation of P ↔ Q by looking at a "failing derivation" of P ↔ Q. If we try to apply rule [comp-o/i] to show P ↔ Q, there exists a derivation branch that fails after a finite number, say n, of steps, i.e. that reaches two processes P , Q which do not match the conclusion of [comp-o/i]. We prove P ↔ Q by induction on n, turning the failing coinductive derivation branch into a derivation of depth n + 1 which concludes P ↔ Q:

• base case n = 0. The derivation fails immediately, i.e. P = P and Q = Q. By cases on the possible shapes of P and Q, we construct a derivation which concludes P ↔ Q in 1 = n + 1 steps, by one of the axioms

[nocomp-0], [nocomp-i], [nocomp-o],
or [nocomp-lab];

• inductive case n = m + 1. The shapes of P, Q match the conclusion of rule [nocomp-hered], but there is some coinductive premise P ↔ Q whose sub-derivation has a branch that fails after m steps. By the induction hypothesis, there exists a derivation of depth m + 1 that concludes P ↔ Q ; using this as a premise of rule [nocomp-hered] we construct a derivation of depth (m + 1) + 1 = n + 1 which concludes P ↔ Q.

A lemma connecting projections of global types with reductions of typed sessions is handy in the proof of the main result of this section (Theorem 7.5). (i) If G p = q?Λ with ∈ msg(Λ), then there is a reduction

M -→ * M | q p!Λ such that ∈ msg(Λ ).
(ii) If G p = q!Λ with ∈ msg(Λ), then there is a reduction

M -→ * M | q p?Λ such that ∈ msg(Λ ).
Proof. The proofs of both items are by induction on w = depth(G, p). (i). If w = 0, then G = q → p : Γ and q Q ∈ M and Q G q . We get the statement without reducing M, since G q = p!Λ and msg(Λ ) = msg(Λ) = msg(Γ).

Direct Composition of Typed Multiparty Sessions

The use of gateways enables us to get a "safe" composition of systems by modifying just the interface participants. Therefore such an approach is useful after implementation, since it minimally affects systems that are already implemented. On the other hand, one would prefer to avoid the overhead due to gateways when composition is performed during development, as part of a modular design of systems via global types. In this setting one could easily modify the behaviour of any participant, since they have not been implemented yet.

One could hence wonder whether gateways are strictly necessary to get safe compositions in our multiparty-sessions setting. One could quite naturally expect that it is possible to "bypass" the use of gateways by removing them and simply applying a renaming function on the other participants' "communication behaviour". This however would be too naive an approach. As pointed out in [2] (Sect. 5.3), a "safe" composition of the systems in [2] which bypasses the use of gateways could require an heavy redesign of the participants involved in the inter-systems interactions. A disciplined setting as the present one, instead, enables direct composition to be handled more easily, both at the level of sessions and of global types, but some care is anyway needed. The following example, in fact, shows that just a renaming would not work in general.

Example 8.1 (Renaming is not Enough for Direct Composition). Consider the following global types and multiparty sessions.

G = p → h : .G G = k → r : .k → s : .G M = p P | h H M = r R | s S | k K where P = h! .P H = p? .H R = k? .R S = k? .S K = r! .s! .K
It is easy to check that M : G and M : G . In order to compose the above multiparty sessions, bypassing the gateways, we could take K out on the side of M , and rename some senders' and receivers' names in R and S so that they can receive the message directly from p, obtaining R = p? . R and S = p? . S. On the side of M, instead, after taking out H, we could not get a sound composition by a simple renaming for the recipient h in P = h! .P , since the message should be delivered,

Lemma 8.3 (Direct Composition is Well-Defined). Let (G, h) ↔ (G , k). Then G h k G is defined and it is a global type.
Proof. This lemma is the analogous of Lemma 6.8. Notice that Figure 9 and Figure 11 have exactly the same global types on the left side of the equalities. The proof of Lemma 6.8 only uses these global types. Therefore we can easily adapt these proofs to G h k G .

The global type G h k G can be shown to be well-formed and to preserve the projections of those participants which do not communicate with h or k.

Theorem 8.4 (Properties of Direct Composition). If (G, h) ↔ (G , k), then G h k G is well-formed. If p ∈ ptg(G) and h ∈ ptp(G p ), then G p = (G h k G ) p . If p ∈ ptg(G ) and k ∈ ptp(G p ), then G p = (G h k G ) p .
Proof.

To show well-formedness of G h k G we have to show that each participant has finite depth in each subterm of G h k G and that G h k G is projectable. It is easy to verify that if We can show that G h k G is projectable using the projectability of G, G and the definition of G h k G . Let us now move to the second property. If p ∈ ptg(Y) and h ∈ ptp(Y p ) we prove that Y p = (Y h k Y ) p for any recursive call Y h↔k Y in G h↔k G by coinduction and by cases on the last applied rule. Since h ∈ ptp(Y p ) only rules (4) and ( 5) can be used and these rules do not modify the communications of p, so we get the statement. The case of p ∈ ptg(Y ) and k ∈ ptp(Y p ) is analogous.

w = max{depth(G 0 , p) | G 0 is a subterm of G
We can hence obtain a direct composition function at the multipartysession level through the use of the function h k on global types.

Definition 8.5 (Multiparty Session Direct Composition

). Let M : G, M : G , (M, h) ↔ (M , k), with M ≡ M 1 | M 2 and M ≡ M 1 | M 2 be such that:
by the environment, rather than by an actual component of the system. Then, according to such an approach, there is actually no distinction between a closed and an open system. In particular, once two systems possess two "compatible" interfaces, they can be composed. The composition mechanism of [START_REF] Barbanera | Global Types for Open Systems[END_REF]2] uses suitable forwarders, dubbed "gateways", for this purpose. The gateways are automatically synthesised out of the compatible interfaces and the composition of two systems simply consists in replacing the latter by the former. It is worth noticing that such a "participants-as-interfaces" approach to compositionality does not affect the expected good features of standard modular techniques for system development, in particular for what concerns the notions of reuse and substitution of code. In fact a system has just to interpret an interface as the "dual"of the standard meaning. As far as we know, modularity of choreographic models has not been explored much. An exception is the approach recently proposed in [START_REF] Carbone | Choreographies for Reactive Programming[END_REF][START_REF] Savanovic | A Type Language for Message Passing Component-based Systems[END_REF]. Modularity is attained by means of a specified protocol regulating the communications at the "interface". Roughly speaking, this protocol represents the composition interface that rules out, among the communications of components, those not allowed in the composition. Components in [START_REF] Carbone | Choreographies for Reactive Programming[END_REF][START_REF] Savanovic | A Type Language for Message Passing Component-based Systems[END_REF] are reactive (similarly to [START_REF] Ferrari | Coordination Via Types in an Event-Based Framework[END_REF][START_REF] Ferrari | JSCL: A Middleware for Service Coordination[END_REF]). More precisely, components exports their input and output ports which are connected by links. A component is a computational unit that applies local transformations on data arriving at their input ports in order to produce events at their output ports. The typing discipline in [START_REF] Savanovic | A Type Language for Message Passing Component-based Systems[END_REF] is not concerned with the preservation of well-formedness of the system; rather, it tracks down data flow dependencies across the communications specified in the protocol.

In the present paper we have provided a MPST formalism where global types are used to describe the overall behaviour of "safe" systems of processes -dubbed multiparty sessions -directly related to the global types projections. We have then adapted and extended to such a formalism the approach of [1, 2], both at the global type and multiparty session levels. In general, managing to look at global types as overall descriptions of open systems results in a MPST-based approach to the modular design of systems. From another point of view, by means of such an approach, one could develop systems where some participants, instead of representing actual processes, describe API calls, along the line of what some researchers refer to as Behavioural API [START_REF]Behapi website[END_REF]. Moreover, this approach is helpful also after the system implementation phase. Let us assume to have a system developed using a MPST software development approach. After the implementation phase, one could realise that the service corresponding to a participant of the system can be more suitably provided by another system. The participant can then be safely replaced by a gateway composition with the other system, and the composition operation on global types enables a global view of what is going on in the resulting system.

Our calculus of multiparty sessions is like those of [START_REF] Dezani-Ciancaglini | Precise Subtyping for Synchronous Multiparty Sessions[END_REF][START_REF] Ghilezan | Precise Subtyping for Synchronous Multiparty Sessions[END_REF], but for the use of coinduction instead of induction, which is inspired by [START_REF] Castagna | A Theory of Contracts for Web Services[END_REF][START_REF] Severi | Observational Equivalence for Multiparty Sessions[END_REF]. As in [START_REF] Severi | Observational Equivalence for Multiparty Sessions[END_REF] we get rid of local types, which in many calculi are similar to processes [START_REF] Castellani | Reversible Sessions with Flexible Choices[END_REF][START_REF] Dezani-Ciancaglini | Precise Subtyping for Synchronous Multiparty Sessions[END_REF][START_REF] Ghilezan | Precise Subtyping for Synchronous Multiparty Sessions[END_REF]. The syntax of global types is the coinductive version of the standard syntax [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF]. With respect to [START_REF] Severi | Observational Equivalence for Multiparty Sessions[END_REF], we relax the conditions imposed on global types in order to be projectable, in particular ensuring projectability of global types resulting from our composition operation (a property that does not hold in the formalism of [START_REF] Severi | Observational Equivalence for Multiparty Sessions[END_REF]).

A relevant feature of our formalism is that the composition by gateways operation on systems can be lifted to the level of global types. In [START_REF] Barbanera | Global Types for Open Systems[END_REF]2], where systems of CFSMs were considered, such a lifting was done by extending the syntax of global descriptions with a new symbol, whose semantics is indeed the composition by gateways at system level. Instead, in the present paper, the session obtained by composition is represented using the standard syntax of global types. Moreover, we have shown that the compatibility relation of [START_REF] Barbanera | Global Types for Open Systems[END_REF]2], which requires duality, can be relaxed to a relation very close to session types subtyping [START_REF] Gay | Subtyping for Session Types in the Pi Calculus[END_REF][START_REF] Demangeon | Full Abstraction in a Subtyped Pi-Calculus with Linear Types[END_REF]. We further investigated the notion of compatibility by also showing that compatibility of global types is actually also a necessary condition in order to get a "safe" composition of systems.

Our formalism is equipped with a structural preorder on processes akin to the subtyping relation between session types of [START_REF] Castellani | Reversible Sessions with Flexible Choices[END_REF], which in turn is a restriction of the subtyping of [START_REF] Demangeon | Full Abstraction in a Subtyped Pi-Calculus with Linear Types[END_REF]. This choice is justified by the fact that the subtyping of [START_REF] Demangeon | Full Abstraction in a Subtyped Pi-Calculus with Linear Types[END_REF] allows process substitution, while the subtyping of [START_REF] Gay | Subtyping for Session Types in the Pi Calculus[END_REF] allows channel substitution, as observed in [START_REF] Gay | A List of Successes That Can Change the World -Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday[END_REF].

We have also shown that the composition by gateways technique can be extended so that the gateways can be actually dropped. This alternative approach has led to the definition of another composition operation that we dubbed direct. The use of direct composition -in particular at type levelyields a powerful tool. In fact, it enables the modular design and development of distributed systems, expecially in case such an operation can be pairedas we did -with another one enabling a global description to be decomposed. Small systems can be separately implemented out of the types obtained by decomposing a global type. Then by direct composition such systems can be merged into a system implementing the original global description, as shown by our results (some constraints have to be imposed on the global type to be decomposed).

A final contribution of the present paper is the discussion on how the properties of the given constructions change when we consider a structural preorder on processes mimicking the subtyping relation of [START_REF] Demangeon | Full Abstraction in a Subtyped Pi-Calculus with Linear Types[END_REF].

In [START_REF] Lange | Synthesising Choreographies from Local Session Types[END_REF][START_REF] Lange | On the Synthesis of Choreographies[END_REF] global types are built out of several local types (under certain conditions). We also aim at getting global types, but we obtain them from the global types describing the two systems which are composed.

The dynamic addition/removal of participants (they can join/leave the session after it has been set up) is supported in the calculus of [START_REF] Hu | Explicit Connection Actions in Multiparty Session Types[END_REF] and recently in [START_REF] Bruni | Data-Driven Choreographies à la Klaim[END_REF]. In [START_REF] Hu | Explicit Connection Actions in Multiparty Session Types[END_REF] the extension of a system is part of the global protocol. The extension operation is sort of internalised. We take instead the standard point of view of open systems, where the possible extensions cannot be decided in advance. This is also the point of view adopted in [START_REF] Bruni | Data-Driven Choreographies à la Klaim[END_REF], however the type system proposed in [START_REF] Bruni | Data-Driven Choreographies à la Klaim[END_REF] aims to guarantee data-flow properties instead of control properties. For instance, in [START_REF] Bruni | Data-Driven Choreographies à la Klaim[END_REF] well-typed systems may have locks. Both those approaches to the dynamic system extension issue look orthogonal to the work presented here.

Another approach to safe composition of systems allows one to replace a fragment of a choreography (essentially a program structured as a multiparty session type) with a new one at run-time [START_REF] Dalla Preda | Dynamic Choreographies: Theory and Implementation[END_REF], possibly also introducing new participants [START_REF] Gabbrielli | The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy -Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday[END_REF]. However, the new fragment could not communicate by exchanging messages with the context choreography, but only through shared state. Also, the change may deeply impact all the participants, and a complex middleware managing the change is needed. Hence, this approach is orthogonal to ours as well.

Both arbiter processes [START_REF] Carbone | Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types[END_REF] and mediums [START_REF] Caires | Multiparty Session Types Within a Canonical Binary Theory, and Beyond[END_REF] coordinate communications described by global types. A difference with the present paper is that their aim is to reduce the interactions in multiparty sessions to interactions in binary sessions. Our gateways do instead act as simple forwarders, with the aim of composing two multiparty systems. Nonetheless, our work could be further developed in the logical context of [START_REF] Carbone | Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types[END_REF]: in the logical interpretation of multiparty sessions one could introduce a "composition cut" corresponding to a sort of composition-by-gateways operator. Then the good properties of the system corresponding to the proof containing the cut should be guaranteed by proving that the "composition cut" is actually an admissible rule. The proof should consist of a "composition cut elimination" procedure corresponding to our direct composition on global types, which bypasses the use of gateways.

The results of this paper would be more applicable accounting for asynchronous communications. In particular, a first relevant step would consist in allowing gateways to interact asynchronously. We expect that compatibility could be extended, since the subtyping for asynchronous multiparty sessions is more permissive than the subtyping for the synchronous ones [START_REF] Mostrous | Global Principal Typing in Partially Commutative Asynchronous Sessions[END_REF]. Of course this extension requires care, since the subtyping of [START_REF] Mostrous | Global Principal Typing in Partially Commutative Asynchronous Sessions[END_REF] is undecidable, as shown in [START_REF] Bravetti | Undecidability of Asynchronous Session Subtyping[END_REF][START_REF] Lange | On the Undecidability of Asynchronous Session Subtyping[END_REF].

The composition via gateways proposed in [START_REF] Barbanera | Global Types for Open Systems[END_REF]2] and exploited in the present paper in a multiparty session setting does produce, by repeated composition, networks of systems possessing a tree-like topology. More precisely, after having composed two global types on a pair of interfaces h and k, one can take the result and compose it with a further global type, on another pair of interfaces h 1 and k 1 . One can iterate this procedure, and the graph where global types are nodes and connections are edges of the resulting system is actually a tree. In order to get graph topologies allowing for cycles, it sounds natural to extend the present single interface composition to a multiple interfaces one, or to allow connections among two roles of the same global type. Such an extension, however, immediately reveals itself to be unsound: by composing via gateways more than one pair of compatible interfaces one could obtain a deadlocked system. A very simple example for that is It is easy to realise that this sort of difficulty stays the same also in case direct composition is considered. In order to guarantee "safeness" of multiple connections, suitable requirements have hence to be devised. An adaptation to the present setting of the interaction type system of [START_REF] Coppo | Global Progress for Dynamically Interleaved Multiparty Sessions[END_REF] could be investigated in future for such an aim.

Figure 1 :

 1 Figure 1: UML-like diagrams of Systems 1 and 2

Figure 2 :

 2 Figure 2: UML-like diagram of Systems 1 and 2 gateway composition

Figure 3 :Figure 4 :

 34 Figure 3: UML-like diagram of Systems 1 and 2 direct composition

  by adding Bob and Carol gives the systems represented in Figure 4. Direct composition and decomposition form the basis of a modular design and implementation development process, where one can take a global description, divide it into descriptions of subsystems to be implemented separately, and then safely compose the resulting implementations.

Figure 5 :

 5 Figure 5: UML-like diagram for Example 2.4

Definition 2. 5 (

 5 Deadlock-freedom and Lock-freedom). Let M be a multiparty session. (i) M is a deadlock-free session if M -→ * M implies either M ≡ p 0 or M -→ M ; (ii) M is a lock-free session if M -→ * p P | M and P = 0 imply p P | M -→ * M λ -→ where p occurs in λ.

Definition 3 . 7 (

 37 Well-formed Global Types). A global type G is wellformed if: (a) depth(G , p) is finite for all G subterms of G and all p ∈ ptg(G); (b) G p is defined for all p ∈ ptg(G).Example 3.8. The global type G of Example 3.2 is well-formed, while the global type G of Example 3.6 is not well-formed, since the depth of r in G is not bounded.

  1≤i≤n} = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = The double-line in rules indicates that the rules are interpreted coinductively.

  [t-sess].

Lemma 4 . 1 (

 41 Inversion Lemma). If M : G and p P ∈ M, then P G p . Lemma 4.2 (Canonical Form Lemma). If M : G and p ∈ ptg(G), then there is p P ∈ M and P G p .

Lemma 4 . 5 .

 45 If G p q

Theorem 4 . 8 (

 48 Subject Reduction). If M : G and M p q--→ M , then G p q --→ G and M : G .

Theorem 4 .

 4 . If M is well-typed, then M is lock-free.Proof. Let M -→ * M ≡ p P | M with P = 0. According to Definition 2.5(ii) (lock-freedom), we have to show that p P | M -→ * M λ -→ where p occurs in λ. By Subject Reduction M can be typed. Let G be a type for M . Since M ≡ p 0, we can infer that G = End. We proceed now by induction on w = depth(G, p).If w = 0 then either G = p → q : Γ or G = q → p : Γ and G λ -→ G with p in λ by rule [ecomm]. Then M λ -→ M by Theorem 4.9(ii).If w > 0 then G = q → r : Γ with p ∈ {q, r} and G q r -→ G for all .G ∈ Γ by rule[ecomm]. By Lemma 4.6 depth(G, p) > depth(G , p) and induction applies.

Figure 6 :

 6 Figure 6: UML-like diagram for Example 5.1

=

  = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =

Figure 7 :

 7 Figure 7: UML-like diagrams for Definition 5.4

Definition 5 . 8 (

 58 Compatible Multiparty Sessions). Two multiparty sessions M, M are compatible via the participants h and k if pts(M) ∩ pts(M ) = ∅ and h H ∈ M and k K ∈ M with H ↔ K.

Figure 8 :

 8 Figure 8: UML-like diagram of Example 5.10

Lemma 6 .

 6 2 (Compatible Sessions have Compatible Types).If (M, h) ↔ (M , k) and M : G and M : G , then(G, h) ↔ (G , k) Proof.The typings M : G andM : G imply ptg(G) ⊆ pts(M) and ptg(G ) ⊆ pts(M ) by rule [t-sess]. Therefore we get that pts(M) ∩ pts(M ) = ∅ implies ptg(G) ∩ ptg(G ) = ∅. Let h H ∈ M and k K ∈ M . By the Inversion Lemma (Lemma 4.1) from M : G we get H G h and from M : G we get K G k . From (M, h) ↔ (M , k) we get H ↔ K by Definition 5.8. Lemma 5.7 implies G h ↔ G k .It is worth noticing that (G, h) ↔ (G , k) and M : G and M : G do not imply (M, h) ↔ (M , k), as shown in the following example. Example 6.3. Take

Figure 9 :Figure 10 :

 910 Figure 9: Definition of h↔k on global types

Example 6 . 5 .

 65 The protocol implemented by the multiparty session M de-fined in Example 5.1 can be represented by the following global type G r :

  k) = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = [rel-comm]

  1≤i≤m}, k) = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = The following lemma connects the agreement relation between pairs of global type/participant with the compatibility of the projections of global types on the participants. Lemma 6.7 (Agreement and Compatibility).

Theorem 6 . 10 (

 610 Typing Gateway Composition). If (M, h) ↔ (M , k) and M : G and M : G , then M h↔k M : G h↔k G . Proof. Let M ≡ M 1 | h H and M ≡ M 1 | k K. By construction

Lemma 7 . 4 (

 74 Projection and Reduction). Let M : G.

  and p ∈ ptg(G)} and w = max{depth(G 0 , p) | G 0 is a subterm of G and p ∈ ptg(G )} then depth( Ĝ, p) ≤ max{w, w } for all Ĝ subterm of G h k G and all p ∈ ptg(G) ∪ ptg(G ).

G

  = p → h : and G = k → s : By projection we get the systems M = p h! | h p? and M = k s! | s k? It is immediate to check that p and s are compatible, as well as h and k. Simultaneously connecting M and M through both the compatible pairs (p, s) and (h, k) would result in the following deadlocked system p s? .h! | h p? .k! | k h? .s! | s k? .p! (This example is similar to one developed in the CFSMs setting of [2]).

As a matter of fact, in[START_REF] Barbanera | Global Types for Open Systems[END_REF] "requests"and "offers"are required to exactly match, whereas in the present paper such a restriction can be safely relaxed.

Acknowledgments. We gratefully acknowledge the fruitful interactions and communications with the anonymous referees through the ICE Forum.

The present version of this paper strongly improved with respect to the journal submission thanks to the careful reports. The referees did a great job in pointing out many places where the technical details appeared without the needed explanations. The difference between the two versions are several illustrating discussions with enlightening examples.

 [START_REF] Barbanera | Global Types for Open Systems[END_REF]Partially supported by the project "Piano Triennale Ricerca" DMI-Università di Catania.

2 Partially supported by INdAM as members of GNCS (Gruppo Nazionale per il Calcolo Scientifico) 3 Research partly supported by the EU H2020 RISE programme under the Marie Sklodowska-Curie grant agreement No 778233 and by the MIUR project PRIN 2017FTXR7S "IT-MaTTerS" (Methods and Tools for Trustworthy Smart Systems).

We prove that the composition operation satisfies the constraints of the definition of global type (cf. Definition 3.1). Lemma 6.8 (Composition via Gateways is Well-Defined). Let (G, h) ↔ (G , k). Then G h↔k G is defined and it is a global type.

Proof. We start showing that the agreement relation is preserved by the recursive calls performed during the composition of global types.

Claim: Let (G, h) (G , k). Then for any call Y h↔k Y or Y k↔h Y in the tree of the recursive calls of G h↔k G we get (Y, h) (Y , k).

The proof of the Claim is by coinduction on the rules of Definition 6.6 and by cases on the rules of Definition 6.4. Rule (2):

is the conclusion of rule [rel-comm] (cf. Definition 6.6) with premises (Y i , h) (Y i , k) for all i, 1 ≤ i ≤ n. The proof for rule [START_REF] Barbanera | Open Multiparty Sessions[END_REF] is similar to the proof for rule (2). Rule (4):

is the conclusion of rule [rel-go] with premises (Y i , h) (Y , k) for all i, 1 ≤ i ≤ n. The proof for rule [START_REF] Barbanera | Reversible Client/Server Interactions[END_REF] is similar to the proof for rule [START_REF] Barbanera | Compliance for Reversible Client/Server Interactions[END_REF]. This ends the proof of the Claim.

We now show the lemma. From (G, h) ↔ (G , k) we have (G, h) (G , k). By the Claim for all recursive calls Y h↔k Y in G h↔k G we always get global types Y, Y such that (Y, h) (Y , k). We show that (Y, h) (Y , k) assures the applicability of one rule in Definition 6.4. The proof is by cases on the rules of Definition 6. [START_REF]Behapi website[END_REF]. Rule [rel-End]: we can apply rule [START_REF] Barbanera | Global Types for Open Systems[END_REF]. Rule [rel-go]: we can apply rule (4) or [START_REF] Barbanera | Reversible Client/Server Interactions[END_REF]. Rule [rel-comm]: we can apply rule (2) or [START_REF] Barbanera | Open Multiparty Sessions[END_REF]. Notice that the applicability of the rules in alternative is due to the symmetry of the relation (Y, h) (Y , k). The regularity of the obtained term follows by observing that the regularity of G and G implies that the tree of the recursive calls has no infinite path with pairwise distinct calls.

If w > 0, then G = r → s : { i .G i | 1≤i≤n} with p ∈ {r, s}, then by Definition 3.3 there is j, 1 ≤ j ≤ n, such that G j p = q?Λ j with ∈ Λ j . By rule [ecomm] of Definition 4.3 G r j s --→ G j . By Theorem 4.9(ii) M r j s --→ M and M : G j . We conclude using induction, since by Lemma 4.6 depth(G j , p) < w.

The proof of (ii) is simpler than the proof of (i), since when w > 0 and G = r → s : { i .G i | 1≤i≤n} with p ∈ {r, s}, then by Definition 3.3 we have

We can now prove that, whereas compatibility between sessions is not a necessary condition for lock-freedom preservation (as shown in Example 7.1), compatibility between global types is.

Theorem 7.5 (Necessity of Compatibility between Global Types

If G h = 0 and G k = 0, then H = 0 and K = 0. This implies gw(H, k) = 0 but gw(K, h) = 0. The messages in gw(K, h) with sender or receiver h will never be consumed. If G h = p?Λ 1 and G k = q?Λ 2 , then H = p?Λ 1 and K = q?Λ 2 . This implies gw(H, k) (after receiving a message from p) wants to send a message to k but gw(K, h) (after receiving a message from q) wants to send a message to h.

This implies gw(H, k) (before sending a message to p) waits for a message from k but gw(K, h) (before sending a message to q) waits for a message from h. Let G h = p!Λ 1 and G k = q?( .P Λ 2 ) and ∈ msg(Λ 1 ), then H = p!Λ 1 with msg(Λ 1 ) = msg(Λ 1 ) and K = q?( .P Λ 2 ) with msg(Λ 2 ) ⊇ msg(Λ 2 ). From Lemma 7.4(i). After Q exchanges the message with gw(K, h), the process gw(K, h) wants to send the message to h, but gw(H, k) cannot receive this message. More precisely

and by the Subject Reduction Theorem (Theorem 4.8) there is

Building G 1 and G 2 as in the proof of Theorem 4.8 we get

When gw(K, h) and gw(H, k) exchange the message they become gw(P, k) and gw(Q, h), so the network is not lock-free by induction hypothesis. More precisely

which is not lock-free by induction hypothesis.

Notice that Theorem 7.5 above is stated for typeable multiparty sessions, since it uses compatibility of their global types. alternately, to R and S. A safe direct composition would hence imply a less straightforward modification of P into P = r! .s! . P .

We implement a direct composition at the level of global types by means of the function h k defined below and we shall then use this function to achieve a similar composition of multiparty sessions as well. The composition of a communication between p as sender and h as receiver with a communication between k as sender and s as receiver gives a communication between p as sender and s as receiver. Similarly when the roles of h and k are exchanged. Instead the communications not involving h and k remain unchanged.

coinductively by the clauses of Figure 11, assuming {p, q, r, s} ∩ {h, k} = ∅. The clauses must be applied in the given order.

( The rules are in direct correspondence with the rules of composition via gateways (Definition 6.4) and the intuition is the same.

Taking G and G of Example 8.1, it is easy to check that (G, h) ↔ (G , k) and hence that we can apply direct composition on these global types, obtaining:

We prove now the soundness of the direct composition definition.

We define

Intuitively, participants not interacting with the interface are left unchanged, while the behaviour of the others is extracted from the composed global type.

The main result of this section connects the direct composition of global types and the direct composition of multiparty sessions.

For direct compositions we cannot compose M and M when M : G and M : G and ¬((G, h) ↔ (G , k)), since G h k G is undefined. So we cannot have a result similar to Theorem 7.5.

Decomposition of Typed Multiparty Sessions

In order to use direct composition in the modular development of systems one needs first to decompose a global specification into modules, then to develop the various modules in isolation, and finally to combine the modules using direct composition. We still miss an operation to decompose a global specification: this will be introduced in the present section. In particular, we will define a function enabling the decomposition of a global type into two global types, whose direct composition represents the same system of processes typed by the original global type. We start by defining the projection of a global type with respect to a set of participants P and a new participant h. In this projection:

• a communication between participants in P remains unchanged;

• a communication between one participant in P and one participant not in P becomes a communication between the participant in P and h;

• a communication between participants not in P is erased.

Definition 9.1 (Type Projection for Decomposition). The projection of a global type G with respect to a set of participants P and one interface participant h ∈ ptg(G) ∪ P is the global type G⇑ h P (if any) defined in Figure 12. It is easy to check that if ptg(G) = P, then G⇑ h P = G. Moreover if P = ∅, then G⇑ h P = End. For example, (p → q : .r → s. )⇑ h {p,q} = p → q : .(r → s. )⇑ h {p,q} = p → q : .End

48

Clearly the projection defined above is a partial function. In fact the condition in case p, q ∈ P is quite demanding. It requires the projection of a choice between participants not in P to be the same for all participants in P (this is a condition used in the standard projection of global types as well, see, e.g. [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF][START_REF] Honda | Multiparty Asynchronous Session Types[END_REF]), as shown by the result below.

and for all r ∈ P.

Proof. By coinduction on G and by cases on the definition of type projection for decomposition (Definition 9.1).

The condition above could be relaxed (similarly to what is done in the definition of projection on a single participant, Definition 3.3), but this would complicate the definition and we preferred simplicity.

We can now define the decomposition function on global types. Basically, the participants are split in two different global types, and two fresh interface participants are created to manage the communications between the two groups.

Definition 9.3 (Global Type Decomposition).

Let G be a global type, {P, Q} a partition of ptg(G) and h, k ∈ ptg(G) with h = k. We set

A first lemma proves that the global types obtained by decomposition are compatible via the fresh participants used in the decomposition.

Lemma 9.4 (Decomposition and Compatibility

The proof is by coinduction on G and by cases on Definition 9.1.

If G = p → q : Γ with p ∈ P and q ∈ Q, then by Definition 9.3

of the definition of the agreement relation (Definition 6.6).

If G = p → q : Γ with p, q ∈ P, then

The following theorem shows that decomposition is the left inverse of direct composition.

Proof. We show the thesis by coinduction on the structure of G and by cases on the definition of projection for decomposition (Definition 9.1).

If G = p → q : Γ with p ∈ P and q ∈ Q then

By definition of direct composition of global types (Definition 8.2), we get

Q for all .G ∈ Γ and hence the thesis.

If G = p → q : Γ with p, q ∈ P then

and we can conclude as in previous case.

Decomposition instead is not the right inverse of direct composition, since in building G 1 h k G 2 we discharge alternatives which cannot be recovered. For example p → h :

In the remainder of this section we discuss the decomposition of typed sessions. For that, a notion of process projection is handy. This projection is again parametrised on a set P of participants and a new participant h ∈ P. The communications of the process with participants in P remain unchanged. Instead the communications of the process with participants not in P become communications with h. Definition 9.6 (Process Projection for Decomposition). The projection of a process P with respect to a set of participants P and one interface participant h ∈ P is the process P⇑ h P defined by:

It is easy to verify that if ptp(P ) ⊆ P, then P ⇑ h P = P . Moreover, if P = ∅, then ptp(P⇑ h P ) = {h}. We look for a decomposition procedure at the multiparty-session level, through the use of the projection in Definition 9.1. Notice that if M : G and {P, Q} is a partition of ptg(G), then M ≡ Π p∈P p P p | Π q∈Q q Q q . We then decompose M in a session with participants P plus h and a session with participants Q plus k. The processes for the participants in P ∪ Q are obtained by means of the process projection in Definition 9.6 with respect to either P and h or Q and k. Instead the processes for h and k are the standard projections of the global types G 1 , G 2 obtained by decomposing G with respect to h and k. The typability of the resulting multiparty session is assured by the typing decomposition theorem (Theorem 9.9 below).

Definition 9.7 (Multiparty Session Decomposition). Let M : G and Dec

Notably, the decomposition function above exploits the type of the session.

A last proposition on structural preorder between input processes (with a trivial proof) is handy in showing the final theorem. Proposition 9.8 (Input Process Preorder). If P p?Λ and P p?Λ and msg(Λ) ∩ msg(Λ ) = ∅, then P p?(Λ Λ ).

The main result of this section is that the sessions obtained by decomposition can be typed by the global types obtained by decomposition. Theorem 9.9 (Typing Decomposition).

Proof. It is enough to show that P G p implies P ⇑ h P (G⇑ h P ) p with p ∈ P. The proof is by coinduction on G and by cases on its shape. The case

, by definition of projection on a single participant (Definition 3.3) and rule [sub-in] for the structural preorder (cf. Definition 3.9) we have

with n ≤ m and P i G i p for all i, 1 ≤ i ≤ n. By coinduction we get

By definitions of projections for decomposition (Definitions 9.6 and 9.1)

where s = q if q ∈ P and s = h otherwise. Then we get P ⇑ h P (G⇑ h P ) p by using the rule [sub-in] for structural preorder (Definition 3.9).

If G = q → p : Γ the proof is similar to the previous case using the rule [sub-out] of Definition 3.9.

If G = r → s : { i .G i | 1≤i≤n} and p ∈ {r, s}, then we have two cases. If {r, s} ∩ P = ∅, then by definition of type projection for decomposition (Definition 9.1), we have (G⇑ h P ) p = G p for some global type G such that G = G i ⇑ h P for all i, 1 ≤ i ≤ n. By the properties of projection for decomposition (Proposition 9.2), G i p = G 1 p for all i, 1 ≤ i ≤ n. So coinduction applies. Otherwise, when {r, s} ∩ P = ∅, by Definition 3.3 of projection on a single participant, we have two subcases:

In case 1 the proof is as before. In case 2, from Λ = Λ 1 . . . Λ n using rule [sub-in] of Definition 3.9, we get G p G i p , which implies P G i p for all i, 1 ≤ i ≤ n. By coinduction P ⇑ h P (G i ⇑ h P ) p for all i, 1 ≤ i ≤ n. By definition of type projection for decomposition (Definition 9.1), we get (G ⇑ h P ) p = t ?(Λ 1 . . . Λ n ) and (G i ⇑ h P ) p = t ?Λ i (where either t = t or t = h) and msg(Λ i ) = msg(Λ i ) for all i, 1 ≤ i ≤ n. We conclude P ⇑ h P (G ⇑ h P ) p by repeated application of the property of input process preorder (Proposition 9.8).

Example 9.10. If G 0 = p → r : .p → s : .G 0 and P = {p} and Q = {r, s}, then we get Dec h,k (G 0 , P, Q) = G, G where G = p → h : .G and G = k → r : .k → s : .G as in Example 8.1. Let P = r! .s! . P , R = p? . R and S = p? . S as in Example 8.7. We have

where P = h! .P , H = p? .H, R = k? .R, S = k? .S, and K = r! .s! .K as in Example 8.1. This shows an instance of Theorem 9.9.

For typed multiparty sessions the decomposition is not the left inverse of the direct composition, as shown by the following example.

Example 9.11. Take M ≡ p r! 1 | q s? 2 | r p?{ 1 , 3 } | s q! 2 and P = {p, q} and Q = {r, s} and G = p → r : 1 .s → q : 2 . We get

The difference between M and M 1 h k M 2 is that participant r in M waits for a message 3 from participant p. However, p will never send this message. As shown in this example, decomposing followed by composing typed sessions eliminates useless inputs. This is due to the replacement of some original processes by the projections of global types into the corresponding participants; see the definition of direct composition of multiparty sessions (Definition 8.5).

Standard Preorder on Processes

We now discuss the impact of adopting a structural preorder on processes mimicking the standard subtyping relation [START_REF] Demangeon | Full Abstraction in a Subtyped Pi-Calculus with Linear Types[END_REF]. We dub standard preorder this preorder and we denote it as + .

The relation + is obtained by replacing [sub-out] with [sub-out + ] below in Definition 3.9, and by replacing the symbol ' 'with ' + 'in the other rules.

[sub-out + ]

The relation + hence allows more outputs in larger processes than in smaller ones.

Let + be the typing system obtained by using + in rule [t-sess] (cf. Definition 3.10).

Lemmas 4.1 and 4.2 easily adapt to the system + .

Lemma 10.1 (Inversion Lemma for + ). If + M : G and p P ∈ M, then P + G p .

Lemma 10.2 (Canonical Form Lemma for + ). If + M : G and p ∈ ptg(G), then there is p P ∈ M and P + G p .

Clearly M : G implies + M : G, and a weakening of the vice versa is shown below.

Proof. The proof is by coinduction on G. Let G = p → q : Γ. Then, by the canonical form Lemma for + (Lemma 10.2) we get M ≡ p q!Λ | q p?Λ | M and q!Λ + G p and p?Λ + G q . By definition of

By definition of + again, we get P i + G i p and Q i + G i q for all i, 1 ≤ i ≤ n. Then we can derive

Thanks to the theorem above, the multiparty sessions that can be typed by and + do coincide.

A first effect of adopting + is a weaker notion of session fidelity (cfr. Theorem 4.9) than the one for . This is easily illustrated by the following example: using + , we can type the session M = p q! 1 | q p?{ 1 , 2 } with G = p → q : { 1 , 2 }, namely + M : G holds. However G p i q --→ End with i = 1, 2, while the only reduction of M is M p 1 q --→ p 0. Notice that G p = q!{ 1 , 2 } and G q = p?{ 1 , 2 }, hence q! 1 + G p but q! 1 G p . This is reminiscent of the notion of whole-spectrum realisation introduced in [START_REF] Bocchi | Resolving Nondeterminism in Choreographies[END_REF][START_REF] Bocchi | On Resolving Nondeterminism in Choreographies[END_REF] and that indeed rules out sessions that bluntly "ignore" some branches in the choices occurring in the global type.

The monotonicity of gateways Lemma (Lemma 5.6) does not hold for + , as shown by the following counterexample.

The reason is that + allows larger processes to contain additional messages in send operations, but the gateway construction would introduce additional messages in inputs.

Instead we can show the analogous of Lemmas 5.7 and 6.2 for + .

Lemma 10.4 (Compatibility is Upward-Closed under + ). If P ↔ Q, then P + P and Q + Q imply P ↔ Q .

Proof. Let us assume

From P ↔ Q we get P i ↔ Q i for all i, 1 ≤ i ≤ n . From P + P we get

. By coinduction we have P i ↔ Q i for all i, 1 ≤ i ≤ n . We can then conclude P ↔ Q .

Proof. The proof mimics that of Lemma 6.2, just using Lemma 10.4 instead of Lemma 5.7.

A main drawback of rule [sub-out + ] is that the typing of gateway composition (cfr. Theorem 6.10) fails to hold due to the fact that + breaks the monotonicity of gateways (cfr. Lemma 5.6). We can anyway prove a similar result for + . Theorem 10.6 (Typing Gateway Composition in + ). If (M, h) ↔ (M , k) and + M : G and + M : G , then + M h↔k M : G for some G .

Proof. Theorem 10.3 implies M : G 1 and M : G 2 for some G 1 , G 2 . Theorem 6.10 gives M h↔k M : G 1 h↔k G 2 . We can choose G = G 1 h↔k G 2 . This concludes the proof.

Compatibility of global types is not necessary to get deadlock-freedom of composition via gateways for the type system + . Let

reduces only as follows:

As this example shows, if the cause of ¬ (G, h) ↔ (G , k) occurs after an output that is not present in M and M , then no deadlock arises by composing them via gateways.

Instead we can show that the direct composition of multiparty sessions can be typed using the direct composition of global types, as in the system , and differently with respect to the composition via gateways. We define M h + + k M as M h k M (cf. Definition 8.5), but using + instead of .

Theorem 10.7 (Typing Direct Composition in + ).

Proof. The proof is as the proof of Theorem 8.6 using Lemma 10.5 instead of Lemma 6.2.

The decomposition of global types and multiparty sessions is insensible to the difference between and + as well. In particular an analogous of Proposition 9.8 holds. This is not surprising since and + only differ for outputs.

Proposition 10.8 (Input Process Standard Preorder). If P + p?Λ and P + p?Λ and msg(Λ) ∩ msg(Λ ) = ∅, then P + p?(Λ Λ ). Theorem 10.9 (Typing Decomposition in + ).

Proof. Like in the proof of the typing decomposition Theorem for (Theorem 9.9), it is enough to show that P + G p implies P ⇑ h P + (G ⇑ h P ) p with p ∈ P. Here we show only the cases whose proofs differ from those considered in Theorem 9.9.

If G = p → q : { i .G i | 1≤i≤n}, by the definition of projection on a single participant (Definition 3.3) we have P = q!{ i .P i | 1≤i≤n} and G p = q!{ i .G If G = r → s : { i .G i | 1≤i≤n} the proof is as for Theorem 9.9, but using Proposition 10.8 instead of Proposition 9.8. We think that this section justifies our choice of structural preorder between processes in building composition by gateways, which is mainly due to the stronger notion of session fidelity it enables and to the fact that it eases the definition of composition via gateways and it makes compatibility a necessary condition for lock-freedom.

Concluding Remarks, Related Work, and Future Developments

The distinguishing feature of an open system of concurrent components is its capacity of communicating with the "outside", i.e. with some environment of the system. This ability provides means for composing open systems into larger systems (which may still be open). In order to compose systems "safely", it is common practice to rely on interface descriptions. MPST systems [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF][START_REF] Coppo | A Gentle Introduction to Multiparty Asynchronous Session Types[END_REF][START_REF] Mostrous | Global Principal Typing in Partially Commutative Asynchronous Sessions[END_REF] are usually assumed to be closed, since all the components needed for the functioning of the system must be already there. As a matter of fact, the MPST framework does work fairly well for the design of closed systems, but does not possess the flexibility open systems can offer. In [START_REF] Barbanera | Global Types for Open Systems[END_REF]2] a novel approach to open systems has been proposed where, according to the current needs, the behaviour of any participant can be regarded as an "interface". An interface is hence intended to represent -somehow dually with respect to the standard notion of interface -part of the expected communication behaviour of the environment. Identifying a participant behaviour as interface corresponds to expecting such a behaviour to be realised