Multiparty Session Types Within a Canonical Binary Theory, and Beyond

Abstract

A widespread approach to software service analysis uses session types. Very different type theories for binary and multiparty protocols have been developed; establishing precise connections between them remains an open problem. We present the first formal relation between two existing theories of binary and multiparty session types: a binary system rooted in linear logic, and a multiparty system based on automata theory. Our results enable the analysis of multiparty protocols using a (much simpler) type theory for binary protocols, ensuring protocol fidelity and deadlock-freedom. As an application, we offer the first theory of multiparty session types with behavioral genericity. This theory is natural and powerful; its analysis techniques reuse results for binary session types.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The purpose of this paper is to demonstrate, in a precise technical sense, how an expressive and extensible theory of multiparty systems can be extracted from a basic theory for binary sessions, thus developing the first formal connection between multiparty and binary session types. Our approach relies on a theory of binary session types rooted in linear logic and on medium processes that capture the behavior of global types.

Relating the global behavior of a distributed system and the components that implement it is a challenging problem in many scenarios. This problem is also important in the analysis of software services, where the focus is on message-passing programs with advanced forms of concurrency and distribution. Within language-based techniques, notable approaches include interface contracts (cf. [8]) and behavioral types [15]. Our interest is in the latter: by classifying behaviors (rather than values), behavioral types abstract structured protocols and enforce disciplined communication exchanges.

Session types [13, 14] are a much-studied class of behavioral types. They organize multiparty protocols as sessions, basic units of structured conversations. Several session typed frameworks have been developed (see [15] for an overview). This diversity makes it hard to compare their associated techniques, and hinders the much desirable transfer of techniques between different typed models.

In this paper, we formally relate two distinct typed models for structured communications. By relying on a type theory of binary sessions rooted in linear logic [5], we establish natural bridges between typed models for binary and multiparty sessions [13, 14]. Our results reveal logically motivated justifications for key concepts in typed models of global/local behaviors, and enable the transfer of reasoning techniques from binary to multiparty sessions. In fact, our approach naturally enables us to define the first model of multiparty session types with parametric polymorphism, which in our setting means behavioral genericity (i.e., passing first-class behavioral interfaces in messages), not just datatype genericity. This new model is very powerful; we equip it with analysis techniques for behavioral genericity by reusing results for binary session types [4].

Binary protocols [13] involve two partners, each abstracted by a behavioral type; correct interactions rely on compatibility, i.e., when one partner performs an action, the other performs a complementary one. Multiparty protocols may involve more than two partners: there is a global specification to which all of them, from their local perspectives, should adhere. In multiparty session types [12, 14], these visions are described by a global type and local types, respectively; a projection function relates the two. Previous research shows that type systems for multiparty protocols have a more involved theory than binary ones. For instance, the analysis of deadlock-freedom in multiparty protocols is challenging [10], and certainly harder than for binary protocols.

The question is then: could multiparty session types be reduced into binary ones? Defining such a reduction is far from trivial, as it should satisfy at least two requirements. First, the resulting collection of binary interactions must preserve crucial sequencing information among multiparty exchanges. Second, it should avoid undesirable behaviors: synchronization errors, deadlocks, non-terminating reductions.

This paper answers the above question in the affirmative. We tightly relate: (i) a standard theory of multiparty session types [12, 14], and (ii) the theory of deadlock-free binary session types proposed in [5]. The key device in our approach is the medium process of a multiparty protocol.

Given a global type G, its medium process $\mathsf {M}\!\!\llbracket G \rrbracket$ is an entity that mediates in all communications. Therefore, $\mathsf {M}\!\!\llbracket G \rrbracket$ extracts the semantics of G, uniformly capturing its sequencing information. Process $\mathsf {M}\!\!\llbracket G \rrbracket$ is meant to interact with well-typed implementations for all participants declared in G. This way, for instance, given the global type $G = \mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l _i\langle U_i\rangle .G_i\}_{i \in I}$ (i.e., a labeled, directed exchange from $\mathtt {p}$ to $\mathtt {q}$, indexed by I, which precedes execution of a protocol $G_i$), its medium $\mathsf {M}\!\!\llbracket G \rrbracket$ first receives a label $l _j$ and message of type $U_j$ sent by $\mathtt {p}$’s implementation (with $j \in I$); then, it forwards these two objects to $\mathtt {q}$’s implementation; lastly, it executes process $\mathsf {M}\!\!\llbracket G_j \rrbracket$.

Interestingly, our medium-based approach applies to global types with name passing, delegation, and parallel composition. To fully characterize a global type G, we determine the conditions under which $\mathsf {M}\!\!\llbracket G \rrbracket$ may be well-typed using binary session types, with respect to its local types. A key ingredient here is the theory for binary session types introduced in [5]. Due to their logical foundations, typability in [5] entails: fidelity (protocols are respected), safety (absence of communication errors), deadlock-freedom (processes do not get stuck), and termination (infinite internal behavior is ruled out). Most relevant for our approach is deadlock-freedom, not directly ensured by alternative type systems.

Here we present an analysis of multiparty session types using a theory of binary session types, ensuring fidelity and deadlock-freedom. Our technical contributions are:

• Characterization results relating (a) a global type that is well-formed (correct projectability) and (b) typability of its medium using binary session types (Theorems 4 and 5).

• Operational correspondence results relating (a) the behavior of a global type and (b) the behavior of its medium (instrumented in a natural way) composed with well-typed implementations for each local type (Theorem 7). These results confirm that our analysis does not introduce extra sequentiality in protocols.

• A proof that behavioral transformations of global types [6] can be justified by typed equalities for binary sessions [19] expressed at the level of mediums (Theorem 6). This result offers a deep semantic justification of structural identities on global types, such as those capturing parallelism via interleaving of causally independent exchanges.

• Transfer of techniques from binary to multiparty protocols. We define the first theory of multiparty session types with behavioral genericity; its analysis techniques reuse the binary session type theory with parametric polymorphism given in [4].

Our results define the first formal relation between multiparty and binary session types. They highlight the fundamental character of the notions involved, since they can be independently explained by communicating automata (cf. [12]) and linear logic (cf. [5]).

Next, we collect definitions on multiparty sessions [12, 14] and binary sessions [5]. Our technical contributions are reported in Sect. 3. In Sect. 4 we illustrate these contributions by means of an example that features non-trivial forms of replication and sharing. In Sect. 5 we introduce multiparty session types with behavioral genericity, and in Sect. 6 we illustrate our approach in the analysis of a multiparty protocol. Section 7 concludes and discusses related works.

2 Preliminaries: Binary and Multiparty Session Types

Binary Session Types. We build upon the theory of binary session types of [5, 21], based on an interpretation of session types as linear logic propositions. We assume no background on linear logic from the reader; we refer to [5] for further details.

The Process Model. We define a synchronous $\pi$-calculus [20] with forwarding and n-ary labeled choice. We use $l _1, l _2, \ldots$ to range over labels. Given an infinite set $\varLambda$ of names (x, y, z, u, v), the set of processes (P, Q, R) is defined by

$$\begin{aligned} \begin{array}{rllllllllllllllllllllllllll} P {:}{:=} &{} \mathbf {0} &{} ~{\large \mid }~&{} P \mathord {\;\varvec{|}\;}Q &{} ~{\large \mid }~&{} ({\varvec{\nu }}y)P ~{\large \mid }~&{} \overline{x}\,y.P &{} ~{\large \mid }~&{} x(y).P &{} ~{\large \mid }~&{} \mathbf {!}x(y).P &{} ~{\large \mid }~\\ &{} x\triangleleft \! l _i;P &{} ~{\large \mid }~&{} x\triangleright \!\{ l _i : P_i\}_{i \in I} &{} ~{\large \mid }~&{}[x\!\leftrightarrow \!y] \end{array} \end{aligned}$$

Operators ${\varvec{0}}$ (inaction), $P\mathord {\;\varvec{|}\;}Q$ (parallel composition), and $({\varvec{\nu }}y)P$ (restriction) are standard. We have $\overline{x}\,y.P$ (send y on x, proceed as P), $x(y).P$ (receive a z on x, proceed as P with y replaced by z), and the replicated input $\mathbf {!}x(y).P$. Operators $x\triangleleft \!\, l ;P$ and $x\triangleright \!\{ l _i{:}P_i\}_{i \in I}$ define labeled choice [13]. Forwarding $[x\!\leftrightarrow \!y]$ equates x and y; it is a copycat process, similar to wires in [20]. Also, $\overline{x}(y)$ denotes the bound output $({\varvec{\nu }}y) \overline{x}\, y$.

In restriction $({\varvec{\nu }}y)P$ and input x(y).P the occurrence of name y is binding, with scope P. The set of free names of a process P is denoted ${ fn}(P)$. In a statement, a name is fresh if it is not among the names of the objects (processes, actions, etc.) of the statement. A process is closed if it does not contain free occurrences of names. We identify processes up to consistent renaming of bound names. The capture-avoiding substitution of x for y in P is denoted . Notation $\widetilde{k}$ denotes a finite sequence of pairwise distinct names $k_1, k_2, \cdots$. We sometimes treat sequences of names as sets.

Reduction expresses the internal behavior of processes. Closed under structural congruence (noted $\equiv$, see [5]), it is the binary relation on processes defined by the rules:

The interaction of a process with its environment is defined by an early labeled transition system (LTS) for the $\pi$-calculus [20], extended with labels and transition rules for choice and forwarding. Transition $P\xrightarrow {\,\lambda \,}Q$ says that P may evolve to Q by performing the action represented by label $\lambda$, defined as: $\lambda \ {:}{:=} \ \tau ~{\large \mid }~x(y) ~{\large \mid }~x\triangleleft \!\, \, {l} ~{\large \mid }~ \overline{x}\,y ~{\large \mid }~\overline{x}(y) ~{\large \mid }~\overline{x\triangleleft \!\, \, {l}}$. Actions are the input x(y), the offer $x\triangleleft \!\, \, {l}$, and their co-actions: the output $\overline{x}\,y$ and bound output $\overline{x}(y)$ actions, and the selection $\overline{x\triangleleft \!\, \, {l}}$, resp. The bound output $\overline{x}(y)$ denotes extrusion of y along x. Internal action is denoted $\tau$. Figure 1 gives a selection of the rules that define $P\xrightarrow {\lambda }Q$. Weak transitions are as usual: $\mathop {\Longrightarrow }\limits ^{}$ is the reflexive, transitive closure of $\xrightarrow {\tau }$. Notation $\mathop {\Longrightarrow }\limits ^{\lambda }$ stands for $\mathop {\Longrightarrow }\limits ^{~}\xrightarrow {\lambda }\mathop {\Longrightarrow }\limits ^{~}$ (given $\lambda \ne \tau$) and $\mathop {\Longrightarrow }\limits ^{\tau }$ stands for $\mathop {\Longrightarrow }\limits ^{}$.

