11institutetext:  University of Glasgow
11email<EMAIL_ADDRESS>
11email<EMAIL_ADDRESS>
# MAG$\pi$: Types for Failure-Prone Communication

Matthew Alan Le Brun  0000-0001-7394-0122 Ornela Dardha  0000-0001-9927-7875

###### Abstract

_Multiparty Session Types_ (MPST) are a typing discipline for communication-
centric systems, guaranteeing communication safety, deadlock freedom and
protocol compliance. Several works have emerged which model failures and
introduce fault-tolerance techniques. However, such works often make
assumptions on the underlying network, e.g., TCP-based communication where
messages are guaranteed to be delivered; or adopt centralised reliable nodes
and an ad-hoc notion of reliability; or address _only_ a single kind of
failure, e.g., node crash failures.

In this work, we develop MAG$\pi$—a Multiparty, Asynchronous and Generalised
$\pi$-calculus, which is the _first language and type system_ to accommodate
in unison: ($i$) the widest range of non-Byzantine faults, including _message
loss, delays_ and _reordering_ ; _crash failures_ and _link failures_ ; and
_network partitioning_ ; ($ii$) a novel and most general notion of
_reliability_ , taking into account the viewpoint of _each_ participant in the
protocol; ($iii$) the spectrum of network assumptions from the lowest UDP-
based network programming to the TCP-based application level. We prove subject
reduction and session fidelity; process properties, (deadlock freedom,
termination); failure-handling safety and reliability adherence.

###### Keywords:

Session types Distributed protocols Failures Timeouts

##  1 Introduction

Despite large investments into fault-prevention techniques, failures still
regularly occur in complex distributed applications. It is widely agreed that
traditional methods of verification using software testing do not provide high
levels of confidence in the correctness of distributed algorithms. This is
mainly due to the _non-deterministic_ behaviour inherent to these protocols,
which makes it unfeasible to manually test for all edge cases. This problem is
bypassed by using exhaustive techniques such as model checking [9, 30],
capable of exploring the entirety of the state space of a program to verify
its correctness. However, building suitable models for complex distributed
algorithms is arduous, expensive, and often intractable (due to the state
explosion problem [10]). Furthermore, even if an algorithm is successfully
encoded into a suitable model and checked, guarantees of correctness are on
the _design_ of the algorithm, and not on the software _implementation_ ;
handwritten code is still prone to human error. Contrastively, types and type
systems [28] are lightweight forms of verification. Baked in programming
languages, types provide guarantees directly on handwritten code and aid
developers in implementing software which is correct by construction. Specific
to concurrent and distributed computing, _session types_ [14, 34, 15, 35, 32,
16] have quickly grown in popularity since their initial conceptualisation
[14], spanning from _binary_ –two participants, to _multiparty_ –many
participants.

Session types enforce that processes communicate according to a protocol
specification. Consequently, desirable properties about communication, e.g.,
_type safety_ (communication occurs error-free), _protocol compliance_ (or
session fidelity; processes behave according to their predefined protocol),
and _deadlock freedom_ (processes do not get stuck waiting), can be
_statically_ determined by a type checker. To this aim, session types have
been implemented in various programming languages, including Java [18, 11], Go
[21], Haskell [17, 26], Scala [31], Rust [19], Elixir [33].

To date, most session type theories are designed for _concurrent_ , as opposed
to _distributed_ processes—i.e., it is commonly assumed that communication
failures do not occur. For the few (and rapidly increasing) works that do
consider failures, heavy assumptions are made that impede their viability for
realistic complex distributed applications. E.g., _asynchronous_ theories [23,
16, 32] use _message buffers_ to model distributed communication under “TCP-
like” assumptions: messages are guaranteed to be delivered and messages from a
single sender do not get reordered. _Affine sessions_ [24, 12, 6] only allow
failure-handling of application level failures through _try-catch_ blocks;
there is no support for _arbitrary_ failures that may stem from hardware
faults, network inconsistencies etc.  _Coordinator model_ approaches [1, 8,
36] assume some degree of reliability, be it as a central resilient process, a
reliable broadcast, or fixed synchronisation points.

The harsh reality is that many real-world distributed protocols (e.g.,
consensus algorithms) cannot assume _any_ of these conditions. Networks
introduce many points of failure into a system: nodes may crash, messages can
be dropped, delayed or duplicated, links between nodes may fail etc. Designers
of distributed protocols have acknowledged that failure is inevitable, and so
algorithms are designed to withstand a threshold of failure whilst still
achieving their expected behaviour—known as _fault-tolerance_ [22]. Examples
of fault-tolerant protocols (extensively) used today include the Paxos [20]
and Raft [25] consensus algorithms, which assume the possibility of _all non-
Byzantine_ faults—i.e., node crashes, link failures, network partitions, and
message inconsistencies.

Although the correctness of these algorithms has been heavily studied, many of
them are developed with limited confidence in the correctness of the
deployable artifact, due to the reasons previously outlined. To fill this gap,
we need type-based verification, which can be made available to programming
languages, thus supporting designers and developers in designing and
implementing correct distributed algorithms. While (multiparty) session types
have made great impact in modelling structured communication and guaranteeing
relevant properties, their theory is not yet expressive to model these complex
algorithms.

In this paper, we take steps towards filling this gap by presenting MAG$\pi$—a
Multiparty, Asynchronous and Generalised $\pi$-calculus—the first language and
type system able to accommodate: ($i$) the widest range of non-Byzantine
faults, including _message loss_ , _delays_ and _reordering_ ; _crash_ and
_link failures_ ; and _network partitioning_ —all by using _timeouts_ ; ($ii$)
a novel and most general notion of _reliability_ , taking into account the
viewpoint of each participant in the protocol; and ($iii$) a spectrum of
network assumptions—from the lowest level of network programming based on UDP,
to application level based on TCP.

######  Example 1 (Ping Pong: Types)

We illustrate MAG$\pi$ with a simplified version of the ping utility from the
Internet Control Message Protocol (ICMP111https://www.rfc-
editor.org/rfc/rfc792), which is our running example. The ping utility
consists of a total of three _roles_ communicating amongst each other: two
roles,  p and  r, communicate _reliably_ with each other, and both communicate
_unreliably_ with a third role  q. Our definition of reliability (§ 3.2) takes
into account the viewpoint of each role, thus allowing roles to have their own
(possibly empty) _reliability set_. Following the assumptions above, the
reliability set for  p is
$\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}\\}$, for  r is
$\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\\}$, and for  q is $\emptyset$.

Below we give the session types, denoted
$\mathbb{S}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}}$,
$\mathbb{S}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}}$ and
$\mathbb{S}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}}$ for roles  r,  p and  q respectively.

$\displaystyle\begin{array}[]{c}\mathbb{S}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}}=\,\&\left\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\,?\,\textsf{ok}().\textsf{{end}},\
\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\,?\,\textsf{ko}().\textsf{{end}}\right\\}\\\\[8.00002pt]
\mathbb{S}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}}=\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{ping}().\,\&\left\\{\begin{array}[]{l}\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,?\,\textsf{pong}().\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}\,!\,\textsf{ok}().\textsf{{end}},\\\ {\scriptstyle\textifclk{\char
155\relax}}.\,\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{ping}().\,\&\left\\{\begin{array}[]{l}\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,?\,\textsf{pong}().\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}\,!\,\textsf{ok}().\textsf{{end}},\\\ {\scriptstyle\textifclk{\char
155\relax}}.\,\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{ping}().\,\&\left\\{\begin{array}[]{l}\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,?\,\textsf{pong}().\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}\,!\,\textsf{ok}().\textsf{{end}},\\\ {\scriptstyle\textifclk{\char
155\relax}}.\,\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}\,!\,\textsf{ko}().\textsf{{end}}\end{array}\right.\end{array}\right.\end{array}\right.\\\\[24.00005pt]
\mathbb{S}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}}=\,\&\left\\{\begin{array}[]{l}\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\,?\,\textsf{ping}().\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\,!\,\textsf{pong}().\textsf{{end}},\\\ {\scriptstyle\textifclk{\char
155\relax}}.\,\,\&\left\\{\begin{array}[]{l}\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\,?\,\textsf{ping}().\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\,!\,\textsf{pong}().\textsf{{end}},\\\ {\scriptstyle\textifclk{\char
155\relax}}.\,\,\&\left\\{\begin{array}[]{l}\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\,?\,\textsf{ping}().\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\,!\,\textsf{pong}().\textsf{{end}},\\\ {\scriptstyle\textifclk{\char
155\relax}}.\,\textsf{{end}}\end{array}\right.\end{array}\right.\end{array}\right.\end{array}$

Role  r is the _receiver_ ($\&$–called _branching_), which waits on two
options: it receives from  p either the label ok or ko and then it terminates
the protocol (end). Role  p is the _sender_ ($\oplus$222For readability, we
adopt a shorthand notation for sending towards a single role and for payloads
of type unit, such that
$\oplus\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{s}}\,!\,\textsf{m}(\texttt{unit}).\mathbb{S}\\}$ is represented by
$\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{s}}\,!\,\textsf{m}().\mathbb{S}$.–called _selection_), and it tries to obtain
information on the status of  q. It begins by sending a ping message to  q
($\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{ping}()$), then waits to receive from  q. If a pong is
received
($\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,?\,\textsf{pong}()$) in the top branch, then it concludes that the
status of  q is _reachable_ and sends this information to  r
($\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}\,!\,\textsf{ok}$()), after which it terminates. Alternatively,  p enters
a _timeout branch_ (). For simplicity, we assume  p will attempt to
communicate with  q three times (shown in the three-time indentation of the
timeout branch) before assuming  q is _unreachable_ ; after which the session
will also terminate by sending ko to  r, followed by end. In the same lines,
the protocol for role  q is given by the session type
$\mathbb{S}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}}$, where its timeout branches match the timeouts from
$\mathbb{S}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}}$.

