1

# Hybrid Multiparty Session Types - Full Version

Compositionality for Protocol Specification through Endpoint Projection

Lorenzo Gheri  0000-0002-3191-7722 University of OxfordUnited Kingdom
<EMAIL_ADDRESS>and  Nobuko Yoshida  0000-0002-3925-8557 University
of OxfordUnited Kingdom<EMAIL_ADDRESS>
###### Abstract.

Multiparty session types (MPST) are a specification and verification framework
for distributed message-passing systems. The communication protocol of the
system is specified as a _global type_ , from which a collection of _local
types_ (local process implementations) is obtained by _endpoint projection_. A
global type is a single disciplining entity for the whole system, specified by
_one designer_ that has full knowledge of the communication protocol. On the
other hand, distributed systems are often described in terms of their
_components_ : a different designer is in charge of providing a subprotocol
for each component. The problem of modular specification of global protocols
has been addressed in the literature, but the state of the art focuses only on
dual input/output compatibility. Our work overcomes this limitation. We
propose the first MPST theory of _multiparty compositionality for distributed
protocol specification_ that is semantics-preserving, allows the composition
of two or more components, and retains full MPST expressiveness. We introduce
_hybrid types_ for describing subprotocols interacting with each other, define
a novel _compatibility relation_ , explicitly describe an algorithm for
composing multiple subprotocols into a _well-formed global type_ , and prove
that compositionality preserves projection, thus retaining semantic
guarantees, such as liveness and deadlock freedom. Finally, we test our work
against real-world case studies and we smoothly extend our novel compatibility
to MPST with delegation and explicit connections.

multiparty session types, compositionality, protocol design, concurrency

††journal: PACMPL††journalvolume: 1††journalnumber: CONF††article:
1††journalyear: 2018††publicationmonth: 1††copyright: none††ccs: Theory of
computation Distributed computing models††ccs: Theory of computation Type
theory

##  1\. Introduction

With the current growth in scale and complexity of systems, their _design_ has
become of central importance for industry and society in general.
Choreographies for interactions among multiple participants, or
_(communication) protocols_ , arise naturally in numerous fields:
authorisation standards (Hardt, 2012; MIT, 2022), the BPMN graphical
specification for business processes (OMG, 2022), or smart contracts for
financial transactions (Ethereum, 2022).

The literature on programming languages offers a variety of formal frameworks
for protocol description (Honda et al., 2016; Barbanera et al., 2020a;
Montesi, 2013), aimed at the verification of behavioural properties of
distributed implementations that comply with the communication discipline
prescribed by the protocol. Such theories focus on distributed implementations
of participants, but rarely feature modularity in the design of protocols,
which are instead seen as standalone, monolithic entities. Mostly, when
modularity is considered, it is either conceived in terms of nesting
(Demangeon and Honda, 2012; Tabareau et al., 2014) or it substantially
modifies protocol description, by adding additional structure (Carbone et al.,
2018; Savanovic et al., 2020; Montesi and Yoshida, 2013). To the best of our
knowledge, only in (Barbanera et al., 2021) and (Stolze et al., 2021) the
result of composition is a well-formed protocol.

_This paper presents hybrid multiparty session types: a novel, general theory
that offers compositionality for distributed protocol specification, improves
on the state of the art, and is immediately compatible with existing
multiparty session types systems._

Multiparty session types (MPST) (Honda et al., 2016; Coppo et al., 2015;
Yoshida and Gheri, 2020) provide a typing discipline for message-passing
concurrency, ensuring deadlock freedom for two or more distributed processes.
A _global type_ or _protocol_ , which describes an entire interaction
scenario, is projected into a collection of _local types_ onto the respective
participants (endpoint projection). MPST cater for the safe implementation of
distributed processes: as long as the process for each participant is
independently type-checked against its local type, its communication behaviour
is disciplined by the semantics of the global type, and its execution does not
get stuck.

Although alternatives to the top-down approach (endpoint projection from a
global type) have been proposed (Scalas and Yoshida, 2019; Deniélou and
Yoshida, 2013; Lange et al., 2015; Lange and Yoshida, 2019), the benefits of
an explicit, concise design of the communication protocol for the whole system
have been recognised by the research community, since the first appearance of
MPST (Honda et al., 2008), until more recent times, e.g., see (Glabbeek et
al., 2021; Cledou et al., 2022). Furthermore, the top-down approach has been
extended, e.g., to fault tolerance (Viering et al., 2021), timed specification
(Bocchi et al., 2014), refinements (Zhou et al., 2020; Gheri et al., 2022),
cost awareness (Castro-Perez and Yoshida, 2020), exception handling
(Lagaillardie et al., 2022), or explicit connections and delegation (Hu and
Yoshida, 2017; Castellani et al., 2020).