Fig. 1.

LTS for processes (Excerpt).

Session Types as Linear Logic Propositions. The type theory of [5] connects session types as linear logic propositions. Main properties derived from typing, absent from other binary session type theories, are global progress (deadlock-freedom) and termination [19]. The syntax of binary types is as follows:

Definition 1

(Binary Types). Types (A, B, C) are given by

We use $A\otimes B$ (resp. $A \,\mathord {\multimap }\,B$) to type a name that performs an output (resp. an input) to its partner, sending (resp. receiving) a name of type A, and then behaves as type B. Thus, $A\otimes B$ and $A\,\mathord {\multimap }\,B$ represent the session types !A; B and ?A; B introduced in [13]. We generalize [5] by considering n-ary offer and choice $\oplus$. Given a finite index set I, types a name that offers a choice between an $l _i$. Dually, $\oplus \!\{ l _i{:}A_i\}_{i \in I}$ types the selection of one of the $l _i$. Type $\mathbf {!}A$ types a shared channel, used by a server to spawn an arbitrary number of new sessions (possibly none), each one conforming to A. Type $\mathbf{1 }$ is the terminated session; names of type $\mathbf{1 }$ may be passed around as opaque values.

A type environment collects type assignments of the form x : A, where x is a name and A is a type, the names being pairwise disjoint. We consider two typing environments, subject to different structural properties: a linear part $\varDelta$ and an unrestricted part $\varGamma$, where weakening and contraction principles hold for $\varGamma$ but not for $\varDelta$.

Fig. 2.

The type system for binary sessions (Excerpt).

A type judgment $\varGamma ; \varDelta \vdash P \ {:}{:} \ z{:}C$ asserts that P provides behavior C at channel z, building on “services” declared in $\varGamma ;\varDelta$. This way, e.g., a client Q that relies on external services and does not provide any is typed as $\varGamma ; \varDelta \vdash Q \ {:}{:} \ z{:}\mathbf{1 }$. The domains of $\varGamma ,\varDelta$ and z : C are required to be pairwise disjoint. We write $dom(\varGamma )$ (resp. $dom(\varDelta )$) to denote the domain of $\varGamma$ (resp. $\varDelta$), a sequence of names. Empty environments are denoted ‘$\,\cdot \,$’. As $\pi$-calculus terms are considered up to structural congruence, typability is closed under $\equiv$ by definition. We sometimes abbreviate $\varGamma ; \varDelta \vdash P \ {:}{:} \ z{:}\mathbf{1 }$ as $\varGamma ; \varDelta \vdash P$.

Figure 2 presents selected typing rules; see [5] for a full account. We have right and left rules: they say how to implement and use a session of a given type, respectively. We briefly comment on some of the rules. Rule (T$\mathsf {id}$) defines identity in terms of forwarding. Rule (T$\mathsf {cut}$) define typed composition via parallel composition and restriction. Implementing a session type amounts to offering a choice between n sessions with type $A_i$ (Rule (T)); its use on name x entails selecting an alternative, using prefix $x\triangleleft \!\, l _j$ (Rules T and (T)). Type $\oplus \!\{ l _i : A_i\}_{i \in I}$ has a dual interpretation.

We now recall some main results for well-typed processes. For any P, define live(P) iff $P \equiv ({\varvec{\nu }}\widetilde{n})(\pi .Q \mathord {\;\varvec{|}\;}R)$, for some names $\widetilde{n}$, a process R, and a non-replicated guarded process $\pi .Q$. Also, we write $P \Downarrow$, if there is no infinite reduction path from process P.

Theorem 1

(Properties of Well-Typed Processes).

• 1. Subject Reduction [5]: If $\varGamma ; \varDelta \vdash P \ {:}{:} \ x{:}A$ and $P \rightarrow Q$ then $\varGamma ; \varDelta \vdash Q {:}{:} x{:}A$.

• 2. Global Progress [5]: If $\cdot ; \cdot \vdash P {:}{:} z{:}\mathbf{1 }$ and live(P) then exists a Q such that $P \rightarrow Q$.

• 3. Termination/Strong Normalization [19]: If $\varGamma ; \varDelta \vdash P \ {:}{:} \ x{:}A$ then $P \Downarrow$.

Theorem 1 (2), key in our work, implies that our type discipline ensures deadlock freedom. Further properties of well-typed processes concern proof conversions and typed behavioral equivalences. The correspondence in [5] is realized by relating proof conversions in linear logic with appropriate process equivalences. There is a group of commuting conversions that induces a behavioral congruence on typed processes, noted $\simeq _{c}$. Process equalities justified by $\simeq _{c}$ include, e.g., (see [19] for details):

These equalities reflect a behavioral equivalence over session-typed processes, called context bisimilarity (noted $\approx$) [19]. Roughly, typed processes $\varGamma ; \varDelta \vdash P \ {:}{:} \ x{:}A$ and $\varGamma ; \varDelta \vdash Q {:}{:} x{:}A$ are context bisimilar if, once composed with their requirements (described by $\varGamma , \varDelta$), they perform the same actions on x (as described by A). Context bisimilarity is a congruence relation on well-typed processes. We have:

Theorem 2

([19]). If $\varGamma ; \varDelta \vdash P \simeq _{c} Q \ {:}{:} \ z{:}C$ then $\varGamma ; \varDelta \vdash P \approx Q\,{{:}{:}}\,z{:}C$.

Multiparty Session Types. Our syntax of global types includes constructs from [12, 14]. With respect to [12], we consider value passing in branching (cf. U below), fully supporting delegation and add parallel composition. Below, participants are ranged over by $\mathtt {p}, \mathtt {q}, \mathtt {r}, \ldots$; labels are ranged over by $l _1, l _2, \ldots$. To streamline the presentation, we consider standard global types without recursion. Our approach extends to global types with recursion, exploiting the extension of [5] with co-recursion [21]. Results for global types with recursion can be found in an online technical report [3].

Definition 2

(Global/Local Types). Define global types (G) and local types (T) as

$$\begin{aligned} \begin{array}{rcl} &{}G \ {:}{:=} &{} \mathtt {end} ~{\large \mid }~\mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l _i\langle U_i\rangle .G_i\}_{i \in I} ~{\large \mid }~G_1 \mathord {\;\varvec{|}\;}G_2 \qquad U \ {:}{:=} \mathsf {bool} ~{\large \mid }~\mathsf {nat} ~{\large \mid }~\mathsf {str} ~{\large \mid }~\ldots ~{\large \mid }~T\\ &{}T \ {:}{:=} &{} \mathsf {end} ~{\large \mid }~\mathtt {p}?\{ l _i\langle U_i\rangle .T_i\}_{i \in I} ~{\large \mid }~\mathtt {p}!\{ l _i\langle U_i\rangle .T_i\}_{i \in I} \end{array} \end{aligned}$$

$\mathcal {G}$ denotes the above set of global types. Given a finite I and pairwise different labels, $\mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l _i\langle U_i\rangle .G_i\}_{i \in I}$ specifies that by choosing label $l _i$, participant $\mathtt {p}$ may send a message of type $U_i$ to participant $\mathtt {q}$, and then continue as $G_i$. We decree $\mathtt {p} \ne \mathtt {q}$, so reflexive interactions are disallowed. The global type $G_1 \mathord {\;\varvec{|}\;}G_2$ allows the concurrent execution of $G_1$ and $G_2$. We write $\mathtt {end}$ to denote the completed global type. The local type $\mathtt {p}?\{ l _i\langle U_i\rangle .T_i\}_{i \in I}$ denotes an offer of a set of labeled alternatives; the local type $\mathtt {p}!\{ l _i\langle U_i\rangle .T_i\}_{i \in I}$ denotes a behavior that chooses one of such alternatives. The terminated local type is $\mathsf {end}$. Following [14], there is no local type for parallel.

Example 1

Consider a global type $G_{\text {BS}}$, a variant of the the two-buyer protocol in [14], in which two buyers ($\mathtt {B_1}$ and $\mathtt {B_2}$) coordinate to buy an item from a seller ($\mathtt {S}$):

$$\begin{aligned} G_{\text {BS}} = \mathtt {B_1}\!\twoheadrightarrow \!\mathtt {S}{:}\big \{ send \langle \mathsf {str}\rangle .\mathtt {S}\!\twoheadrightarrow \!\mathtt {B_1}{:}\{ rep \langle \mathsf {int}\rangle .\mathtt {S}\!\twoheadrightarrow \!\mathtt {B_2}{:}\{ rep \langle \mathsf {int}\rangle . ~~~~~~~~ \\ ~~ \mathtt {B_1}\!\twoheadrightarrow \!\mathtt {B_2}{:}\{ shr \langle \mathsf {int}\rangle .\mathtt {B_2}\!\twoheadrightarrow \!\mathtt {S}{:}\{ ok \langle \mathsf {{\varvec{1}}}\rangle .\mathtt {end} \, , \, quit \langle \mathsf {{\varvec{1}}}\rangle .\mathtt {end} \}\!\}\!\}\!\}\!\big \}_{} \end{aligned}$$

Intuitively, $\mathtt {B_1}$ requests the price of an item to $\mathtt {S}$, who replies to $\mathtt {B_1}$ and $\mathtt {B_2}$. Then $\mathtt {B_1}$ communicates to $\mathtt {B_2}$ her contribution in the transaction; finally, $\mathtt {B_2}$ either confirms the purchase to $\mathtt {S}$ or closes the transaction.

We now define projection for global types. Following [12], projection relies on a merge operator on local types, which in our case considers messages U.

Definition 3

(Merge). We define $\sqcup$ as the commutative partial operator on base and local types such that: 1. $\mathsf {bool} \sqcup \mathsf {bool} = \mathsf {bool}$ (and similarly for other base types); 2. $\mathsf {end} \sqcup \mathsf {end} = \mathsf {end}$; 3. $\mathtt {p}!\{ l _i \langle U_i\rangle .T_i\}_{i \in I} \sqcup \mathtt {p}!\{ l _i \langle U_i\rangle .T_i\}_{i \in I} = \mathtt {p}!\{ l _i \langle U_i\rangle .T_i\}_{i \in I}$; and