###  1.1 Contributions

We now present our contributions w.r.t. our Multiparty, Asynchronous, and
Generalised $\pi$-calculus (MAG$\pi$).

  1. 1.

MAG$\pi$ language (§ 2):

     * •

MAG$\pi$ is _the first language_ to support the widest set of non-Byzantine
faults, including  message loss,  message delays and  message reordering;
crash failures and  link failures; and  network partitioning.

     * •

MAG$\pi$ is _the first language_ to introduce timeouts in receive branches
(used for handling network failures), as well as support undirected branching
in a _generalised_ setting—the ability to simultaneously expect an incoming
message from more than one sender.

  2. 2.

MAG$\pi$ type system (§ 3):

     * •

is a _conservative extension_ of a generalised asynchronous MPST theory [32],
benefiting from: the ability to model _more protocols_ than traditional
syntactic theories (e.g. global types); and the flexibility of checking
desired properties, such as deadlock freedom or termination, _a posteriori_
—as opposed to during the design phase.

     * •

supports undirected branching/selection and is the first type system to
introduce timeout branches.

     * •

supports a novel and most general _reliability_ definition (§ 3.2), taking
into account the viewpoint of _each_ participating role, and is built on
_optional role-dependant_ reliability assumptions.

  3. 3.

Type properties (§ 4): We prove subject reduction (theorem 4.1) and session
fidelity (theorem 4.2). We show failure-handling safety (cor. 1) and its
inverse, reliability adherence (cor. 2), which strictly connect timeouts and
reliability. We prove process properties (theorem 4.3) e.g. deadlock-freedom,
termination, liveness, in line with [32]. Finally, as our MAG$\pi$ type system
is Turing-complete, we prove decidable type checking (theorem 4.4) and
decidability of process properties for finite message buffers (theorem 4.5).

  4. 4.

TCP vs. UDP (§ 5): MAG$\pi$ is expressive enough to capture a range of network
assumptions: from low-level network programming operating over the User
Datagram Protocol (UDP); to application-level software operating over the
Transmission Control Protocol (TCP).

  5. 5.

Case study (§ 6): we further demonstrate the use of timeouts and undirected
branching to model a Domain Name System (DNS) distributed protocol with a
cache and in-built load-balancer; we also show the properties it satisfies,
including safety and deadlock freedom. Further examples are available in
appendix 0.D, including a prototype specification of a leader election
algorithm used by consensus protocols.

##  2 MAG$\pi$: Language

We present a multiparty session $\pi$-calculus, based on the theory of Scalas
and Yoshida [32], extended to accurately model real-world distributed network
environments. We assume the _lowest level_ of abstraction—the only _failure
detection mechanism_ available to a process is an upper-bound wait limit,
i.e., a _timeout_.

Our calculus presents three novel features:  (i) the new _timeout_ primitive;
(ii) the capability of expecting a message from _different senders_ ; and
(iii) operational semantics which can model _various non-Byzantine failures_.
Timeouts can be attached to receive actions—henceforth referred to as
_branches_ —and are used to describe an alternative process to be executed in
case failures are _assumed_ to occur (akin to error handlers).

Failures are said to be _assumed_ , as opposed to detected, since we model the
impossibility result of distinguishing between a delayed _vs_ lost message.
Thus, it is possible for a processes to prematurely timeout without its
corresponding message having been lost—just like the real-world!

The benefit of our approach is that the _failure detection mechanism is
agnostic to the type of fault_ , allowing us to model in unison message loss,
message delay, crash-stop failures, link failures, and network partitions.

###  2.1 Syntax

######  Definition 1 (Language Syntax)

The Multiparty, Asynchronous and Generalised $\pi$-calculus syntax is defined
by the grammar in fig. 1.

$\displaystyle c$
$\displaystyle::=\>\>\>x\>\>\>|\>\>\>s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]$ $\displaystyle(\textit{variable, session w/ role})$ $\displaystyle d$
$\displaystyle::=\>\>\>v\>\>\>|\>\>\>c$ $\displaystyle(\textit{basic value,
variable, session w/ role})$ $\displaystyle w$
$\displaystyle::=\>\>\>v\>\>\>|\>\>\>s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]$ $\displaystyle(\textit{basic value, session w/ role})$ $\displaystyle
P,Q$ $\displaystyle::=\>\>\>\bm{0}\>\>\>|\>\>\>(\nu s)\,P$
$\displaystyle(\textit{inaction, restriction})$
$\displaystyle\\!\>\>\>|\>\>\>P\,|\,Q\>\>\>|\>\>\>P+Q$
$\displaystyle(\textit{composition, non-deterministic choice})$
$\displaystyle\\!\>\>\>|\>\>\>c\oplus[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,!\,\textsf{m}\langle d\rangle.\,P$ $\displaystyle(\textit{selection
towards role
}\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}})$ $\displaystyle\\!\>\>\>|\>\>\>c\,\&_{i\in
I}\\{[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{i}$}}]\,?\,\textsf{m${}_{i}$}(x_{i}).P_{i}\\}$
$\displaystyle(\textit{reliable branching from roles
}\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{i}$}})$ $\displaystyle\\!\>\>\>|\>\>\>c\,\&_{i\in
I}\\{[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{i}$}}]\,?\,\textsf{m${}_{i}$}(x_{i}).P_{i},\;\;{\scriptstyle\textifclk{\char
155\relax}}.\,Q\\}$ $\displaystyle(\textit{branching from roles
}\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{i}$}}\textit{ w/ {timeout} Q})$
$\displaystyle\\!\>\>\>|\>\>\>\textsf{def}\;D\;\textsf{in}\;P\;\>\>\>|\>\>\>X\langle\tilde{d}\rangle$
$\displaystyle(\textit{process definition, process call})$
$\displaystyle\\!\>\>\>|\>\>\>s:\sigma$ $\displaystyle(\textit{session
buffer})$ $\displaystyle D$ $\displaystyle::=\>\>\>X(\tilde{x})=P$
$\displaystyle(\textit{process declaration})$ $\displaystyle\sigma$
$\displaystyle::=(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\triangleright\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\triangleleft\textsf{m}\langle w\rangle)\cdot\sigma\>\>\>|\>\>\>\epsilon$
$\displaystyle(\textit{session queue, empty session queue})$
Figure 1: Syntax for MAG$\pi$

Communication happens over sessions ($s,s^{\prime}$) between a number of roles
( p,  q) ranging over set $\bm{\rho}$. The primitives of the calculus are
_sessions with roles_ $s$[ p], and basic values $v$, both of which can be
abstracted using _variables_ ($x,y$). Processes ($P,Q$), include the following
standard constructs:  (i) _inaction_ $\bm{0}$represents process termination;
(ii) session _restriction_ $(\nu s)\,$ $\\!\\!P$ binds a new session $s$ in
$P$;  (iii) parallel _composition_ declares two concurrent processes;  (iv)
_selection_ $c$$\oplus$[ q]$\,!\,$m$\langle$$d$$\rangle.\,$$P$ uses channel
$c$ to send a message to  q with label m and payload $d$—after sending, the
process continues according to $P$;  (v) _definition_ and _declaration_ allow
processes to be assigned names, modelling recursion through the use of process
_calls_.  We now elaborate on the novelties in our language.

c$\,\&$${}_{i\in I}\\{$[ qi]$\,?\,$mi$($$d$$).$$P$$\\}$

Quantification over roles in a branch allows processes to receive from one in
a range of other roles. This has practical applications in a multitude of
distributed protocols, e.g.  _load balancers_.

c$\,\&$${}_{i\in I}\\{$[ qi]$\,?\,$mi$($$d$$).$$P$, $.\,$$Q$$\\}$

Timeouts are used as a _failure detection mechanism_ in receive branches. If a
failure is assumed to have lost or prevented the incoming message, then
process $Q$ is initiated. It is key to note that timeouts are non-
deterministic—they model an arbitrary and unknown duration of time a process
waits before assuming a failure has occurred.

$P+Q$

Non-deterministic choice randomly picks between two possible process
continuations. We use this construct to simplify examples for better
presentation. Concretely, it replaces the need for _expressions_ and _if-then-
else_ constructs, which are routine and orthogonal to our formulation.

$s:\sigma$

Message buffer for session $s$. An entry in the buffer
$(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\triangleright\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\triangleleft\textsf{m}\langle w\rangle)$ models a message “in transit”
from role  p to  q with label m and payload $w$. This is needed to accommodate
asynchrony in our language.

[R-$\bm{\oplus}$] |  $s$[ p]$\oplus$[ q]$\,!\,$m$\langle$$w$$\rangle.\,$$P$ $\,|\,$ $s$$:$$\sigma$ $\longrightarrow$ $P$ $\,|\,$ $s$$:$$\sigma$ $\cdot$ $(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {p}}\triangleright\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {q}}\triangleleft\textsf{m}\langle w\rangle)$ $\cdot$ $\epsilon$ |
---|---|---
[R-$\bm{\,}\&$] |  $s$[ q]$\,\&$${}_{i\in I}\\{$[ pi]$\,?\,$mi$($$x_{i}$$).$$P_{i}$ [, $.\,$$Q$]$\\}$ $\,|\,$ $s$$:$$(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {p${}_{k}$}}\triangleright\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {q}}\triangleleft\textsf{m${}_{k}$}\langle w\rangle)$ $\cdot$ $\sigma$ |
|  $\>\>\>\>\>\>\longrightarrow$ $P_{k}[^{w}/_{x_{k}}]$ $\,|\,$ $s$$:$$\sigma$ | for $k\in I$
[R-] |  $s$[ q]$\,\&$${}_{i\in I}\\{$[ pi]$\,?\,$mi$($$x_{i}$$).$$P_{i}$, $.\,$$Q$$\\}$ $\,|\,$ $s$$:$$\sigma$ $\longrightarrow$ $Q$ $\,|\,$ $s$$:$$\sigma$ |
[R-+] |  $P_{1}$$+$$P_{2}$ $\longrightarrow$ $P_{i}$ | for $i\in\\{1,2\\}$
[R-$\bm{X}$] |  def $X$$($$x_{1}$,$\dotsc$,$x_{n}$$)=$ $P$ in ($X$$\langle$$w_{1}$,$\dotsc$,$w_{n}$$\rangle$ $\,|\,$ $Q$) |
|  $\>\>\>\>\>\>\longrightarrow$ def $X$$($$x_{1}$,$\dotsc$,$x_{n}$$)=$ $P$ in ($P$[${}^{w_{1}}$/${}_{x_{1}}$]$\,\dotsb$[${}^{w_{n}}$/${}_{x_{n}}$] $\,|\,$ $Q$) |
[R-$\mathbb{C}$] |  $P$ $\longrightarrow$ $P^{\prime}$ $\implies$ $\mathbb{C}$[$P$] $\longrightarrow$ $\mathbb{C}$[$P^{\prime}$] |
[R-$\bm{\downarrow}$] |  $s$$:$$h$ $\cdot$ $\sigma$ $\longrightarrow$ $s$$:$$\sigma$ |
Figure 2: Reduction rules for MAG$\pi$