Concretely, the underlying assumption to top-down MPST systems is that a
single designer has _full knowledge_ of the communication protocol and can
give its formal specification in terms of a global type. Distributed systems,
however, are designed modularly, by multiple designers. Recently, the
literature has addressed the problem of obtaining a single coherent global
type from independently specified subprotocols (components of a protocol) and
some solutions have been offered: Barbanera et al. (2021) achieve direct
composition of _two_ global types, through a dual compatibility relation that
matches inputs and outputs, based on gateways (Barbanera et al., 2018, 2019,
2020b). Stolze et al. (2021) describe a dual methodology beyond gateways, but
severely restrict the syntax for global types. In contrast to this approach,
our theory substitutes dual compatibility, based only on input/output
matching, with the notion of _compatibility through projection_. Thus, we
improve on the state of the art:  (1) we can compose more than two
subprotocols into a well-formed global type and  (2) we retain the full
expressiveness of MPST (including recursion and parallel composition).  See §6
for a broader, in-detail discussion. Moreover, metathoretical results about
the semantics of traditional MPST systems (Deniélou and Yoshida, 2013; Honda
et al., 2016) immediately translate to ours (_semantics preservation_): from
distributed specifications in terms of subprotocols, our theory synthesises a
global protocol for the whole system; we prove once and for all, as a
metatheoretical result, that such global protocol is a traditionally well-
formed global type.

_Contributions._ This paper develops _a theory of compositionality for
distributed protocol description in MPST systems_ and introduces the following
novel MPST concepts:

  * •

_hybrid types_ , a generalisation of both global and local types, for the
specification of communicating subprotocols (Definition 3.3);

  * •

_generalised projection_ onto sets of roles (Definition 3.6), which well-
behaves with respect to set inclusion (Theorem 4.9);

  * •

_localiser_ (Definition 3.8), a novel operator that isolates, in a
subprotocol, the inter-component communication from the intra-component one;

  * •

_compatibility_ based on projection and localiser (Equation C, §4.1);

  * •

_build-back_ , an explicit algorithm to compose _two or more_ subprotocols
into a more general one (Definitions 4.1 and 4.6 and Theorems 4.4 and 4.7).

To the best of our knowledge, our approach is the first that:

  * •

enables the correct composition of _two or more_ subprotocols into a global
type, while capturing _full MPST expressiveness_ : branching, parallel
composition, and recursion (Corollary 4.10);

  * •

operates at a purely syntactic level, thus retaining previously developed MPST
semantics results (_semantics preservation_); correctness is guaranteed by
compositionality resulting in a traditionally well-formed global type and
preserving endpoint projection (Corollary 4.10);

  * •

provides a notion of compatibility that is _more expressive than dual
input/output matching_ and hence suitable for extension to more sophisticated
MPST systems (Example 5.7).

We discuss the applicability and generality of our work, through _case
studies_.  (1) We give a distributed specification of the real-world protocol
OAuth 2.0 (Hardt, 2012), which showcases modularity features of our theory
(§5.2) and leads to an optimisation (§5.3, Corollary 5.1).  (2) We extend our
theory beyond traditional MPST, to delegation and explicit connections (§5.4).

_Outline._ §2 gives an overview of our development, with a simple, but
realistic, application scenario. §3 and §4 are dedicated to our technical
contributions. §5 tests the strengths of our theory with case studies. §6
discusses in detail, with examples, related work. §8 concludes with future
work. Further detail for definitions and proofs can be found in Appendix B.

##  2\. Overview of Our Development

This work achieves _distributed protocol specification_ for MPST: different
_(protocol) designers_ specify protocols (naively as global types, Figure 1)
for different components of the communicating system; then, these compose into
a single global type for the whole system. Composition must _preserve
(endpoint) projection_ (indicated with $\upharpoonright$): local types, for
the distributed implementation of _roles_ (or _participants_), need to be
obtained by projection of each separate component, but, also, they need to be
projections of the same global type (obtained by composition), if we want
semantic guarantees (e.g., deadlock freedom) to hold. In other words, our
protocol-compositionality theory relies on multiparty compatibility,
guaranteed by a well-formed global type, and on semantics proofs from previous
work (e.g., (Deniélou and Yoshida, 2013)). This approach makes our development
_semantics-preserving_ : it endows existing MPST systems with distributed
protocol specification.