• 4. $\mathtt {p}?\{ l _k\langle U_k\rangle .T_k\}_{k \in K} \sqcup \mathtt {p}?\{ l '_j\langle U'_j\rangle .T'_j\}_{j \in J} =$ $~\qquad \mathtt {p}?\big (\{ l _k\langle U_k\rangle .T_k\}_{k \in K\setminus J} \cup \{ l '_j\langle U'_j\rangle .T'_j\}_{j \in J\setminus K} \cup \{ l _l\langle U_l \sqcup U'_l \rangle .(T_l \sqcup T'_l)\}_{l \in K\cap J}\big )$

and is undefined otherwise.

Therefore, for $U_1 \sqcup U_2$ to be defined there are two options: (a) $U_1$ and $U_2$ are identical base, terminated or selection types; (b) $U_1$ and $U_2$ are branching types, but not necessarily identical: they may offer different options but with the condition that the behavior in labels occurring in both $U_1$ and $U_2$ must be mergeable. The set of participants of G ($\mathsf {part}(G)$) is defined as:  $\mathsf {part}(\mathtt {end}) =\emptyset$, $\mathsf {part}(G_1 \mathord {\;\varvec{|}\;}G_2) = \mathsf {part}(G_1 ) \cup \mathsf {part}(G_2)$, $\mathsf {part}(\mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l _i\langle U_i\rangle .G_i\}_{i \in I}) = \{\mathtt {p} , \mathtt {q}\} \cup \bigcup _{i \in I} \mathsf {part}(G_i)$.

Definition 4

(Projection [12]). Let G be a global type. The projection of G under participant $\mathtt {r}$, denoted $G\!\!\upharpoonright \!{\mathtt {r}}$, is defined as: $\mathtt {end} \!\!\upharpoonright \!{\mathtt {r}} = \mathsf {end}$ and

• $\mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l _i\langle U_i\rangle .G_i\}_{i \in I}\!\!\upharpoonright \!{\mathtt {r}} = {\left\{ \begin{array}{ll} \mathtt {p}!\{ l _i \langle U_i\rangle .G_i\!\!\upharpoonright \!{\mathtt {r}}\}_{i \in I} &{} \text {if } \mathtt {r} = \mathtt {p} \\ \mathtt {p}?\{ l _i \langle U_i\rangle .G_i\!\!\upharpoonright \!{\mathtt {r}}\}_{i \in I} &{} \text {if } \mathtt {r} = \mathtt {q} \\ \sqcup _{i \in I} \,G_i\!\!\upharpoonright \!{\mathtt {r}} &{} \text {otherwise } (\sqcup \text { as in Definition 3)} \end{array}\right. }$

• $(G_1 \mathord {\;\varvec{|}\;}G_2) \!\!\upharpoonright \!{\mathtt {r}} = {\left\{ \begin{array}{ll} G_i\!\!\upharpoonright \!{\mathtt {r}} &{} \ {if \ } \mathtt {r} \in \mathsf {part}(G_i) { \ and \ } \mathtt {r} \not \in \mathsf {part}(G_j), i \ne j \in \{1,2\} \\ \mathsf {end} &{} \ {if \ } \mathtt {r} \not \in \mathsf {part}(G_1) { \ and \ } \mathtt {r} \not \in \mathsf {part}(G_2) \end{array}\right. }$

When a side condition does not hold, the map is undefined.

Definition 5

(Well-Formed Global Types [12]). Global type $G \in \mathcal {G}$ is well-formed (WF) if for all $\mathtt {r} \in \mathsf {part}(G)$, the projection $G\!\!\upharpoonright \!{\mathtt {r}}$ is defined.

Fig. 3.

Swapping relation on global types (Definition 6). $A\#B$ denotes that sets A, B are disjoint.

The last notion required in our characterization of multiparty session types as binary sessions is a swapping relation over global types [6], which enables transformations among causally independent communications. Such transformations may represent optimizations that increase parallelism while preserving the intended global behavior.

Definition 6

(Global Swapping). The swapping relation $\simeq _{\mathtt {sw}}$ is the smallest congruence on $\mathcal {G}$ which satisfies the rules in Fig. 3. (The symmetric of (sw2) is omitted.)

3 Relating Multiparty and Binary Session Type Theories

Our analysis of multiparty protocols as binary sessions relies on the medium process of a global type. Mediums offer a simple device for analyzing global types using the binary session types of [5]. Mediums uniformly capture the sequencing behavior in a global type, for they take part in all message exchanges between local participants.

After defining mediums (Definition 7), we establish their characterization results (Theorems 4 and 5). We then present a process characterization of global swapping (Definition 6) in terms of context bisimilarity (Theorem 6). Subsequently, we state operational correspondence results (Theorem 7), exploiting the auxiliary notions of instrumented mediums (Definition 10) and multiparty systems (Definition 11). We use the following conventions.

Convention 3

(Indexed/Annotated Names). We consider names indexed by participants $\mathtt {p}, \mathtt {q}, \ldots$, noted $c_{\mathtt {p}}, c_{\mathtt {q}}, \ldots$ and names annotated by participants, noted $k^{\mathtt {p}}, k^{\mathtt {q}}, \ldots$. Given $\mathtt {p} \ne \mathtt {q}$, indexed names $c_{\mathtt {p}}$ and $c_{\mathtt {q}}$ denote two different objects; in contrast, annotated names $k^{\mathtt {p}}$ and $k^{\mathtt {q}}$ denote the same name k with different annotations. Given a G with $\mathsf {part}(G) = \{\mathtt {p}_1, \ldots , \mathtt {p}_n\}$, we will write $\mathsf {npart}(G)$ to denote the set that contains a unique name $c_{\mathtt {p}_j}$ for every participant ${\mathtt {p}_j}$ of G. We will occasionally use $\mathsf {npart}(G)$ as an unordered sequence of names.

Definition 7

(Mediums). The medium of $G \in \mathcal {G}$, denoted $\mathsf {M}\!\!\llbracket G \rrbracket$, is defined as follows:

• $\mathsf {M}\!\!\llbracket \mathtt {end} \rrbracket = {\varvec{0}}$

• $\mathsf {M}\!\!\llbracket G_1 \mathord {\;\varvec{|}\;}G_2 \rrbracket = \mathsf {M}\!\!\llbracket G_1 \rrbracket \mathord {\;\varvec{|}\;}\mathsf {M}\!\!\llbracket G_2 \rrbracket$

• $\mathsf {M}\!\!\llbracket \mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l _i\langle U_i\rangle .G_i\}_{i \in I} \rrbracket = c_\mathtt {p}\triangleright \!\big \{ l _i : c_\mathtt {p}(u).c_\mathtt {q}\triangleleft \! l _i;\overline{c_\mathtt {q}}(v).( [u\!\leftrightarrow \!v] \mathord {\;\varvec{|}\;}\mathsf {M}\!\!\llbracket G_i \rrbracket )\big \}_{i \in I}$

The key case is $\mathsf {M}\!\!\llbracket \mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l _i\langle U_i\rangle .G_i\}_{i \in I} \rrbracket$: note how the medium uses two prefixes (on name $c_\mathtt {p}$) to mediate with $\mathtt {p}$, followed by two prefixes (on name $c_\mathtt {q}$) to mediate with $\mathtt {q}$. We illustrate mediums by means of an example:

Example 2

The medium process for global type ${G_{\text {BS}}}$ in Example 1 is:

$$\begin{aligned} \begin{array}{cl} \mathsf {M}\!\!\llbracket G_{\text {BS}} \rrbracket = &{} c_\mathtt {B1}\triangleright \!\big \{ send : c_\mathtt {B1}(v).c_\mathtt {S}\triangleleft \! send ;\overline{c_\mathtt {S}}(w).([w\!\leftrightarrow \!v] \mathord {\;\varvec{|}\;}\\ &{} \quad c_\mathtt {S}\triangleright \!\{ rep : c_\mathtt {S}(v).c_\mathtt {B1}\triangleleft \! rep ;\overline{c_\mathtt {B1}}(w).([w\!\leftrightarrow \!v] \mathord {\;\varvec{|}\;}\\ &{} \qquad c_\mathtt {S}\triangleright \!\{ rep : c_\mathtt {S}(v).c_\mathtt {B2}\triangleleft \! rep ;\overline{c_\mathtt {B2}}(w).([w\!\leftrightarrow \!v] \mathord {\;\varvec{|}\;}\\ &{} \qquad \quad c_\mathtt {B1}\triangleright \!\{ shr : c_\mathtt {B1}(v).c_\mathtt {B2}\triangleleft \! shr ;\overline{c_\mathtt {B2}}(w).([w\!\leftrightarrow \!v] \mathord {\;\varvec{|}\;}\\ &{} \qquad \qquad c_\mathtt {B2}\triangleright \!\{~ ok : c_\mathtt {B2}(v).c_\mathtt {S}\triangleleft \! ok ;\overline{c_\mathtt {S}}(w).([w\!\leftrightarrow \!v] \mathord {\;\varvec{|}\;}{\varvec{0}}) \, , \, \\ &{} \qquad \qquad \qquad quit : c_\mathtt {B2}(v).c_\mathtt {S}\triangleleft \! quit ;\overline{c_\mathtt {S}}(w).([w\!\leftrightarrow \!v] \mathord {\;\varvec{|}\;}{\varvec{0}}) \}_{})\}_{})\}_{})\}_{})\big \}_{} \end{array} \end{aligned}$$

Intuitively, we expect that (well-typed) process implementations for $\mathtt {B_1}$, $\mathtt {B_2}$, and $\mathtt {S}$ should interact with $\mathsf {M}\!\!\llbracket G_{\text {BS}} \rrbracket$ through channels $c_\mathtt {B1}$, $c_\mathtt {B2}$, and $c_\mathtt {S}$, respectively.    $\square$

We now move on to state our characterization results. We require two auxiliary notions, given next. Below, we sometimes write $\varGamma ; \varDelta \vdash \mathsf {M}\!\!\llbracket G \rrbracket$ instead of $\varGamma ; \varDelta \vdash \mathsf {M}\!\!\llbracket G \rrbracket \ {:}{:} \ z {:}\mathbf{1 }$, when $z \not \in { fn}(\mathsf {M}\!\!\llbracket G \rrbracket )$.

Definition 8