###  2.2 Operational Semantics

We begin with definitions of a reduction context and buffer congruence.

######  Definition 2 (Reduction Context)

A reduction context $\mathbb{C}$ abstracts away an outer environment from a
process, and is given by:

$\mathbb{C}\ ::=\ \mathbb{C}\,|\,P\>\>\>|\>\>\>(\nu
s)\,\mathbb{C}\>\>\>|\>\>\>\textnormal{{def} $D$ {in}
$\mathbb{C}$}\>\>\>|\>\>\>[\;]$

Hence, $\mathbb{C}[P]$ refers to process $P$ under some arbitrary context
$\mathbb{C}$.

######  Definition 3 (Buffer Congruence)

A process containing only a buffer under its restriction is congruent to
inaction. Message buffers observe total reordering.

$(\nu
s)\,s\\!:\\!\sigma\;\equiv\;\bm{0}\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>s\\!:\\!\sigma_{1}\cdot
h_{1}\cdot h_{2}\cdot\sigma_{2}\;\equiv\;s\\!:\\!\sigma_{1}\cdot h_{2}\cdot
h_{1}\cdot\sigma_{2}$

######  Definition 4 (OS)

The operational semantics for MAG$\pi$ is given via a _reduction relation_
$\longrightarrow$ inductively defined in fig. 2, together with standard
_structural congruence rules_ [32] and two _buffer congruence rules_ defined
in def. 3.

Let us now comment on the reduction rules (fig. 2). Processes send messages
using the selection rule [R-$\bm{\oplus}$]; this adds the sent message as a
new entry in the session buffer, and advances the process to its continuation.
Sent messages are read from the buffer using the branching rule
[R-$\bm{\,}\&$]. If the receiver has a valid branch matching the sender and
message label, then it advances to the specific continuation of said branch (a
timeout branch for this rule is optional). The substitution
$P_{k}[^{w}/_{x_{k}}]$ denotes the replacement of variable $x_{k}$ with the
payload value $w$ in the continuation process $P_{k}$. The timeout rule [R-]
advances processes to their timeout branch _without_ changing the buffer. Non-
deterministic choice is resolved using the choice rule [R-+], which advances
the process to one of the two possible continuations. The call rule
[R-$\bm{X}$] replaces a process call with its defined process, substituting
each parameter. Processes can reduce under a context using the context rule
[R-$\mathbb{C}$]. Lastly, messages can be lost from the buffer with the drop
rule [R-$\bm{\downarrow}$].

We now unpack how our semantics deals with failures. The reduction rules in
fig. 2 allow various forms of failures to be modelled, stemming from the
versatility and elegance of the drop rule [R-$\bm{\downarrow}$]. The following
elaborates on how this rule can be utilised to model different types of
failure:

  * •

Message loss is modelled directly through the reduction rule
[R-$\bm{\downarrow}$].

  * •

Crash-failure is modelled through repeated applications of
[R-$\bm{\downarrow}$] for a particular role. E.g., to model a crash of role
p, the reduction step [R-$\bm{\downarrow}$] should be applied to all messages
that enter the buffer matching the pattern
$(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\triangleright\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{\\_}}\triangleleft\textsf{\\_}\langle\\_\rangle)$ (_ symbolises a “don’t
care” value).

  * •

Link-failure is modelled using a similar method; the difference being that
messages between _two_ specific recipients are dropped. E.g., modelling a
link-failure between roles  p and  q requires [R-$\bm{\downarrow}$] to be
applied to all messages entering the buffer with the patterns
$(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\triangleright\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\triangleleft\textsf{\\_}\langle\\_\rangle)$ and
$(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\triangleright\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\triangleleft\textsf{\\_}\langle\\_\rangle)$.

  * •

Message delay is modelled by applying rule [R-] to a branch whilst a valid
message resides in the buffer. E.g.:

$\displaystyle
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,\&_{i\in
I}\\{[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{i}$}}]\,?\,\textsf{m${}_{i}$}(x_{i}).P_{i},\
{\scriptstyle\textifclk{\char 155\relax}}.\,Q\\}\ \,|\,\
s\\!:\\!(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{k}$}}\triangleright\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\triangleleft\textsf{m${}_{k}$}\langle w\rangle)\cdot\sigma$
$\displaystyle\>\>\>\>\>\>\longrightarrow\ Q\ \,|\,\
s\\!:\\!(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{k}$}}\triangleright\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\triangleleft\textsf{m${}_{k}$}\langle w\rangle)\cdot\sigma\>$
$\displaystyle\text{for}\ k\in I.$

  * •

Total  message reordering is modelled via _buffer congruence rules_ (def. 3).

  * •

Network partitions can be represented using multiple _link failures_.

The granularity at which we model failures allows for degrees of
customisation. E.g., benign fault-tolerant consensus algorithms typically
assume the possibility of _all_ non-Byzantine faults, therefore all the
aforementioned failures are required. Alternatively, an application assumed to
run over a trusted TCP network need not worry about single message drops, and
hence [R-$\bm{\downarrow}$] should only be applied to model node crash and
link failures.

######  Definition 5 (Well-formedness)

To ensure that communication is possible, we require that a well-formed
process has a buffer for each session, i.e.,

$P=(\nu s)\,Q\implies
Q\equiv(\nu\tilde{s^{\prime}})\,(Q^{\prime}\>\,|\,\>s\\!:\\!\sigma)$

Def. 5 introduces a well-formedness condition to guarantee that a session
always guards its buffer, hence ensuring that messages always have a queue to
be placed in. From now on, we will only consider well-formed processes.

Before concluding this section, we recall our ping pong running example from
the introduction, and present below the processes for roles  p,  q and  r.

######  Example 2 (Ping Pong: Processes)