$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G_{n}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{11}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{1k_{1}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{n1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{nk_{n}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$${\bf\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}{=}}$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{11}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{1k_{1}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{nk_{n}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\upharpoonright$$\upharpoonright$$\upharpoonright$$\upharpoonright$$\upharpoonright$$\upharpoonright$$\upharpoonright$composition
Figure 1. Distributed Protocol Specification, Naively

Traditionally, a global type is a “closed” standalone entity that describes a
one-component communication protocol: all interactions among participants are
_internal_ to such component. We consider instead the distributed
specification of a system, in terms of multiple components (disjoint sets of
participants). Each participant can send both internal messages, within its
component, or _external_ , to other components. Therefore, we “open” the
syntax of global types, so that it allows not only for intra-component
communication, but also for inter-component communication. By extending the
syntax of global types with an interface for inter-component communication, we
obtain _hybrid types_. The communication protocol of each component of the
system is specified as a hybrid type; multiple components can be composed into
a well-formed global type thanks to a novel notion of _compatibility, based on
projection._

In what follows: we consider a three-component system: a company with three
departments, for each of which, a different _(protocol) designer_ is in charge
of describing the communication protocol. The departments, with respective
(internal) roles, are the following:  (a) the _strategy team_ , the roles of
which are the director d of the company and the advertisement team ad;  (b)
the _sales department_ , with a salesman s and the website administrator w;
(c) the _finance department_ , with two employees,
${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}$
and
${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}2}}$.
We assume that internal roles of different components are _distinct_.

_Global Types for Intra-Component Communication._ When no inter-component
communication happens, each protocol designer gives a global type for the
_internal_ communication of their department (Figure 2(a)). In
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G_{\sf
str}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$, the
global type for the strategy department, the director d sends the product ID
to the responsible for advertisement ad; then, d gives an ok or asks ad to
stop. For the sales department
($\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G_{\sf
sales}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$) s
decides whether w can publish some content on the company website. In the
financial department
($\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G_{\sf
fin}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$),
${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}$
sends the product ID to
${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}2}}$
and gets back either a price or a stop.

$\begin{array}[]{l}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G_{\sf
str}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{ad}}}}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{ad}}}}:}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\\{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{ok}}}}}.\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathtt{end}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5},{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{stop}}}}}.\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathtt{end}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\\}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\\\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G_{\sf
sales}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{w}}}}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\\{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{publish}}}}}.\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathtt{end}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5},{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{stop}}}}}.\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathtt{end}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\\}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\\\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G_{\sf
fin}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}\to{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}2}}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}2}}\to{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}:}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\\{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{price}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathtt{end}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5},{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{stop}}}}}.\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathtt{end}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\\}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\end{array}$
(a) Global Types for Internal Communication

$\begin{array}[]{l}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\prime}_{\sf
str}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{ad}}}}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\hbox{\pagecolor{lightyellow}\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{d}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{s}}}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\small
nat}}})}.}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\hbox{\pagecolor{papayawhip}\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{d}}}}}!{${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}$};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\small
nat}}})}.}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{ad}}}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}\\{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{ok}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1},{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{stop}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}\\}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\\\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\prime}_{\sf
sales}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\hbox{\pagecolor{lightyellow}\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{d}}}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{s}}}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\small
nat}}})}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{w}}}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}\\{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{publish}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1},{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{stop}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}\\}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\\\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\prime}_{\sf
fin}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\hbox{\pagecolor{papayawhip}\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{d}}}}}?{${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}$};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\small
nat}}})}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}\to{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}2}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}2}}\to{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}\\{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{price}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1},{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{stop}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}\\}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\end{array}$
(b) Hybrid Types for Basic Inter-Department Interactions

$\begin{array}[]{l}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
str}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{ad}}}}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}!{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\left\\{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{ok}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{ad}}}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{go}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1},{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{wait}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{ad}}}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{wait}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}\right\\}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\\\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
sales}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}};}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\left\\{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{price}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{w}}}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{publish}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1},{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{wait}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{w}}}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{wait}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}\right\\}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\\\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
fin}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}?{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}};}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}\to{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}2}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}2}}\to{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}\left\\{\begin{array}[]{l}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{price}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{ok}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{price}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1},\\\
{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{wait}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{wait}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{wait}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}}\end{array}\right\\}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\\\
\end{array}$
(c) More Expressive Hybrid Types

