# On global types and multi-party sessions

Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Luca Padovani

► To cite this version:

Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Luca Padovani. On global types and multi-party sessions. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEschniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. pp.1-28, 10.1007/978-3-642-21461-5_1 . hal-00618814

HAL Id: hal-00618814

https://hal.science/hal-00618814v1

Submitted on 3 Sep 2011

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# On Global Types and Multi-Party Sessions

Giuseppe Castagna¹, Mariangiola Dezani-Ciancaglini², and Luca Padovani²

¹ CNRS, Université Paris Diderot – Paris 7

² Dipartimento d'Informatica, Università degli Studi di Torino

**Abstract.** We present a new, streamlined language of global types equipped with a trace-based semantics and whose features and restrictions are semantically justified. The multi-party sessions obtained projecting our global types enjoy a live-ness property in addition to the traditional progress and are shown to be sound and complete with respect to the set of traces of the originating global type. Our notion of completeness is less demanding than the classical ones, allowing a multi-party session to leave out redundant traces from an underspecified global type.

## 1 Introduction

Relating the global specification of a system of communicating entities with an implementation (or description) of the single entities is a great classic in many different areas of computer science. The recent development of *session-based computing* has renewed the interest in this problem. In this work we attack it from the behavioral type and process algebra perspectives and briefly compare the approaches used in other areas.

A (multi-party) session is a place of interaction for a restricted number of participants that communicate messages. The interaction may involve the exchange of arbitrary sequences of messages of possibly different types. Sessions are restricted to a (usually fixed) number of participants, which makes them suitable as a structuring construct for systems of communicating entities. In this work we define a language to describe the interactions that may take place among the participants implementing a given session. In particular, we aim at a definition based on few “essential” assumptions that should not depend on the way each single participant is implemented. To give an example, a bargaining protocol that includes two participants, “seller” and “buyer”, can be informally described as follows:

> Seller sends *buyer a price and a description of the product; then buyer sends seller acceptance or it quits the conversation.*

If we abstract from the value of the price and the content of the description sent by the seller, this simple protocol describes just two possible executions, according to whether the buyer accepts or quits. If we consider that the price and the description are in distinct messages then the possible executions become four, according to which communication happens first. While the protocol above describes a finite set of possible interactions, it can be easily modified to accommodate infinitely many possible executions, as well as additional conversations: for instance the protocol may allow “buyer” to answer “seller” with a counteroffer, or it may interleave this bargaining with an independent bargaining with a second seller.
All essential features of protocols are in the example above, which connects some basic communication actions by the flow control points we underlined in the text. More generally, a protocol is a possibly infinite set of finite sequences of interactions between a fixed set of participants. We argue that the set of sequences that characterizes a protocol—and thus the protocol itself—can be described by a language with one form of atomic actions and three composition operators.

**Atomic actions.** The only atomic action is the interaction, which consists of one (or more) sender(s) (eg, “seller sends”), the content of the communication (eg, “a price”, “a description”, “acceptance”), and one (or more) receiver(s) (eg, “buyer”).

**Compound actions.** Actions and, more generally, protocols can be composed in three different ways. First, two protocols can be composed sequentially (eg, “Seller sends buyer a price…; then buyer sends…”) thus imposing a precise order between the actions of the composed protocols. Alternatively, two protocols can be composed unconstrainedly, without specifying any order (eg, “Seller sends a price and (sends) a description”) thus specifying that any order between the actions of the composed protocols is acceptable. Finally, protocols can be composed in alternative (eg, “buyer sends acceptance or it quits”), thus offering a choice between two or more protocols only one of which may be chosen.

More formally, we use $p \stackrel{a}{\to} q$ to state that participant p sends participant q a message whose content is described by a, and we use “;”, “∧”, and “$\vee$” to denote sequential, unconstrained, and alternative composition, respectively. Our initial example can thus be rewritten as follows:

$$ \begin{array}{l} (\mathit{seller} \xrightarrow{\mathit{descr}} \mathit{buyer} \wedge \mathit{seller} \xrightarrow{\mathit{price}} \mathit{buyer}); \\ (\mathit{buyer} \xrightarrow{\mathit{accept}} \mathit{seller} \vee \mathit{buyer} \xrightarrow{\mathit{quit}} \mathit{seller}) \end{array} \qquad (1) $$

The first two actions are composed unconstrainedly, and they are to be followed by one (and only one) action of the alternative before ending. Interactions of unlimited length can be defined by resorting to a Kleene star notation. For example to extend the previous protocol so that the buyer may send a counter-offer and wait for a new price, it suffices to add a Kleene-starred line:

$$ \begin{array}{l} (\mathit{seller} \xrightarrow{\mathit{descr}} \mathit{buyer} \wedge \mathit{seller} \xrightarrow{\mathit{price}} \mathit{buyer}); \\ (\mathit{buyer} \xrightarrow{\mathit{offer}} \mathit{seller}; \mathit{seller} \xrightarrow{\mathit{price}} \mathit{buyer})*; \\ (\mathit{buyer} \xrightarrow{\mathit{accept}} \mathit{seller} \vee \mathit{buyer} \xrightarrow{\mathit{quit}} \mathit{seller}) \end{array} \qquad (2) $$

The description above states that, after having received (in no particular order) the price and the description from the seller, the buyer can initiate a loop of zero or more interactions and then decide whether to accept or quit.

Whenever there is an alternative there must be a participant that decides which path to take. In both examples it is buyer that makes the choice by deciding whether to send *accept* or *quit*. The presence of a participant that decides holds true in loops too, since it is again buyer that decides whether to enter or repeat the iteration (by sending *offer*) or to exit it (by sending *accept* or *quit*). We will later show that absence of such decision-makers gives protocols impossible to implement. This last point critically
depends on the main hypothesis we assume about the systems we are going to describe, that is the absence of *covert channels*. One the one hand, we try to develop a protocol description language that is as generic as possible; on the other hand, we limit the power of the system and require all communications between different participants to be explicitly stated. In doing so we bar out protocols whose implementation essentially relies on the presence of secret/invisible communications between participants: a protocol description must contain all and only the interactions used to implement it.

Protocol specifications such as the ones presented above are usually called *global types* to emphasize the fact that they describe the acceptable behaviours of a system from a global point of view. In an actual implementation of the system, though, each participant autonomously implements a different part of the protocol. To understand whether an implementation satisfies a specification, one has to consider the set of all possible sequences of synchronizations performed by the implementation and check whether this set satisfies five basic properties:

1. *Sequentiality*: if the specification states that two interactions must occur in a given order (by separating them by a “;”), then this order must be respected by all possible executions. So an implementation in which *buyer* may send *accept* before receiving *price* violates the specification.

2. *Alternativeness*: if the specification states that two interactions are alternative, then every execution must exhibit one and only one of these two actions. So an implementation in which *buyer* emits both *accept* and *quit* (or none of them) in the same execution violates the specification.

3. *Shuffling*: if the specification composes two sequences of interactions in an unconstrained way, then all executions must exhibit some shuffling (in the sense used in combinatorics and algebra) of these sequences. So an implementation in which *seller* emits *price* without emitting *descr* violates the specification.

4. *Fitness*: if the implementation exhibits a sequence of interactions, then this sequence is expected by (*ie*, it fits) the specification. So any implementation in which *seller* sends *buyer* any message other than *price* and *descr* violates the specification.

5. *Exhaustivity*: if some sequence of interactions is described by the specification, then there must exist at least an execution of the implementation that exhibits these actions (possibly in a different order). So an implementation in which no execution of *buyer* emits *accept* violates the specification.

Checking whether an implemented system satisfies a specification by comparing the actual and the expected sequences of interactions is non-trivial, for systems are usually infinite-state. Therefore, on the lines of [9, 16], we proceed the other way round: we extract from a global type the local specification (usually dubbed *session type* [20, 15]) of each participant in the system and we type-check the implementation of each participant against the corresponding session type. If the projection operation is done properly and the global specification satisfies some well-formedness conditions, then we are guaranteed that the implementation satisfies the specification. As an example, the global type (1) can be projected to the following behaviors for *buyer* and *seller*:

*seller* $\mapsto$ *buyer!descr.buyer!price*.(*buyer?accept* + *buyer?quit*)

*buyer* $\mapsto$ *seller?descr.seller?price*.(*seller!accept* $\oplus$ *seller!quit*)
or to

$$ 
\begin{aligned}
seller &\mapsto \text{buyer!price.buyer!descr.}(\text{buyer?accept} + \text{buyer?quit}) \\
\text{buyer} &\mapsto \text{seller?price.seller?descr.}(\text{seller!accept} \oplus \text{seller!quit})
\end{aligned}
 $$

where p!a denotes the output of a message a to participant p, p?a the input of a message a from participant p, p?a.T + q?b.S the (external) choice to continue as T or S according to whether a is received from p or b is received from q and, finally, p!a.T ⊕ q!b.S denotes the (internal) choice between sending a to p and continue as T or sending S to q and continue as T. We will call *session environments* the mappings from participants to their session types. It is easy to see that any two processes implementing buyer and seller will satisfy the global type (1) if and only if their visible behaviors matches one of the two session environments above (these session environments thus represent some sort of minimal typings of processes implementing buyer and seller). In particular, both the above session environments are fitting and exhaustive with respect to the specification since they precisely describe what the single participants are expected and bound to do.

We conclude this introduction by observing that there are global types that are intrinsically flawed, in the sense that they do not admit any implementation (without covert channels) satisfying them. We classify flawed global types in three categories, according to the seriousness of their flaws.

[No sequentiality] The mildest flaws are those in which the global type specifies some sequentiality constraint between independent interactions, such as in $(p \xrightarrow{a} q; r \xrightarrow{b} s)$, since it is impossible to implement r so that it sends b only after that q has received a (unless this reception is notified on a covert channel, of course). Therefore, it is possible to find exhaustive (but not fitting) implementations that include some unexpected sequences which differ from the expected ones only by a permutation of interactions done by independent participants. The specification at issue can be easily patched by replacing some “;” by “^”.

[No knowledge for choice] A more severe kind of flaw occurs when the global type requires some participant to behave in different ways in accordance with some choice it is unaware of. For instance, in the global type

$$ (p \xrightarrow{a} q; q \xrightarrow{a} r; r \xrightarrow{a} p) \lor (p \xrightarrow{b} q; q \xrightarrow{a} r; r \xrightarrow{b} p) $$

participant p chooses the branch to execute, but after having received a from q participant r has no way to know whether it has to send a or b. Also in this case it is possible to find exhaustive (but not fitting) implementations of the global type where the participant r chooses to send a or b independently of what p decided to do.

[No knowledge, no choice] In the worst case it is not possible to find an exhaustive implementation of the global type, for it specifies some combination of incompatible behaviors, such as performing and input or an output in mutual exclusion. This typically is the case of the absence of a decision-maker in the alternatives such as in

$$ p \xrightarrow{a} q \lor q \xrightarrow{b} p $$

where each participant is required to choose between sending or receiving. There seems to be no obvious way to patch these global types without reconsidering also the intended semantics.
**Contributions and outline.** A first contribution of this work is to introduce a streamlined language of global specifications—that we dub *global types* (Section 2)—and to relate it with *session environments* (Section 3), that is, with sets of independent, sequential, asynchronous *session types* to be type-checked against implementations. Global types are just regular expressions augmented with a shuffling operator and their semantics is defined in terms of finite sequences of interactions. The second contribution, which is a consequence of the chosen semantics of global types, is to ensure that every implementation of a global type preserves the possibility to reach a state where every participant has successfully terminated.

In Section 4 we study the relationship between global types and sessions. We do so by defining a projection operation that extracts from a global type *all* the (sets of) possible session types of its participants. This projection is useful not only to check the implementability of a global description (and, incidentally, to formally define the notions of errors informally described so far) but, above all, to relate in a compositional and modular way a global type with the sets of distributed processes that implement it. We also identify a class of well-formed global types whose projections need no covert channels. Interestingly, we are able to effectively characterize well-formed global types solely in terms of their semantics.