$\displaystyle\begin{array}[]{c}P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}}=s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\oplus[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,!\,\textsf{ping}\langle\rangle.\,s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,\&\left\\{\begin{array}[]{l}[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,?\,\textsf{pong}().P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}}^{\textit{ok}},\\\ {\scriptstyle\textifclk{\char
155\relax}}.\,s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\oplus[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,!\,\textsf{ping}\langle\rangle.\,s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,\&\left\\{\begin{array}[]{l}[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,?\,\textsf{pong}().P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}}^{\textit{ok}},\\\ {\scriptstyle\textifclk{\char
155\relax}}.\,s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\oplus[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,!\,\textsf{ping}\langle\rangle.\,P^{\prime}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}}\end{array}\right.\end{array}\right.\\\\[16.00003pt]
P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}}^{\textit{ok}}=s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\oplus[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}]\,!\,\textsf{ok}\langle\rangle.\,\bm{0}\>\>\>\>\>\>P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}}^{\prime}=s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,\&\left\\{\begin{array}[]{l}[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,?\,\textsf{pong}().P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}}^{\textit{ok}},\\\ {\scriptstyle\textifclk{\char
155\relax}}.\,s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\oplus[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}]\,!\,\textsf{ko}\langle\rangle.\,\bm{0}\end{array}\right.\\\\[16.00003pt]
P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}}=s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,\&\left\\{\begin{array}[]{l}[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,?\,\textsf{ping}().P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}}^{\textit{pong}},\\\ {\scriptstyle\textifclk{\char
155\relax}}.\,s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,\&\left\\{\begin{array}[]{l}[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,?\,\textsf{ping}().P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}}^{\textit{pong}},\\\ {\scriptstyle\textifclk{\char
155\relax}}.\,s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,\&\\{[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,?\,\textsf{ping}().P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}}^{\textit{pong}},\ {\scriptstyle\textifclk{\char
155\relax}}.\,\bm{0}\\}\end{array}\right.\end{array}\right.\\\\[16.00003pt]
P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}}^{\textit{pong}}=s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\oplus[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,!\,\textsf{pong}\langle\rangle.\,\bm{0}\\\\[8.00002pt]
P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}}=s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}]\,\&\\{[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,?\,\textsf{ok}().\bm{0},[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,?\,\textsf{ko}().\bm{0}\\}\end{array}$

##  3 MAG$\pi$: Type System

We introduce the type system for MAG$\pi$, which is a conservative extension
of the _generalised_ asynchronous MPST theory [32, sec. 7]. _Generalised_ MPST
stray away from global protocol specifications (global types) and instead
operate on user-defined localised specifications of each participating role
(local types). The benefits of working with such theory include:  (i) the
ability to capture a larger set of viable protocols compared to traditional
syntactic methods (e.g. global types) of enforcing consistent communication;
(ii) the ability to model protocols of different requirements.  In particular,
instead of syntactically enforcing programmers to write, e.g., deadlock-free
code, a generalised theory allows programmers to unrestrictedly design
protocols that are checked _a posteriori_ against any number of required
properties, such as deadlock-freedom, termination etc.

The novelties of our type system include:  (i) _undirected
branching/selection_ ;  (ii) _timeout branches_(syntax in § 3.1); and  (iii)
_reliability sets_ —sets of roles assumed to not fail, from the perspective of
_each_ role (§ 3.2).  Reliability sets (possibly empty) enforce the use of
_timeouts_ for all failure-prone communication.

As in [32], our type system does _not_ use global types, but solely relies on
local types. Consequently, typing contexts must obey a safety property to
ensure subject reduction (§ 3.3). Finally, we present the rules for our type
system in § 3.4, and discuss its key properties in § 4.

###  3.1 Types

Our MPST theory is designed for the distributed computing setting. Concretely,
our type system (def. 6) is _asynchronous_ ; it allows _branching_ (resp.
_selection_) from (resp. to) multiple roles; and supports _timeout_
continuation types.

######  Definition 6 (Typing syntax)

The typing syntax is defined using the grammar in fig. 3.

Basic and Session Types
$\mathbb{T}$ ::= $\mathbb{B}$ $|$ $\mathbb{S}$ $\mathbb{B}$ ::= int $|$ bool
$|$ real $|$ unit $|$ $\dotsb$ $\mathbb{S}$ ::= $\,\&$${}_{i\in I}\\{$
pi$\,?\,$mi$($$\mathbb{T}$i$).$$\mathbb{S}$i[, $.\,$$\mathbb{S}$′]$\\}$ $|$
$\oplus$${}_{i\in I}\\{$ pi$\,!\,$mi$($$\mathbb{T}$i$).$$\mathbb{S}$i$\\}$ $|$
$\mu$t.$\mathbb{S}$ $|$ t $|$ end

Buffer Types
$\mathbb{M}$ ::= p$\,!\,$m$($$\mathbb{T}$$)\cdot$$\mathbb{M}$ $|$ $\epsilon$

Session-Buffer Types
$\tau$ ::= $\mathbb{M}$ $|$ $\mathbb{S}$ $|$ ($\mathbb{M}$$\,;\,$$\mathbb{S}$)

Figure 3: Basic Types, Session Types, Buffer Types and Session-Buffer Types
$\displaystyle\displaystyle{\hbox{\hskip
2.5pt\vbox{\hbox{\hskip-2.5pt\hbox{\hbox{$\displaystyle\displaystyle\
$}}}\vbox{}}}\over\hbox{\hskip
11.11113pt\vbox{\vbox{}\hbox{\hskip-11.11113pt\hbox{\hbox{$\displaystyle\displaystyle\mathbb{T}\equiv\mathbb{T}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
2.5pt\vbox{\hbox{\hskip-2.5pt\hbox{\hbox{$\displaystyle\displaystyle\
$}}}\vbox{}}}\over\hbox{\hskip
30.60007pt\vbox{\vbox{}\hbox{\hskip-30.60007pt\hbox{\hbox{$\displaystyle\displaystyle\mathbb{M}_{1}\cdot\mathbb{M}_{2}\equiv\mathbb{M}_{2}\cdot\mathbb{M}_{1}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
2.5pt\vbox{\hbox{\hskip-2.5pt\hbox{\hbox{$\displaystyle\displaystyle\
$}}}\vbox{}}}\over\hbox{\hskip
16.36623pt\vbox{\vbox{}\hbox{\hskip-16.36623pt\hbox{\hbox{$\displaystyle\displaystyle\epsilon\cdot\epsilon\equiv\epsilon$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
34.04007pt\vbox{\hbox{\hskip-34.04007pt\hbox{\hbox{$\displaystyle\displaystyle\mathbb{M}\equiv\mathbb{M}^{\prime}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathbb{S}\equiv\mathbb{S}^{\prime}$}}}}\vbox{}}}\over\hbox{\hskip
38.48433pt\vbox{\vbox{}\hbox{\hskip-38.48433pt\hbox{\hbox{$\displaystyle\displaystyle(\mathbb{M}\,;\,\mathbb{S})\equiv(\mathbb{M}^{\prime}\,;\,\mathbb{S}^{\prime})$}}}}}}$
Figure 4: Type congruence rules

For undirected branching and selection, $I\neq\emptyset$ and role-label tuples
$(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{i}$}},\textsf{m${}_{i}$})$ must be pairwise distinct. Recursion
variables cannot be free and must appear guarded under branching/selection
types.

Type $\mathbb{T}$ denotes either a _basic_ type $\mathbb{B}$, or a _session
type_ $\mathbb{S}$, and is used to type variables. Session types describe how
a channel should be used:  (i) _undirected branching_(external choice)
$\,\&$${}_{i\in I}\\{$ pi$\,?\,$mi$($$\mathbb{T}$i$).$$\mathbb{S}$i[,
$.\,$$\mathbb{S}$′]$\\}$ denotes _receiving_ a message with label mi and
payload of type $\mathbb{T}$i from role  pi, then continuing according to
$\mathbb{S}$i. The (optional) timeout continuation type $\mathbb{S}$′
describes the protocol for handling failure on that branch;  (ii) _undirected
selection_(internal choice) $\oplus$${}_{i\in I}\\{$
pi$\,!\,$mi$($$\mathbb{T}$i$).$$\mathbb{S}$i$\\}$ denotes _sending_ a message
with label mi and payload $\mathbb{T}$i to role  pi, then continuing according
to $\mathbb{S}$i;  (iii) type end marks a channel as closed, and terminates
communication.  A session buffer is typed using the _buffer type_
$\mathbb{M}$. Entries in the buffer must correspond to the type
p$\,!\,$m$($$\mathbb{T}$$)\cdot$$\mathbb{M}$, denoting a message sent to  p
with label m and payload of type $\mathbb{T}$. A session with role is typed
using _session-buffer_ types, combining a session type and a buffer type.

Type _congruence_ $\equiv$ is defined in fig. 4. Notably, buffer types can be
reordered, and two session-buffer types are congruent if their individual
buffer and session types are congruent. Buffer type reordering is necessary to
match the _total message reordering_ supported by the language (def. 3).

###  3.2 Reliability

We go on a short detour and talk about reliability. Previous related work [4,
1, 37] have included the notion of _reliability_ into their type systems.
Generally, either one specific role, or a pre-defined set of roles, are
assumed to be reliable—i.e., no failures occur for communication involving the
identified set of roles.

Our definition of reliability (def. 7) is the most general and the first to
take into account the viewpoint of each role. We argue that this is necessary
in a distributed setting since reliability in networks is dependant on the
physical topology of processes. Recalling the ping utility (example 1), we
could imagine the processes representing roles  p and  r reside on the same
physical hardware, thus their communication cannot be affected by network
faults; and the process for  q resides on geographically separated hardware,
therefore its communication with both  p and  r is vulnerable to failure.

######  Definition 7 (Reliability)

The reliability set $\mathfrak{R}$ for a role
$\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\in\bm{\rho}$ is defined as
$\mathfrak{R}\subseteq\bm{\rho}\setminus\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\\}$, capturing the viewpoint of  p. Reliability $\mathcal{R}$ is defined
as a function mapping roles to their reliability set, i.e.,
$\mathcal{R}:\bm{\rho}\to\mathfrak{R}$.

To better model real distributed environments, our definition of reliability
allows each role to have its own (possibly empty) reliability set.

######  Example 3 (Ping Pong: Reliability Sets)

W.r.t. example 1, as the three roles have different viewpoints on each other,
then the reliability set for each of them is different. In particular, we have
$\mathcal{R}(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}})=\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}\\},\
\mathcal{R}(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}})=\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\\},\
\mathcal{R}(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}})=\emptyset$.

Investigating the extremes, we have: for a set of roles $\bm{\rho}$, if for
all
$\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\in\bm{\rho}\cdot\mathcal{R}(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}})=\emptyset$, then _no_ communication is reliable; conversely, if for all
$\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\in\bm{\rho}\cdot\mathcal{R}(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}})=\bm{\rho}\setminus\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\\}$, then _all_ communication is reliable—referred to as a _reliable
network_. This work only considers static configurations for $\mathcal{R}$,
thus reliability sets cannot change at runtime. We find that even with this
restriction, our definition is the most general compared to related work.

###  3.3 Contexts

######  Definition 8 (Type contexts)

Context
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}$
is a partial mapping from process variables to $n$-tuples of types and context
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$
is a partial mapping from variables to types, and sessions with roles to
session-buffer types, both defined below:

${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}::=\;\emptyset\>\>\>|\>\>\>{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta},X:\mathbb{T}_{1},\dotsc,\mathbb{T}_{n}\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}::=\;\emptyset\>\>\>|\>\>\>{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},x:\mathbb{T}\>\>\>|\>\>\>{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\tau$

The composition of contexts
$({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}},{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}})$
is defined iff:

$\forall
c\in\textsf{dom}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}})\cap\textsf{dom}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}}):\>\>\>{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{i}}(c)=\mathbb{M}\
\land\
{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{j}}(c)=\mathbb{S}$

For such $c$,
(${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}}$,${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}}$)(c)
= ($\mathbb{M}$$\,;\,$$\mathbb{S}$).

Contexts are congruent
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}}\equiv{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}}$
iff:

$\textsf{dom}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}})=\textsf{dom}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}})\
\land\ \forall
c\in\textsf{dom}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}}):{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}}(c)\equiv{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}}(c)$

Context
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}$
is _non-linear_ and types _process variables_ by tracking the types of their
parameters. Context
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$
is _linear_ and allows _variables_ to have _basic_ or _session types_ , and
_sessions with roles_ to have _session-buffer types_ ; as a program
progresses, a role may simultaneously have both an active session type and
messages queued in the message buffer.

Context _composition_ allows two contexts to coexist as long as their common
channels map to buffer types in one context, and session types in the other.