Figure 2. Types for Interactions in the Company

_Hybrid Types for Inter-Component Interactions._ The components of a
distributed system are expected to communicate with each other. Therefore, we
introduce a _hybrid syntax of global and local constructs_ (and we call
_hybrid types_ the terms of this syntax): to the global-type syntax (e.g.,
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{ad}}}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$),
for intra-component communication, we add local send and receive constructs
(e.g.,
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}?{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$),
as the interface for inter-component communication. In our example, a first
message is sent by d, with a product ID prod, externally, to the other two
departments (Figure 2(b)):
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}!{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.
These are _dually_ received by the sales team
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and by the finance team
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}?{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
respectively (as highlighted in Figure 2(b)).

###### Remark 2.1 (Generalising Global and Local Types).

We observe that hybrid types are a generalisation of both global and local
types. A global type is a “closed” hybrid type, where only internal messages
are exchanged. The intuition for local types is more subtle: a local type can
be interpreted as a basic, _one-participant component_ of a communicating
system, which communicates only externally, with participants of other
components. E.g., the local type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}};}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{1}}}}.}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{r}}}}};}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{2}}}}.\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{end}}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
for the participant q, can be written as the hybrid type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{1}}}}.}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{r}}}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{2}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$:
q is the only internal participant that first receives from p and then sends
to r (both p and r are of other components). Being able to express global and
local types as hybrid types is fundamental: it makes our results correct and
compatible with existing MPST theories (see Remark 2.2 below, and Corollary
4.10 in §4).

_Expressiveness and Compatibility._ We describe a more expressive version of
the protocols (Figure 2(c)) that combines inter-component messages with
branching and recursion. Figure 3 shows the communication for each component
of the system, as described by the protocol designer of each department. We
imagine that the price of the product prod is decided within the finance
department: the finance expert
${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}2}}$
either gives a price or asks all processes to wait in a recursive loop; then,
the decision is communicated to the other departments. Figure 3(c) shows the
execution of the protocol for the finance department, where
${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}2}}$
makes such choice. Figure 2(c) shows the formal specifications, as hybrid
types, of the three protocols. We observe that, to compose
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
str}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
sales}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$, and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
fin}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$ (and,
in general, to compose, more than two communicating protocols), dual relations
are not sufficient for compatibility (for a broader discussion see §6). Our
proposal is to give separately the specification of a _communication
discipline for inter-component interactions only_ : intra-component
interactions are left to the designer of each respective component and some
_chief designer_ gives the description of one more protocol, for global
guidance of inter-component communication. For our example, we collect all the
interactions between any two different departments in the protocol in Figure
4(a), and we formalise it with a _compatibility (global) type_ :

$\begin{array}[]{l}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}:=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}\to{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\left\\{\begin{array}[]{l}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{ok}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{price}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1},\\\
{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{wait}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}:}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{wait}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}}\end{array}\right\\}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\end{array}$

_Compatibility_ of subprotocols
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
str}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
sales}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$, and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
fin}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$, with
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
is achieved by asking that the _(generalised) projection_
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{}}$,
of
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
with respect to the internal participants of each subprotocol, is equal to the
_localisation_
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf{loc}}\;}}{}\\!\\!$,
of that subprotocol, where “localising a protocol” means isolating its inter-
component communication (by retaining only its _local_ constructs). E.g., we
consider
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
str}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$ and
its internal participants
$\\{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}},{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{ad}}}}\\}$.

$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\\{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}},{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{ad}}}}\\}}}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf{loc}}\;}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
str}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}}};}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}!{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{prod}}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}};}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\left\\{{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{ok}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1},{\textit{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{wait}}}}}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}\right\\}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$

Analogously we require that
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\\{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{s}}}},{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{w}}}}\\}}}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf{loc}}\;}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
sales}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$ and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\\{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}},{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}2}}\\}}}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf{loc}}\;}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
str}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.

We observe that not only we have enriched the syntax of global types with
local constructs to get hybrid types, but also we have _generalised
projection_ to _sets_ of participants, introduced a new operator (_localiser_)
to isolate external communication, and, based on these, defined compatibility.

dads${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}$prodprodprodokgowaitwait
(a) Strategy Department

swd${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}$prodpricepublishwaitwait
(b) Sales Department

${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}$${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}2}}$dsprodprodpriceokpricewaitwaitwait
(c) Finance Department

pinternal participantqexternal participantinternal interactionexternal
interactionchoiceloop (recursion)

Figure 3. Communication for Each Department in the Company