In Section 5 we present a projection algorithm for global types. The effective generation of all possible projections is impossible. The reason is that the projectability of a global type may rely on some global knowledge that is no longer available when working at the level of single session types: while in a global approach we can, say, add to some participant new synchronization offers that, thanks to our global knowledge, we know will never be used, this cannot be done when working at the level of single participant. Therefore in order to work at the projected level we will use stronger assumptions that ensure a sound implementation in all possible contexts.

In Section 6 we show some limitations deriving from the use of the Kleene star operator in our language of global types, and we present one possible way to circumvent them. We conclude with an extended discussion on related work (Section 7) and a few final considerations (Section 8).

Proofs, more examples and an extended survey of related work were omitted and can be found in the long version available on the authors' home pages.

## 2 Global Types

In this section we define syntax and semantics of global types. We assume a set $\mathcal{A}$ of *message types*, ranged over by $a, b, \dots$, and a set $\Pi$ of *roles*, ranged over by $p, q, \dots$, which we use to uniquely identify the participants of a session; we let $\pi, \dots$ range over non-empty, finite sets of roles.

Global types, ranged over by $\mathcal{G}$, are the terms generated by the grammar in Table 1. Their syntax was already explained in Section 1 except for two novelties. First, we include a *skip* atom which denotes the unit of sequential composition (it plays the same role as the empty word in regular expressions). This is useful, for instance, to express optional interactions. Thus, if in our example we want the buyer to do at most one
<table><caption>**Table 1.** Syntax of global types.</caption><thead><tr><th colspan="2">G ::=</th><th>Global Type</th><th></th><th></th></tr></thead><tbody><tr><td></td><td>skip</td><td>(skip)</td><td>| π <sup>a</sup> → p</td><td>(interaction)</td></tr><tr><td>|</td><td>G; G</td><td>(sequence)</td><td>| G ∧ G</td><td>(both)</td></tr><tr><td>|</td><td>G ∨ G</td><td>(either)</td><td>| G*</td><td>(star)</td></tr></tbody></table>

counteroffer instead of several ones, we just replace the starred line in (2) by

$$ (\text{buyer} \xrightarrow{\text{offer}} \text{seller}; \text{seller} \xrightarrow{\text{price}} \text{buyer}) \lor \text{skip} $$

which, using syntactic sugar of regular expressions, might be rendered as

$$ (\text{buyer} \xrightarrow{\text{offer}} \text{seller}; \text{seller} \xrightarrow{\text{price}} \text{buyer})? $$

Second, we generalize interactions by allowing a finite set of roles on the l.h.s. of interactions. Therefore, $\pi \xrightarrow{a} p$ denotes the fact that (the participant identified by) p waits for an $a$ message from all of the participants whose tags are in $\pi$. We will write $p \xrightarrow{a} q$ as a shorthand for $\{p\} \xrightarrow{a} q$.

To be as general as possible, one could also consider interactions of the form $\pi \xrightarrow{a} \pi'$, which could be used to specify broadcast communications between participants. It turns out that this further generalization is superfluous in our setting since the interaction $\pi \xrightarrow{a} \{p_i\}_{i \in I}$ can be encoded as $\bigwedge_{i \in I}(\pi \xrightarrow{a} p_i)$. The encoding is made possible by the fact that communication is asynchronous and output actions are not blocking (see Section 3), therefore the order in which the participants in $\pi$ send $a$ to the $p_i$'s is irrelevant. Vice versa, we will see that allowing sets of multiple senders enriches the expressiveness of the calculus, because $\pi \xrightarrow{a} p$ can be used to join different activities involving the participants in $\pi \cup \{p\}$, while $\bigwedge_{i \in I}(p_i \xrightarrow{a} q)$ represents fork of parallel activities. For example, we can represent two buyers waiting for both the price from a seller and the mortgage from a bank before deciding the purchase:

$$ \begin{array}{l} (\text{seller} \xrightarrow{\text{price}} \text{buyer1} \land \text{bank} \xrightarrow{\text{mortgage}} \text{buyer2}); \\ (\{\text{buyer1, buyer2}\} \xrightarrow{\text{accept}} \text{seller} \land \{\text{buyer1, buyer2}\} \xrightarrow{\text{accept}} \text{bank}) \end{array} \qquad (3) $$

In general we will assume $p \notin \pi$ for every interaction $\pi \xrightarrow{a} p$ occurring in a global type, that is, we forbid participants to send messages to themselves. For the sake of readability we adopt the following precedence of global type operators $\to^*$; $\land \lor$.

Global types denote languages of legal interactions that can occur in a multi-party session. These languages are defined over the alphabet of interactions

$$ \Sigma = \{ \pi \xrightarrow{a} p \mid \pi \subset_{\text{fin}} \Pi, p \in \Pi, p \notin \pi, a \in \mathcal{A} \} $$

and we use $\alpha$ as short for $\pi \xrightarrow{a} p$ when possible; we use $\varphi, \psi, \dots$ to range over strings in $\Sigma^*$ and $\varepsilon$ to denote the empty string, as usual. To improve readability we will sometimes use “;” to denote string concatenation.
In order to express the language of a global type having the shape $\mathcal{G}_1 \wedge \mathcal{G}_2$ we need a standard shuffling operator over languages, which can be defined as follows:

**Definition 2.1 (shuffling).** The shuffle of $L_1$ and $L_2$, denoted by $L_1 \sqcup L_2$, is the language defined by: $L_1 \sqcup L_2 \stackrel{\text{def}}{=} \{\varphi_1 \psi_1 \cdots \varphi_n \psi_n \mid \varphi_1 \cdots \varphi_n \in L_1 \wedge \psi_1 \cdots \psi_n \in L_2\}$.

Observe that, in $L_1 \sqcup L_2$, the order of interactions coming from one language is preserved, but these interactions can be interspersed with other interactions coming from the other language.

**Definition 2.2 (traces of global types).** The set of traces of a global type is inductively defined by the following equations:

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \mathrm{tr}(\mathrm{skip}) = \{\varepsilon\} & \mathrm{tr}(\mathcal{G}_1; \mathcal{G}_2) = \mathrm{tr}(\mathcal{G}_1)\mathrm{tr}(\mathcal{G}_2) & \mathrm{tr}(\mathcal{G}_1 \vee \mathcal{G}_2) = \mathrm{tr}(\mathcal{G}_1) \cup \mathrm{tr}(\mathcal{G}_2) \\ \mathrm{tr}(\pi \xrightarrow{a} p) = \{\pi \xrightarrow{a} p\} & \mathrm{tr}(\mathcal{G}^*) = (\mathrm{tr}(\mathcal{G}))^* & \mathrm{tr}(\mathcal{G}_1 \wedge \mathcal{G}_2) = \mathrm{tr}(\mathcal{G}_1) \sqcup \mathrm{tr}(\mathcal{G}_2) \end{array} $$

where juxtaposition denotes concatenation and $(\cdot)^*$ is the usual Kleene closure of regular languages.

Before we move on, it is worth noting that $\mathrm{tr}(\mathcal{G})$ is a regular language (recall that regular languages are closed under shuffling). Since a regular language is made of finite strings, we are implicitly making the assumption that a global type specifies interactions of finite length. This means that we are considering interactions of arbitraty length, but such that the termination of all the involved participants is always within reach. This is a subtle, yet radical change from other multi-party session theories, where infinite interactions are considered legal.

# 3 Multi-Party Sessions

We devote this section to the formal definition of the behavior of the participants of a multiparty session.

## 3.1 Session Types

We need an infinite set of recursion variables ranged over by $X$, $\dots$. Pre-session types, ranged over by $T$, $S$, $\dots$, are the terms generated by the grammar in Table 2 such that all recursion variables are guarded by at least one input or output prefix. We consider pre-session types modulo associativity, commutativity, and idempotence of internal and external choices, fold/unfold of recursions and the equalities

$$ \pi!a.T \oplus \pi!a.S = \pi!a.(T \oplus S) \qquad \pi?a.T + \pi?a.S = \pi?a.(T + S) $$

Pre-session types are behavioral descriptions of the participants of a multiparty session. Informally, end describes a successfully terminated party that no longer participates to a session. The pre-session type $p!a.T$ describes a participant that sends an $a$ message to participant $p$ and afterwards behaves according to $T$; the pre-session type $\pi?a.T$ describes a participant that waits for an $a$ message from all the participants in $\pi$
<table><caption>**Table 2.** Syntax of pre-session types.</caption><thead><tr><th colspan="2">T ::=</th><th colspan="2">Pre-Session Type</th></tr></thead><tbody><tr><td></td><td>end</td><td>(termination)</td><td>X (variable)</td></tr><tr><td></td><td>p!a.T</td><td>(output)</td><td>π?a.T (input)</td></tr><tr><td></td><td>T ⊕ T</td><td>(internal choice)</td><td>T + T (external choice)</td></tr><tr><td></td><td>rec X.T</td><td>(recursion)</td><td></td></tr></tbody></table>

and, upon arrival of the message, behaves according to *T*; we will usually abbreviate {p}?a.T with p?a.T. Behaviors can be combined by means of behavioral choices ⊕ and +: T ⊕ S describes a participant that internally decides whether to behave according to *T* or S; T + S describes a participant that offers to the other participants two possible behaviors, *T* and S. The choice as to which behavior is taken depends on the messages sent by the other participant. In the following, we sometimes use *n*-ary versions of internal and external choices and write, for example, ⊕<sub>i=1</sub><sup>n</sup> p<sub>i</sub>?a<sub>i</sub>.T<sub>i</sub> for p<sub>1</sub>?a<sub>1</sub>.T<sub>1</sub> ⊕ ... ⊕ p<sub>n</sub>?a<sub>n</sub>.T<sub>n</sub> and Σ<sub>i=1</sub><sup>n</sup> π<sub>i</sub>?a<sub>i</sub>.T<sub>i</sub> for π<sub>1</sub>?a<sub>1</sub>.T<sub>1</sub> + ... + π<sub>n</sub>?a<sub>n</sub>.T<sub>n</sub>. As usual, terms *X* and *rec X.T* are used for describing recursive behaviors. As an example, rec X.(p!a.X ⊕ p?!b.end) describes a participant that sends an arbitrary number of *a* messages to *p* and terminates by sending a *b* message; dually, rec X.(p?a.X + p?!b.end) describes a participant that is capable of receiving an arbitrary number of *a* messages from *p* and terminates as soon a *b* message is received.

Session types are the pre-session types where internal choices are used to combine outputs, external choices are used to combine inputs, and the continuation after every prefix is uniquely determined by the prefix. Formally:

**Definition 3.1 (session types).** A pre-session type *T* is a session type if either:

- *T* = end, or

- *T* = ⊕<sub>i∈I</sub> p<sub>i</sub>?a<sub>i</sub>.T<sub>i</sub> and ∀i, j ∈ I we have that p<sub>i</sub>?a<sub>i</sub> = p<sub>j</sub>?a<sub>j</sub> implies i = j and each T<sub>i</sub> is a session type, or

- *T* = Σ<sub>i∈I</sub> π<sub>i</sub>?a<sub>i</sub>.T<sub>i</sub> and ∀i, j ∈ I we have that π<sub>i</sub> ⊆ π<sub>j</sub> and a<sub>i</sub> = a<sub>j</sub> imply i = j and each T<sub>i</sub> is a session type.

## 3.2 Session Environments

A session environment is defined as the set of the session types of its participants, where each participant is uniquely identified by a role. Formally:

**Definition 3.2 (session environment).** A session environment (briefly, session) is a finite map {p<sub>i</sub> : T<sub>i</sub>}<sub>i∈I</sub>.

In what follows we use Δ to range over sessions and we write Δ ⊕ Δ' to denote the union of sessions, when their domains are disjoint.

To describe the operational semantics of a session we model an asynchronous form of communication where the messages sent by the participants of the session are stored within a buffer associated with the session. Each message has the form p<sub>i</sub> →<sub>a</sub> q describing the sender *p*, the receiver *q*, and the type *a* of message. Buffers, ranged over by B,
..., are finite sequences $p_1 \xrightarrow{a_1} q_1 :: \dots :: p_n \xrightarrow{a_n} q_n$ of messages considered modulo the least congruence $\simeq$ over buffers such that:

$$p \xrightarrow{a} q :: p' \xrightarrow{b} q' \simeq p' \xrightarrow{b} q' :: p \xrightarrow{a} q \quad \text{for } p \neq p' \text{ or } q \neq q'$$

that is, we care about the order of messages in the buffer only when these have both the same sender and the same receiver. In practice, this corresponds to a form of communication where each pair of participants of a multiparty session is connected by a distinct FIFO buffer.

There are two possible reductions of a session:

$$\mathbb{B}^{\diamond}_{\diamond} \{ \mathbf{p} : \bigoplus_{i \in I} \mathbf{p}_i! a_i . T_i \} \uplus \Delta \longrightarrow (\mathbf{p} \xrightarrow{a_k} \mathbf{p}_k) :: \mathbb{B}^{\diamond}_{\diamond} \{ \mathbf{p} : T_k \} \uplus \Delta \quad (k \in I) \\ \mathbb{B}^{::} (\mathbf{p}_i \xrightarrow{a} \mathbf{p})_{i \in I^{\diamond}} \{ \mathbf{p} : \sum_{j \in J} \pi_j? a_j . T_j \} \uplus \Delta \xrightarrow{\pi_k \xrightarrow{a} \mathbf{p}} \mathbb{B}^{\diamond}_{\diamond} \{ \mathbf{p} : T_k \} \uplus \Delta \quad \begin{pmatrix} k \in J & a_k=a \\ \pi_k=\{\mathbf{p}_i | i \in I\} \end{pmatrix}$$

The first rule describes the effect of an output operation performed by participant p, which stores the message p $\xrightarrow{a_k} p_k$ in the buffer and leaves participant p with a residual session type $T_k$ corresponding to the message that has been sent. The second rule describes the effect of an input operation performed by participant p. If the buffer contains enough messages of type a coming from all the participants in $\pi_k$, those messages are removed from the buffer and the receiver continues as described in $T_k$. In this rule we decorate the reduction relation with $\pi_k \xrightarrow{a} p$ that describes the occurred interaction (as we have already remarked, we take the point of view that an interaction is completed when messages are received). This decoration will allow us to relate the behavior of an implemented session with the traces of a global type (see Definition 2.2). We adopt some conventional notation: we write $\implies$ for the reflexive, transitive closure of $\to$; we write $\stackrel{\alpha}{\implies}$ for the composition $\implies \alpha \implies$ and $\stackrel{\alpha_1 \cdots \alpha_n}{\implies}$ for the composition $\stackrel{\alpha_1}{\implies} \cdots \stackrel{\alpha_n}{\implies}$.

We can now formally characterize the “correct sessions” as those in which, no matter how they reduce, it is always possible to reach a state where all of the participants are successfully terminated and the buffer has been emptied.

**Definition 3.3 (live session).** We say that $\Delta$ is a live session if $\varepsilon^{\diamond}_{\diamond} \Delta \stackrel{\varphi}{\implies} \mathbb{B}^{\diamond}_{\diamond} \Delta'$ implies $\mathbb{B}^{\diamond}_{\diamond} \Delta' \stackrel{\psi}{\implies} \varepsilon^{\diamond}_{\diamond} \{\mathbf{p}_i : \text{end}\}_{i \in I}$ for some $\psi$.

We adopt the term “live session” to emphasize the fact that Definition 3.3 states a *liveness property*: every finite computation $\varepsilon, \Delta \stackrel{\varphi}{\implies} \mathbb{B}^{\diamond}_{\diamond} \Delta'$ can always be extended to a successful computation $\varepsilon^{\diamond}_{\diamond} \Delta \stackrel{\varphi}{\implies} \mathbb{B}^{\diamond}_{\diamond} \Delta' \stackrel{\psi}{\implies} \varepsilon^{\diamond}_{\diamond} \{\mathbf{p}_i : \text{end}\}_{i \in I}$. This is stronger than the progress property enforced by other multiparty session type theories, where it is only required that a session must never get stuck (but it is possible that some participants starve for messages that are never sent). As an example, the session

$$\Delta_1 = \{ \mathbf{p} : \text{rec } X.(q!a.X \oplus q!b.end), q : \text{rec } Y.(p?a.Y + p?b.end) \}$$