Context _congruence_ holds if two contexts have the same domain and the types
of their channels are congruent. It is key to note that by the definitions of
context composition and congruence we have
$s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:(\mathbb{M}\,;\,\mathbb{S})\equiv
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\mathbb{M},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\mathbb{S}$. Buffer types (resp. session-buffer types) are only used
internally by the type system; end-users are not expected to explicitly define
these types.

######  Definition 9 (Context reduction)

An action $\alpha$ is given as:

$\alpha\ ::=\
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,!\,\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}:\textsf{m}(\mathbb{T})\>\>\>|\>\>\>s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}][\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]:\textsf{m}\>\>\>|\>\>\>s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,{\scriptstyle\textifclk{\char 155\relax}}$

From left to right, this reads as  (i) a sent message;  (ii) communicationof a
message; and  (iii) the timeout of a channel.  Context transition
$\xrightarrow{\alpha}_{(\Sigma;\mathcal{R})}$ is defined in fig. 5. We write
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\xrightarrow{\alpha}_{(\Sigma;\mathcal{R})}\
$ iff $\
\exists\,{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}:{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\xrightarrow{\alpha}_{(\Sigma;\mathcal{R})}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}$.
We define two context reductions $\rightarrow_{(\Sigma;\mathcal{R})}$ and
$\rightarrow_{\Sigma}$ as:

$\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\rightarrow_{(\Sigma;\mathcal{R})}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}\textit{
holds iff
}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\xrightarrow{\alpha}_{(\Sigma;\mathcal{R})}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\
{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\rightarrow_{\Sigma}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}\textit{
holds iff
}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\xrightarrow{\alpha}_{\Sigma}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}\textit{
for
}\alpha\in\\{s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,!\,\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}:\textsf{m}(\mathbb{T}),\
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}][\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]:\textsf{m}\\}$

We write $\rightarrow_{(\Sigma;\mathcal{R})}^{+}$ (resp.
$\rightarrow_{\Sigma}^{+}$) and $\rightarrow_{(\Sigma;\mathcal{R})}^{*}$
(resp. $\rightarrow_{\Sigma}^{*}$) for their transitive and
reflexive/transitive closures respectively.

A context
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$
keeps track of open buffers using a _buffer-tracker_ $\Sigma$. Whenever a new
session is initialised, it is added to $\Sigma$, details in § 3.4 item
[T-$\nu$]. For now it suffices to know that buffer trackers restrict
communication to occur only over restricted sessions, thus by def. 5 (well-
formedness), it guarantees that a session buffer exists for all sessions in
$\Sigma$.

[$\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-]
$\displaystyle\displaystyle{\hbox{\hskip
67.92065pt\vbox{\hbox{\hskip-67.92064pt\hbox{\hbox{$\displaystyle\displaystyle
s\in\Sigma$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\exists\,k\in
I:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{k}$}}\not\in\mathcal{R}(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}})$}}}}\vbox{}}}\over\hbox{\hskip
102.08382pt\vbox{\vbox{}\hbox{\hskip-102.0838pt\hbox{\hbox{$\displaystyle\displaystyle
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\\!\,\&_{i\in
I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{i}$}}\,?\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i},\
{\scriptstyle\textifclk{\char
155\relax}}.\,\mathbb{S}^{\prime}\\}\xrightarrow{s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,{\scriptstyle\textifclk{\char
155\relax}}}_{(\Sigma;\mathcal{R})}s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\mathbb{S}^{\prime}$}}}}}}$
[$\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-Snd1]
$\displaystyle\displaystyle{\hbox{\hskip
33.52768pt\vbox{\hbox{\hskip-33.52768pt\hbox{\hbox{$\displaystyle\displaystyle
s\in\Sigma$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle k\in
I$}}}}\vbox{}}}\over\hbox{\hskip
151.86633pt\vbox{\vbox{}\hbox{\hskip-151.86632pt\hbox{\hbox{$\displaystyle\displaystyle
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\oplus_{i\in
I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{i}$}}\,!\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i}\\}\xrightarrow{s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,!\,\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{k}$}}:\textsf{m${}_{k}$}(\mathbb{T}_{k})}_{(\Sigma;\mathcal{R})}s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{k}$}}\,!\,\textsf{m${}_{k}$}(\mathbb{T}_{k})\cdot\epsilon\,;\,\mathbb{S}_{k})$}}}}}}$
[$\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-Snd2]
$\displaystyle\displaystyle{\hbox{\hskip
33.52768pt\vbox{\hbox{\hskip-33.52768pt\hbox{\hbox{$\displaystyle\displaystyle
s\in\Sigma$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle k\in
I$}}}}\vbox{}}}\over\hbox{\hskip
172.69958pt\vbox{\vbox{}\hbox{\hskip-172.69957pt\hbox{\hbox{$\displaystyle\displaystyle
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:(\mathbb{M}\,;\,\oplus_{i\in
I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{i}$}}\,!\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i}\\})\xrightarrow{s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,!\,\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{k}$}}:\textsf{m${}_{k}$}(\mathbb{T}_{k})}_{(\Sigma;\mathcal{R})}s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:(\mathbb{M}\cdot\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{k}$}}\,!\,\textsf{m${}_{k}$}(\mathbb{T}_{k})\cdot\epsilon\,;\,\mathbb{S}_{k})$}}}}}}$
[$\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-Com]
$\displaystyle\displaystyle{\hbox{\hskip
92.05397pt\vbox{\hbox{\hskip-92.05397pt\hbox{\hbox{$\displaystyle\displaystyle
s\in\Sigma$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\exists\,k\in
I:(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}},\textsf{m},\mathbb{T})=(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{k}$}},\textsf{m${}_{k}$},\mathbb{T}_{k})$}}}}\vbox{}}}\over\hbox{\hskip
181.29715pt\vbox{\vbox{}\hbox{\hskip-181.29713pt\hbox{\hbox{$\displaystyle\displaystyle
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{m}(\mathbb{T})\cdot\mathbb{M},\
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]:\\!\,\&_{i\in
I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{i}$}}\,?\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i}\
[,{\scriptstyle\textifclk{\char
155\relax}}.\,\mathbb{S}^{\prime}]\\}\xrightarrow{s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}][\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]:\textsf{m}}_{(\Sigma;\mathcal{R})}s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\mathbb{M},\
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]:\mathbb{S}_{k}$}}}}}}$
[$\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-$\displaystyle\mu$]
$\displaystyle\displaystyle{\hbox{\hskip
43.22998pt\vbox{\hbox{\hskip-43.22998pt\hbox{\hbox{$\displaystyle\displaystyle
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\mathbb{S}[^{\mu\textnormal{{t}}.\mathbb{S}}/_{\textnormal{{t}}}]\xrightarrow{\alpha}_{(\Sigma;\mathcal{R})}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
39.48888pt\vbox{\vbox{}\hbox{\hskip-39.48888pt\hbox{\hbox{$\displaystyle\displaystyle
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\mu\textnormal{{t}}.\mathbb{S}\xrightarrow{\alpha}_{(\Sigma;\mathcal{R})}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}$}}}}}}$
[$\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-Cong]
$\displaystyle\displaystyle{\hbox{\hskip
21.78743pt\vbox{\hbox{\hskip-21.78743pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}}\xrightarrow{\alpha}_{(\Sigma;\mathcal{R})}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}}$}}}\vbox{}}}\over\hbox{\hskip
30.20412pt\vbox{\vbox{}\hbox{\hskip-30.20412pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{,}}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}}\xrightarrow{\alpha}_{(\Sigma;\mathcal{R})}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}}$}}}}}}$
Figure 5: Context reduction rules

Context reduction (def. 9) models communication at the _type-level_. Context
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$
can reduce by sending, communicating, or timing out. By
[${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-],
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}=s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\\!\,\&_{i\in
I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{i}$}}\,?\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i},\
{\scriptstyle\textifclk{\char 155\relax}}.\,\mathbb{S}^{\prime}\\}$ can reduce
to a _timeout_ branch continuation type $\mathbb{S}^{\prime}$ if $s$ is in the
buffer-tracker (i.e., a buffer exists for session $s$), and _at least one_ of
the roles in the branch is _unreliable_. The latter prevents taking a timeout
for communication that is sure to be delivered. Reductions
[${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-Snd1]
and
[${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-Snd2]
simulate sending a message by reducing the selection type $\oplus_{i\in
I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{i}$}}\,!\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i}\\}$ to one
of its continuations $\mathbb{S}_{i}$, and by inserting the sent message into
the buffer type. The difference is that
[${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-Snd1]
creates the buffer type if it was previously not specified, whereas
[${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-Snd2]
appends the message to an already existing buffer type. Communication between
two roles is simulated through
[${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-Com],
where a branch type
$s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]:\\!\,\&_{i\in
I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{i}$}}\,?\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i}\
[,{\scriptstyle\textifclk{\char 155\relax}}.\,\mathbb{S}^{\prime}]\\}$
consumes the message from a buffer type
$s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{m}(\mathbb{T})\cdot\mathbb{M}$, reducing to the continuations
$s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\mathbb{M},\
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]:\mathbb{S}_{k}$. Lastly,
[${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-$\mu$]
allows reduction through recursion and
[${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$-Cong]
reduces substructures of compatibly composed contexts.

###### Definition 10

Property $\varphi_{\texttt{s}}$ is a $(\Sigma;\mathcal{R})$-safety property on
typing contexts iff:

[S-$\mathcal{R}_{1}$] | $\textnormal{$\varphi_{\texttt{s}}$}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},\ s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {p}}]:\,\&_{i\in I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {q${}_{i}$}}\,?\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i}\\})\ \implies\ \forall i\in I:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {q${}_{i}$}}\in\mathcal{R}(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {p}})$
---|---
[S-$\mathcal{R}_{2}$] | $\textnormal{$\varphi_{\texttt{s}}$}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},\ s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {p}}]:\,\&_{i\in I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {q${}_{i}$}}\,?\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i},\ {\scriptstyle\textifclk{\char 155\relax}}.\,\mathbb{S}^{\prime}\\})\ \implies\ \exists i\in I:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {q${}_{i}$}}\not\in\mathcal{R}(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {p}})$
[S-Com] | $\textnormal{$\varphi_{\texttt{s}}$}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},\ s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {p}}]:\,\&_{i\in I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {q${}_{i}$}}\,?\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i}\,[,\,{\scriptstyle\textifclk{\char 155\relax}}.\,\mathbb{S}^{\prime}]\\},\,s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {q}}]\\!:\\!\mathbb{M})$
| $\>\>\>\>\>\>\text{and
}\mathbb{M}\equiv\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\,!\,\textsf{m}(\mathbb{T})\cdot\mathbb{M}^{\prime}$
| $\>\>\>\>\>\>\text{and }\exists\,k\in
I:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{k}$}}=\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\land\textsf{m${}_{k}$}=\textsf{m}\ \implies\ \mathbb{T}_{k}=\mathbb{T}$
[S-$\mu$] | $\textnormal{$\varphi_{\texttt{s}}$}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},\ s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {p}}]:\mu\textnormal{{t}}.\mathbb{S})\ \implies\ \textnormal{$\varphi_{\texttt{s}}$}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},\ s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375} {p}}]:\mathbb{S}[^{\mu\textnormal{{t}}.\mathbb{S}}/_{\textnormal{{t}}}])$
[S-$\rightarrow$] | $\textnormal{$\varphi_{\texttt{s}}$}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma})\text{ and }{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\rightarrow_{(\Sigma;\mathcal{R})}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}\ \implies\ \textnormal{$\varphi_{\texttt{s}}$}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}})$