_Compositionality and Correctness._ Our theory (§3 and §4) provides an
explicit function
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathcal{B}}$
that _builds back_ a single global type for the communication in the company,
from the distributed specification above:
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathcal{B}\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;([\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
str}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
sales}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
fin}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}])}}$.
It holds that
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
str}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{d}}}}}}$,
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}}}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{\sf
fin}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}}}$,
and analogously for all participants: _projection is preserved_. A figure,
representing such
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
for our example, can be found in Appendix A.

More generally (see Figure 4(b)), from a compatibility type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and hybrid types
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
for each component (with set of internal participants $E_{i}$), such that they
are compatible
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\upharpoonright_{E_{i}}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf{loc}}\;}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
our theory synthesises a global type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathcal{B}\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;([\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}_{n}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}])}}$
(Definition 4.6 and Theorem 4.7). Correctness of our theory is given by
Corollary 4.10. Formally, this result guarantees that _the local types,
projections of
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
on each participant, are the same as if obtained by the respective subprotocol
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$_:
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}}$
if p is a participant of the $i$-th subprotocol
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.
We have achieved _distributed protocol specification_ : we can both obtain
local types for implementation in a distributed fashion, by projection of the
respective component
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
(no designer or programmer needs the full knowledge of
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$),
and rest assured that all local types (for all participants, in all
components) are projections of a single, well-formed global type. This makes
our development compatible with existing MPST theories, with no need for
developing new semantics (_semantics preservation_): a well-formed global type
projecting on all participants gives traditional _multiparty compatibility_ ,
which, thanks to the semantics results in the literature (Deniélou and
Yoshida, 2013; Coppo et al., 2015; Honda et al., 2016), leads to guarantees,
such as liveness and deadlock freedom.

###### Remark 2.2 (Hybrid Types and Generalised Projection).

With reference to Figure 4(b), Let us consider the set of participants $E_{i}$
of the generic
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
and
${{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\in
E_{i}$. Generalised projection takes a hybrid type and returns a hybrid type;
since _global and local types are hybrid types_ (Remark 2.1), e.g., we can
project
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
onto $E_{i}$ for compatibility
($\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\upharpoonright_{E_{i}}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf{loc}}\;}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$),
or
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
onto $E_{i}$ and verify that it is equal to
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
(see Theorem 4.7, §4). Most importantly, Theorem 4.9 in §4 guarantees that
projection composes over set inclusion
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}}=(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{E_{i}}}){\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}}$:
by projecting
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
onto the participant p, we obtain the same local type for p. Namely, we can
obtain local types from the specific component
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and then _implement them in a distributed fashion_ , but also they all are
projections of a well-formed global type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.

To summarise (see Figure 4(b)), our proposal for distributed protocol
specification is the following:

  1. (1)

a different designer specifies, for each component of the system, a hybrid
type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$;

  2. (2)

a chief designer gives the compatibility type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
to discipline inter-component interactions;

  3. (3)

compatibility is a simple equality check:
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{E_{i}}}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf{loc}}\;}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
($E_{i}$ is the set of participants for
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$).

In return, as a metatheoretical result proved once and for all by our theory,
the designers obtain
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathcal{B}\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;([\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}_{n}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}])}}$,
_a global type for the whole communication_ , for which _projections are
preserved_ (and, hence, MPST semantic guarantees hold).

In §3 and §4 we detail our compositionality theory, including generalised
projection, localiser, compatibility, build-back, and correctness results.

ds${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}$prodprodokpricewaitwait
(a) Inter-Component
Communication

$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}^{\prime}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}^{\prime}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}^{\prime}_{n}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{n}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{11}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{1k_{1}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{21}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{2k_{2}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{n1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{nk_{n}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$${\bf\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}{=}}$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{11}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{1k_{1}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{21}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\dots$$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L_{nk_{n}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$$\upharpoonright$$\upharpoonright$$\upharpoonright$${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf{loc}}\;}}{}$${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf{loc}}\;}}{}$${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf{loc}}\;}}{}$$\upharpoonright$$\upharpoonright$$\upharpoonright$$\upharpoonright$$\upharpoonright$$\upharpoonright$$\upharpoonright$$\upharpoonright$$\upharpoonright$$\upharpoonright$composition
(b) Distributed Protocol Specification, Compatibility through Projection

Figure 4. Inter-Component Communication and Compatibility via Projection

##  3\. Hybrid Types for Protocol Specification

###  3.1. Background: Preliminaries of Multiparty Session Types