is alive because, no matter how many a messages p sends, q can receive all of them and, if p chooses to send a b message, the interaction terminates successfully for both p and q. This example also shows that, despite the fact that session types describe finite-state
processes, the session $\Delta_1$ is not finite-state, in the sense that the set of configurations $\{(\mathbb{B}; \Delta') | \exists \varphi, \mathbb{B}, \Delta' : \varepsilon; \Delta_1 \stackrel{\varphi}{\Rightarrow} \mathbb{B}; \Delta'\}$ is infinite. This happens because there is no bound on the size of the buffer and an arbitrary number of $a$ messages sent by $p$ can accumulate in $\mathbb{B}$ before $q$ receives them. As a consequence, the fact that a session is alive cannot be established in general by means of a brute force algorithm that checks every reachable configuration. By contrast, the session

$$ \Delta_2 = \{p : \text{rec } X.q!a.X, q : \text{rec } Y.p?a.Y\} $$

which is normally regarded correct in other session type theories, is not alive because there is no way for $p$ and $q$ to reach a successfully terminated state. The point is that hitherto correctness of session was associated to progress (*ie*, the system is never stuck). This is a weak notion of correctness since, for instance the session $\Delta_2 \uplus \{r : p?c.end\}$ satisfies progress even though role $r$ starves waiting for its input. While in this example starvation is clear since no $c$ message is ever sent, determining starvation is in general more difficult, as for

$$ \Delta_3 = \{p : \text{rec } X.q!a.q!b.X, q : \text{rec } Y.(p?a.p?b.Y + p?b.r!c.end), r : q?c.end\} $$

which satisfies progress, where every input corresponds to a compatible output, and viceversa, but which is not alive.

We can now define the traces of a session as the set of sequences of interactions that can occur in every possible reduction. It is convenient to define the traces of an incorrect (*ie*, non-live) session as the empty set (observe that $\text{tr}(\mathcal{G}) \neq \emptyset$ for every $\mathcal{G}$).

**Definition 3.4 (session traces).**

$$ \text{tr}(\Delta) \stackrel{\text{def}}{=} \begin{cases} \{\varphi \mid \varepsilon; \Delta \stackrel{\varphi}{\Rightarrow} \varepsilon; \{p_i : \text{end}\}_{i \in I}\} & \text{if } \Delta \text{ is a live session} \\ \emptyset & \text{otherwise} \end{cases} $$

It is easy to verify that $\text{tr}(\Delta_1) = \text{tr}((p \xrightarrow{a} q)^*; p \xrightarrow{b} q)$ while $\text{tr}(\Delta_2) = \text{tr}(\Delta_3) = \emptyset$ since neither $\Delta_2$ nor $\Delta_3$ is a live session.

# 4 Semantic projection

In this section we show how to project a global type to the session types of its participants —*ie*, to a session— in such a way that the projection is correct with respect to the global type. Before we move on, we must be more precise about what we mean by correctness of a session $\Delta$ with respect to a global type $\mathcal{G}$. In our setting, correctness refers to some relationship between the traces of $\Delta$ and those of $\mathcal{G}$. In general, however, we cannot require that $\mathcal{G}$ and $\Delta$ have exactly the same traces: when projecting $\mathcal{G}_1 \wedge \mathcal{G}_2$ we might need to impose a particular order in which the interactions specified by $\mathcal{G}_1$ and $\mathcal{G}_2$ must occur (shuffling condition). At the same time, asking only $\text{tr}(\Delta) \subseteq \text{tr}(\mathcal{G})$ would lead us to immediately loose the exhaustivity property, since for instance $\{p : q!a.end, q : p?a.end\}$ would implement $p \xrightarrow{a} q \lor p \xrightarrow{b} q$ even though
<table><caption>**Table 3.** Rules for semantic projection.</caption><tr><td>(SP-ACTION)</td><td>(SP-SKIP)<br>Δ ⊢ skip ▷ Δ</td></tr><tr><td>{<b>p</b><sub>i</sub>: <b>T</b><sub>i</sub>}<sub>i∈I</sub> ⊎ {<b>p</b>: <b>T</b>} ⊎ Δ ⊢ {<b>p</b><sub>i</sub>}<sub>i∈I</sub></td><td><sup>a</sup> ⇒ <b>p</b> ▷ {<b>p</b><sub>i</sub>: <b>p</b>!a.T<sub>i</sub>}<sub>i∈I</sub> ⊎ {<b>p</b>: {<b>p</b><sub>i</sub>}<sub>i∈I</sub>?a.T} ⊎ Δ</td></tr><tr><td>(SP-SEQUENCE)</td><td>(SP-ALTERNATIVE)</td></tr><tr><td>Δ ⊢ <b>G</b><sub>2</sub> ▷ Δ'<br>Δ' ⊢ <b>G</b><sub>1</sub> ▷ Δ''</td><td>Δ ⊢ <b>G</b><sub>1</sub> ▷ {<b>p</b>: <b>T</b><sub>1</sub>} ⊎ Δ'<br>Δ ⊢ <b>G</b><sub>2</sub> ▷ {<b>p</b>: <b>T</b><sub>2</sub>} ⊎ Δ'</td></tr><tr><td>Δ ⊢ <b>G</b><sub>1</sub>; <b>G</b><sub>2</sub> ▷ Δ''</td><td>Δ ⊢ <b>G</b><sub>1</sub> ∨ <b>G</b><sub>2</sub> ▷ {<b>p</b>: <b>T</b><sub>1</sub> ⊕ <b>T</b><sub>2</sub>} ⊎ Δ'</td></tr><tr><td>(SP-ITERATION)</td><td>(SP-SUBSUMPTION)</td></tr><tr><td>{<b>p</b>: <b>T</b><sub>1</sub> ⊕ <b>T</b><sub>2</sub>} ⊎ Δ ⊢ <b>G</b> ▷ {<b>p</b>: <b>T</b><sub>1</sub>} ⊎ Δ<br>{<b>p</b>: <b>T</b><sub>2</sub>} ⊎ Δ ⊢ <b>G</b><sup>*</sup> ▷ {<b>p</b>: <b>T</b><sub>1</sub> ⊕ <b>T</b><sub>2</sub>} ⊎ Δ</td><td>Δ ⊢ <b>G</b>' ▷ Δ'<br><b>G</b>' ≤ <b>G</b><br>Δ'' ≤ Δ'<br>Δ ⊢ <b>G</b> ▷ Δ''</td></tr></table>

the implementation systematically exhibits only one ($p \stackrel{a}{\to} q$) of the specified alternative behaviors. In the end, we say that $\Delta$ is a correct implementation of $\mathcal{G}$ if: first, every trace of $\Delta$ is a trace of $\mathcal{G}$ (soundness); second, every trace of $\mathcal{G}$ is the permutation of a trace of $\Delta$ (completeness). Formally:

$$ \mathrm{tr}(\Delta) \subseteq \mathrm{tr}(\mathcal{G}) \subseteq \mathrm{tr}(\Delta)^{\circ} $$

where $L^{\circ}$ is the closure of $L$ under arbitrary permutations of the strings in $L$:

$$ L^{\circ} \stackrel{\mathrm{def}}{=} \{ \alpha_1 \cdots \alpha_n \mid \text{there exists a permutation } \sigma \text{ such that } \alpha_{\sigma(1)} \cdots \alpha_{\sigma(n)} \in L \} $$

Since these relations between languages (of traces) play a crucial role, it is convenient to define a suitable pre-order relation:

**Definition 4.1 (implementation pre-order).** We let $L_1 \le L_2$ if $L_1 \subseteq L_2 \subseteq L_1^{\circ}$ and extend it to global types and sessions in the natural way, by considering the corresponding sets of traces. Therefore, we write $\Delta \preceq \mathcal{G}$ if $\mathrm{tr}(\Delta) \preceq \mathrm{tr}(\mathcal{G})$.

It is easy to see that soundness and completeness respectively formalize the notions of fitness and exhaustivity that we have outlined in the introduction. For what concerns the remaining three properties listed in the introduction (ie, sequentiality, alternativeness, and shuffling), they are entailed by the formalization of the semantics of a global type in terms of its traces (Definition 2.2). In particular, we have that soundness implies sequentiality and alternativeness, while completeness implies shuffling. Therefore, in the formal treatment that follows we will focus on soundness and completeness as to the only characterizing properties connecting sessions and global types. The relation $\Delta \preceq \mathcal{G}$ summarizes the fact that $\Delta$ is both sound and complete with respect to $\mathcal{G}$, namely that $\Delta$ is a correct implementation of the specification $\mathcal{G}$.

Table 3 presents our rules to build the projections of global types. Projecting a global type basically means compiling it to an “equivalent” set of session types. Since the source language (global types) is equipped with sequential composition while the target language (session types) is not, it is convenient to parameterize projection on a
continuation, ie, we consider judgments of the shape:

$$ \Delta \vdash \mathcal{G} \triangleright \Delta' $$

meaning that if $\Delta$ is the projection of some $\mathcal{G}'$, then $\Delta'$ is the projection of $\mathcal{G};\mathcal{G}'$. This immediately gives us the rule (SP-SEQUENCE). We say that $\Delta'$ is a projection of $\mathcal{G}$ with continuation $\Delta$.

The projection of an interaction $\pi \xrightarrow{a} p$ adds $p!a$ in front of the session type of all the roles in $\pi$, and $\pi?a$ in front of the session type of $p$ (rule (SP-ACTION)). For example we have:

$$ \{p : \text{end}, q : \text{end}\} \vdash p \xrightarrow{a} q \triangleright \{p : q!a.\text{end}, q : p?a.\text{end}\} $$

An alternative $\mathcal{G}_1 \vee \mathcal{G}_2$ (rule (SP-ALTERNATIVE)) can be projected only if there is a participant $p$ that actively chooses among different behaviors by sending different messages, while all the other participants must exhibit the same behavior in both branches. The subsumption rule (SP-SUBSUMPTION) can be used to fulfil this requirement in many cases. For example we have $\Delta_0 \vdash p \xrightarrow{a} q \triangleright \{p : q!a.\text{end}, q : p?a.\text{end}\}$ and $\Delta_0 \vdash p \xrightarrow{b} q \triangleright \{p : q!b.\text{end}, q : p?b.\text{end}\}$, where $\Delta_0 = \{p : \text{end}, q : \text{end}\}$. In order to project $p \xrightarrow{a} q \vee p \xrightarrow{b} q$ with continuation $\Delta_0$ we derive first by subsumption $\Delta_0 \vdash p \xrightarrow{a} q \triangleright \{p : q!a.\text{end}, q : T\}$ and $\Delta_0 \vdash p \xrightarrow{b} q \triangleright \{p : q!b.\text{end}, q : T\}$ where $T = p?a.\text{end} + p?b.\text{end}$. Then we obtain

$$ \Delta_0 \vdash p \xrightarrow{a} q \vee p \xrightarrow{b} q \triangleright \{p : q!a.\text{end} \oplus q!b.\text{end}, q : T\} $$

Notice that rule (SP-ALTERNATIVE) imposes that in alternative branches there must be one *and only one* participant that takes the decision. For instance, the global type

$$ \{p, q\} \xrightarrow{a} r \lor \{p, q\} \xrightarrow{b} r $$

cannot be projected since we would need a covert channel for $p$ to agree with $q$ about whether to send to $r$ the message $a$ or $b$.

To project a *starred* global type we also require that one participant $p$ chooses between repeating the loop or exiting by sending messages, while the session types of all other participants are unchanged. If $T_1$ and $T_2$ are the session types describing the behavior of $p$ when it has respectively decided to perform one more iteration or to terminate the iteration, then $T_1 \oplus T_2$ describes the behavior of $p$ before it takes the decision. The projection rule requires that one execution of $\mathcal{G}$ followed by the choice between $T_1$ and $T_2$ projects in a session with type $T_1$ for $p$. This is possible only if $T_1$ is a recursive type, as expected, and it is the premise of rule (SP-ITERATION). For example if $T_1 = q!a.\text{rec } X.(q!a.X \oplus q!b.\text{end})$, $T_2 = q!b.\text{end}$, and $S = \text{rec } Y.(p?a.Y + p?b.\text{end})$ we can derive $\{p : T_1 \oplus T_2, q : S\} \vdash p \xrightarrow{a} q \triangleright \{p : T_1, q : S\}$ and then

$$ \{p : T_2, q : S\} \vdash (p \xrightarrow{a} q)^* \triangleright \{p : T_1 \oplus T_2, q : S\} $$

Notably there is no rule for “&”, the *both* constructor. We deal with this constructor by observing that all interleavings of the actions in $\mathcal{G}_1$ and $\mathcal{G}_2$ give global types $\mathcal{G}$ such
that $\mathcal{G} \leq \mathcal{G}_1 \wedge \mathcal{G}_2$, and therefore we can use the subsumption rule to eliminate every occurrence of $\wedge$. For example, to project the global type $p \underset{a}{\to} q \wedge r \underset{b}{\to} s$ we can use $p \underset{a}{\to} q; r \underset{b}{\to} s$: since the two actions that compose both global types have disjoint participants, then the projections of these global types (as well as that of $r \underset{b}{\to} s; p \underset{a}{\to} q$) will have exactly the same set of traces.

Other interesting examples of subsumptions useful for projecting are

$$r \underset{b}{\to} p; p \underset{a}{\to} q \le (p \underset{a}{\to} q; r \underset{b}{\to} p) \lor (r \underset{b}{\to} p; p \underset{a}{\to} q) \quad (4)$$

$$r \underset{b}{\to} p; (p \underset{a}{\to} q \lor p \underset{b}{\to} q) \le (r \underset{b}{\to} p; p \underset{a}{\to} q) \lor (r \underset{b}{\to} p; p \underset{b}{\to} q) \quad (5)$$

In (4) the $\leq$-larger global type describes the shuffling of two interactions, therefore we can project one particular ordering still preserving completeness. In (5) we take advantage of the flat nature of traces to push the $\lor$ construct where the choice is actually being made.

We are interested in projections without continuations, that is, in judgments of the shape $\{p_i : \text{end} \mid p_i \in \mathcal{G}\} \vdash \mathcal{G} \triangleright \Delta$ (where $p \in \mathcal{G}$ means that $p$ occurs in $\mathcal{G}$) which we shortly will write as

$$\vdash \mathcal{G} \triangleright \Delta$$

The mere existence of a projection does not mean that the projection behaves as specified in the global type. For example, we have

$$\vdash p \underset{a}{\to} q; r \underset{a}{\to} s \triangleright \{p : q!a.end, q : p?a.end, r : s!a.end, s : r?a.end\}$$

but the projection admits also the trace $r \underset{a}{\to} s; p \underset{a}{\to} q$ which is not allowed by the global type. Clearly the problem resides in the global type, which tries to impose a temporal ordering between interactions involving disjoint participants. What we want, in accordance with the traces of a global type $\mathcal{G}_1; \mathcal{G}_2$, is that no interaction in $\mathcal{G}_2$ can be completed before all the interactions in $\mathcal{G}_1$ are completed. More in details:

- an action $\pi \underset{a}{\to} p$ is completed when the participant $p$ has received the message $a$ from all the participants in $\pi$;

- if $\varphi; \pi \underset{a}{\to} p; \pi' \underset{b}{\to} p'$; $\psi$ is a trace of a global type, then either the action $\pi' \underset{b}{\to} p'$ cannot be completed before the action $\pi \underset{a}{\to} p$ is completed, or they can be executed in any order. The first case requires $p$ to be either $p'$ or a member of $\pi'$, in the second case the set of traces must also contain the trace $\varphi; \pi' \underset{b}{\to} p'; \pi \underset{a}{\to} p; \psi$.

This leads us to the following definition of well-formed global type.

**Definition 4.2 (well-formed global type).** We say that a set of traces $L$ is well formed if $\varphi; \pi \underset{a}{\to} p; \pi' \underset{b}{\to} p'; \psi \in L$ implies either $p \in \pi' \cup \{p'\}$ or $\varphi; \pi' \underset{b}{\to} p'; \pi \underset{a}{\to} p; \psi \in L$. We say that a global type $\mathcal{G}$ is well formed if so is $\text{tr}(\mathcal{G})$.

It is easy to decide well-formedness of an arbitrary global type $\mathcal{G}$ by building in a standard way the automaton that recognises the language of traces generated by $\mathcal{G}$.
Projectability and well-formedness must be kept separate because it is sometimes necessary to project ill-formed global types. For example, the ill-formed global type $p \stackrel{a}{\rightarrow} q; r \stackrel{a}{\rightarrow} s$ above is useful to project $p \stackrel{a}{\rightarrow} q \wedge r \stackrel{a}{\rightarrow} s$ which is well formed.

Clearly, if a global type is projectable (ie, $\vdash \mathcal{G} \triangleright \Delta$ is derivable) then well-formedness of $\mathcal{G}$ is a necessary condition for the soundness and completeness of its projection (ie, for $\Delta \leqslant \mathcal{G}$). It turns out that well-formedness is also a sufficient condition for having soundness and completeness of projections, as stated in the following theorem.

**Theorem 4.1.** If $\mathcal{G}$ is well formed and $\vdash \mathcal{G} \triangleright \Delta$, then $\Delta \leqslant \mathcal{G}$.

In summary, if a well-formed global type $\mathcal{G}$ is projectable, then its projection is a *live* projection (it cannot be empty since $\mathrm{tr}(\mathcal{G}) \subseteq \mathrm{tr}(\Delta)^{\circ}$) which is sound and complete wrt $\mathcal{G}$ and, therefore, satisfies the sequentiality, alternativeness, and shuffling properties outlined in the introduction.

We conclude this section by formally characterizing the three kinds of problematic global types we have described earlier. We start from the least severe problem and move towards the more serious ones. Let $L^\#$ denote the smallest well-formed set such that $L \subseteq L^\#$.

*No sequentiality.* Assuming that there is no $\Delta$ that is both sound and complete for $\mathcal{G}$, it might be the case that we can find a session whose traces are complete for $\mathcal{G}$ and sound for the global type $\mathcal{G}'$ obtained from $\mathcal{G}$ by turning some «;»'s into «$\wedge$»'s. This means that the original global type $\mathcal{G}$ is ill formed, namely that it specifies some sequentiality constraints that are impossible to implement. For instance, $\{p:q!a.end, q:p?a.end, r:s!b.end, s:r?b.end\}$ is a complete but not sound session for the ill-formed global type $p \stackrel{a}{\rightarrow} q; r \stackrel{b}{\rightarrow} s$ (while it is a sound and complete session for $p \stackrel{a}{\rightarrow} q \wedge r \stackrel{b}{\rightarrow} s$). We characterize the global types $\mathcal{G}$ that present this error as:

$$ \exists \Delta : \Delta \leqslant \mathcal{G} \text{ and } \exists \Delta : \mathrm{tr}(\mathcal{G}) \subseteq \mathrm{tr}(\Delta) \subseteq \mathrm{tr}(\mathcal{G})^\# $$

*No knowledge for choice.* In this case every session $\Delta$ that is complete for $\mathcal{G}$ invariably exhibits some interactions that are not allowed by $\mathcal{G}$ despite the fact that $\mathcal{G}$ is well formed. This happens when the global type specifies alternative behaviors, but some participants do not have enough information to behave consistently. For example, the global type

$$ (p \stackrel{a}{\rightarrow} q; q \stackrel{a}{\rightarrow} r; r \stackrel{a}{\rightarrow} p) \lor (p \stackrel{b}{\rightarrow} q; q \stackrel{a}{\rightarrow} r; r \stackrel{b}{\rightarrow} p) $$

mandates that $r$ should send either $a$ or $b$ in accordance with the message that $p$ sends to $q$. Unfortunately, $r$ has no information as to which message $q$ has received, because $q$ notifies $r$ with an $a$ message in both branches. A complete implementation of this global type is

$$ \{p:q!a.(r?a.end+r?b.end) \oplus q!b.(r?a.end+r?b.end), q:p?a.r!a.end+p?b.r!a.end, r:q?a.(q!a.end \oplus q!b.end)\} $$

which also produces the traces $p \stackrel{a}{\rightarrow} q; q \stackrel{a}{\rightarrow} r; r \stackrel{b}{\rightarrow} p$ and $p \stackrel{b}{\rightarrow} q; q \stackrel{a}{\rightarrow} r; r \stackrel{a}{\rightarrow} p$. We characterize this error as:

$$ \exists \Delta : \mathrm{tr}(\mathcal{G}) \subseteq \mathrm{tr}(\Delta) \subseteq \mathrm{tr}(\mathcal{G})^\# \text{ and } \exists \Delta : \mathrm{tr}(\mathcal{G}) \subseteq \mathrm{tr}(\Delta). $$
No knowledge, no choice. In this case we cannot find a complete session $\Delta$ for $\mathcal{G}$. This typically means that $\mathcal{G}$ specifies some combination of incompatible behaviors. For example, the global type $p \stackrel{a}{\to} q \lor q \stackrel{a}{\to} p$ implies an agreement between p and q for establishing who is entitled to send the a message. In a distributed environment, however, there can be no agreement without a previous message exchange. Therefore, we can either have a sound but not complete session that implements just one of the two branches (for example, $\{p : q!a.end, q : p? a.end\}$) or a session like $\{p : q!a.q? a.end, q : p? a.p!a.end\}$ where both p and q send their message but which is neither sound nor complete. We characterize this error as:

$$ \nV \Delta : \mathrm{tr}(\mathcal{G}) \subseteq \mathrm{tr}(\Delta). $$

# 5 Algorithmic projection

We now attack the problem of computing the projection of a global type. We are looking for an algorithm that “encompasses” the projection rules of Section 4, that is, that given a session continuation $\Delta$ and a global type $\mathcal{G}$, produces a projection $\Delta'$ such that $\Delta \vdash \mathcal{G} : \Delta'$. In other terms this algorithm must be sound with respect to the semantic projection (completeness, that is, returning a projection for every global type that is semantically projectable, seems out of reach, yet).

The deduction system in Table 3 is not algorithmic because of two rules: the rule (SP-ITERATION) that does not satisfy the subformula property since the context $\Delta$ used in the premises is the result of the conclusion; the rule (SP-SUBSUMPTION) since it is neither syntax-directed (it is defined for a generic $\mathcal{G}$) nor does it satisfy the subformula property (the $\mathcal{G}'$ and $\Delta''$ in the premises are not uniquely determined).<fnref n="3" /> The latter rule can be expressed as the composition of the two rules

$$ \frac{\begin{array}{ccc} \text{(SP-SUBSUMPTION)} & & \\ \Delta \vdash \mathcal{G}' \triangleright \Delta' & \mathcal{G}' \leq \mathcal{G} & \\ & & \\ \Delta \vdash \mathcal{G} \triangleright \Delta' & & \end{array}}{\Delta \vdash \mathcal{G} \triangleright \Delta'} $$

$$ \frac{\begin{array}{ccc} \text{(SP-SUBSUMPTIONS)} & & \\ \Delta \vdash \mathcal{G} \triangleright \Delta' & \Delta'' \leq \Delta' & \\ & & \\ \Delta \vdash \mathcal{G} \triangleright \Delta'' & & \end{array}}{\Delta \vdash \mathcal{G} \triangleright \Delta''} $$

Splitting (SP-SUBSUMPTION) into (SP-SUBSUMPTIONG) and (SP-SUBSUMPTIONS) is useful to explain the following problems we have to tackle to define an algorithm:

1. How to eliminate (SP-SUBSUMPTIONS), the subsumption rule for sessions.

2. How to define an algorithmic version of (SP-ITERATION), the rule for Kleene star.

3. How to eliminate (SP-SUBSUMPTIONG), the subsumption rule for global types.

We address each problem in order and discuss the related rule in the next sections.

## 5.1 Session subsumption

Rule (SP-SUBSUMPTIONS) is needed to project alternative branches and iterations (a loop is an unbound repetition of alternatives, each one starting with the choice of

<footnote n="3">³ The rule (SP-ALTERNATIVE) is algorithmic: in fact there is a finite number of participants in the two sessions of the premises and at most one of them can have different session types starting with outputs.</footnote>
whether to enter the loop or to skip it): each participant different from the one that actively chooses must behave according to the same session type in both branches. More precisely, to project $\mathcal{G}_1 \lor \mathcal{G}_2$ the rule (SP-ALTERNATIVE) requires to deduce for $\mathcal{G}_1$ and $\mathcal{G}_2$ the same projection: if different projections are deduced, then they must be previously subsumed to a common lower bound. The algorithmic projection of an alternative (see the corresponding rule in Table 4) allows premises with two different sessions, but then *merges* them. Of course not every pair of projections is mergeable. Intuitively, two projections are mergeable if so are the behaviors of each participant. This requires participants to respect a precise behavior: as long as a participant cannot determine in which branch (ie, projection) it is, then it must do the same actions in all branches (ie, projections). For example, to project $\mathcal{G} = (p \underset{a}{\stackrel{c}{\rightleftharpoons}} q; r \underset{b}{\stackrel{a}{\rightleftharpoons}} q; \dots) \lor (p \underset{b}{\stackrel{c}{\rightleftharpoons}} q; r \underset{a}{\stackrel{c}{\rightleftharpoons}} q; \dots)$ we project each branch separately obtaining $\Delta_1 = \{p : q!a...; q : p?ar?c...; r : q!c...\}$ and $\Delta_2 = \{p : q!b...; q : p?br?c...; r : q!c...\}$. Since p performs the choice, in the projection of $\mathcal{G}$ we obtain $p : q!a... \oplus q!b...$ and we must merge $\{q : p?ar?c...; r : q!c...\}$ with $\{q : p?br?c...; r : q!c...\}$. Regarding q, observe that it is the receiver of the message from p, therefore it becomes aware of the choice and can behave differently right after the first input operation. Merging its behaviors yields $q : p?ar?c... + p?br?c...$. Regarding r, it has no information as to which choice has been made by p, therefore it must have the same behavior in both branches, as is the case. Since merging is idempotent, we obtain $r : q!c...$. In summary, *mergeability* of two branches of an “$\lor$” corresponds to the “awareness” of the choice made when branching (see the discussion in Section 4 about the “No knowledge for choice” error), and it is possible when, roughly, each participant performs the same internal choices and disjoint external choices in the two sessions.

Special care must be taken when merging external choices to avoid unexpected interactions that may invalidate the correctness of the projection. To illustrate the problem consider the session types $T = p?a.q?b.end$ and $S = q?b.end$ describing the behavior of a participant $r$. If we let $r$ behave according to the merge of $T$ and $S$, which intuitively is the external choice $p?a.q?b.end + q?b.end$, it may be possible that the message $b$ from $q$ is read *before* the message $a$ from $p$ arrives. Therefore, $r$ may mistakenly think that it should no longer participate to the session, while there is still a message targeted to $r$ that will never be read. Therefore, $T$ and $S$ are *incompatible* and it is not possible to merge them safely. On the contrary, $p?a.p?b.end$ and $p?b.end$ are compatible and can be merged to $p?a.p?b.end + p?b.end$. In this case, since the order of messages coming from the same sender is preserved, it is not possible for $r$ to read the $b$ message coming from $p$ before the $a$ message, assuming that $p$ sent both. More formally:

**Definition 5.1 (compatibility).** We say that an input $p?a$ is compatible with a session type $T$ if either (i) $p?a$ does not occur in $T$, or (ii) $T = \bigoplus_{i \in I} p_i!a_i.T_i$ and $p?a$ is compatible with $T_i$ for all $i \in I$, or (iii) $T = \sum_{i \in I} \pi_i?a_i.T_i$ and for all $i \in I$ either $p \in \pi_i$ and $a \neq a_i$ or $p \notin \pi_i$ and $p?a$ is compatible with $T_i$.

We say that an input $\pi?a$ is compatible with a session type $T$ if $p?a$ is compatible with $T$ for some $p \in \pi$.

Finally, $T = \sum_{i \in I} \pi_i?a_i.T_i + \sum_{j \in J} \pi_j?a_j.T_j$ and $S = \sum_{i \in I} \pi_i?a_i.S_i + \sum_{h \in H} \pi_h?a_h.S_h$ are compatible if $\pi_j?a_j$ is compatible with $S$ for all $j \in J$ and $\pi_h?a_h$ is compatible with $T$ for all $h \in H$.
<table><caption>**Table 4.** Rules for algorithmic projection.</caption><tr><td>(AP-Skip)</td></tr><tr><td>Δ ⊢<sub>a</sub> skip ▷ Δ</td></tr><tr><td>(AP-ACTION)</td></tr><tr><td>{p<sub>i</sub> : T<sub>i</sub>}<sub>i∈I</sub> ⊎ {p : T} ⊎ Δ ⊢<sub>a</sub> {p<sub>i</sub>}<sub>i∈I</sub> →<sup>a</sup> p ▷ {p<sub>i</sub> : p!a.T<sub>i</sub>}<sub>i∈I</sub> ⊎ {p : {p<sub>i</sub>}<sub>i∈I</sub>?a.T} ⊎ Δ</td></tr><tr><td>(AP-Sequence)</td></tr><tr><td>Δ ⊢<sub>a</sub> G<sub>2</sub> ▷ Δ'<br>Δ' ⊢<sub>a</sub> G<sub>1</sub> ▷ Δ''<br>Δ ⊢<sub>a</sub> G<sub>1</sub>; G<sub>2</sub> ▷ Δ''</td></tr><tr><td>(AP-Alternative)</td></tr><tr><td>Δ ⊢<sub>a</sub> G<sub>1</sub> ▷ {p : T<sub>1</sub>} ⊎ Δ<sub>1</sub><br>Δ ⊢<sub>a</sub> G<sub>1</sub> ∨ G<sub>2</sub> ▷ {p : T<sub>1</sub> ⊕ T<sub>2</sub>} ⊎ (Δ<sub>1</sub> ⋀ Δ<sub>2</sub>)</td></tr><tr><td>(AP-Iteration)</td></tr><tr><td>{p : X} ⊎ {p<sub>i</sub> : X<sub>i</sub>}<sub>i∈I</sub> ⊢<sub>a</sub> G ▷ {p : S} ⊎ {p<sub>i</sub> : S<sub>i</sub>}<sub>i∈I</sub><br>{p : T} ⊎ {p<sub>i</sub> : T<sub>i</sub>}<sub>i∈I</sub> ⊎ Δ ⊢<sub>a</sub> G* ▷ {p : rec X.(T ⊕ S)} ⊎ {p<sub>i</sub> : rec X<sub>i</sub>.(T<sub>i</sub> ⋀ S<sub>i</sub>)}<sub>i∈I</sub> ⊎ Δ</td></tr></table>

The merge operator just connects sessions with the *same* output guards by internal choices and with *compatible* input guards by external choices:

**Definition 5.2 (merge).** The merge of *T* and *S*, written *T* ⋀*S*, is defined coinductively and by cases on the structure of *T* and *S* thus:

- if $T = S = \text{end}$, then $T \not\sqcap S = \text{end}$;

- if $T = \bigoplus_{i \in I} p_i! a_i.T_i$ and $S = \bigoplus_{j \in I} p_j! a_j.S_j$, then $T \not\sqcap S = \bigoplus_{i \in I} p_i! a_i.(T_i \not\sqcap S_i)$;

- if $T = \sum_{i \in I} \pi_i? a_i.T_i + \sum_{j \in J} \pi_j? a_j.T_j$ and $S = \sum_{i \in I} \pi_i? a_i.S_i + \sum_{h \in H} \pi_h? a_h.S_h$ are compatible, then $T \not\sqcap S = \sum_{i \in I} \pi_i? a_i.(T_i \not\sqcap S_i) + \sum_{j \in J} \pi_j? a_j.T_j + \sum_{h \in H} \pi_h? a_h.S_h$.

We extend merging to sessions so that $\Delta \not\sqcap \Delta' = \{p : T \not\sqcap S \mid p : T \in \Delta \& p : S \in \Delta'\}$.

Rules (AP-ALTERNATIVE) and (AP-ITERATION) of Table 4 are the algorithmic versions of (SP-ALTERNATIVE) and (SP-ITERATION), but instead of relying on substitution they use the merge operator to compute common behaviors.

The merge operation is a sound but incomplete approximation of session subsumption insofar as the merge of two sessions can be undefined even though the two sessions completed with the participant that makes the decision have a common lower bound according to $\leq$. This implies that there are global types which can be semantically but not algorithmically projected. Take for example $G_1 \lor G_2$ where $G_1 = p \xrightarrow{a} r; r \xrightarrow{a} p; p \xrightarrow{a} q$; $q \xrightarrow{b} r$ and $G_2 = p \xrightarrow{b} q; q \xrightarrow{b} r$. The behavior of $r$ in $G_1$ and $G_2$ respectively is $T = p? a.p! a.q? b.$ end and $S = q? b$. Then we see that $G_1 \lor G_2$ is semantically projectable, for instance by inferring the behavior $T+S$ for $r$. However, $T$ and $S$ are incompatible and $G_1 \lor G_2$ is not algorithmically projectable. The point is that the $\leq$ relation on projections has a comprehensive perspective of the *whole* session and “realizes” that, if $p$ initially chooses to send $a$, then $r$ will not receive a $b$ message coming from $q$ until $r$ has sent $a$ to $p$. The merge operator, on the other hand, is defined locally on pairs of session types and ignores that the $a$ message that $r$ sends to $p$ is used to enforce the arrival of the $b$ message from $q$ to $r$ only afterwards. For this reason it conservatively declares $T$ and $S$ incompatible, making $G_1 \lor G_2$ impossible to project algorithmically.
## 5.2 Projection of Kleene star

Since an iteration $\mathcal{G}^*$ is intuitively equivalent to $\text{skip} \lor \mathcal{G}; \mathcal{G}^*$ it comes as no surprise that the algorithmic rule (AP-ITERATION) uses the merge operator. The use of recursion variables for continuations is also natural: in the premise we project $\mathcal{G}$ taking recursion variables as session types in the continuation; the conclusion projects $\mathcal{G}^*$ as the choice between exiting and entering the loop. There is, however, a subtle point in this rule that may go unnoticed: although in the premises of (AP-ITERATION) the only actions and roles taken into account are those occurring in $\mathcal{G}$, in its conclusion the projection of $\mathcal{G}^*$ may require a continuation that includes actions and roles that precede $\mathcal{G}^*$. The point can be illustrated by the global type

$$ (p \xrightarrow{a} q; (p \xrightarrow{b} q)^*); p \xrightarrow{c} q $$

where $p$ initially decides whether to enter the outermost iteration (by sending $a$) or not (by sending $c$). If it enters the iteration, then it eventually decides whether to also enter the innermost iteration (by sending $b$), whether to repeat the outermost one (by sending $a$), or to exit both (by sending $c$). Therefore, when we project $(p \xrightarrow{b} q)^*$, we must do it in a context in which both $p \xrightarrow{c} q$ and $p \xrightarrow{a} q$ are possible, that is a continuation of the form $\{p: q!a... \oplus q!c.end\}$ even though no $a$ is sent by an action (syntactically) following $(p \xrightarrow{b} q)^*$. For the same reason, the projection of $(p \xrightarrow{b} q)^*$ in $(p \xrightarrow{a} q; p \xrightarrow{a} r; (p \xrightarrow{b} q)^*)^*; p \xrightarrow{c} q; q \xrightarrow{c} r$ will need a recursive session type for $r$ in the continuation.

## 5.3 Global type subsumption

Elimination of global type subsumption is the most difficult problem when defining the projection algorithm. While in the case of sessions the definition of the merge operator gives us a sound—though not complete—tool that replaces session subsumption in very specific places, we do not have such a tool for global type containment. This is unfortunate since global type subsumption is necessary to project several usage patterns (see for example the inequations (4) and (5)), but most importantly it is the only way to eliminate $\wedge$-types (neither the semantic nor the algorithmic deduction systems have projection rules for $\wedge$). The minimal facility that a projection algorithm should provide is to feed the algorithmic rules with all the variants of a global type obtained by replacing occurrences of $\mathcal{G}_1 \land \mathcal{G}_2$ by either $\mathcal{G}_1; \mathcal{G}_2$ or $\mathcal{G}_2; \mathcal{G}_1$. Unfortunately, this is not enough to cover all the occurrences in which rule (SP-SUBSUMPTIONG) is necessary. Indeed, while $\mathcal{G}_1; \mathcal{G}_2$ and $\mathcal{G}_2; \mathcal{G}_1$ are in many cases projectable (for instance, when $\mathcal{G}_1$ and $\mathcal{G}_2$ have distinct roles and are both projectable), there exist $\mathcal{G}_1$ and $\mathcal{G}_2$ such that $\mathcal{G}_1 \land \mathcal{G}_2$ is projectable only by considering a clever interleaving of the actions occurring in them. Consider for instance $\mathcal{G}_1 = (p \xrightarrow{a} q; q \xrightarrow{c} s; s \xrightarrow{e} q) \lor (p \xrightarrow{b} r; r \xrightarrow{d} s; s \xrightarrow{f} r)$ and $\mathcal{G}_2 = r \xrightarrow{g} s; s \xrightarrow{h} r; s \xrightarrow{i} q$. The projection of $\mathcal{G}_1 \land \mathcal{G}_2$ from the environment $\{q: p!a.end, r: p!b.end\}$ can be obtained only from the interleaving $r \xrightarrow{g} s; \mathcal{G}_1; s \xrightarrow{h} r; s \xrightarrow{i} q$. The reason is that $q$ and $r$ receive messages only in one of the two branches
of the $\lor$, so we need to compute the $\mathcal{A}$ of their types in these branches with their types
in the continuations. The example shows that to project $\mathcal{G}_1 \wedge \mathcal{G}_2$ it may be necessary
to arbitrarily decompose one or both of $\mathcal{G}_1$ and $\mathcal{G}_2$ to find the particular interleaving of
actions that can be projected. As long as $\mathcal{G}_1$ and $\mathcal{G}_2$ are finite (no non-trivial iteration
occurs in them), we can use a brute force approach and try to project all the elements
in their shuffle, since there are only finitely many of them. In general —*ie*, in pres-
ence of iteration— this is not an effective solution. However, we conjecture that even
in the presence of infinitely many traces one may always resort to the finite case by
considering only zero, one, and two unfoldings of starred global types. To give a rough
idea of the intuition supporting this conjecture consider the global type $\mathcal{G}^* \wedge \mathcal{G}'$: its
projectability requires the projectability of $\mathcal{G}'$ (since $\mathcal{G}$ can be iterated zero times), of
$\mathcal{G} \wedge \mathcal{G}'$ (since $\mathcal{G}$ can occur only once) and of $\mathcal{G}$; $\mathcal{G}$ (since the number of occurences of
$\mathcal{G}$ is unbounded). It is enough to require also that either $\mathcal{G}$; $(\mathcal{G} \wedge \mathcal{G}')$ or $(\mathcal{G} \wedge \mathcal{G}')$; $\mathcal{G}$
can be projected, since then the projectability of either $\mathcal{G}^n$; $(\mathcal{G} \wedge \mathcal{G}')$ or $(\mathcal{G} \wedge \mathcal{G}')$; $\mathcal{G}^n$ for an
arbitrary $n$ follows (see the appendix in the extended version).

So we can —or, conjecture we can— get rid of all occurences of $\wedge$ operators auto-
matically, without loosing in projectability. However, examples (4) and (5) in Section 4
show that rule (SP-SUBSUMPTIONG) is useful to project also global types in which the
$\wedge$-constructor does not occur. A fully automated approach may consider (4) and (5) as
right-to-left rewriting rules that, in conjunction with some other rules, form a rewriting
system generating a set of global types to be fed to the algorithm of Table 4. The choice
of such rewriting rules must rely on a more thorough study to formally characterize the
sensible classes of approximations to be used in the algorithms. An alternative approach
is to consider a global type $\mathcal{G}$ as somewhat underspecified, in that it may allow for a
large number of different implementations (exhibiting different sets of traces) that are
sound and complete. Therefore, rule (SP-SUBSUMPTIONG) may be interpreted as a
human-assisted refinement process where the designer of a system proposes one partic-
ular implementation $\mathcal{G} \le \mathcal{G}'$ of a system described by $\mathcal{G}'$. In this respect it is interesting
to observe that checking whether $L_1 \le L_2$ when $L_1$ and $L_2$ are regular is decidable, since
this is a direct consequence of the decidability of the Parikh equivalence on regular lan-
guages [18].

**5.4 Properties of the algorithmic rules**

Every deduction of the algorithmic system given in Table 4, possibly preceeded by
the elimination of $\wedge$ and other possible sources of failures by applying the rewrit-
ings/heuristics outlined in the previous subsection, induces a similar deduction using
the rules for semantic projection (Table 3).

**Theorem 5.1.** If $\vdash_a \mathcal{G} \succ \Delta$, then $\vdash \mathcal{G} \succ \Delta$.

As a corollary of Theorems 4.1 and 5.1, we immediately obtain that the projection
$\Delta$ of $\mathcal{G}$ obtained through the algorithm is sound and complete with respect to $\mathcal{G}$.
# 6 k-Exit Iterations

The syntax of global types (Table 1) includes that of regular expressions and therefore is expressive enough for describing any protocol that follows a regular pattern. Nonetheless, the simple Kleene star prevents us from projecting some useful protocols. To illustrate the point, suppose we want to describe an interaction where two participants p and q alternate in a negotiation in which each of them may decide to bail out. On p's turn, p sends either a *bailout* message or a *handover* message to q; if a *bailout* message is sent, the negotiation ends, otherwise it continues with q that behaves in a symmetric way. The global type

$$ (p \xrightarrow{\text{handover}} q; q \xrightarrow{\text{handover}} p)^*; (p \xrightarrow{\text{bailout}} q \lor p \xrightarrow{\text{handover}} q; q \xrightarrow{\text{bailout}} p) $$

describes this protocol as an arbitrarily long negotiation that may end in two possible ways, according to the participant that chooses to bail out. This global type cannot be projected because of the two occurrences of the interaction $p \xrightarrow{\text{handover}} q$, which make it ambiguous whether p actually chooses to bail out or to continue the negotiation. In general, our projection rules (SP-ITERATION) and (AP-ITERATION) make the assumption that an iteration can be exited in one way only, while in this case there are two possibilities according to which role bails out. This lack of expressiveness of the simple Kleene star used in a nondeterministic setting [17] led researchers to seek for alternative iteration constructs. One proposal is the *k-exit iteration* [2], which is a generalization of the binary Kleene star and has the form

$$ (\mathcal{G}_1, \dots, \mathcal{G}_k)^{k*} (\mathcal{G}'_1, \dots, \mathcal{G}'_k) $$

indicating a loop consisting of *k* subsequent phases $\mathcal{G}_1, \dots, \mathcal{G}_k$. The loop can be exited just before each phase through the corresponding $\mathcal{G}'_i$. Formally, the traces of the *k*-exit iteration can be expressed thus:

$$ \mathrm{tr}((\mathcal{G}_1, \dots, \mathcal{G}_k)^{k*} (\mathcal{G}'_1, \dots, \mathcal{G}'_k)) \stackrel{\mathrm{def}}{=} \mathrm{tr}((\mathcal{G}_1; \dots; \mathcal{G}_k)^*; (\mathcal{G}'_1 \lor \mathcal{G}_1; \mathcal{G}'_2 \lor \dots \lor \mathcal{G}_2; \dots; \mathcal{G}_{k-1}; \mathcal{G}'_k)) $$

and, for example, the negotiation above can be represented as the global type

$$ (p \xrightarrow{\text{handover}} q, q \xrightarrow{\text{handover}} p)^{2*} (p \xrightarrow{\text{bailout}} q, q \xrightarrow{\text{bailout}} p) \qquad (6) $$

while the unary Kleene star $\mathcal{G}^*$ can be encoded as $(\mathcal{G})^{1*}$ (skip).

In our setting, the advantage of the *k*-exit iteration over the Kleene star is that it syntactically identifies the *k* points in which a decision is made by a participant of a multi-party session and, in this way, it enables more sophisticated projection rules such as that in Table 5. Albeit intimidating, rule (SP-*k*-EXIT ITERATION) is just a generalization of rule (SP-ITERATION). For each phase *i* a (distinct) participant $p_i$ is identified: the participant may decide to exit the loop behaving as $S_i$ or to continue the iteration behaving as $T_i$. While projecting each phase $\mathcal{G}_i$, the participant $p_{(i \bmod k)+1}$ that will decide at the next turn is given the continuation $T_{(i \bmod k)+1} \oplus S_{(i \bmod k)+1}$, while the others must behave according to some $R_i$ that is the same for every phase in which
<caption>**Table 5.** Semantic projection of *k*-exit iteration.</caption>

(SP-*k*-EXIT ITERATION)
$$
\begin{array}{l}
\Delta \vdash \mathcal{G}'_i \triangleright \{\mathbf{p}_i : S_i\} \uplus \{\mathbf{p}_j : R_j\}_{j=1,...,i-1,i+1,...,k} \uplus \Delta'_i \quad (i \in \{1,...,k\}) \\
\{\mathbf{p}_2 : T_2 \oplus S_2\} \uplus \{\mathbf{p}_i : R_i\}_{i=1,3,...,k} \uplus \Delta'_i \vdash \mathcal{G}'_1 \triangleright \{\mathbf{p}_1 : T_1\} \uplus \{\mathbf{p}_i : R_i\}_{i=2,...,k} \uplus \Delta'_1 \\
\{\mathbf{p}_3 : T_3 \oplus S_3\} \uplus \{\mathbf{p}_i : R_i\}_{i=1,2,4,...,k} \uplus \Delta'_i \vdash \mathcal{G}'_2 \triangleright \{\mathbf{p}_2 : T_2\} \uplus \{\mathbf{p}_i : R_i\}_{i=1,3,...,k} \uplus \Delta'_1 \\
\vdots \\
\{\mathbf{p}_1 : T_1 \oplus S_1\} \uplus \{\mathbf{p}_i : R_i\}_{i=2,...,k} \uplus \Delta'_i \vdash \mathcal{G}'_k \triangleright \{\mathbf{p}_k : T_k\} \uplus \{\mathbf{p}_i : R_i\}_{i=1,...,k-1} \uplus \Delta'_k \\
\Delta \vdash (\mathcal{G}'_1,...,\mathcal{G}'_k)^{k*} (\mathcal{G}'_1,...,\mathcal{G}'_k) \triangleright \{\mathbf{p}_1 : T_1 \oplus S_1\} \uplus \{\mathbf{p}_i : R_i\}_{i=2,...,k} \uplus \Delta'_k
\end{array}
$$

they play no active role. Once again, rule (SP-SUBSUMPTION) is required in order to
synthesize these behaviors. For example, the global type (6) is projected to

$$
\{ \mathbf{p} : \text{rec } X. (\mathbf{q} ! \text{handover.} (\mathbf{q} ! \text{handover.} X + \mathbf{q} ! \text{bailout.} \text{end}) \oplus \mathbf{q} ! \text{bailout.} \text{end}) , \\
\mathbf{q} : \text{rec } Y. (\mathbf{p} ! \text{handover.} (\mathbf{p} ! \text{handover.} Y \oplus \mathbf{p} ! \text{bailout.} \text{end}) + \mathbf{p} ! \text{bailout.} \text{end}) \}
$$

as one expects.

7 Related work

The formalization and analysis of the relation between a global description of a dis-
tributed system and a more machine-oriented description of a set of components that
implments it, is a problem that has been studied in several contexts and by different
communities. In this context, important properties that are consider are the verification
that an implementation satisfies the specification, the implementability of the specifica-
tion by automatically producing an implementation from it, and the study of different
properties on the specification that can then be transposed to every (possibly automat-
ically produced) implementation satisfying it. In this work we concentrated on the im-
plementability problem, and we tackled it from the “Web service coordination” angle
developed by the community that focuses on behavioral types and process algebra.
We are just the latest to attack this problem. So many other communities have been
considering it before us that even a sketchy survey has no chance to be exhaustive.

In what follows we compare the “behavioral types/process algebra” approach we
adopted, with two alternative approaches studied by important communities with a large
amount of different and important contributions, namely the “automata” and “crypto-
graphic protocols” approaches. In the full version of this article the reader will find a
deeper survey of these two approaches along with a more complete comparison. In a
nutshell, the “automata/model checking” community has probably done the most exten-
sive research on the problem. The paradigmatic global descriptions language they usu-
ally refer to are *Message Sequence Charts* (MSC, ITU Z.120 standard) enriched with
branching and iteration (which are then called *Message Sequence Graphs* or, as in the
Z.120 standard, *High-Level Message Sequence Charts*) and they are usually projected
into *Communicating Finite State Machines* (CFM) which form the theoretical core of
the *Specification and Description Language* (SDL ITU Z.100 standard). This commu-
nity has investigated the expressive power of the two formalisms and their properties,
<figure><img src="image_2.png" /><figcaption>**Fig. 1.** Global types and multiparty sessions in a nutshell.</figcaption></figure>

studied different notions of implementability (but not the notion we studied here which, as far as we know, is original to our work), and several variants of these formalisms especially to deal with the decidability or tractability of the verification of properties, in particular model-checking. The community that works on the formal verification of cryptographic protocols uses MSC as global descriptions, as well, though they are of different nature from the previous ones. In particular, for cryptographic protocols much less emphasis is put on control (branching and iteration have a secondary role) and expressivity, while much more effort is devoted to the description of the messages (these include cryptographic primitives, at least), of properties of the participants, and of local treatment of the messages. The global descriptions are then projected into local descriptions that are more detailed than in the automata approach since they precisely track single values and the manipulations thereof. The verification of properties is finer grained and covers execution scenarios that fall outside the global description since the roles described in the global type can be concurrently played by different participants, messages can be intercepted, read, destroyed, and forged and, generally, the communication topology may be changed. Furthermore different executions of the protocol may be not independent as attackers can store and detour information in one execution to use it in a later execution.

Our work springs from the research done to formally describe and verify compositions of Web services. This research has mainly centered on using process algebras to describe and verify visible local behavior of services and just recently (all the references date of the last five years) has started to consider global *choreographic* descriptions of multiple services and the problem of their projection. This yielded the three layered structure depicted in Figure 1 where a global type describing the choreography is projected into a set of session types that are then used to type-check the processes that implement it (as well as guide their implementation). The study thus focuses on defining the relation between the different layers. Implementability is the relation between the first and second layer. Here the important properties are that projection produces systems that are sound and complete with respect to the global description (in the sense stated by Theorem 4.1) and deadlock free (eg, we bar out specifications as
$p \stackrel{a}{\rightarrow} q \lor p \stackrel{a}{\rightarrow} r$ when it has no continuation, since whatever the choice either $q$ or $r$ will be stuck). Typeability is the relation between the second and third layer. Here the important properties are subject reduction (well-typed processes reduce only to well-typed processes) and progress (which in this context implies deadlock freedom).

Although in this work we disregarded the lower layer of processes, it is nevertheless an essential component of this research. In particular, it explains the nature of the messages that characterize this approach, which are *types*. One of the principal aims of this research, thus, is to find the right level of abstraction that must be expressed by types and session types. Consider again Figure 1. The process layer clearly shows the relation between the message received by bob and the one it sends to carol, but this relation (actually, any relation) is abstracted out both in the session and the global type layers. The level of abstraction is greater than that of cryptographic protocols since values are not tracked by global descriptions. Although tracking of values could be partially recovered by resorting to singleton types, there is a particular class of values that deserves special care and whose handling is one of the main future challenges of this research, that is, *channels*. The goal is to include higher order types in global specifications thus enabling the transmission of session channels and therefore the reconfiguration of dynamic reconfiguration of session topology. We thus aim at defining reconfiguration in the specification itself, as opposed to the case of cryptographic protocols where the reconfiguration of the communication topology is considered at meta-level for verification purposes. As a matter of fact, this feature has already been studied in the literature. For instance, the extension of WS-CDL [1] with channel passing is studied in [11] (as the automata approach has the MSC as their reference standard, so the Web service-oriented research refers to the WS-CDL standard whose implementability has been studied in [19]); the paper that first introduced global descriptions for session types [9] explicitly mentions channels in messages that can be sent to other participants to open new sessions on them. In our opinion the existing works on session types are deeply syntactic in nature and suffer from the fact that their global types are defined in function of the languages used to define processes and session types. The consequence is that the design choices done in defining session types are amplified in the passage to global types yielding a somewhat unnatural syntax for global types and restrictive conditions devoid of semantic characterizations. Here we preferred to take a step back and to start by defining global descriptions whose restrictions are semantically justified. So we favored a less rich language with few semantically justified features and leave the addition of more advanced features for a later time.

Coming back to the comparison of the three approaches, the Web service-oriented approach shares several features in common with the other two. As for the automata approach we (in the sense of the Web service-oriented research) focus on the expressiveness of the control, the possibility of branching and iterate, and the effective implementability into deadlock-free local descriptions. However the tendency for Web services is to impose syntactic restrictions from the beginning rather than study the general case and then devise appropriate restrictions with the sought properties (in this respects our work and those of Bravetti, Zavattaro and Lanese [6, 7, 5] are few exceptions in the panorama of the Web service approach). Commonalities with the cryptographic protocol approach are more technical. In particular we share the dynamism of the com-
munication topology (with the caveat about whether this dynamism is performed at the
linguistic or meta-linguistic level) and the robustness with respect to reconfiguration
(the projected session types should ensure that well-typed process will be deadlock free
even in the presence of multiple interleaved sessions and session delegation, though
few works actually enforce this property [3, 13]). As for cryptographic protocols, this
dynamism is also accounted at level of participants since recent work in session types
studies global descriptions of roles that can then be implemented by several different
agents [12]. Finally, there are some characteristics specific to our approach such as the
exploration of new linguistic features (for instance in this work we introduced actions
with multi-senders and encoded multi-receivers) and a pervasive use of compositional
deduction systems that we inherit from type theory. We conclude this section with a
more in-depth description of the main references in this specific area so as to give a
more detailed comparison with our work.

**Multiparty session types.** Global types were introduced in [9] for dyadic sessions and in [16] for multi-party sessions. Channels are present in the global types of both [9] and [16] while the first also allows messages to have a complex structure. Their presence, however, requires the definition of syntactic restrictions that ensure projectability: channels need to be “well-threaded” (to avoid that the use of different channels disrupts the sequentiality constraints of the specification) and message structures must be used “coherently” in different threads (to assure that a fixed server offers the same services to different clients). We did not include such features in our treatment since we wanted to study the problems of sequentiality (which yielded Definition 4.2 of well-formed global type) and of coherence (which is embodied by the subsession relation whose algorithmic counterpart is the ⋀ merge operator) in the simplest setting without further complexity induced by extra features. As a consequence of this choice, our merge between session types is a generalization of the merge in [21, 12] since we allow inputs from different senders (this is the reason why our compatibility is more demanding than the corresponding notion in [21]).

Another feature we disregarded in the present work is *delegation*. This was intro-
duced in [16] for multi-party sessions and is directly inherited from that of dyadic ses-
sions [15]. A participant can delegate another agent to play his role in a session. This
delegation is transparent for all the remaining participant of the session. Delegation is
implemented by exchanging channels, *ie*, by allowing higher-order channels. In this
way the topology of communications may dynamically evolve.

Our crusade for simplification did not restrict itself to exclude features that seemed
inessential or too syntax dependent, but it also used simpler forms of existing constructs.
In particular an important design choice was to use Kleene star instead of more expres-
sive recursive global types used in [15, 9, 16, 12]. Replacing the star for the recursion
gives us a fair implementation of the projected specification almost for free. Fairness
seems to us an important —though neglected by current literature— requirement for
multi-party sessions. Without it a session in which a part continuously interacts leaving
a second one to starve is perfectly acceptable. This is what happens in all the papers
referred in this subsection. Without Kleene star, fairness would be more difficult to en-
force. Clearly recursion is more expressive than iteration, even though we can partially
bridge this gap using k-exit iterations (Section 6).

Finally, although we aimed at simplifying as much as possible, we still imposed
few restrictions that seemed unavoidable. Foremost, the sequentiality condition of Sec-
tion 4, that is, that any two actions that are bound by a semicolon must always appear
in the same order in all traces of (sound and complete) implementations. Surprisingly,
in all current literature of multi-party session types we are aware of, just one work [9]
enforces the sequential semantics of “;”. In [9] the sequentiality condition, called con-
nectedness is introduced (albeit in a simplified setting since—as in [15, 16]— instead
of the “;” the authors consider the simpler case of prefixed actions) and identified as
one of three basic principles for global descriptions under which a sound and com-
plete implementation can be defined. All others (even later) works admit to project, say,
$q \stackrel{a}{\rightarrow} p; r \stackrel{a}{\rightarrow} p$ in implementations in which $p$ reads from $r$ before having read from $q$.
While the technical interest of relaxing the sequentiality constraint in the interpretation
of the “;” operator is clear —it greatly simplifies projectability— we really cannot see
any semantically plausible reason to do it.

Of course all this effort of simplification is worth only if it brings clear advantages.
First and foremost, our simpler setting allows us to give a semantic justification of the
formalism and of the restrictions and the operators we introduced in it. For these reasons
many restrictions that are present in other formalisms are pointless in our framework.
For instance, two global types whose actions can be interleaved in an arbitrary way
(ie, composed by $\wedge$ in our calculus) can share common participants in our global types,
while in the work of [9] and [16] (which use the parallel operator for $\wedge$) this is forbidden.
So these works fail to project (actually, they reject) protocols as simple as the first line
of the example given in the specification (1) in the introduction. Likewise we can have
different receivers in a choice like, for example, the case in which two associated buyers
wait for a price from a given seller:

seller $\xrightarrow{price}$ buyer1; buyer1 $\xrightarrow{price}$ buyer2 $\lor$ seller $\xrightarrow{price}$ buyer2; buyer2 $\xrightarrow{price}$ buyer1

while such a situation is forbidden in [9, 16].

Another situation possible in our setting but forbidden in [9, 16, 12] is to have dif-
ferent sets of participants for alternatives, such as in the following case where a buyer
is notified about a price by the broker or directly by the seller, but in both cases gives
an answer to the broker:

$(seller \xrightarrow{agency} broker; broker \xrightarrow{price} buyer \lor seller \xrightarrow{price} buyer); buyer \xrightarrow{answer} broker$

A similar situation may arise when choosing between repeating or exiting a loop:

seller $\xrightarrow{agency}$ broker; (broker $\xrightarrow{offer}$ buyer; buyer $\xrightarrow{counteroffer}$ broker)*;
(broker $\xrightarrow{result}$ seller $\wedge$ broker $\xrightarrow{result}$ buyer)

which is again forbidden in [9, 16, 12].

The fact of focusing on a core calculus did not stop us from experimenting. On the
contrary, having core definitions for global and session types allowed us to explore new
linguistic and communication primitives. In particular, an original contribution of our work is the addition of actions with multiple senders and encoded multiple receivers (as explained at the beginning of Section 2). This allows us to express both joins and forks of interactions as shown by the specification (3) given in Section 2.

**Choreographies.** Global types can be seen as choreographies [1] describing the interaction of some distributed processes connected through a private multiparty session. Therefore, there is a close relationship between our work and [6, 7, 5], which concern the projection of choreographies into the contracts of their participants. The choreography language in these works essentially coincides with our language of global types and, just like in our case, a choreography is correct if it preserves the possibility to reach a state where all of the involved Web services have successfully terminated. There are some relevant differences though, starting from choreographic interactions that invariably involve exactly one sender and one receiver, while in the present work we allow for multiple senders and we show that this strictly improves the expressiveness of the formalism, which is thus capable of specifying the join of independent activities. Other differences concern the communication model and the projection procedure. In particular, the communication model is synchronous in [6] and based on FIFO buffers associated with each participant of a choreography in [7]. In our model (Section 3) we have a single buffer and we add the possibility for a receiver to specify the participant from which a message is expected. In [6, 7, 5] the projection procedure is basically an homomorphism from choreographies to the behavior of their participants, which is described by a contract language equipped with parallel composition, while our session types are purely sequential. [6, 7] give no conditions to establish which choreographies produce correct projects. In contrast, [5] defines three connectedness conditions that guarantee correctness of the projection. The interesting aspect is that these conditions are solely stated on properties of the set of traces of the choreography, while we need the combination of projectability (Table 3) and well-formedness (Definition 4.2). However, the connectedness conditions in [5] impose stricter constraints on alternative choreographies by requiring that the roles in both branches be the same. This forbids the definition of the two global types described just above that involve the broker participant. In addition, they need a causal dependency between actions involving the same operation which immediately prevents the projection of recursive behaviors (the choreography language in [5] lacks iteration and thus can only express finite interactions).

Finally, in discussing MSG in the long version of this work we argue that requiring the specification and its projection produce the same set of traces (called *standard implementation* in [14]) seemed overly constraining and advocated a more flexible solution such as the definitions of soundness and completeness introduced here. However it is interesting that Bravetti and Zavattaro in [5] take the opposite viewpoint, and make this relation even more constraining by requiring the relation between a choreography and its projection to be a strong bisimulation.

**Other calculi.** In this brief overview we focused on works that study the relation between global specifications and local machine-oriented implementations. However in the literature there is an important effort to devise new description paradigms for ei-
ther global descriptions or local descriptions. In the latter category we want to cite [15, 4], while [10] seems a natural candidate in which to project an eventual higher order extension of our global types. For what concerns global descriptions, the Conversation Calculus [8] stands out for the originality of its approach.

## 8 Conclusion

We think that the design-by-contract approach advocated in [9, 16] and expanded in later works is a very reasonable way to implement distributed systems that are correct by construction. In this work we have presented a theory of global types in an attempt of better understanding their properties and their relationship with multi-party session types. We summarize the results of our investigations in the remaining few lines. First of all, we have defined a proper algebra of global types whose operators have a clear meaning. In particular, we distinguish between sequential composition, which models a strictly sequential execution of interactions, and unconstrained composition, which allows the designer to underspecify the order of possibly dependent interactions. The semantics of gobal types is expressed in terms of regular languages. Aside from providing an accessible intuition on the behavior of the system being specified, the most significant consequence is to induce a *fair* theory of multi-party session types where correct sessions preserve the ability to reach a state in which all the participants have successfully terminated. This property is stronger than the usual progress property within the same session that is guaranteed in other works. We claim that eventual termination is both desirable in practice and also technically convenient, because it allows us to easily express the fact that every participant of a session makes progress (this is non-trivial, especially in an asynchronous setting). We have defined two projection methods from global to session types, a semantic and an algorithmic one. The former allows us to reason about *which* are the global types that can be projected, the latter about *how* these types are projected. This allowed us to define three classes of flawed global types and to suggest if and how they can be amended. Most notably, we have characterized the absence of sequentiality solely in terms of the traces of global types, while we have not been able to provide similar trace-based characterizations for the other flaws. Finally, we have defined a notion of completeness relating a global type and its implementation which is original to the best of our knowledge. In other theories we are aware of, this property is either completely neglected or it is stricter, by requiring the equivalence between the traces of the global type and those of the corresponding implementation.

*Acknowledgments.* We are indebted to several people from the LIAFA lab: Ahmed Bouajjani introduced us to Parikh's equivalence, Olivier Carton explained us subtle aspects of the shuffle operator, Mihaela Sighireanu pointed us several references to global specification formalisms, while Wiesław Zielonka helped us with references on trace semantics. Anca Muscholl helped us on surveying MSC and Martín Abadi and Roberto Amadio with the literature on security protocols (see the long version). Finally, Roberto Bruni gave us serveral useful suggestions to improve the final version of this work. This work was partially supported by the ANR Codex project, by the MIUR Project IPODS, by a visiting researcher grant of the "Fondation Sciences Mathématiques de Paris", and by a visiting professor position of the Université Paris Diderot.
References

1. Web services choreography description language version 1.0. W3C Candidate Recommendation, available at http://www.w3.org/TR/ws-cdl-10/, 2005.

2. J. A. Bergstra, I. Bethke, and A. Ponse. Process algebra with iteration. Technical Report CS-R9314, Programming Research Group, University of Amsterdam, 1993.

3. L. Bettini, M. Coppo, L. D'Antoni, M. De Luca, M. Dezani-Ciancaglini, and N. Yoshida. Global progress in dynamically interleaved multiparty sessions. In Proceedings of CONCUR'08, LNCS 5201, pages 418-433. Springer, 2008.

4. M. Boreale, R. Bruni, R. De Nicola, and M. Loreti. Sessions and pipelines for structured service programming. In Proceedings of FMOODS'08, LNCS 5051, pages 19-38. Springer, 2008.

5. M. Bravetti, I. Lanese, and G. Zavattaro. Contract-driven implementation of choreographies. In Proceedings of TGC'09, LNCS 5474, pages 1-18. Springer, 2008.

6. M. Bravetti and G. Zavattaro. Towards a unifying theory for choreography conformance and contract compliance. In Proceedings of SC'07, LNCS 4829, pages 34-50. Springer, 2007.

7. M. Bravetti and G. Zavattaro. Contract compliance and choreography conformance in the presence of message queues. In Proceedings of WS-FM'08, LNCS 5387, pages 37-54. Springer, 2008.

8. L. Caires and H. T. Vieira. Conversation types. In Proceedings of ESOP'09, LNCS 5502, pages 285-300. Springer, 2009.

9. M. Carbone, K. Honda, and N. Yoshida. Structured communication-centred programming for web services. In Proceedings of ESOP'07, LNCS 4421, pages 2-17. Springer, 2007.

10. G. Castagna and L. Padovani. Contracts for mobile processes. In Proceedings of CONCUR'09, LNCS 5710, pages 211-228. Springer, 2009.

11. C. Chao and Q. Zongyan. An approach to check choreography with channel passing in WS-CDL. In Proceedings of ICWS'08, pages 700-707. IEEE Computer Society, 2008.

12. P.-M. Deniélou and N. Yoshida. Dynamic multirole session types. In Proceedings of POPL'11, pages 435-446, 2011.

13. M. Dezani-Ciancaglini, U. de' Liguoro, and N. Yoshida. On progress for structured communications. In Proceedings of TGC'07, LNCS 4912, pages 257-275. Springer, 2008.

14. B. Genest, A. Muscholl, and D. Peled. Message sequence charts. In Lectures on Concurrency and Petri Nets, LNCS 3098, pages 537-558, 2003.

15. K. Honda, V. Vasconcelos, and M. Kubo. Language primitives and type disciplines for structured communication-based programming. In Proceedings of ESOP'98, LNCS 1381, pages 22-138. Springer, 1998.

16. K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In Proceedings of POPL'08, pages 273-284. ACM, 2008.

17. R. Milner. A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences, 28(3):439-466, 1984.

18. R. J. Parikh. On context-free languages. Journal of the Association for Computing Machinery, 13(4):570-581, 1966.

19. Z. Qiu, X. Zhao, C. Cai, and H. Yang. Towards the theoretical foundation of choreography. In Proceedings WWW'07, pages 973-982. ACM, 2007.

20. K. Takeuchi, K. Honda, and M. Kubo. An interaction-based language and its typing system. In Proceedings of PARLE'94, LNCS 817, pages 398-413. Springer, 1994.

21. N. Yoshida, P.-M. Deniélou, A. Bejleri, and R. Hu. Parameterised multiparty session types. In Proceedings of FOSSACS'10, LNCS 6014, pages 128-145, 2010.