As previously mentioned, our type system is a _generic_ one that does not use
syntactic methods of enforcing consistent communication. Therefore, we define
a _safety_ property in def. 10 on type contexts that is used to guarantee
subject reduction and other theorems (presented in § 4).

We say $\varphi_{\texttt{s}}$ is the _largest_ safety property required to
guarantee subject reduction. The property can be re-instantiated with more
specific conditions (as demonstrated in § 5) as per the requirements of the
implementation. Concretely,  [S-$\mathcal{R}_{1}$] and  [S-$\mathcal{R}_{2}$]
ensure that timeouts are only not defined if communication is reliable and
that timeouts are defined if communication is unreliable respectively.
Condition  [S-Com] ensures that communicating messages have matching payload
types. Lastly,  [S-$\mu$] preserves $\varphi_{\texttt{s}}$ through recursion
unfolding and  [S-$\rightarrow$] requires safety to hold after context
reduction.

###  3.4 Typing Rules

[T-$\displaystyle\bm{0}$] $\displaystyle\displaystyle{\hbox{\hskip
14.7917pt\vbox{\hbox{\hskip-14.7917pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{end}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma})$}}}\vbox{}}}\over\hbox{\hskip
21.73608pt\vbox{\vbox{}\hbox{\hskip-21.73607pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash\ \bm{0}$}}}}}}$ [T-Var] $\displaystyle\displaystyle{\hbox{\hskip
2.5pt\vbox{\hbox{\hskip-2.5pt\hbox{\hbox{$\displaystyle\displaystyle\
$}}}\vbox{}}}\over\hbox{\hskip
27.93855pt\vbox{\vbox{}\hbox{\hskip-27.93855pt\hbox{\hbox{$\displaystyle\displaystyle
c:\mathbb{T}\ \vdash\ c:\mathbb{T}$}}}}}}$ [T-Val]
$\displaystyle\displaystyle{\hbox{\hskip
10.86688pt\vbox{\hbox{\hskip-10.86688pt\hbox{\hbox{$\displaystyle\displaystyle
v\in\mathbb{B}$}}}\vbox{}}}\over\hbox{\hskip
22.2557pt\vbox{\vbox{}\hbox{\hskip-22.2557pt\hbox{\hbox{$\displaystyle\displaystyle\emptyset\
\vdash\ v:\mathbb{B}$}}}}}}$ [T-X] $\displaystyle\displaystyle{\hbox{\hskip
34.42094pt\vbox{\hbox{\hskip-34.42094pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}(X)=\mathbb{T}_{1},\dotsc,\mathbb{T}_{n}$}}}\vbox{}}}\over\hbox{\hskip
38.86531pt\vbox{\vbox{}\hbox{\hskip-38.8653pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\
\vdash\ X:\mathbb{T}_{1},\dotsc,\mathbb{T}_{n}$}}}}}}$
[T-$\displaystyle\oplus$] $\displaystyle\displaystyle{\hbox{\hskip
162.50871pt\vbox{\hbox{\hskip-162.5087pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}}\
\vdash\ c:\oplus_{i\in
I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{i}$}}\,!\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i}\\}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle k\in I$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}}\
\vdash\ d:\mathbb{T}_{k}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},c:\mathbb{S}_{k}\
\vdash\ P$}}}}}}\vbox{}}}\over\hbox{\hskip
70.1873pt\vbox{\vbox{}\hbox{\hskip-70.18729pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}},{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}}\
\vdash\
c\oplus[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{k}$}}]\,!\,\textsf{m${}_{k}$}\langle d\rangle.\,P$}}}}}}$
[T-$\displaystyle\,\&$] $\displaystyle\displaystyle{\hbox{\hskip
199.23042pt\vbox{\hbox{\hskip-199.23042pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}\
\vdash\ c:\,\&_{i\in
I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{i}$}}\,?\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i}\,[,\
{\scriptstyle\textifclk{\char 155\relax}}.\,\mathbb{S}^{\prime}]\\}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle[{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},c:\mathbb{S}^{\prime}\
\vdash\ Q]$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall
i\in
I\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},x_{i}:\mathbb{T}_{i},c:\mathbb{S}_{i}\
\vdash\ P_{i}$}}}}}\vbox{}}}\over\hbox{\hskip
88.1779pt\vbox{\vbox{}\hbox{\hskip-88.17789pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}\
\vdash\ c\,\&_{i\in
I}\\{[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{i}$}}]\,?\,\textsf{m${}_{i}$}(x_{i}).P_{i}\,[,\
{\scriptstyle\textifclk{\char 155\relax}}.\,Q]\\}$}}}}}}$ [T-Call]
$\displaystyle\displaystyle{\hbox{\hskip
123.60527pt\vbox{\hbox{\hskip-123.60526pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\
\vdash\ X:\mathbb{T}_{1},\dotsc,\mathbb{T}_{n}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{end}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall i\in
1..n\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{i}}\
\vdash\ d_{i}:\mathbb{T}_{i}$}}}}}\vbox{}}}\over\hbox{\hskip
61.32365pt\vbox{\vbox{}\hbox{\hskip-61.32365pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}},\dotsc,{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{n}},{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}\
\vdash\ X\langle d_{1},\dotsc,d_{n}\rangle$}}}}}}$ [T-Def]
$\displaystyle\displaystyle{\hbox{\hskip
136.2839pt\vbox{\hbox{\hskip-136.2839pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta},X:\mathbb{T}_{1},\dotsc,\mathbb{T}_{n}\cdot
x_{1}:\mathbb{T}_{1},\dotsc,x_{n}:\mathbb{T}_{n}\ \vdash\ P$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta},X:\mathbb{T}_{1},\dotsc,\mathbb{T}_{n}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash\ Q$}}}}\vbox{}}}\over\hbox{\hskip
89.61577pt\vbox{\vbox{}\hbox{\hskip-89.61575pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash\ \textsf{def}\ X(x_{1}:\mathbb{T}_{1},\dotsc,x_{n}:\mathbb{T}_{n})=P\
\textsf{in}\ Q$}}}}}}$ [T-+] $\displaystyle\displaystyle{\hbox{\hskip
59.08119pt\vbox{\hbox{\hskip-59.08119pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash\ P_{1}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash\ P_{2}$}}}}\vbox{}}}\over\hbox{\hskip
34.8451pt\vbox{\vbox{}\hbox{\hskip-34.8451pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash\ P_{1}+P_{2}$}}}}}}$ [T-Lift] $\displaystyle\displaystyle{\hbox{\hskip
23.1406pt\vbox{\hbox{\hskip-23.14058pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash\ P$}}}\vbox{}}}\over\hbox{\hskip
23.15173pt\vbox{\vbox{}\hbox{\hskip-23.15173pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash_{\emptyset}\ P$}}}}}}$ [T-$\displaystyle\epsilon$]
$\displaystyle\displaystyle{\hbox{\hskip
11.73615pt\vbox{\hbox{\hskip-11.73613pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{gc}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma})$}}}\vbox{}}}\over\hbox{\hskip
31.6996pt\vbox{\vbox{}\hbox{\hskip-31.6996pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash_{\\{s\\}}\ s:\epsilon$}}}}}}$ [T-$\displaystyle\sigma_{1}$]
$\displaystyle\displaystyle{\hbox{\hskip
63.46957pt\vbox{\hbox{\hskip-63.46956pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}\vdash_{\\{s\\}}\
s:\sigma$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash\ w:\mathbb{T}$}}}}\vbox{}}}\over\hbox{\hskip
110.06503pt\vbox{\vbox{}\hbox{\hskip-110.06502pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{m}(\mathbb{T})\cdot\epsilon\ \vdash_{\\{s\\}}\
s:(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\triangleright\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\triangleleft\textsf{m}\langle w\rangle)\cdot\sigma$}}}}}}$
[T-$\displaystyle\sigma_{2}$] $\displaystyle\displaystyle{\hbox{\hskip
86.5077pt\vbox{\hbox{\hskip-86.5077pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\mathbb{M}\ \vdash_{\\{s\\}}\ s:\sigma$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash\ w:\mathbb{T}$}}}}\vbox{}}}\over\hbox{\hskip
111.50777pt\vbox{\vbox{}\hbox{\hskip-111.50777pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{m}(\mathbb{T})\cdot\mathbb{M}\ \vdash_{\\{s\\}}\
s:(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\triangleright\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\triangleleft\textsf{m}\langle w\rangle)\cdot\sigma$}}}}}}$
[T-$\displaystyle\sigma_{w}$] $\displaystyle\displaystyle{\hbox{\hskip
101.94252pt\vbox{\hbox{\hskip-101.94252pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}=({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{0}}\rightsquigarrow{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}}),{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}}\
\vdash_{\Sigma}\ s:\sigma$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{gc}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{0}},{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}})$}}}}}\vbox{}}}\over\hbox{\hskip
29.23686pt\vbox{\vbox{}\hbox{\hskip-29.23685pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash_{\Sigma}\ s:\sigma$}}}}}}$ [T-$\displaystyle|$]
$\displaystyle\displaystyle{\hbox{\hskip
96.99237pt\vbox{\hbox{\hskip-96.99236pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}}\
\vdash_{\Sigma_{1}}\ P_{1}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}}\
\vdash_{\Sigma_{2}}\ P_{2}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma_{1}\cap\Sigma_{2}=\emptyset$}}}}}\vbox{}}}\over\hbox{\hskip
53.55896pt\vbox{\vbox{}\hbox{\hskip-53.55896pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}},{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}}\
\vdash_{\Sigma_{1}\cup\Sigma_{2}}\ P_{1}\ \,|\,\ P_{2}$}}}}}}$
[T-$\displaystyle\nu$] $\displaystyle\displaystyle{\hbox{\hskip
140.95451pt\vbox{\hbox{\hskip-140.9545pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}=\\{s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\tau_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}}\\}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\in\bm{\rho}}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
s\not\in{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle(\\{s\\}\,;\mathcal{R})$-$\displaystyle\textnormal{$\displaystyle\varphi_{\texttt{s}}$}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}\
\vdash_{\Sigma}\ P$}}}}}}\vbox{}}}\over\hbox{\hskip
47.19511pt\vbox{\vbox{}\hbox{\hskip-47.1951pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash_{\Sigma\setminus\\{s\\}}\ (\nu
s\\!:\\!{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}})\,P$}}}}}}$
Figure 6: Typing rules $\displaystyle\displaystyle{\hbox{\hskip
2.5pt\vbox{\hbox{\hskip-2.5pt\hbox{\hbox{$\displaystyle\displaystyle\
$}}}\vbox{}}}\over\hbox{\hskip
14.1667pt\vbox{\vbox{}\hbox{\hskip-14.1667pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{end}}(\emptyset)$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
95.99164pt\vbox{\hbox{\hskip-95.99162pt\hbox{\hbox{$\displaystyle\displaystyle\forall
i\in 1..n\ \cdot\
\textnormal{{basic}}(\mathbb{T}_{i})\>\>\>\lor\>\>\>x_{i}:\mathbb{T}_{i}\
\vdash\ x_{i}:\textsf{{end}}$}}}\vbox{}}}\over\hbox{\hskip
40.89325pt\vbox{\vbox{}\hbox{\hskip-40.89325pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{end}}(x:\mathbb{T}_{1},\dotsc,x_{n}:\mathbb{T}_{n})$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
42.38342pt\vbox{\hbox{\hskip-42.38342pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{end}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{end}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}})$}}}}\vbox{}}}\over\hbox{\hskip
22.1056pt\vbox{\vbox{}\hbox{\hskip-22.1056pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{end}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}},{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}})$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
92.35352pt\vbox{\hbox{\hskip-92.35352pt\hbox{\hbox{$\displaystyle\displaystyle\forall
i\in
1..n,\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\in\bm{\rho}\ \cdot\
s_{i}[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\tau_{i}\ \vdash\
s_{i}[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\textsf{{end}}$}}}\vbox{}}}\over\hbox{\hskip
55.87445pt\vbox{\vbox{}\hbox{\hskip-55.87444pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{end}}(s_{i}[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\tau_{1},\dotsc,s_{i}[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\tau_{n})$}}}}}}$ Figure 7: Predicate
end(${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$)
$\displaystyle\displaystyle{\hbox{\hskip
2.5pt\vbox{\hbox{\hskip-2.5pt\hbox{\hbox{$\displaystyle\displaystyle\
$}}}\vbox{}}}\over\hbox{\hskip
11.11115pt\vbox{\vbox{}\hbox{\hskip-11.11113pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{gc}}(\emptyset)$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
11.73615pt\vbox{\hbox{\hskip-11.73613pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{gc}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma})$}}}\vbox{}}}\over\hbox{\hskip
29.72046pt\vbox{\vbox{}\hbox{\hskip-29.72044pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{gc}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\epsilon)$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
59.24658pt\vbox{\hbox{\hskip-59.24658pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{basic}}(\mathbb{T})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{gc}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\mathbb{M})$}}}}\vbox{}}}\over\hbox{\hskip
52.41318pt\vbox{\vbox{}\hbox{\hskip-52.41316pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{gc}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{m}(\mathbb{T})\cdot\mathbb{M})$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
72.2814pt\vbox{\hbox{\hskip-72.28139pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}={\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}},s^{\prime}[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}^{\prime}$}}]:\mathbb{T}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{gc}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\mathbb{M})$}}}}\vbox{}}}\over\hbox{\hskip
52.41318pt\vbox{\vbox{}\hbox{\hskip-52.41316pt\hbox{\hbox{$\displaystyle\displaystyle\textnormal{{gc}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{m}(\mathbb{T})\cdot\mathbb{M})$}}}}}}$ Figure 8: The garbage
collector predicate
gc(${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$)
$\displaystyle
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{m}(\mathbb{T})\cdot\epsilon\rightsquigarrow{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\mathbb{M}$
$\displaystyle={\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{m}(\mathbb{T})\cdot\mathbb{M}$ $\displaystyle
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{m}(\mathbb{T})\cdot\epsilon\rightsquigarrow{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\textit{
when
}s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\mathbb{M}\not\in{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$
$\displaystyle={\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\,!\,\textsf{m}(\mathbb{T})\cdot\epsilon$ Figure 9: Message insertion
function
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}$$\rightsquigarrow$${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$

Our type system is defined by the typing rules in fig. 6. Below we explain
them in detail. Typing judgements are of the form:
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash\ P$ reading “process $P$ is well typed under type contexts
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}$
and
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$”;
and
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash\ d:\mathbb{T}$ reading “value (or variable, or channel) $d$ is of type
$\mathbb{T}$ under type context
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$”.

[T-$\bm{0}$]

The inaction process $\bm{0}$ is typed by a context that is “end typed”,
determined by the predicate
end(${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$)—defined
in fig. 7. The predicate holds:  (i) if
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}=\emptyset$;
(ii) if
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$
consists of variables, then it holds if all the variables are either of a
basic type, or can be typed by end; and  (iii) if
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$
consists of sessions with roles, then it holds if all the channels can be
typed by end.

[T-Var]

A variable or session with role $c$ has type $\mathbb{T}$ in a context only
containing the mapping of $c$ to $\mathbb{T}$.

[T-Val]

A value $v$ is typed by a basic type $\mathbb{B}$ if $v$ is contained in the
set of that basic type. E.g., $42:\mathbb{N}$ is typed under an empty context
$\emptyset$ since $42\in\mathbb{N}$.

[T-X]

A process variable $X$ is typed to an $n$-tuple of types
$\mathbb{T}_{1},\dotsc,\mathbb{T}_{n}$ under context
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}$,
if
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}$
maps the process variable to the same $n$-tuple of types.

[T-$\oplus$]

The _selection_ process
$c\oplus[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{k}$}}]\,!\,\textsf{m${}_{k}$}\langle d\rangle.\,P$ is typed under a
context which maps the sending channel $c$ to a selection session type
$\oplus_{i\in
I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q${}_{i}$}}\,!\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i}\\}$, where
a selection option matches the send process, i.e., $k\in I$. The context
should match the payload $d$ to the type indicated in the selection
($\mathbb{T}_{k}$), and continuation process $P$ should be typed under the
continuation type $\mathbb{S}_{k}$.