We give a short summary of _multiparty session types_ (Honda et al., 2016;
Scalas et al., 2019; Coppo et al., 2015; Yoshida and Gheri, 2020);
specifically, our theory is based on the formulation in (Deniélou and Yoshida,
2013), extended to parallel composition of global types. The notation for our
MPST system is standard (directly adapted from (Castro-Perez et al., 2021)).

Atoms of our syntax are: a set of _roles_ (or _participants_), ranged over by
${{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}},{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}},\dots$,
a set of _(type) variables_ , ranged over by
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{Y}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\dots$;
and a set of labels, ranged over by
${{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{0}}}},{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{1}}}},\dots,{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}},{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{j}}}},\dots$.

###### Definition 3.1 (Sorts, Global Types, and Local Types).

Sorts, global types, and local types, ranged over by S,
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
respectively, are inductive datatypes generated by:

$\begin{array}[]{l}{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}::={\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
unit}}}~{}~{}\mathbf{|\\!\\!|}~{}~{}{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}~{}~{}\mathbf{|\\!\\!|}~{}~{}{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
int}}}~{}~{}\mathbf{|\\!\\!|}~{}~{}{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
bool}}}~{}~{}\mathbf{|\\!\\!|}~{}~{}{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}\texttt{\small+}{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}}}~{}~{}\mathbf{|\\!\\!|}~{}~{}{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}\texttt{\small*}{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}}}\qquad\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}::=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}~{}~{}\mathbf{|\\!\\!|}~{}~{}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}~{}~{}\mathbf{|\\!\\!|}~{}~{}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mu\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{X}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}.\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}~{}~{}\mathbf{|\\!\\!|}~{}~{}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}:\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell}}}_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}}_{i}}}).\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}~{}~{}\mathbf{|\\!\\!|}~{}~{}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}_{1}\,|\,\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}_{2}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\\\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}::=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}~{}~{}\mathbf{|\\!\\!|}~{}~{}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}~{}~{}\mathbf{|\\!\\!|}~{}~{}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mu\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}.\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}~{}~{}\mathbf{|\\!\\!|}~{}~{}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell}}}}}}_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L}\color[rgb]{0,0,1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}~{}~{}\mathbf{|\\!\\!|}~{}~{}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell}}}}}}_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L}\color[rgb]{0,0,1}{}_{i}\\}_{i\in
I}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\end{array}$

where,
${{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\neq{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}$,
$I\neq\emptyset$, and
${{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}\neq{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{j}}}}$
when $i\neq j,$ for all $i,j\in I$, in
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}:\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell}}}_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}}_{i}}}).\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell}}}}}}_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L}\color[rgb]{0,0,1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$, and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell}}}_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L}\color[rgb]{0,0,1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.

The _global message_
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}:\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell}}}_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}}_{i}}}).\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
describes a protocol where participant p sends to q one message with label
${{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}$
and a value of sort
${\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}$ as payload, for some $i\in I$; then, depending on which
${{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}$
was sent by p, the protocol continues as
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{0,0,0}{}_{i}$.
The type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
represents a _terminated protocol_. _Recursive protocol_ is modelled as
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mu}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{X}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}.\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
where recursion _variable_
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
is bound. The _parallel_ construct
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}_{1}\,|\,\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
describes a protocol composed by two independent ones. The participants of
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
are required to be disjoint: no communication happens between
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{G}\color[rgb]{.5,0,.5}{}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
but only internally in each one of them (for a broader discussion, see §5.1).
The intuition for local types
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mu\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}.\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
is the same as for global types. The _send type_
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell}}}_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L}\color[rgb]{0,0,1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$ says
that the participant implementing the type must choose a labelled message to
send to q; if the participant chooses the label
${{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}$,
it must include in the message to q a payload value of sort
${\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}$, and continue as prescribed by
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L}\color[rgb]{0,0,1}{}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.
The _receive type_
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell}}}_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L}\color[rgb]{0,0,1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$ requires
to wait to receive a value of sort
${\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}$ (for some $i\in I$) from the participant p, via a message with label
${{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}$;
then the process continues as prescribed by
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{L}\color[rgb]{0,0,1}{}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.

We are interested in types that are (1) _guarded_ —e.g.,
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mu}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}.\allowbreak\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
nat}}}).\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{X}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
is a valid global type, whereas
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mu}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{.}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
is not—(detail in Appendix B.1, Definition B.1) and (2) _closed_ , i.e., all
variables are bound by