(Compositional Typing). We say $\varGamma ; \varDelta \vdash \mathsf {M}\!\!\llbracket G \rrbracket {:}{:} z{:}C$ is a compositional typing if: (i) it is a valid typing derivation; (ii) $\mathsf {npart}(G) \subseteq dom(\varDelta )$; and (iii) $C = \mathbf{{1}}$.

A compositional typing says that $\mathsf {M}\!\!\llbracket G \rrbracket$ depends on behaviors associated to each participant of G; it also specifies that $\mathsf {M}\!\!\llbracket G \rrbracket$ does not offer any behaviors of its own. We relate binary session types and local types: the main difference is that the former do not mention participants. Below, B ranges over base types ($\mathsf {bool}, \mathsf {nat}, \ldots$) in Definition 2.

Definition 9

(Local Types $\rightarrow$ Binary Types). Mapping $\langle \!\langle \cdot \rangle \!\rangle$ from local types T (Definition 2) into binary types A (Definition 1) is inductively defined as $\langle \!\langle \mathsf {end} \rangle \!\rangle = \langle \!\langle B \rangle \!\rangle = \mathbf{1 }$ and

3.1 Characterization Results

Our characterization results relate process $\mathsf {M}\!\!\llbracket G \rrbracket$ (well-typed with a compositional typing) and $\langle \!\langle G\!\!\upharpoonright \!{\mathtt {p}_1} \rangle \!\rangle , \ldots , \langle \!\langle G\!\!\upharpoonright \!{\mathtt {p}_n} \rangle \!\rangle$ (i.e., the local types of G transformed into binary session types via Definition 9). Our characterization results are in two directions, given by Theorems 4 and 5. The first direction says that well-formedness of global types (Definition 5) ensures compositional typings for mediums with (logic based) binary session types:

Theorem 4

(Global Types $\rightarrow$ Typed Mediums). Let $G \in \mathcal {G}$. If G is WF with $\mathsf {part}(G)\!= \{\mathtt {p}_1, \ldots , \mathtt {p}_n\}$ then $\varGamma ; c_{\mathtt {p}_1}{:}\langle \!\langle G\!\!\upharpoonright \!{\mathtt {p}_1} \rangle \!\rangle , \ldots , c_{\mathtt {p}_n}{:}\langle \!\langle G\!\!\upharpoonright \!{\mathtt {p}_n} \rangle \!\rangle \vdash \mathsf {M}\!\!\llbracket G \rrbracket$ is a compositional typing, for some $\varGamma$.

The second direction of the characterization is the converse of Theorem 4: compositional typings for mediums induce global types which are WF. Given local types $T_1, T_2$, below we write $T_1 \preceq ^\sqcup T_2$ if there exists a local type $T'$ such that $T_1 \sqcup T' = T_2$ (cf. Definition 3). This notation allows us to handle the labeled alternatives silently introduced by rule (T).

Theorem 5

(Well-Typed Mediums $\rightarrow$ Global Types). Let $G \in \mathcal {G}$. If $\varGamma ; c_{\mathtt {p}_1}{:}A_1, \ldots , c_ {\mathtt {p}_n}{:}A_ n \vdash \mathsf {M}\!\!\llbracket G \rrbracket$ is a compositional typing then $\exists T_1, \ldots , T_ n$ such that $G\!\!\upharpoonright \!{\mathtt {p}_j} \preceq ^\sqcup T_j$ and $\langle \!\langle T_j \rangle \!\rangle = A_j$, for all $\mathtt {p}_j \in \mathsf {part}(G)$.

Theorems 4 and 5 tightly connect (i) global types, local types and projection, and (ii) medium processes, and logic-based binary session types. They also provide an independent deep justification, through purely logical arguments, to the notion of projection.

3.2 A Behavioral Characterization of Global Swapping

Global swapping (Definition 6, Fig. 3) can be directly justified from more primitive notions, based on the characterizations given by Theorems 4 and 5. By abstracting a global type’s behavior in terms of its medium we may reduce transformations on global types to type-preserving transformations on processes. This is the content of Theorem 6 below, which connects global swapping ($\simeq _{\mathtt {sw}}$) and context bisimilarity ($\approx$). Hence, sequentiality of mediums can be relaxed in the case of causally independent exchanges captured by $\simeq _{\mathtt {sw}}$.

Theorem 6

Let $G_1 \in \mathcal {G}$ such that $\mathsf {M}\!\!\llbracket G_1 \rrbracket$ has a compositional typing $\varGamma ; \varDelta \vdash \mathsf {M}\!\!\llbracket G_1 \rrbracket$, for some $\varGamma , \varDelta$. If $G_1 \simeq _{\mathtt {sw}} G_2$ then $\varGamma ; \varDelta \vdash \mathsf {M}\!\!\llbracket G_1 \rrbracket \approx \mathsf {M}\!\!\llbracket G_2 \rrbracket$.

Since $\mathsf {M}\!\!\llbracket G \rrbracket$ is a low-level representation of G, the converse of Theorem 6 is less interesting, for type-preserving transformations at the (low) level of mediums do not always correspond to behavior-preserving transformations at the (high) level of global types. That is, since $\mathsf {M}\!\!\llbracket G \rrbracket$ implements each communication in G using several prefixes, swapping in G occurs only when all relevant prefixes in $\mathsf {M}\!\!\llbracket G \rrbracket$ can be commuted via $\simeq _{c}$.

3.3 Operational Correspondence Results

The results given so far focus on the static semantics of multiparty and binary systems, and are already key to justify essential properties such as absence of global deadlock. We now move on to dynamic semantics, and establish operational correspondence results between a global type and its medium process (Theorem 7).

We define the instrumented medium of a global type G, denoted ${\mathbf {M}}_{\widetilde{k}}\llbracket G \rrbracket$, as a natural extension of Definition 7. Process ${\mathbf {M}}_{\widetilde{k}}\llbracket G \rrbracket$ exploits fresh sessions (denoted $\widetilde{k}$), to emit a visible signal for each action of G. We use $\widetilde{k}$ as annotated names (cf. Convention 3): each action on a $k_i$ contains the identity of the participant of G which performs it. Then, using ${\mathbf {M}}_{\widetilde{k}}\llbracket G \rrbracket$ we define the set of systems associated to G (Definition 11), which collects process implementations for G mediated by ${\mathbf {M}}_{\widetilde{k}}\llbracket G \rrbracket$. Since interactions between local implementations and ${\mathbf {M}}_{\widetilde{k}}\llbracket G \rrbracket$ are unobservable actions, Theorem 7 connects (i) the visible behavior of a system along annotated names $\widetilde{k}$, and (ii) the visible behavior of G, defined by an LTS on global types (a variant of that in [12]). Below, $k^{\mathtt {p}}.P$ stands for $k^{\mathtt {p}}(x).P$ when x is not relevant in P. Also, $\widehat{k^{\mathtt {p}}}.P$ stands for $\overline{k^{\mathtt {p}}}(v).({\varvec{0}} \mathord {\;\varvec{|}\;}P)$ for some v.

Definition 10

(Instrumented Mediums). Let $\widetilde{k}$ be fresh, annotated names. The instrumented medium of $G \in \mathcal {G}$ with respect to $\widetilde{k}$, denoted ${\mathbf {M}}_{\widetilde{k}}\llbracket G \rrbracket$, is defined as follows:

• ${\mathbf {M}}_{k}\llbracket \mathtt {end} \rrbracket = \mathbf {0}$

• ${\mathbf {M}}_{k_1,k_2}\llbracket G_1 \mathord {\;\varvec{|}\;}G_2 \rrbracket = {\mathbf {M}}_{k_1}\llbracket G_1 \rrbracket \mathord {\;\varvec{|}\;}{\mathbf {M}}_{k_2}\llbracket G_2 \rrbracket$

• ${\mathbf {M}}_{k}\llbracket \mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l _i\langle U_i\rangle .G_i\}_{i \in I} \rrbracket =$ $c_\mathtt {p}\triangleright \!\big \{ l _i :~ k^{\mathtt {p}}\triangleleft \! l _i; c_\mathtt {p}(u).\widehat{k^{\mathtt {p}}}.\big (c_\mathtt {q}\triangleleft \!\, l _i;k^{\mathtt {q}}\,\triangleright \!\{ l _i : \overline{c_\mathtt {q}}(v).( [u\!\leftrightarrow \!v] \mathord {\;\varvec{|}\;}k^{\mathtt {q}}.{\mathbf {M}}_{k}\llbracket G_i \rrbracket )\}_{\{i\}}\, \big )\big \}_{i \in I}$

The key case is ${\mathbf {M}}_{k}\llbracket \mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l _i\langle U_i\rangle .G_i\}_{i \in I} \rrbracket$. Each action of the multiparty exchange is “echoed” by an action on annotated name k: the selection of label $l _i$ by $\mathtt {p}$ is followed by prefix $k^{\mathtt {p}}\triangleleft \!\, l _i$; the output from $\mathtt {p}$ (captured by the medium by the input $c_\mathtt {p}(u)$) is echoed by prefix $k^{\mathtt {p}}$. This way, the instrumented process ${\mathbf {M}}_{\widetilde{k}}\llbracket G \rrbracket$ induces a fine-grained correspondence with G, exploiting process actions with explicit participant identities.

To state our operational correspondence result, we introduce extended global types and a labeled transition system (LTS) for (extended) global types. The syntax of extended global types is defined as $G \ {:}{:=} \ \mathbf {G} ~ ~{\large \mid }~~ \mathbf {G}_1 \mathord {\;\varvec{|}\;}\mathbf {G}_2$ with

$$\begin{aligned} \mathbf {G} \ {:}{:=} \ \mathtt {end} ~{\large \mid }~\mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l _i\langle U_i\rangle .\mathbf {G}_i\}_{i \in I} ~{\large \mid }~\mathtt {p}\!\leadsto \!\mathtt {q}{:}\, l \langle U\rangle .\mathbf {G} ~{\large \mid }~\mathtt {p}\!\leadsto \!\mathtt {q}{:}\, l (\!(U)\!).\mathbf {G} ~{\large \mid }~\mathtt {p}\!\leadsto \!\mathtt {q}{:}\,(\!(U)\!).\mathbf {G} \end{aligned}$$

We consider parallel composition of sequential global types. We also have three auxiliary forms for global types, denoted with $\leadsto$: they represent intermediate steps. Types $\mathtt {p}\!\leadsto \!\mathtt {q}{:}\, l \langle U\rangle .G$ and $\mathtt {p}\!\leadsto \!\mathtt {q}{:}\, l (\!(U)\!).G$ denote the commitment of $\mathtt {p}$ to output and input along label $l$, resp. Type $\mathtt {p}\!\leadsto \!\mathtt {q}{:}\,(\!(U)\!).G$ represents the state just before the actual input action by $\mathtt {q}$. We need the expected extension of Definition 10 for these types.