[T-$\,\&$]

The _branching_ process $c\,\&_{i\in
I}\\{[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{i}$}}]\,?\,\textsf{m${}_{i}$}(x_{i}).P_{i}\\}$ is typed under a context
which maps the receiving channel $c$ to a branch type $\,\&_{i\in
I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{i}$}}\,?\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i}\\}$, where
all roles and message labels of each branch match. Every continuation process
$P_{i}$ must be typed under the continuation type $\mathbb{S}_{i}$ and payload
typed by $\mathbb{T}_{i}$. If the process is a _timeout_ branch $c\,\&_{i\in
I}\\{[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{i}$}}]\,?\,\textsf{m${}_{i}$}(x_{i}).P_{i},\
{\scriptstyle\textifclk{\char 155\relax}}.\,Q\\}$, then it should be typed by
a session type also containing a timeout continuation $\,\&_{i\in
I}\\{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{i}$}}\,?\,\textsf{m${}_{i}$}(\mathbb{T}_{i}).\mathbb{S}_{i},\
{\scriptstyle\textifclk{\char 155\relax}}.\,\mathbb{S}^{\prime}\\}$, and the
timeout process $Q$ must be typed by $\mathbb{S}^{\prime}$.

[T-Call]

A process _call_ $X\langle d_{1},\dotsc,d_{n}\rangle$ is correctly typed if
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}$
types the process variable to a $n$-tuple of types
$\mathbb{T}_{1},\dotsc,\mathbb{T}_{n}$ and
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$
maps each parameter $d_{i}$ to the corresponding $\mathbb{T}_{i}$ (for $i\in
1..n$). Any remaining channels in
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$
cannot be open, and hence must be end typed.

[T-Def]