Fig. 4.

LTS over finite, extended global types (Excerpt).

We adapt the LTS in [12] to the case of (extended) global types. The set of observables is $\sigma \ {:}{:=} \ \mathtt {p} ~{\large \mid }~\mathtt {p}\triangleleft \! l ~{\large \mid }~ \overline{\mathtt {p}}\, ~{\large \mid }~\overline{\mathtt {p}\triangleleft \! l }$. Below, $psubj(\sigma )$ denotes the participant in $\sigma$. This way, e.g., $psubj( \mathtt {p}\triangleleft \! l ) = \mathtt {p}$. The LTS over global types, noted $G\xrightarrow {\sigma }G'$, is defined by rules including those in Fig. 4. Since Definition 10 annotates prefixes on k with participant identities, their associated actions will be annotated too; given a participant $\mathtt {p}$, we may define the set of annotated visible actions as: $\lambda ^{\mathtt {p}} \ {:}{:=} \ k^{\mathtt {p}}(y) ~{\large \mid }~ k^{\mathtt {p}}\triangleleft \! l ~{\large \mid }~ \overline{ k^{\mathtt {p}}}\,y ~{\large \mid }~\overline{ k^{\mathtt {p}}}(y) ~{\large \mid }~\overline{ k^{\mathtt {p}}\triangleleft \! l }$. We write $k^{\mathtt {p}}$ and $\widehat{k^{\mathtt {p}}}$ to denote actions $k^{\mathtt {p}}(y)$ and $\overline{ k^{\mathtt {p}}}(y)$, resp., whenever object y is unimportant. Also, $psubj(\lambda ^{\mathtt {p}})$ denotes the participant $\mathtt {p}$ which annotates $\lambda$. This way, e.g., $psubj(k^{\mathtt {p}}) = \mathtt {p}$ and $psubj(\overline{ k^{\mathtt {q}}\triangleleft \! l }) = \mathtt {q}$. To relate labels for global types and process labels, given an annotated name k, we define mappings $\{\!\!\{\cdot \}\!\!\}^{k}$ and $|\!|\cdot |\!|$ as follows:

$$\begin{aligned} \begin{array}{c} \{\!\!\{\mathtt {p}\}\!\!\}^{k} = k^{\mathtt {p}} \qquad \{\!\!\{\mathtt {p}\triangleleft \! l \}\!\!\}^{k} = k^{\mathtt {p}}\triangleleft \! l \qquad \{\!\!\{ \overline{\mathtt {p}}\,\}\!\!\}^{k} = \widehat{k^{\mathtt {p}}} \qquad \{\!\!\{\,\overline{\mathtt {p}\triangleleft \! l } \,\}\!\!\}^{k} = \overline{k^{\mathtt {p}}\triangleleft \! l } \\ |\!|k^{\mathtt {p}}|\!| = \mathtt {p} \qquad |\!|k^{\mathtt {p}}\triangleleft \! l |\!| = \mathtt {p}\triangleleft \! l \qquad |\!|\widehat{k^{\mathtt {p}}}|\!| = \overline{\mathtt {p}}\, \qquad |\!|\,\overline{k^{\mathtt {p}}\triangleleft \! l }\,|\!| = \overline{\mathtt {p}\triangleleft \! l } \end{array} \end{aligned}$$

Operational correspondence is stated in terms of the multiparty systems of a global type. Following Definition 8, we say that $\varGamma ; \varDelta , \varDelta ' \vdash {\mathbf {M}}_{\widetilde{k}}\llbracket G \rrbracket \ {:}{:} \ z{:}C$ is an instrumented compositional typing if (i) it is a valid typing derivation; (ii) $\mathsf {npart}(G) \subseteq dom(\varDelta )$; (iii) $C = \mathbf{1 }$; (iv) $dom(\varDelta ') = \widetilde{k}$:

Definition 11

(Systems). Let $G \in \mathcal {G}$ be a WF global type, with $\mathsf {part}(G) = \{\mathtt {p}_1, \ldots , \mathtt {p}_n\}$. Also, let $\varGamma ; \varDelta , \varDelta ' \vdash {\mathbf {M}}_{\widetilde{k}}\llbracket G \rrbracket$ be an instrumented compositional typing, with $\varDelta = c_{\mathtt {p}_1}{:}\langle \!\langle G\!\!\upharpoonright \!{\mathtt {p}_1} \rangle \!\rangle , \ldots , c_{\mathtt {p}_n}{:}\langle \!\langle G\!\!\upharpoonright \!{\mathtt {p}_n} \rangle \!\rangle$, for some $\varGamma$. Let $\widetilde{z} = \mathsf {npart}(G)$. The set of systems of G is defined as:

$$\begin{aligned} \mathcal {S}_{\widetilde{k}}(G) = \big \{({\varvec{\nu }}\widetilde{z})( Q_1 \mathord {\;\varvec{|}\;}\!\! \cdots \!\!\mathord {\;\varvec{|}\;}Q_n \mathord {\;\varvec{|}\;}{\mathbf {M}}_{\widetilde{k}}\llbracket G \rrbracket ) ~ ~{\large \mid }~~ \cdot ; \cdot \vdash Q_{j} \ {:}{:} \ c_{\mathtt {p}_j}{:}\langle \!\langle G\!\!\upharpoonright \!{\mathtt {p}_j} \rangle \!\rangle ,\, j \in 1\ldots n\big \} \end{aligned}$$

Thus, given G, a multiparty system is obtained by composing ${\mathbf {M}}_{\widetilde{k}}\llbracket G \rrbracket$ with well-typed implementations for each of the local projections of G. An $R \in \mathcal {S}_{\widetilde{k}}(G)$ is an implementation of the multiparty protocol G. By construction, its only visible actions are on annotated names: interactions between all the $Q_j$ and ${\mathbf {M}}_{\widetilde{k}}\llbracket G \rrbracket$ will be unobservable.

Theorem 7 below connects global types and systems: it confirms that (instrumented) medium processes faithfully mirror the communicating behavior of extended global types. Below, we write $G \xrightarrow {\,\sigma [\mathtt {p}]\,} G'$ if $G \xrightarrow {\,\sigma \,} G'$ and $psubj(\sigma ) = \mathtt {p}$. Also, we write $P \xrightarrow {\,\lambda [\mathtt {p}]\,} P'$ (resp. $P \mathop {\Longrightarrow }\limits ^{\,\lambda [\mathtt {p}]\,} P'$) if $P \xrightarrow {\,\lambda \,} P'$ (resp. $P \mathop {\Longrightarrow }\limits ^{\,\lambda \,} P'$) holds and $psubj(\lambda ) = \mathtt {p}$.

Theorem 7

(Operational Correspondence). Let G be an extended WF global type and $R \in \mathcal {S}_{\widetilde{k}}(G)$. We have: If $G \xrightarrow {\,\sigma [\mathtt {p}]\,} G'$ then $R \mathop {\Longrightarrow }\limits ^{\,\lambda [\mathtt {p}]\,} R'$, for some $\lambda , R',k \in \widetilde{k}$ such that $\lambda = \{\!\!\{\sigma \}\!\!\}^{k}$ and $R' \in \mathcal {S}_{\widetilde{k}}(G')$. Moreover, if there is some $R_0$ s.t. $R \mathop {\Longrightarrow }\limits ^{} R_0 \xrightarrow {\,\lambda [\mathtt {p}]\,} R'$ then $G \xrightarrow {\,\sigma [\mathtt {p}]\,} G'$, for some $\sigma , G'$ such that $\sigma = |\!|\lambda |\!|$ and $R' \in \mathcal {S}_{\widetilde{k}}(G')$.

4 Example: Sharing in Multiparty Conversations

Here we further illustrate reasoning about global types in $\mathcal {G}$ by exploiting the properties given in Sect. 3. In particular, we illustrate non-trivial forms of replication and sharing.

Let us consider the global type $G_{\text {BS}}$, given in Example 1. The medium processes of $G_{\text {BS}}$, denoted $\mathsf {M}\!\!\llbracket G_{\text {BS}} \rrbracket$, has been detailed in Example 2; we proceed to examine its properties. Relying on Theorems 4 and 5, we have the compositional typing:

$$\begin{aligned} \varGamma ;\, c_1{:} \mathsf {B1}, c_2{:} \mathsf {S}, c_3{:} \mathsf {B2} \vdash \mathsf {M}\!\!\llbracket G_{\text {BS}} \rrbracket \ {:}{:} \ -{:}\mathbf{1 } \end{aligned}$$

(1)

for some $\varGamma$ and with $\mathsf {B1} = \langle \!\langle G_{\text {BS}}\!\!\upharpoonright \!{\mathtt {B_1}} \rangle \!\rangle$, $\mathsf {S} = \langle \!\langle G_{\text {BS}}\!\!\upharpoonright \!{\mathtt {S}} \rangle \!\rangle$, and $\mathsf {B2} = \langle \!\langle G_{\text {BS}}\!\!\upharpoonright \!{\mathtt {B_2}} \rangle \!\rangle$. To implement the protocol, one may simply compose $\mathsf {M}\!\!\llbracket G_{\text {BS}} \rrbracket$ with type compatible processes $\cdot ; \cdot \vdash Buy1 \ {:}{:} \ c_1{:}\mathsf {B1}$,  $\cdot ; \cdot \vdash Sel \ {:}{:} \ c_2{:}\mathsf {S}$, and  $\cdot ; \cdot \vdash Buy2 \ {:}{:} \ c_3{:}\mathsf {B2}$:

$$\begin{aligned} \varGamma ; \cdot \vdash ({\varvec{\nu }}c_1)( Buy1 \!\mathord {\;\varvec{|}\;}\!({\varvec{\nu }}c_2)( Sel \mathord {\;\varvec{|}\;}({\varvec{\nu }}c_3)( Buy2 \!\mathord {\;\varvec{|}\;}\! \mathsf {M}\!\!\llbracket G_{\text {BS}} \rrbracket ))) \end{aligned}$$

(2)

The binary session types in Sect. 2 allows us to infer that the multiparty system defined by (2) adheres to the declared projected types, is deadlock-free, and terminating.

Just as we inherit strong properties for $Buy1$, $Sel$, and $Buy2$ above, we may inherit the same properties for more interesting system configurations. In particular, local implementations which appeal to replication and sharing, admit also precise analyses thanks to the characterizations in Sect. 3. Let us consider a setting in which the processes to be composed with the medium must be invoked from a replicated service (a source of generic process definitions). We may have $\cdot ; \cdot \vdash \, !u_1(w). Buy1 _w \ {:}{:} \ u_1{:}\,!\mathsf {B1}$ and

$$\begin{aligned} \begin{array}{c} \nonumber \cdot ; \cdot \vdash \, !u_2(w). Sel _w \ {:}{:} \ u_2{:}\,!\mathsf {S} \qquad \nonumber \cdot ; \cdot \vdash \, !u_3(w). Buy2 _w \ {:}{:} \ u_3{:}\,!\mathsf {B2} \end{array} \end{aligned}$$

and the following “initiator processes” would spawn a copy of the medium’s requirements, instantiated at appropriate names:

$$\begin{aligned} \begin{array}{c} \nonumber \cdot ; u_1{:}\,!\mathsf {B1} \vdash \overline{u_1}(x).[x\!\leftrightarrow \!c_1] \ {:}{:} \ c_1{:}\mathsf {B1} \qquad \nonumber \cdot ; u_2{:}\,!\mathsf {S} \vdash \overline{u_2}(x).[x\!\leftrightarrow \!c_2] \ {:}{:} \ c_2{:}\mathsf {S} \\ \nonumber \cdot ; u_3{:}\,!\mathsf {B2} \vdash \overline{u_3}(x).[x\!\leftrightarrow \!c_3] \ {:}{:} \ c_3{:}\mathsf {B2} \end{array} \end{aligned}$$

Let us write $RBuy1$, $RBuy2$, and $RSel$ to denote the composition of replicated definitions and initiators above. Intuitively, they represent the “remote” variants of $Buy1$, $Buy2$, and $RSel$, respectively. We may then define the multiparty system:

$$\begin{aligned} \varGamma ; \cdot \vdash ({\varvec{\nu }}c_1)( RBuy1 \!\mathord {\;\varvec{|}\;}\!({\varvec{\nu }}c_2)( RSel \!\mathord {\;\varvec{|}\;}\! ({\varvec{\nu }}c_3)( RBuy2 \!\mathord {\;\varvec{|}\;}\! \mathsf {M}\!\!\llbracket G_{\text {BS}} \rrbracket ))) \end{aligned}$$

which, with a concise specification, improves (2) with concurrent invocation/instantiation of replicated service definitions. As (2), the revised composition above is correct, deadlock-free, and terminating.

Rather than appealing to initiators, a scheme in which the medium invokes and instantiates services directly is also expressible in our framework, in a type consistent way. Using (1), and assuming $\varGamma = u_1{:}\mathsf {B1}, u_2{:}\mathsf {S}, u_3{:}\mathsf {B2}$, we may derive:

$$\begin{aligned} \!\!\!\!\!\!\! \varGamma ; \cdot \vdash \overline{u_1}(c_1).\overline{u_2}(c_2).\overline{u_3}(c_3).\mathsf {M}\!\!\llbracket G_{\text {BS}} \rrbracket \end{aligned}$$

(3)

Hence, prior to engaging in the mediation behavior for $G_{\text {BS}}$, the medium first spawns a copy of the required services. We may relate the guarded process in (3) with the multicast session request construct in multiparty session processes [14]. Observe that (3) cleanly distinguishes between session initiation and actual communication behavior: the distinction is given at the level of processes (cf. output prefixes on $u_1, u_2$, and $u_3$) but also at the level of typed interfaces.

The service invocation (3) may be regarded as “eager”: all required services must be sequentially invoked prior to executing the protocol. We may also obtain, in a type-consistent manner, a medium process implementing a “lazy” invocation strategy that spawns services only when necessary. For the sake of example, consider process

$$\begin{aligned} Eager_{\text {BS}} \triangleq \overline{u_3}(c_3).\mathsf {M}\!\!\llbracket G_{\text {BS}} \rrbracket \end{aligned}$$

in which only the invocation on $u_3$ is blocking the protocol, with “open” dependencies on $c_1, c_2$. That is, we have $\varGamma ; c_1{:} \mathsf {B1}, c_2{:} \mathsf {S} \vdash Eager_{\text {BS}} \ {:}{:} \ z{:}\mathbf{1 }$. It could be desirable to postpone the invocation on $u_3$ as much as possible. By combining the commutations on process prefixes realized by $\simeq _{c}$  [19] and Theorem 2, we may obtain:

$$\begin{aligned} \varGamma ; c_1{:} \mathsf {B1}, c_2{:} \mathsf {S} \vdash Eager_{\text {BS}} \approx Lazy_{\text {BS}} \ {:}{:} \ -{:}\mathbf{1 } \end{aligned}$$

where $Lazy_{\text {BS}}$ is obtained from $Eager_{\text {BS}}$ by “pushing inside” prefix $\overline{u_3}(c_3)$.

5 Multiparty Session Types with Behavioral Genericity

To illustrate the modularity of our approach, we conservatively extend, for the first time, multiparty session types with parametric polymorphism, developed for binary sessions in [4, 22]. Although expressed by second-order quantifiers on (session) types—in the style of the polymorphic $\lambda$-calculus—parametric polymorphism in our setting means behavioural genericity in multiparty conversations (i.e., passing first-class behavioral interfaces in messages), not just datatype genericity. In this section we describe how to extend the approach and results in Sect. 3 to polymorphic, multiparty session types.

In [4] we have extended the framework of [5] with impredicative universal and existential quantification over session types, denoted with $\forall X.A$ and $\exists X. A$, respectively. These two types are interpreted as the input and output of a session type, respectively. More precisely, $\forall X.A$ is the type of a process that inputs some session type S (which we may as a kind of interface passing) and then behaves as prescribed by . $\exists X.A$ is the type of a process that sends some session type S and then behaves as prescribed by . From the point of view of the receiver of such S, the protocol S is in a sense opaque; therefore, after inputting S the receiver behaves parametrically (in the sense of behavioral polymorphism) for any such S. In any case, any usage of S by the sender will necessarily be matched by some appropriate parties in the system. A relevant example of the phenomenon can be recovered from [4]. Consider the type

$$\begin{aligned} \mathsf {CloudServer}:\forall X. (\mathsf {api} \mathord {\multimap }X) \mathord {\multimap }X \end{aligned}$$

A session with this type will first input some session type X, say $\mathsf {GMail}$, and then will input a session with type $\mathsf {api} \mathord {\multimap }\mathsf {GMail}$ (that may be realized by a piece of code that will first receive a channel implementing the $\mathsf {api}$ behavior and will after—building on it—behave as specified by $\mathsf {GMail}$) and then offers the behavior $\mathsf {GMail}$. A system implementing the $\mathsf {CloudServer}$ type must somehow provide the $\mathsf {api}$ service internally and pass it to the channel of type $\mathsf {api} \mathord {\multimap }\mathsf {GMail}$ (e.g., representing a piece of mobile code). Notice that after that the $\mathsf {GMail}$ service may be produced by copy-cating the resulting behavior to the cloud server client. The crucial point here is that the cloud server behaves uniformly for whatever session type X is requested for it to execute; its role in this case is to provide the suitable $\mathsf {api}$. Of course, at runtime, all interactions at X will take place as prescribed by the concrete session type involved (in this example, $\mathsf {GMail}$), which may be an arbitrarily complex (behaviorally generic) session type.

5.1 Binary Session Types with Parametric Polymorphism

We now recall key definitions from [4]. The process model in Sect. 2 is extended with processes $\overline{x}\,A.P$ (output type A, proceed as P) and x(X).P (receive a type A, proceed as ) and the reduction rule: , where is the substitution of type variable X with session type A. Thus, our process syntax allows terms such as, e.g., $\overline{x}\,{A}.Q \mathord {\;\varvec{|}\;}x(X). \overline{y}\,{X}.P$, where A is a session typed protocol.

We extend binary types (cf. Definition 1) with existential and universal quantification:

Besides $\varDelta$ and $\varGamma$, the polymorphic type system uses environment $\varOmega$ to record type variables. We have two judgments. Judgment $\varOmega \vdash A\;\mathsf {type}$ denotes that A is a well-formed type with free variables registered in $\varOmega$ (see [4] for well-formedness rules). Also, judgement $\varOmega ; \varGamma ; \varDelta \vdash P \ {:}{:} \ x {:} A$ states that P implements a session of type A along channel x, provided it is composed with processes providing sessions linearly in $\varDelta$ and persistently in $\varGamma$, such that the types occurring in $\varOmega$ are well-formed.

The required typing rules result by adding $\varOmega$ in Fig. 2 and by considering rules in Fig. 5, which explain how to provide and use sessions of a polymorphic type. Rule (T${{\forall }\mathsf {R}}$) types the offering of a session of universal type $\forall X. A$ by inputing an arbitrary type, bound to X, and proceeding as A, which may bind the type variable X, regardless of what the received type is. Rule (T${{\forall }\mathsf {L}}$) says that the use of type $\forall X . A$ consists of the output of a type B (well-formed under $\varOmega$) which then warrants the use of the session as . The existential type is dual: providing an existentially typed session $\exists X . A$ is accomplished by outputting a type B and then providing a session of type (Rule (T${{\exists }\mathsf {R}}$)). Using an existential session $\exists X . A$ implies inputing a type and then using the session as A, regardless of the received session type (Rule (T${{\exists }\mathsf {L}}$)).

Fig. 5.

Typing rules for polymorphic, binary session types.

Well-typed polymorphic processes satisfy Theorem 1 and relational parametricity [4], a reasoning principle stated next. We require some notation, fully detailed in [4]: $\omega {:}\varOmega$ denotes a type substitution that assigns a closed type to variables in $\varOmega$. Notation $\widehat{\omega }(P)$ denotes the application of $\omega$ to type variables in P. Also, $\eta {:}\omega _1\Leftrightarrow \omega _2$ is an equivalence candidate assignment (a typed relation on processes) between $\omega _1$ and $\omega _2$. Moreover, $\approx _\mathtt {L}$ denotes a logical equivalence relation that coincides with barbed congruence.

Theorem 8