Process _declaration_ $X(x_{1}:\mathbb{T}_{1},\dotsc,x_{n}:\mathbb{T}_{n})=P\
$ is well typed if $P$ is self-contained, i.e., contexts containing the types
of the declaration parameters (along with any previous
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}$)
should type $P$. Process _definition_ $\textsf{def}\
X(x_{1}:\mathbb{T}_{1},\dotsc,x_{n}:\mathbb{T}_{n})=P\ \textsf{in}\ Q$ is
typed under
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$
if its declaration is well typed and $Q$ is typed under
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$
and
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}$
composed with the new process variable.

[T-+]

Non-deterministic choice is well typed if processes are typed by
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$
in isolation. This is in line with how _case_ or _if-then-else_ processes are
typed.

[T-Lift]

We annotate the typing judgement
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\vdash
P$ with the buffer-tracker to obtain
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash_{\Sigma}P$, denoting that the sessions in $\Sigma$ occur in $P$. The
lifting rule annotates the typing judgement with an empty buffer-tracker if
the buffer-less judgement ($\vdash$) types $P$ (using the rules mentioned thus
far).

[T-$\epsilon$]

In standard asynchronous MPST theory, the empty buffer $s:\epsilon$ is typed
under the empty context $\emptyset$, ensuring a one-to-one correlation between
buffer types in the context and messages in a session buffer. However, since
our calculus _models message loss_ , it is possible that a context contains
buffer types for messages that have been dropped from the process buffer.
Thus, our theory types $s:\epsilon$ under a _garbage collected_
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$.
The predicate gc is defined in fig. 8, and states that valid leftover types
$\textnormal{{gc}}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma})$
are:  (i) empty;  (ii) empty buffer types;  (iii) message buffer types with
basic-type payloads; or  (iv) message buffer types with channel payloads that
are typed under
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$.

[T-$\sigma_{1}$] [T-$\sigma_{2}$]

An entry in a session buffer
$s:(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\triangleright\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\triangleleft\textsf{m}\langle w\rangle)\cdot\sigma$ is typed under a
context containing a mapping from $s$[ p] to a buffer type
q$\,!\,$m$($$\mathbb{T}$$)\cdot$$\mathbb{M}$, matching the recipient and
message label. The message payload $w$ must be of type $\mathbb{T}$, indicated
by the buffer type, and buffer continuation $s:\sigma$ should be typed under
the buffer continuation type $\mathbb{M}$ in the case that it is not empty
([T-$\sigma_{2}$]).

[T-$\sigma_{w}$]

Weakening allows a session buffer to be typed under a larger context if the
addition can be garbage collected and inserted into the original context using
the message insertion function (fig. 9). This is partial function that either
appends a message to an existing buffer type, or inserts it as the head of a
new buffer type. Put differently, weakening allows a buffer to be typed under
a larger context containing irrelevant types that can be garbage collected.

[T-$|$]

If a process $P_{1}$ is typed by
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}}$,
and process $P_{2}$ is typed by
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}}$,
then the composition
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{1}}$,${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma_{2}}$
types the _parallel_ composition $P_{1}$ $\,|\,$ $P_{2}$. It is also required
that parallel processes _cannot_ each contain a buffer for the same session
$s$. This guarantees the uniqueness of one session buffer per restricted
session.

[T-$\nu$]

Session restriction $(\nu
s\\!:\\!{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}})\,P$
requires session $s$ to be instantiated with a
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}$
mapping each session with role to its session-buffer type.
$\varphi_{\texttt{s}}$(${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}$)
must hold to ensure subject reduction, as discussed in § 3.3. Session $s$
should not be present in a previous context
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$,
and process $P$ should be typed under the composition of the previous and
newly instantiated context with the updated buffer-tracker
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma},{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}\
\vdash_{\Sigma}P$ (since the buffer for $s$ is contained in $P$).

######  Example 4 (Ping Pong: Type Context)

Recalling the ping pong example, the whole system can then be described by a
parallel composition of the three processes representing each role  p,  q,  r
together with an empty buffer, which is closed under a type context
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}$
with the following typing assumptions.

$\displaystyle\begin{array}[]{c}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}=\\{s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]:\mathbb{S}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}},\
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]:\mathbb{S}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}},s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}]:\mathbb{S}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}}\\}\\\\[8.00002pt] P_{\textit{ping}}=(\nu
s:{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma})\,\
P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}}\ \,|\,\
P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}}\ \,|\,\
P_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{r}}}\ \,|\,\ s:\epsilon\end{array}$

##  4 Type Properties

The main results of our MPST system for MAG$\pi$ processes are _subject
reduction_ (theorem 4.1) and _session fidelity_ (theorem 4.2). It is key to
note that our results are parametric on the reliability function
$\mathcal{R}$. Thus, the theorems we present hold for _any_ configuration of
reliability, i.e., from _no_ reliable communication all the way to
_completely_ reliable networks.

In order to synchronise reliability assumptions between types and processes,
we define the _reliable process reduction_ $\longrightarrow_{\mathcal{R}}$,
such that $\longrightarrow_{\mathcal{R}}\ \subseteq\ \longrightarrow$.

######  Definition 11 (Reliable process reduction)

The reliable process reduction $\longrightarrow_{\mathcal{R}}$ is inductively
defined by the same reduction rules for $\longrightarrow$ (in fig. 2), with
the following changes 333For a fully unreliable network, i.e.,
$\forall\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\in\bm{\rho}\cdot\mathcal{R}(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}})=\emptyset$, $\longrightarrow_{\mathcal{R}}$ is equivalent to
$\longrightarrow$.:

$\displaystyle\begin{array}[]{lcr}\textbf{[R-${\scriptstyle\textifclk{\char
155\relax}}$]}&s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,\&_{i\in
I}\\{[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{i}$}}]\,?\,\textsf{m${}_{i}$}(x_{i}).P_{i},{\scriptstyle\textifclk{\char
155\relax}}.\,Q\\}\,|\,s:\sigma\longrightarrow_{\mathcal{R}}Q\,|\,s:\sigma&\text{if
}\exists k\in
I:\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p${}_{k}$}}\not\in\mathcal{R}(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}})\\\ \\\
\textbf{[R-$\bm{\downarrow}$]}&s:(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\triangleright\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\triangleleft\textsf{m}\langle
w\rangle)\cdot\sigma\longrightarrow_{\mathcal{R}}s:\sigma&\text{for
}\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}\not\in\mathcal{R}(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}})\end{array}$

Intuitively, the reliable process reduction disregards network faults for
reliable communication. Concretely, a timeout reduction [R-] is only possible
if _at least one role_ in the branch is unreliable; and message loss
[R-$\bm{\downarrow}$] can only occur for messages that are _not_ reliable from
the viewpoint of the sender. This ensures that no messages are ignored or lost
for reliable communication. Proofs of our technical results, along with any
auxiliary results, are given in appendices 0.A, 0.B and 0.C.

###  4.1 Subject Reduction

Using $\longrightarrow_{\mathcal{R}}$, we now present our result of _subject
reduction_. Intuitively, subject reduction states that, if a process $P$ is
typed under a safe context, and $P$ reliably reduces to some process
$P^{\prime}$, then the context also reduces (in 0 or 1 steps) to a safe
context, which types the new process $P^{\prime}$.

######  Theorem 4.1 (Subject Reduction)

${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash_{\Sigma}\ P\ \ \textit{and }\
(\Sigma;\mathcal{R})\textnormal{-}\textnormal{$\varphi_{\texttt{s}}$}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma})\
\ \textit{and }\ P\rightarrow_{\mathcal{R}}P^{\prime}\ \implies\\\
\exists{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}:{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\rightarrow_{(\Sigma;\mathcal{R})}^{\\{0,1\\}}{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}\
\ \textit{and }\
(\Sigma;\mathcal{R})\textnormal{-}\textnormal{$\varphi_{\texttt{s}}$}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}})\
\ \textit{and }\
{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma^{\prime}}\vdash_{\Sigma}P^{\prime}$

A key novel result of our type system is that no unexpected network failures
can occur at runtime, i.e., a process always has a failure-handling
subprotocol defined for unreliable communication. This follows from the
definition of our safety property $\varphi_{\texttt{s}}$ (def. 10) and holds
through subject reduction. We state the result in cor. 1. More precisely, this
corollary states that timeout branches are guaranteed to be defined for
unreliable communication. The inverse is stated in cor. 2, i.e., timeouts are
not defined for branches containing _only_ reliable sources.

######  Corollary 1 (Failure handling safety)

Given a reliability function $\mathcal{R}$ :
$\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}\not\in\mathcal{R}(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}})$ and
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash_{\Sigma}\ P$ with
$(\Sigma;\mathcal{R})$-$\textnormal{$\varphi_{\texttt{s}}$}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma})$
and $P\longrightarrow_{\mathcal{R}}^{*}P^{\prime}\equiv\mathbb{C}[Q]$ implies
$Q\neq
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,\&_{i\in
I}\\{\dots,[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{p}}]\,?\,\textsf{m}(x).Q^{\prime}\\}$. I.e., $Q$ cannot be a branch at  q
receiving from  p and not define a timeout.

######  Corollary 2 (Reliability adherence)

Given a reliability function $\mathcal{R}$ :
$\mathcal{R}(\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}})=\mathfrak{R}_{\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}}$ and
${\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Theta}\cdot{\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma}\
\vdash_{\Sigma}\ P$ with
$(\Sigma;\mathcal{R})$-$\textnormal{$\varphi_{\texttt{s}}$}({\color[rgb]{0.0546875,0.6796875,0.41015625}\definecolor[named]{pgfstrokecolor}{rgb}{0.0546875,0.6796875,0.41015625}\Gamma})$
and $P\longrightarrow_{\mathcal{R}}^{*}P^{\prime}\equiv\mathbb{C}[Q]$ implies
$Q\neq
s[\textsf{\color[rgb]{0.94921875,0.234375,0.234375}\definecolor[named]{pgfstrokecolor}{rgb}{0.94921875,0.234375,0.234375}
{q}}]\,\&_{i\in