(Relational Parametricity [4]). If $\varOmega ; \varGamma ; \varDelta \vdash P \ {:}{:} \ z {:} A$ then, for all $\omega _1{:}\varOmega$, $\omega _2{:}\varOmega$, and $\eta {:}\omega _1\Leftrightarrow \omega _2$: $\varGamma ; \varDelta \vdash \widehat{\omega _1}(P) \approx _\mathtt {L} \widehat{\omega _2}(P) \ {:}{:} \ z {:} A[\eta {:}\omega _1\Leftrightarrow \omega _2]$.

Theorem 8 entails behavioral genericity, a form of representation independence: it says that process P behaves the same independently from instantiations of its free type variables.

5.2 Multiparty Session Types with Polymorphism

We extend global types in $\mathcal {G}$ (Definition 2) with variables $X, X', \ldots$ and with a construct $\mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l [X].G'\}$, which introduces parametric polymorphism (X is meant to occur in $G'$). To our knowledge, this is the first theory of its kind:

Definition 12

(Polymorphic Session Types). Define global types and local types as

$$\begin{aligned} \begin{array}{rcl} G &{}{:}{:=} &{} \mathtt {end} ~{\large \mid }~G_1 \mathord {\;\varvec{|}\;}G_2 ~{\large \mid }~\mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l _i\langle U_i\rangle .G_i\}_{i \in I} ~{\large \mid }~\mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l [X].G\} ~{\large \mid }~X \\[1mm] U &{} {:}{:=} &{} \mathsf {bool} ~{\large \mid }~\mathsf {nat} ~{\large \mid }~\mathsf {str} ~{\large \mid }~\ldots ~{\large \mid }~T ~{\large \mid }~(T)^{\dagger } \\[1mm] T &{} {:}{:=} &{} \mathsf {end} ~{\large \mid }~\mathtt {p}?\{ l _i\langle U_i\rangle .T_i\}_{i \in I} ~{\large \mid }~\mathtt {p}!\{ l _i\langle U_i\rangle .T_i\}_{i \in I} ~{\large \mid }~\mathtt {p}!\{l[X]. T\} ~{\large \mid }~\mathtt {p}?\{l[X].T\} ~{\large \mid }~X \end{array} \end{aligned}$$

Above $(\cdot )^{\dagger }$ denotes a function on local types that discards participant identities. E.g., $(\mathtt {p}?\{l[X].T\} )^{\dagger } = ?\{l[X].(T)^{\dagger }\}$ and $(\mathtt {p}?\{ l _i\langle U_i\rangle .T_i\}_{i \in I} )^{\dagger } = ?\{ l _i\langle U_i\rangle .(T_i)^{\dagger }\}_{i \in I}$.

We write $\mathcal {G}^{\forall \exists }$ to denote the above global types. The global type $\mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l [X].G\}$ signals that $\mathtt {p}$ sends to $\mathtt {q}$ an arbitrary local type (protocol), thus specifying $\mathtt {q}$ as a generic partner. Also, G is a generic global specification: its behavior will be depend on the type sent by $\mathtt {p}$ to $\mathtt {q}$, which should be explicit in $\mathtt {p}$’s implementation. This new global type is related to local types $\mathtt {p}!\{l[X]. T\}$ and $\mathtt {p}?\{l[X].T\}$, which are to be understood as existential and universal quantification on local types, respectively—see below. The global type X should be intuitively understood as a behavior that remains “globally abstract”, in the sense that it is determined by a concrete local type exchanged between two participants, namely, as a result of a (previous) communication of the form $\mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l [X].G\}$. As a result, the (global) communication behavior associated to local type exchanged between $\mathtt {p}$ and $\mathtt {q}$ should remain abstract (opaque) to other participants of the protocol.

The projection of $G \in \mathcal {G}^{\forall \exists }$ onto participant $\mathtt {r}$, denoted $G\!\!\upharpoonright \!{\mathtt {r}}$, extends Definition 4 by adding $X\!\!\upharpoonright \!{\mathtt {r}} = X$ and by letting:

$$\begin{aligned} (\mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l [X].G\})\!\!\upharpoonright \!{\mathtt {r}} = {\left\{ \begin{array}{ll} \mathtt {p}!\{l[X]. (G\!\!\upharpoonright \!{\mathtt {r}})\} &{} \text {if } \mathtt {r} = \mathtt {p} \\ \mathtt {p}?\{l[X]. (G\!\!\upharpoonright \!{\mathtt {r}})\} &{} \text {if } \mathtt {r} = \mathtt {q} \\ G\!\!\upharpoonright \!{\mathtt {r}} &{} \text {otherwise} \end{array}\right. } \end{aligned}$$

Well-formedness of global types in $\mathcal {G}^{\forall \exists }$ is based on projectability but also on consistent uses of type variables: a participant can only communicate the types it knows. (This condition is similar to history-sensitivity, as in [1].) This way, e.g., an ill-formed type is $\mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{l_1[X]. \mathtt {r}\!\twoheadrightarrow \!\mathtt {s}{:}\{ l _2\langle ?\{l\langle \mathsf {int}\rangle .X\}\rangle .\mathtt {end} \}\}$, since $\mathtt {r}$, $\mathtt {s}$ do not know the type sent by $\mathtt {p}$.

5.3 Mediums for Multiparty Session Types with Polymorphism

Mediums for global types in $\mathcal {G}^{\forall \exists }$ are defined by extending Definition 7 as follows:

$$\begin{aligned} \mathsf {M}\!\!\llbracket \mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\{ l [X].G\} \rrbracket = c_\mathtt {p}\triangleright \!\big \{ l : c_\mathtt {p}(X).c_\mathtt {q}\triangleleft \! l ; \overline{c_\mathtt {q}}\,{X}.\mathsf {M}\!\!\llbracket G \rrbracket \big \}_{} \qquad \qquad \mathsf {M}\!\!\llbracket X \rrbracket = {\varvec{0}} \end{aligned}$$

Observe that type variable X should not generate a mediator behavior, as we want to remain generic. The relation between local types and binary types extends Definition 9 with:

and by letting $\langle \!\langle X \rangle \!\rangle = X$ and $\langle \!\langle (T)^{\dagger } \rangle \!\rangle = \langle \!\langle T \rangle \!\rangle$. The characterization results in Sect. 3.1 hold also for global types in $\mathcal {G}^{\forall \exists }$.

6 Mediums at Work: A Behaviorally Generic Multiparty Protocol

We illustrate our approach and results via a simple example. Consider the global type $G_{\text {p}}$, inspired by the CloudServer from [4] already hinted to above. It features behavioral genericity (as enabled by parametric polymorphism); below, $\mathsf {str}$, $\mathsf {bool}$, denote basic data types, and $\mathsf {api}$ is a session type describing the cloud infrastructure API.

$$\begin{aligned} G_{\text {p}} = \mathtt {p}\!\twoheadrightarrow \!\mathtt {q}{:}\big \{ l_1 \langle \mathsf {bool}\rangle . \mathtt {q}\!\twoheadrightarrow \!\mathtt {r}{:}\{ l [X]. \mathtt {q}\!\twoheadrightarrow \!\mathtt {r}{:}\{ l_2 \big \langle ?\{l_3\langle \mathsf {api}\rangle .X\} \big \rangle .X\}\} \big \}_{} \end{aligned}$$

We have participants $\mathtt {p}$, $\mathtt {q}$, and $\mathtt {r}$. The intent is that $\mathtt {r}$ is a behaviorally generic participant, that provides a behavior of type $\mathsf {api}$ required by $\mathtt {q}$. Crucially, $\mathtt {r}$ may interact with $\mathtt {q}$ independently of the local type sent by $\mathtt {q}$. Such a local type is explicit in $\mathtt {q}$’s implementation (see below), rather than in the global type $G_{\text {p}}$.

In $G_{\text {p}}$, participant $\mathtt {p}$ first sends a boolean value to $\mathtt {q}$; then, $\mathtt {q}$ sends an unspecified protocol to $\mathtt {r}$, say M, which is to be used subsequently in an exchange from $\mathtt {q}$ to $\mathtt {r}$. Notice that M occurs in the value that $\mathtt {r}$ receives from $\mathtt {q}$ and influences the behavior after that exchange. Indeed, the value $?\{l_3\langle \mathsf {api}\rangle .X\}$ denotes an unspecified session type that relies on the reception of a session of type $\mathsf {api}$. The local projections for $G_{\text {p}}$ are $G_{\text {p}}\!\!\upharpoonright \!{\mathtt {p}} = \mathtt {p}!\{ l_1\langle \mathsf {bool} \rangle . \mathsf {end} \}$ and

$$\begin{aligned} G_{\text {p}}\!\!\upharpoonright \!{\mathtt {q}}= & {} \mathtt {p}?\big \{ l_1\langle \mathsf {bool} \rangle .\mathtt {q}!\{ l [X]. \mathtt {q}!\{l_2\langle ?\{l_3\langle \mathsf {api}\rangle .X\} \rangle . X \}\}\big \} \\ G_{\text {p}}\!\!\upharpoonright \!{\mathtt {r}}= & {} \mathtt {q}?\big \{ l [X]. \mathtt {q}?\{l_2\langle ?\{l_3\langle \mathsf {api}\rangle .X\} \rangle . X \}\big \} \end{aligned}$$

Above, the occurrences of X at the end of both $G_{\text {p}}\!\!\upharpoonright \!{\mathtt {q}}$ and $G_{\text {p}}\!\!\upharpoonright \!{\mathtt {r}}$ may appear surprising, as they should represent dual behaviors. Notice that in each case, X should be interpreted according to the local type that “bounds” X (i.e., the output $\mathtt {q}!\{ l [X] \ldots \}$ in $G_{\text {p}}\!\!\upharpoonright \!{\mathtt {q}}$ and the input $\mathtt {q}?\{ l [X] \ldots \}$ in $G_{\text {p}}\!\!\upharpoonright \!{\mathtt {r}}$). This dual perspective should become evident when looking at the binary session types associated to these projections. First, notice that we have that . Writing $(\mathsf {api} \mathord {\multimap }X)$ to stand for ), we have the binary session types $\langle \!\langle G_{\text {p}}\!\!\upharpoonright \!{\mathtt {p}} \rangle \!\rangle = \oplus \!\{ l_1: \mathbf{1 } \otimes \mathbf{1 } \}_{}$ and

The medium process for $G_{\text {p}}$ is then:

$$\begin{aligned} \begin{array}{rcl} \mathsf {M}\!\!\llbracket G_{\text {p}} \rrbracket &{} = &{} c_{\mathtt {p}}\triangleright \!\big \{ l _{1} : c_{\mathtt {p}}(u).c_{\mathtt {q}}\triangleleft \! l _{1};\overline{c_{\mathtt {q}}}(v).\big ( [u\!\leftrightarrow \!v] \mathord {\;\varvec{|}\;}\\ &{} &{} \qquad \qquad \quad c_{\mathtt {q}}\triangleright \!\{ l : c_{\mathtt {q}}(X).c_{\mathtt {r}}\triangleleft \! l ; \overline{c_{\mathtt {r}}}\,{X}. \\ &{} &{} \qquad \qquad \qquad \qquad \qquad c_{\mathtt {q}}\triangleright \!\{ l _{2} : c_{\mathtt {q}}(u).c_{\mathtt {r}}\triangleleft \! l _{2};\overline{c_{\mathtt {r}}}(v).( [u\!\leftrightarrow \!v] \mathord {\;\varvec{|}\;}{\varvec{0}} )\}_{} \}_{}\big )\big \}_{} \end{array} \end{aligned}$$

Using our extended characterization results, we may show that $\mathsf {M}\!\!\llbracket G_{\text {p}} \rrbracket$ can safely interact with implementations for $\mathtt {p}$, $\mathtt {q}$, and $\mathtt {r}$ whose types correspond to the projections of $G_{\text {p}}$ onto $\mathtt {p}$, $\mathtt {q}$, and $\mathtt {r}$. Indeed, $\mathsf {M}\!\!\llbracket G_{\text {p}} \rrbracket$ can safely interact with any P, ${Q}_i$, and R such that $\varOmega ; \varGamma ; \varDelta _1 \vdash \!{P} \ {:}{:} \ c_\mathtt {p}{:} \langle \!\langle G_{\text {p}}\!\!\upharpoonright \!{\mathtt {p}} \rangle \!\rangle$ and

$$\begin{aligned} \begin{array}{c} \varOmega ; \varGamma ; \varDelta _3 \vdash \! {R} \ {:}{:} \ c_\mathtt {r}{:} \langle \!\langle G_{\text {p}}\!\!\upharpoonright \!{\mathtt {r}} \rangle \!\rangle \qquad \varOmega ; \varGamma ; \varDelta _2 \vdash \!{Q}_i \ {:}{:} \ c_\mathtt {q}{:} \langle \!\langle G_{\text {p}}\!\!\upharpoonright \!{\mathtt {q}} \rangle \!\rangle \end{array} \end{aligned}$$

Process $({\varvec{\nu }}{c_\mathtt {p},c_\mathtt {q},c_\mathtt {r}})(\mathsf {M}\!\!\llbracket G_{\text {p}} \rrbracket \mathord {\;\varvec{|}\;}{P} \mathord {\;\varvec{|}\;}{R} \mathord {\;\varvec{|}\;}{Q}_i)$ is a system for $G_{\text {p}}$ (cf. Definition 11). It is well-typed; we have $\varOmega ; \varGamma ; \varDelta _{1}, \varDelta _{2}, \varDelta _{3} \vdash ({\varvec{\nu }}{c_{\mathtt {p}},c_{\mathtt {q}},c_{\mathtt {r}}})(\mathsf {M}\!\!\llbracket G_{\text {p}} \rrbracket \mathord {\;\varvec{|}\;}{P} \mathord {\;\varvec{|}\;}{R} \mathord {\;\varvec{|}\;}{Q}_{i}) \ {:}{:} \ -:{\varvec{1}}$. Process $c_\mathtt {p}\triangleleft \!\, l _1; \overline{c_\mathtt {p}}(f).(B_f \mathord {\;\varvec{|}\;}{\varvec{0}})$ is a concrete implementation for P, where name f stands for a boolean implemented by $B_f$. As for R and ${Q}_i$, we may have:

$$\begin{aligned} {R}= & {} c_\mathtt {r}\triangleright \!\{ l :c_\mathtt {r}(Y).c_\mathtt {r}\triangleright \!\{ l _2 :c_\mathtt {r}(y).\overline{y}(a).(A_a \mathord {\;\varvec{|}\;}[c_\mathtt {r}\!\leftrightarrow \!a])\}_{}\}_{} \\ {Q}_1= & {} c_\mathtt {q}\triangleright \!\{ l _1 :c_\mathtt {q}(b).c_\mathtt {q}\triangleleft \! l ; \overline{c_\mathtt {q}}\,{S}.c_\mathtt {q}\triangleleft \! l _2;\overline{c_\mathtt {q}}(w).(w(a).\mathtt {SMTP}_{w,a}^{b} \mathord {\;\varvec{|}\;}[m\!\leftrightarrow \!c_{\mathtt {q}}])\}_{} \end{aligned}$$

Crucially, following the type $\langle \!\langle G_{\text {p}}\!\!\upharpoonright \!{\mathtt {r}} \rangle \!\rangle$, process R is behaviorally generic: independently of the type received from ${Q}_i$ via the medium $\mathsf {M}\!\!\llbracket G_{\text {p}} \rrbracket$ (cf. the type input prefix $c_\mathtt {r}(Y)$), R enables process $A_a$ to provide the API along name a. Process $Q_1$ is just one possible implementation for $\mathtt {q}$: it provides an implementation of a service $\mathtt {SMTP}_{w,a}^{b}$ that relies on behavior $\mathsf {api}$ along name a and a boolean along b to implement protocol S along w. A different implementation for $\mathtt {q}$ is process ${Q}_2$ below, which concerns session protocol I:

$$\begin{aligned} {Q}_2 = c_\mathtt {q}\triangleright \!\{ l _1 :c_\mathtt {q}(b).c_\mathtt {q}\triangleleft \! l ; \overline{c_\mathtt {q}}\,{I}.c_\mathtt {q}\triangleleft \! l _2;\overline{c_\mathtt {q}}(w).(w(a).\mathtt {IMAP}_{w,a}^{b} \mathord {\;\varvec{|}\;}[m\!\leftrightarrow \!c_{\mathtt {q}}])\}_{} \end{aligned}$$

where $\mathtt {IMAP}_{w,a}^{b}$ uses $\mathsf {api}$ along a and boolean b to implement protocol I along w. Note that R and any ${Q}_i$ have limited interactions with $\mathsf {M}\!\!\llbracket G_{\text {p}} \rrbracket$: to respect the genericity stipulated by $G_{\text {p}}$, the polymorphic process $\mathsf {M}\!\!\llbracket G_{\text {p}} \rrbracket$ only mediates the exchange of the local type (S or I) and plugs the necessary connections; other exchanges are direct between R and ${Q}_1$ or ${Q}_2$, and known to comply with the (dynamically passed protocol) specified by the session type S or I.

Both $({\varvec{\nu }}{c_\mathtt {p},c_\mathtt {q},c_\mathtt {r}})(\mathsf {M}\!\!\llbracket G_{\text {p}} \rrbracket \mathord {\;\varvec{|}\;}{P} \mathord {\;\varvec{|}\;}{R} \mathord {\;\varvec{|}\;}{Q}_1)$ and $({\varvec{\nu }}{c_\mathtt {p},c_\mathtt {q},c_\mathtt {r}})(\mathsf {M}\!\!\llbracket G_{\text {p}} \rrbracket \mathord {\;\varvec{|}\;}{P} \mathord {\;\varvec{|}\;}{R} \mathord {\;\varvec{|}\;}{Q}_2)$ are well-typed systems; hence, they satisfy fidelity and deadlock-freedom (Theorem 1). Using properties of well-typed processes together with relational parametricity (Theorem 8), we may further show that they are observationally equivalent, provided a typed relation between session types S and I. That is, Theorem 8 allows us to state the behavioral independence of the sub-system formed by $\mathsf {M}\!\!\llbracket G_{\text {p}} \rrbracket$, P, and R with respect to any implementation $Q_i$ for participant $\mathtt {q}$.

7 Concluding Remarks and Related Works

We developed the first analysis of multiparty protocols using binary session types. Our medium processes capture the semantics of multiparty session types and connect global types to well-typed implementations; this allows us to exploit properties for typed processes to reason about multiparty systems. Since mediums have a uniform definition, we may analyze global types with features such as delegation, which go beyond the scope of recent automata-based analyses of global types [12, 16]. Our work thus complements such recent works. Our approach naturally supports the analysis of multiparty session types with behavioral genericity. This model, the first of its kind, is very powerful; it reuses techniques from binary sessions [4], notably relational parametricity. These features suggest that extensions of known multiparty sessions with behavioral genericity would be hard to obtain without following linear logic foundations, as done here.

Given a global type, our characterization results relate its medium and its local projections; these relations allow us to transfer properties of [5] (e.g., deadlock-freedom) to multiparty protocols. Our results stress the fundamental character of key notions in multiparty sessions (e.g., projections), and build on connections between two distinct session type theories based on linear logic [5] and on automata [12]. Our developments do not depend on the interpretation of session types in [5] being intuitionistic; clearly, its reasoning techniques (e.g., behavioral equivalences [19]) are important in our results. Our approach should extend also to interpretations based on classical linear logic [22].

Related Work. One challenge in decomposing a multiparty session type is preserving its sequencing information. The work [9] shows how to decompose a global type into simpler, independent pieces: global types use an additional $\mathtt {calls}$ construct to invoke these pieces in the appropriate order, but connections with binary sessions are not established. Correspondence assertions [2] track data dependencies and detect unintended operations; they may allow to relate independent binary sessions. Using standard binary/multiparty session types, we capture sequencing information using a process extracted from a global type. Our approach relies on deadlock-freedom (not available in [2]) and offers a principled way of transferring it to multiparty systems.

To our knowledge, ours is the first formal characterization of multiparty session types using binary session types. Previous works have, e.g., compared different multiparty session types but without connecting to binary types [11]. The work [18] (extended version) identifies a class of multiparty systems for which deadlock-freedom analysis can be reduced to the analysis of linear $\pi$-calculus processes. This reduction, however, does not connect with binary session types, nor exploits other properties of processes to analyze global types. The work [7] relates global types and a variant of classical linear logic; as in our work, a challenge in [7] is capturing sequencing information in global types. While [7] captures sequencing information in global types via role annotations in propositions/types (using an extra proof system, called coherence), our medium-based approach enables process reasoning on global types, uses standard linear logic propositions, and allows for conservative extensions with powerful reasoning techniques, notably behavioral genericity as enabled by parametric polymorphism.

Medium processes are loosely related to the concept of orchestrators in service-oriented computing. The work [17] shows how to synthesize an orchestrator from a service choreography, using finite state machines. In contrast, we consider choreographies given as behavioral types; mediums are obtained directly from those types.