Università di Torino,
Italyluca.ciccone@unito.ithttps://orcid.org/0000-0001-9515-5280 Università di
Genova, Italyfrancesco.dagnino@dibris.unige.ithttps://orcid.org/
0000-0003-3599-3535 Università di Torino,
Italyluca.padovani@unito.ithttps://orcid.org/0000-0001-9097-1297 Luca Ciccone,
Francesco Dagnino and Luca Padovani [500]Theory of computation Process calculi
[500]Theory of computation Type structures [300]Theory of computation Program
analysis John Q. Open and Joan R. Access 2 42nd Conference on Very Important
Topics (CVIT 2016) CVIT 2016 CVIT 2016 December 24–27, 2016 Little Whinging,
United Kingdom 42 23

# Fair Termination of Multiparty Sessions

Luca Ciccone  Francesco Dagnino  Luca Padovani

###### Abstract

There exists a broad family of multiparty sessions in which the progress of
one session participant is not unconditional, but depends on the choices
performed by other participants. These sessions fall outside the scope of
currently available session type systems that guarantee progress. In this work
we propose the first type system ensuring that well-typed multiparty sessions,
including those exhibiting the aforementioned dependencies, fairly terminate.
Fair termination is termination under a fairness assumption that disregards
those interactions deemed unfair and therefore unrealistic. Fair termination,
combined with the usual safety properties ensured within sessions, not only is
desirable _per se_ , but it entails progress and enables a compositional form
of static analysis such that the well-typed composition of fairly terminating
sessions results in a fairly terminating program.

###### keywords:

Multiparty sessions, fair termination, fair subtyping, deadlock freedom

##  1 Introduction

Sessions [23, 24, 26] are private conversations among processes following a
protocol specification called session type. The decomposition of a distributed
program into sessions enables its modular static analysis and the enforcement
of useful properties through a type system. Examples of such properties are
_communication safety_ (no message of the wrong type is ever exchanged),
_protocol fidelity_ (messages are exchanged in the order prescribed by session
types) and _deadlock freedom_ (the program keeps running unless all sessions
have terminated). These are all instances of _safety properties_ , implying
that “nothing bad” happens. In general, one is also interested in reasoning
and possibly enforcing _liveness properties_ , those implying that “something
good” happens [38]. Examples of liveness properties are _junk freedom_ (every
message is eventually received), _progress_ (every non-terminated participant
of a session eventually performs an action) and _termination_ (every session
eventually comes to an end).

An enduring limitation of current type systems for multiparty sessions is that
_they ensure progress for any participant of a session only when such progress
can be established independently of the choices performed by the other
participants_. To illustrate the impact of this limitation, consider a session
made of three participants named
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}buyer}$,
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}$
and
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}carrier}$
in which the buyer aims at purchasing an unspecified number of items from the
seller and the seller relies on a carrier for delivering the purchased items
to the buyer. The buyer behaves according to the session type $S$ that
satisfies the equation

$S=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.S+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}pay}.{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$
(1)

indicating that it either pays the seller or it adds an item to the shopping
cart and then repeats the same behavior. In this session type, add and pay are
messages targeted to the participant with role
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}$.
In turn, the seller accepts add messages from the buyer until a pay message is
received, at which point it instructs the carrier to ship the items. Thus, its
behavior is described by the session type $T$ that satisfies the equation

$T=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}buyer}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.T+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}buyer}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}pay}.\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}carrier}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}ship}.{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$
(2)

Finally, the carrier just waits for the ship message from the seller. So, its
behavior is described by the session type

$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}ship}.{?}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$
(3)

No available type system is able to guarantee progress for every participant
of this multiparty session. What makes this session somewhat difficult to
reason about is that _the progress of the carrier is not unconditional but
depends on the choices performed by the buyer_ : the carrier can make progress
only if the buyer eventually pays the seller.

In this work we propose a type system that guarantees the _fair termination_
of sessions, that is termination under a _fairness assumption_. The assumption
we make is an instance of _relative fairness_ [44] and can be roughly spelled
out as follows:

If termination is always possible, then it is inevitable. (4)

The multiparty session sketched above terminates under this fairness
assumption: since it is always possible for the buyer to pay the seller and
terminate, in every fair execution of the session the buyer eventually pays
the seller, even though we do not know (nor do we impose) an upper bound to
the number of items that the buyer may add to the shopping cart. Simply, the
non-terminating execution of the session in which the buyer keeps adding items
to the shopping cart but never pays is assumed unrealistic and so it can be
ignored insofar as termination is concerned.

The reader might wonder why we focus on fair termination instead of
considering some fair version of progress. There are three reasons why we
think that fair termination is overall more appropriate than just progress.
First of all, ensuring that sessions (fairly) terminate is consistent with the
usual interpretation of the word “session” as an activity that lasts for a
_finite amount of time_ , even when the maximum duration of the activity is
not known _a priori_. Second, _fair termination implies progress_ when it is
guaranteed along with the usual safety properties of sessions. Indeed, if the
session eventually terminates, it must be the case that any non-terminated
participant (think of the carrier waiting for a ship message) is guaranteed to
eventually make progress, even when such progress _depends_ on choices made by
other participants (like the buyer sending pay to the seller). Last but not
least, _fair session termination enables compositional reasoning_ in the
presence of multiple sessions. This is not true for progress: if an action on
a session $s$ is blocked by actions on a different session $t$, then knowing
that the session $t$ enjoys progress does not necessarily guarantee that the
action on $s$ will eventually be performed (the interaction on $t$ might
continue forever). On the contrary, knowing that $t$ fairly terminates
guarantees that the action on $s$ will eventually be scheduled and performed,
so that $s$ may in turn progress towards termination.

Remarkably, the fairness assumption alone does not suffice to turn any
multiparty session type system into one that ensures fair termination. In
fact, there are several sources of potentially non-terminating behaviors that
must be ruled out in well-typed processes:

  1. 1.

Fairly terminating (and even finite) sessions may be chained, nested,
interleaved in such a way that some pending activities are postponed forever.
To avoid this problem, our type system makes sure that the effort required by
a well-typed process in order to terminate remains finite. At the same time,
it does not (always) prevent the modeling of processes that create an
unbounded number of sessions.

  2. 2.

The type-level constraints usually imposed to well-typed sessions – _duality_
[23, 24, 26], _liveness_ [45], _coherence_ [9], just to mention a few – are in
general too weak to entail fair session termination. Our type system adopts a
stronger notion of “correct multiparty session” that entails fair termination.
Variants of this notion have already appeared in the literature [5, 41], but
we use it here for the first time to relate types and processes.

  3. 3.

A certain mismatch is usually allowed between the structure of session types
and the structure of the processes that adhere to those types. This mismatch
is formalized by a subtyping relation for session types which, in its standard
formulation [22], may introduce non-terminating behaviors. Our type system
adopts _fair subtyping_ [41], a liveness-preserving refinement of the standard
subtyping relation for session types [22].

#### Summary of contributions.

We present the first type system ensuring the fair termination of multiparty
sessions and capable of addressing a number of natural communication patterns
that are out of scope of existing multiparty session type systems [45, 47]. We
exploit the compositional reasoning enabled by fair termination to prove a
strong soundness result whereby a well-typed composition of fairly terminating
sessions is a fairly terminating program (Theorem 5.4). This result scales
smoothly also in presence of session chaining, session nesting, session
interleaving, session delegation and dynamic session creation. In sharp
contrast, the liveness properties ensured by previous multiparty session type
systems are either limited to single-session programs [45, 47] or require a
richer type structure [42, 14]. Our contributions extend and generalize
previous work on the fair termination of binary sessions [13] and allow for
the modeling of (intra-session) cyclic network topologies and of multiparty
sessions that cannot be decomposed into equivalent (well-typed) binary
sessions. Decidability of type checking is not substantially more difficult
than the same problem in the binary setting [13]. _En passant_ , in this paper
we also provide a new characterization of fair subtyping for (multiparty)
session types (Table 5) that is substantially simpler than those appearing in
previous works [39, 41, 12, 13].

#### Structure of the paper.

We recall the key notions related to fair termination (Section 2) before
presenting our language of multiparty sessions (Section 3). Then, we define
multiparty session types and fair subtyping (Section 4) and present the typing
rules and the soundness properties of the type system (Section 5). In the
latter part of the paper we illustrate a few more advanced examples of well-
typed processes (Section 6), we discuss related work in more detail (Section
7) and we provide hints at further developments (Section 8). Additional
technical material and all the proofs of the presented results can be found in
the Appendix, which we provide for completeness but is not necessary for
reviewing the submission.

##  2 Fair Termination

Since the notion of fair termination will apply to several different entities
(session types, multiparty sessions, processes) here we define it for a
generic reduction system. Later on we will show various instantiations of this
definition. A _reduction system_ is a pair $(\mathcal{S},{\rightarrow})$ where
$\mathcal{S}$ is a set of _states_ and
${\rightarrow}\subseteq\mathcal{S}\times\mathcal{S}$ is a _reduction
relation_. We adopt the following notation: we let $C$ and $D$ range over
states; we write $C\rightarrow$ if there exists $D\in\mathcal{S}$ such that
$C\rightarrow D$; we write $C\arrownot\rightarrow$ if not $C\rightarrow$; we
write $\Rightarrow$ for the reflexive, transitive closure of $\rightarrow$. We
say that $D$ is _reachable_ from $C$ if $C\Rightarrow D$.

As an example, the reduction system $(\\{A,B\\},\\{(A,A),(A,B)\\})$ models an
entity that can be in two states, $A$ or $B$, and such that the entity may
perform a reduction to remain in state $A$ or a reduction to move from state
$A$ to state $B$. To formalize the evolution of an entity from a particular
state we define _runs_.

######  Definition 2.1 (runs and maximal runs).

A _run_ of $C$ is a (finite or infinite) sequence $C_{0}C_{1}\dots C_{i}\dots$
of states such that $C_{0}=C$ and $C_{i}\rightarrow C_{i+1}$ for every valid
$i$. A run is _maximal_ if either it is infinite or if its last state $C_{n}$
is such that $C_{n}\arrownot\rightarrow$.

Hereafter we let $\rho$ range over runs. Each run in the previously defined
reduction system is either of the form $A^{n}$ – a finite sequence of $A$ – or
of the form $A^{n}B$ – a finite sequence of $A$ followed by one $B$ – or
$A^{\omega}$ – an infinite sequence of $A$. Among these, the runs of the form
$A^{n}B$ and $A^{\omega}$ are maximal, whereas no run of the form $A^{n}$ is
maximal.

We now use runs to define different termination properties of states: we say
that $C$ is _weakly terminating_ if there exists a maximal run of $C$ that is
finite; we say that $C$ is _terminating_ if every maximal run of $C$ is
finite; we say that $C$ is _diverging_ if every maximal run of $C$ is
infinite. _Fair termination_ [20] is a termination property that only
considers a subset of all (maximal) runs of a state, those that are considered
to be “realistic” or “fair” according to some fairness assumption. The
assumption that we make in this work, and that we stated in words in (4), is
formalized thus:

######  Definition 2.2 (fair run).

A run is _fair_ if it contains finitely many weakly terminating states.
Conversely, a run is _unfair_ if it contains infinitely many weakly
terminating states.

Continuing with the previous example, the runs of the form $A^{n}$ and
$A^{n}B$ are fair, whereas the run $A^{\omega}$ is unfair. In general, an
unfair run is an execution in which termination is always within reach, but is
never reached.

A key requirement of any fairness assumption is that it must be possible to
extend every finite run to a maximal fair one. This property is called
_feasibility_ [4, 46] or _machine closure_ [36]. It is easy to see that our
fairness assumption is feasible:

######  Lemma 2.3.

If $\rho$ is a finite run, then there exists $\rho^{\prime}$ such that
$\rho\rho^{\prime}$ is a maximal fair run.

Fair termination is finiteness of all maximal fair runs:

######  Definition 2.4 (fair termination).

We say that $C$ is _fairly terminating_ if every maximal fair run of $C$ is
finite.

In the reduction system given above, $A$ is fairly terminating. Indeed, all
the maximal runs of the form $A^{n}B$ are finite whereas $A^{\omega}$, which
is the only infinite fair run of $A$, is unfair.

For the particular fairness assumption that we make, it is possible to provide
a sound and complete characterization of fair termination that does not
mention fair runs. This characterization will be useful to relate fair
termination with the notion of correct multiparty session (Definition 4.2) and
the soundness property of the type system (Theorem 5.4).

######  Theorem 2.5.

Let $(\mathcal{S},{\rightarrow})$ be a reduction system and $C\in\mathcal{S}$.
Then $C$ is fairly terminating if and only if every state reachable from $C$
is weakly terminating.

######  Remark 2.6 (fair reachability of predicates [44]).

Most fairness assumptions have the form “if _something_ is infinitely often
possible then _something_ happens infinitely often” and, in this respect, our
formulation of fair run (Definition 2.2) looks slightly unconventional.
However, it is not difficult to realize that Definition 2.2 is an instance of
the notion of fair reachability of predicates as defined by Queille and
Sifakis [44, Definition 3]. According to Queille and Sifakis, a run $\rho$ is
fair with respect to some predicate $\mathcal{C}\subseteq\mathcal{S}$ if,
whenever in $\rho$ there are infinitely many states from which a state in
$\mathcal{C}$ is reachable, then in $\rho$ there are infinitely many
occurrences of states in $\mathcal{C}$. When we take $\mathcal{C}$ to be
$\arrownot\rightarrow$, that is the set of terminated states that do not
reduce, pretending that irreducible states should occur infinitely often in
the run is nonsensical. So, the fairness assumption boils down to assuming
that such states should _not_ be reachable infinitely often, which is
precisely the formulation of Definition 2.2. $\lrcorner$

##  3 A Calculus of Multiparty Sessions

In this section we define the calculus for multiparty sessions on which we
apply our static analysis technique. The calculus is an extension of the one
presented by Ciccone and Padovani [13] to multiparty sessions in the style of
Scalas and Yoshida [45].

We use an infinite set of _variables_ ranged over by $x$, $y$, $z$, an
infinite set of _session names_ ranged over by $s$ and $t$, a set of _roles_
ranged over by
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$,
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}$,
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}r}$,
a set of _message tags_ ranged over by m, and a set of _process names_ ranged
over by $A$, $B$, $C$. In the literature of sessions tags are usually called
labels. We adopt a different terminology to avoid confusion with another
notion of label that we introduce in Section 4. We use roles to distinguish
the participants of a session. In particular, an _endpoint_
$s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]$
consists of a session name $s$ and a role
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$
and is used by the participant with role
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$
to interact with the other participants of the session $s$. We use $u$ and $v$
to range over _channels_ , which are either variables or session endpoints. We
write $\overline{x}$ and $\overline{u}$ to denote possibly empty sequences of
variables and channels, extending this notation to other entities. We use
$\pi$ to range over the elements of the set $\\{\mathsf{?},\mathsf{!}\\}$ of
_polarities_ , distinguishing input actions ($\mathsf{?}$) from output actions
($\mathsf{!}$).

Table 1: Syntax of processes.

$\displaystyle\begin{array}[t]{@{}rcll@{}}P,Q,R&::=&&\textbf{Process}\\\
&&\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}&\text{termination}\\\
&|&\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,u.{P}&\text{signal
input}\\\
&|&u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{?}(x).P&\text{channel
input}\\\
&|&u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\pi\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.P_{i}\\}_{i\in
I}&\text{tag input/output}\\\
&|&(s)(P_{1}\mathbin{\mid}\cdots\mathbin{\mid}P_{n})&\text{session}\\\
\end{array}\leavevmode\nobreak\ \begin{array}[t]{@{}rcll@{}}\\\
&|&A\langle\overline{u}\rangle&\text{invocation}\\\
&|&\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,u&\text{signal
output}\\\
&|&u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{!}v.P&\text{channel
output}\\\ &|&P\oplus Q&\text{choice}\\\ &|&\lceil u\rceil P&\text{cast}\\\
\end{array}$

A _program_ is a finite set of _definitions_ of the form
$A(\overline{x})\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}P$,
at most one for each process name, where $P$ is a term generated by the syntax
shown in Table 1. The term done denotes the terminated process that performs
no action. The term $A\langle\overline{u}\rangle$ denotes the invocation of
the process with name $A$ passing the channels $\overline{u}$ as arguments.
When $\overline{u}$ is empty we just write $A$ instead of $A\langle\rangle$.
The term
$\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,u$
denotes the process that sends a termination signal on the channel $u$,
whereas
$\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,u.P$
denotes the process that waits for a termination signal from channel $u$ and
then continues as $P$. The term
$u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{!}v.P$
denotes the process that sends the channel $v$ on the channel $u$ to the role
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$
and then continues as $P$. Dually,
$u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{?}(x).P$
denotes the process that receives a channel from the role
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$
on the channel $u$ and then continues as $P$ where $x$ is replaced with the
received channel. The term
$u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\pi\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.P_{i}\\}_{i\in
I}$ denotes a process that exchanges one of the tags
$\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}$
on the channel $u$ with the role
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$
and then continues as $P_{i}$. Whether the tag is sent or received depends on
the polarity $\pi$ and, as it will be clear from the operational semantics,
the polarity $\pi$ also determines whether the process behaves as an internal
choice (when $\pi$ is $\mathsf{!}$) or an external choice (when $\pi$ is
$\mathsf{?}$). In the first case the process chooses _actively_ the tag being
sent, whereas in the second case the process reacts _passively_ to the tag
being received. We assume that $I$ is finite and non-empty and also that the
tags
$\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}$
are pairwise distinct. For brevity, we write
$u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\pi\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}.P_{k}$
instead of
$u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\pi\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.P_{i}\\}_{i\in
I}$ when $I$ is the singleton set $\\{k\\}$. The term $P\oplus Q$ denotes a
process that non-deterministically behaves either as $P$ or as $Q$.

A term $(s)(P_{1}\mathbin{\mid}\cdots\mathbin{\mid}P_{n})$ with $n\geq 1$
denotes the parallel composition of $n$ processes, each of them being a
participant of the session $s$. Each process is associated with a distinct a
role
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}$
and communicates in $s$ through the endpoint
$s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]$.
Combining session creation and parallel composition in a single form is common
in session type systems based on linear logic [6, 48, 37] and helps
guaranteeing deadlock freedom. Finally, a _cast_ $\lceil u\rceil P$ denotes a
process that behaves exactly as $P$. This form is only relevant for the type
system (Section 5) and denotes the fact that the type of $u$ is subject to an
application of subtyping.

The free and bound names of a process are defined as usual, the latter ones
being easily recognizable as they occur within round parenteses. We write
$\mathsf{fn}(P)$ for the set of free names of $P$ and we identify processes
modulo renaming of bound names. Note that $\mathsf{fn}(P)$ may contain
variables and session names, but not endpoints. Occasionally we write
$A(\overline{x})\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}P$
as a predicate or side condition, meaning that $P$ is the process associated
with the process name $A$. For each of such definitions we assume that
$\mathsf{fn}(P)\subseteq\\{\overline{x}\\}$.

Table 2: Structural precongruence of processes.

$\displaystyle\begin{array}[]{@{}lr@{~}c@{~}ll@{}}\hypertarget{rule:s-par-
comm}{\textup{{\small[s-par-
comm]}}}&(s)(\overline{P}\mathbin{\mid}P\mathbin{\mid}Q\mathbin{\mid}\overline{Q})\leavevmode\nobreak\
&\preccurlyeq\hfil\leavevmode\nobreak\
&(s)(\overline{P}\mathbin{\mid}Q\mathbin{\mid}P\mathbin{\mid}\overline{Q})\\\
\hypertarget{rule:s-par-assoc}{\textup{{\small[s-par-
assoc]}}}&(s)(\overline{P}\mathbin{\mid}(t)(R\mathbin{\mid}\overline{Q}))\leavevmode\nobreak\
&\preccurlyeq\hfil\leavevmode\nobreak\
&(t)((s)(\overline{P}\mathbin{\mid}R)\mathbin{\mid}\overline{Q})&\text{if
$s\in\mathsf{fn}(R)$}\\\ \hypertarget{rule:s-cast-
comm}{\textup{{\small[s-cast-comm]}}}&\lceil u\rceil{\lceil
v\rceil{P}}\leavevmode\nobreak\ &\preccurlyeq\hfil\leavevmode\nobreak\ &\lceil
v\rceil{\lceil u\rceil{P}}\\\ \hypertarget{rule:s-cast-
new}{\textup{{\small[s-cast-new]}}}&(s)(\lceil
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil
P\mathbin{\mid}\overline{Q})\leavevmode\nobreak\
&\preccurlyeq\hfil\leavevmode\nobreak\ &(s)(P\mathbin{\mid}\overline{Q})\\\
\hypertarget{rule:s-cast-swap}{\textup{{\small[s-cast-swap]}}}&(s)(\lceil
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil{P}\mathbin{\mid}\overline{Q})\leavevmode\nobreak\
&\preccurlyeq\hfil\leavevmode\nobreak\ &\lceil
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil{(s)(P\mathbin{\mid}\overline{Q})}&\text{if
$s\neq t$}\\\
\hypertarget{rule:s-call}{\textup{{\small[s-call]}}}&A\langle\overline{u}\rangle\leavevmode\nobreak\
&\preccurlyeq\hfil\leavevmode\nobreak\
&P\\{\overline{u}/\overline{x}\\}&\text{if
$A(\overline{x})\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}P$}\end{array}$

Table 3: Reduction of processes.
$\displaystyle{\vbox{\hbox{\hypertarget{rule:r-choice}{{{\small[r-choice]}}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
24.94824pt\vbox{\vbox{}\hbox{\hskip-24.94823pt\hbox{\hbox{$\displaystyle\displaystyle
P_{1}\oplus P_{2}\rightarrow P_{k}$}}}}}}$}}}\leavevmode\nobreak\
k\in\\{1,2\\}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:r-signal}{{{\small[r-signal]}}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
91.43137pt\vbox{\vbox{}\hbox{\hskip-91.43135pt\hbox{\hbox{$\displaystyle\displaystyle(s)(\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}].{P}\mathrel{|}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{1}]\mathrel{|}\cdots\mathrel{|}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{n}])\rightarrow
P$}}}}}}$}}}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:r-channel}{{{\small[r-channel]}}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
111.1498pt\vbox{\vbox{}\hbox{\hskip-111.14978pt\hbox{\hbox{$\displaystyle\displaystyle(s)(s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\mathsf{!}v.P\mathrel{|}s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{?}(x).Q\mathrel{|}\overline{R})\rightarrow(s)(P\mathrel{|}Q\\{v/x\\}\mathrel{|}\overline{R})$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:r-pick}{{{\small[r-pick]}}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
97.59802pt\vbox{\vbox{}\hbox{\hskip-97.59802pt\hbox{\hbox{$\displaystyle\displaystyle(s)(s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\mathsf{!}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.P_{i}\\}_{i\in
I}\mathrel{|}\overline{Q})\rightarrow(s)(s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}.P_{k}\mathrel{|}\overline{Q})$}}}}}}$}}}\leavevmode\nobreak\
k\in I\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:r-tag}{{{\small[r-tag]}}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
109.25359pt\vbox{\vbox{}\hbox{\hskip-109.25357pt\hbox{\hbox{$\displaystyle\displaystyle(s)(s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}.P\mathrel{|}s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{?}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.Q_{i}\\}_{i\in
I}\mathrel{|}\overline{R})\rightarrow(s)(P\mathrel{|}Q_{k}\mathrel{|}\overline{R})$}}}}}}$}}}\leavevmode\nobreak\
k\in I\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:r-par}{{{\small[r-par]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
13.13501pt\vbox{\hbox{\hskip-13.13501pt\hbox{\hbox{$\displaystyle\displaystyle
P\rightarrow Q$}}}\vbox{}}}\over\hbox{\hskip
41.15591pt\vbox{\vbox{}\hbox{\hskip-41.15591pt\hbox{\hbox{$\displaystyle\displaystyle(s)(P\mathrel{|}\overline{R})\rightarrow(s)(Q\mathrel{|}\overline{R})$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:r-cast}{{{\small[r-cast]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
13.13501pt\vbox{\hbox{\hskip-13.13501pt\hbox{\hbox{$\displaystyle\displaystyle
P\rightarrow Q$}}}\vbox{}}}\over\hbox{\hskip
24.97076pt\vbox{\vbox{}\hbox{\hskip-24.97076pt\hbox{\hbox{$\displaystyle\displaystyle\lceil
u\rceil{P}\rightarrow\lceil u\rceil{Q}$}}}}}}$}}}\penalty 50\hskip 20.00003pt
plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:r-struct}{{{\small[r-struct]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
62.48512pt\vbox{\hbox{\hskip-62.48512pt\hbox{\hbox{$\displaystyle\displaystyle
P\preccurlyeq P^{\prime}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle P^{\prime}\rightarrow
Q^{\prime}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
Q^{\prime}\preccurlyeq Q$}}}}}\vbox{}}}\over\hbox{\hskip
13.13501pt\vbox{\vbox{}\hbox{\hskip-13.13501pt\hbox{\hbox{$\displaystyle\displaystyle
P\rightarrow Q$}}}}}}$}}}$

The operational semantics of processes is given by the structural
precongruence relation $\preccurlyeq$ defined in Table 2 and the reduction
relation $\rightarrow$ defined in Table 3. As usual, structural precongruence
allows us to rearrange the structure of processes without altering their
meaning, whereas reduction expresses an actual computation or interaction
step. The adoption of a structural _pre_ congruence (as opposed to a more
common congruence relation) is not strictly necessary, but it simplifies the
technical development by reducing the number of cases we have to consider in
proofs without affecting the properties of the calculus in any way.

Rules [s-par-comm] and [s-par-assoc] state commutativity and associativity of
parallel composition of processes (we write $\overline{P}$ to denote possibly
empty parallel compositions of processes). In [s-par-assoc], the side
condition $s\in\mathsf{fn}(R)$ makes sure that $R$ is indeed a participant of
the session $s$. Note that this rule only states right-to-left associativity.
Left-to-right associativity is derivable from this rule and repeated uses of
[s-par-comm]. Rule [s-cast-comm] allows us to swap two consecutive casts. Rule
[s-cast-new] removes an unguarded cast on an endpoint of the restricted
session (we refer to this operation as “performing the cast”). Rule [s-cast-
swap] swaps a cast and a restricted session as long as the endpoint in the
cast refers to a different session. Finally, rule [s-call] unfolds a process
invocation to its definition. Hereafter, we write $\\{u/x\\}$ for the capture-
avoiding substitution of each free occurrence of $x$ with $u$ and
$\\{\overline{u}/\overline{x}\\}$ for its natural extension to equal-length
tuples of variables and names. The rules [s-cast-new], [s-cast-swap] and
[s-call] are not invertible: by [s-cast-new] casts can only be removed but
never added; by [s-cast-swap] casts can only be moved closer to their
restriction, so that they can be eventually performed by [s-cast-new]; by
[s-call] process invocations can only be unfolded.

The reduction relation is quite standard. Rule [r-choice] reduces $P_{1}\oplus
P_{2}$ to either $P_{1}$ or $P_{2}$, non deterministically. Rule [r-signal]
terminates a session in which all participants
($\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{1},\ldots,\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{n}$)
but one
($\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$)
are sending a termination signal and
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$
is waiting for it; the resulting process is the continuation of the
participant
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$.
Rule [r-channel] models the exchange of a channel among two participants of a
session. Rule [r-pick] models an internal choice whereby a process picks one
particular tag
$\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}$
to send on a session. Rule [r-tag] synchronizes two participants
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$
and
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}$
on the tag chosen by
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$.
Finally, rules [r-par], [r-cast] and [r-struct] close reductions under
parallel compositions and casts and by structural precongruence.

In the rest of this section we illustrate the main features of the calculus
with some examples. For none of them the existing multiparty session type
systems are able to guarantee progress.

######  Example 3.1 (purchase).

We model a particular instance of the buyer-seller-carrier interaction that we
have informally discussed in Section 1 with the following definitions:

Main
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}(s)(\textit{Buyer}\langle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}buyer}]\rangle\mathbin{\mid}\textit{Seller}\langle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}]\rangle\mathbin{\mid}\textit{Carrier}\langle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}carrier}]\rangle)$
$\displaystyle\textit{Buyer}(x)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}]\mathsf{!}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.\textit{Buyer}\langle
x\rangle,\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}pay}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,x\\}$
$\displaystyle\textit{Seller}(x)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}buyer}]\mathsf{?}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.\textit{Seller}\langle
x\rangle,\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}pay}.x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}carrier}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}ship}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,x\\}$
$\displaystyle\textit{Carrier}(x)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}]\mathsf{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}ship}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,x.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$

Note that the buyer either sends pay or it sends two add messages in a row
before repeating this behavior. That is, this particular buyer always adds an
even number of items to the shopping cart. Nonetheless, the buyer periodically
has a chance to send a pay message and terminate. Therefore, the execution of
the program in which the buyer only sends add is unfair according to
Definition 2.2 hence this program is fairly terminating. $\lrcorner$

######  Example 3.2 (purchase with negotiation).

Consider a variation of Example 3.1 in which the buyer, before making the
payment, negotiates with a secondary buyer for an arbitrarily long time. The
interaction happens in two nested sessions, an outer one involving the primary
buyer, the seller and the carrier, and an inner one involving only the two
buyers. We model the interaction as the program below, in which we collapse
role names to their initials.

Main
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}(s)(\textit{Buyer}\langle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}]\rangle\mathbin{\mid}\textit{Seller}\langle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}s}]\rangle\mathbin{\mid}\textit{Carrier}\langle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}c}]\rangle)$
$\displaystyle\textit{Buyer}(x)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}s}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}query}.x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}s}]\mathsf{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}price}.(t)(\textit{Buyer}_{1}\langle
x,t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{1}]\rangle\mathbin{\mid}\textit{Buyer}_{2}\langle
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{2}]\rangle)$
$\displaystyle\textit{Seller}(x)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}]\mathsf{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}query}.x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}price}.x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}]\mathsf{?}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}pay}.x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}c}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}ship}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,x,\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}cancel}.x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}c}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}cancel}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,x\\}$
$\displaystyle\textit{Carrier}(x)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}s}]\mathsf{?}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}ship}.x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}box}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,x,\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}cancel}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,x\\}$
$\displaystyle\textit{Buyer}_{1}(x,y)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}y[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{2}]\mathsf{!}\\{\begin{array}[t]{@{}l@{}}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}split}.y[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{2}]\mathsf{?}\\{\begin{array}[t]{@{}l@{}}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}yes}.\lceil
x\rceil
x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}s}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}ok}.x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}c}]\mathsf{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}box}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,x.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,y.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done},\\\
\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}no}.\textit{Buyer}_{1}\langle
x,y\rangle\\},\end{array}\\\
\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}giveup}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,y.\lceil
x\rceil
x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}s}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}cancel}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,x.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}\\}\end{array}$
$\displaystyle\textit{Buyer}_{2}(y)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}y[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{1}]\mathsf{?}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}split}.y[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{1}]\mathsf{!}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}yes}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,y,\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}no}.\textit{Buyer}_{2}\langle
y\rangle\\},\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}giveup}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,y\\}$

The buyer queries the seller which replies with a price. At this point, Buyer
creates a new session $t$ and forks as a primary buyer $\textit{Buyer}_{1}$
and a secondary buyer $\textit{Buyer}_{2}$. The interaction between the two
sub-buyers goes on until either $\textit{Buyer}_{1}$ gives up or
$\textit{Buyer}_{2}$ accepts its share of the price. In the former case, the
primary buyer waits for the internal session to terminate and cancels the
order with the seller which, in turn, aborts the transaction with the carrier.
In the latter case, the buyer confirms the order to the seller, which then
instructs the carrier to ship a box to the buyer.

Note that the outermost session $s$, taken in isolation, terminates in a
bounded number of interactions, but its progress cannot be established without
assuming that the innermost session $t$ terminates. In particular, if the two
buyers keep negotiating forever, the seller and the carrier starve. However,
the innermost session can terminate if $\textit{Buyer}_{1}$ sends giveup to
$\textit{Buyer}_{2}$ or if $\textit{Buyer}_{2}$ sends yes to
$\textit{Buyer}_{1}$. Thus, the run in which the two buyers negotiate forever
is unfair, the session $t$ fairly terminates and the session $s$ terminates as
well.

On the technical side, note that the definition of $\textit{Buyer}_{1}$
contains two casts on the variable $x$. As we will see in Example 6.1, these
casts are necessary for the typeability of $\textit{Buyer}_{1}$ to account for
the fact that $x$ is used _differently_ in two distinct branches of the
process. $\lrcorner$

######  Example 3.3 (parallel merge sort).

To illustrate an example of program that creates an unbounded number of
sessions we model a parallel version of the merge sort algorithm.

Main
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}(s)(s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}m}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}w}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}req}.s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}m}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}w}]\mathsf{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}res}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,s.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}\mathrel{|}\textit{Sort}\langle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}w}]\rangle)$
$\displaystyle\textit{Sort}(x)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}m}]\mathsf{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}req}.((t)(\textit{Merge}\langle
x,t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}m}]\rangle\mathrel{|}\textit{Sort}\langle
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}w}_{1}]\rangle\mathrel{|}\textit{Sort}\langle
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}w}_{2}]\rangle)\oplus
x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}m}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}res}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,x)$
$\displaystyle\textit{Merge}(x,y)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}y[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}w}_{1}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}req}.y[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}w}_{2}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}req}.y[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}w}_{1}]\mathsf{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}res}.y[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}w}_{2}]\mathsf{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}res}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,y.x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}m}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}res}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,x$

The program starts as a single session $s$ in which a master
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}m}$
sends the initial collection of data to the worker
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}w}$
as a req message and waits for the result. The worker is modeled as a process
Sort that decides whether to sort the data by itself (right branch of the
choice in Sort), in which case it sends the result directly to the master, or
to partition the collection (left branch of the choice in Sort). In the latter
case, it creates a new session $t$ in which it sends requests to two sub-
workers
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}w}_{1}$
and
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}w}_{2}$,
it gathers the partial results from them and gets back to the master with the
complete result.

Since a worker may always choose to start two sub-workers in a new session,
the number of sessions that may be created by this program is unbounded. At
the same time, each worker may also choose to complete its task without
creating new sessions. So, while in principle there exists a run of this
program that keeps creating new sessions forever, this run is unfair according
to Definition 2.2. $\lrcorner$

##  4 Multiparty Session Types and Fair Subtyping

In this section we define syntax and semantics of multiparty session types
(Section 4.1) as well as an inference system for fair subtyping (Section 4.2).

###  4.1 Syntax and Semantics

A _session type_ is a regular tree [15] coinductively generated by the
productions below:

$\textstyle\textbf{Session type}\qquad
S,T,U,V::=\pi\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}\mid\sum_{i\in
I}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\pi\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.S_{i}\mid\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\pi{S}.T$

The session type
$\pi\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$
describes the behavior of a process that sends/receives a termination signal.
The session type $\sum_{i\in
I}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\pi\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.S_{i}$
describes the behavior of a process that sends to or receives from the
participant
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$
one of the tags
$\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}$
and then behaves according to $S_{i}$. Note that the source or destination
role
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$
and the polarity $\pi$ are the same in every branch. We require that $I$ is
not empty and $i,j\in I$ with $i\neq j$ implies
$\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}\neq\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{j}$.
Occasionally we write
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\pi\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{1}.S_{1}+\cdots+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\pi\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{n}.S_{n}$
instead of
$\sum_{i=1}^{n}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\pi\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.S_{i}$.
Finally, a session type
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\pi{S}.T$
describes the behavior of a process that sends to or receives from the
participant
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$
an endpoint of type $S$ and then behaves according to $T$. We often specify
infinite session types as solutions of equations of the form $S=\cdots$ where
the metavariable $S$ may occur on the right hand side of $=$ guarded by at
least one prefix. A regular tree satisfying such equation is guaranteed to
exist and to be unique [15].

In order to describe a whole multiparty session at the level of types we
introduce the notion of _session map_.

######  Definition 4.1 (session map).

A _session map_ is a finite, partial map from roles to session types written
$\\{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright
S_{i}\\}_{i\in I}$. We let $M$ and $N$ range over session maps, we write
$\mathsf{dom}(M)$ for the domain of $M$, we write $M\mathrel{|}N$ for the
union of $M$ and $N$ when $\mathsf{dom}(M)\cap\mathsf{dom}(N)=\emptyset$, and
we abbreviate the singleton map
$\\{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{S}\\}$
as
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{S}$.

We describe the evolution of a session at the level of types by means of a
_labeled transition system_ for session maps. Labels are generated by the
grammar below:

$\textbf{Label}\qquad\ell::=\tau\mid\alpha\qquad\qquad\textbf{Action}\qquad\alpha,\beta::=\pi\checkmark\mid\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\pi\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}}\mid\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\pi
S}$

The label $\tau$ represents either an internal action performed by a
participant independently of the others or a synchronization between two
participants. The labels of the form $\pi\checkmark$ describe the input/output
of termination signals, whereas the labels of the form
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\pi\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}$
and
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\pi
S$ represent the input/output of a tag m or of an endpoint of type $S$.

Table 4:  Labeled transition system for session maps.
$\displaystyle{\vbox{\hbox{\hypertarget{rule:l-end}{{{\small[l-end]}}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
43.55045pt\vbox{\vbox{}\hbox{\hskip-43.55043pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright\pi\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}\xrightarrow{\pi\checkmark}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright\pi\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:l-channel}{{{\small[l-channel]}}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
45.60445pt\vbox{\vbox{}\hbox{\hskip-45.60443pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\pi
U.S\xrightarrow{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\pi
U}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{S}$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:l-pick}{{{\small[l-pick]}}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
59.34673pt\vbox{\vbox{}\hbox{\hskip-59.34671pt\hbox{\hbox{$\displaystyle\displaystyle\textstyle\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{\sum_{i\in
I}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.S_{i}}\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}.S_{k}}$}}}}}}$}}}\leavevmode\nobreak\
k\in I\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:l-tag}{{{\small[l-tag]}}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
61.15591pt\vbox{\vbox{}\hbox{\hskip-61.1559pt\hbox{\hbox{$\displaystyle\displaystyle\textstyle\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{\sum_{i\in
I}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\pi\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.S_{i}}\xrightarrow{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\pi\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}}}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{S_{k}}$}}}}}}$}}}\leavevmode\nobreak\
k\in I\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:l-tau}{{{\small[l-tau]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
18.23055pt\vbox{\hbox{\hskip-18.23055pt\hbox{\hbox{$\displaystyle\displaystyle
M\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}M^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
30.1333pt\vbox{\vbox{}\hbox{\hskip-30.1333pt\hbox{\hbox{$\displaystyle\displaystyle
M\mathrel{|}N\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}M^{\prime}\mathrel{|}N$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:l-terminate}{{{\small[l-terminate]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
50.19269pt\vbox{\hbox{\hskip-50.19269pt\hbox{\hbox{$\displaystyle\displaystyle
M\stackrel{{\scriptstyle{?}\checkmark}}{{\longrightarrow}}M^{\prime}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
N\stackrel{{\scriptstyle{!}\checkmark}}{{\longrightarrow}}N^{\prime}$}}}}\vbox{}}}\over\hbox{\hskip
33.94272pt\vbox{\vbox{}\hbox{\hskip-33.9427pt\hbox{\hbox{$\displaystyle\displaystyle
M\mathrel{|}N\stackrel{{\scriptstyle{?}\checkmark}}{{\longrightarrow}}M^{\prime}\mathrel{|}N^{\prime}$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:l-sync}{{{\small[l-sync]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
45.08446pt\vbox{\hbox{\hskip-45.08444pt\hbox{\hbox{$\displaystyle\displaystyle
M\stackrel{{\scriptstyle\overline{\alpha}}}{{\longrightarrow}}M^{\prime}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
N\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}N^{\prime}$}}}}\vbox{}}}\over\hbox{\hskip
30.9033pt\vbox{\vbox{}\hbox{\hskip-30.90329pt\hbox{\hbox{$\displaystyle\displaystyle
M\mathrel{|}N\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}M^{\prime}\mathrel{|}N^{\prime}$}}}}}}$}}}$

The labeled transition system is defined by the rules in Table 4, most of
which are straightforward. Rule [l-pick] models the fact that the participant
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$
may internally choose one particular tag
$\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}$
before sending it to
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}$.
The chosen tag is not negotiable with the receiver. Rule [l-terminate] models
termination of a session. A session terminates when there is exactly one
participant waiting for the termination signal and all the others are sending
it. This property follows from a straightforward induction on the derivation
of $M\stackrel{{\scriptstyle{?}\checkmark}}{{\longrightarrow}}N$ using
[l-terminate] and [l-end]. The existence of a single participant waiting for
the termination signal ensures that there is a uniquely determined
continuation process after the session has been closed. Finally, rule [l-sync]
models the synchronization between two participants performing complementary
actions. The complement of an action $\alpha$, denoted by $\overline{\alpha}$,
is the partial operation defined by the equations

$\overline{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\pi\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}}\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\triangleright\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{\overline{\pi}}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}\qquad\overline{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\pi
S}\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\triangleright\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{\overline{\pi}}S$

where $\overline{\pi}$ denotes the complement of the polarity $\pi$. The
complement of actions of the form $\pi\checkmark$ is undefined, so rule
[l-sync] cannot be applied to terminated sessions. Hereafter we write
$\Rightarrow$ for the reflexive, transitive closure of
$\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}$ and
$\stackrel{{\scriptstyle\alpha}}{{\Longrightarrow}}$ for the composition
${\Rightarrow}{\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}}$.

We call _coherence_ the property of multiparty sessions that we wish to
enforce with our type system, namely the fact that a session can always
terminate no matter how it evolves. We formulate coherence directly on the
transition system of session maps, in line with the approach of Scalas and
Yoshida [45] and without introducing global types.

######  Definition 4.2.

We say that $M$ is _coherent_ , notation ${\\#}M$, if $M\Rightarrow N$ implies
$N\stackrel{{\scriptstyle{?}\checkmark}}{{\Longrightarrow}}$.

The term “coherence” is borrowed from Carbone et al. [8, 9], although the
property is actually stronger than the one of Carbone et al.as it entails fair
termination of multiparty sessions through Theorem 2.5. In particular, if we
consider the reduction system whose states are session maps and whose
reduction relation is $\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}$, then
${\\#}M$ implies $M$ fairly terminating.

######  Example 4.3 (buyer-seller-carrier session map).

Consider the session types

$\begin{array}[]{l@{~}c@{~}l}S_{b}\hfil\leavevmode\nobreak\
&=\hfil\leavevmode\nobreak\
&\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.S_{b}+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}pay}.{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}\\\
S_{s}\hfil\leavevmode\nobreak\ &=\hfil\leavevmode\nobreak\
&\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}buyer}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.S_{s}+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}buyer}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}pay}.\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}carrier}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}ship}.{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}\\\
S_{c}\hfil\leavevmode\nobreak\ &=\hfil\leavevmode\nobreak\
&\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}ship}.{?}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}\end{array}$

which describe the behavior of the processes Buyer, Seller and Carrier in
Example 3.1. The session map
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}buyer}\triangleright{S_{b}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}\triangleright{S_{s}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}carrier}\triangleright{S_{c}}$
is coherent. To see that, consider any interaction between the buyer and the
seller. One of two cases applies: either the buyer has sent an even number of
add messages to the seller, in which case it can send pay and the session
eventually terminates, or the buyer has sent an odd number of add messages to
the seller, in which case it can send one more add message followed by a pay
message and once again the session eventually terminates. $\lrcorner$

Coherence allows us to provide a semantic definition of _fair subtyping_ , the
relation that defines the safe substitution principle for session endpoints in
our type system.

######  Definition 4.4 (fair subtyping).

We say that $S$ is a _fair subtype_ of $T$, notation $S\sqsubseteq T$, if
$M\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{S}$
coherent implies
$M\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{T}$
coherent for every $M$ and
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$.

Definition 4.4 does not say much about the properties of fair subtyping except
for the fact that it is a coherence-preserving preorder. For this reason, we
devote Section 4.2 to defining an alternative characterization of fair
subtyping that highlights its relationship with the standard subtyping
relation for session types [22].

###  4.2 Inference System for Fair Subtyping

Table 5:  Inference system for fair subtyping. [f-end]
$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
26.82542pt\vbox{\vbox{}\hbox{\hskip-26.82541pt\hbox{\hbox{$\displaystyle\displaystyle\pi\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}\leqslant_{n}\pi\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$}}}}}}$
[f-channel] $\displaystyle\displaystyle{\hbox{\hskip
13.9289pt\vbox{\hbox{\hskip-13.9289pt\hbox{\hbox{$\displaystyle\displaystyle
S\leqslant_{n}T$}}}\vbox{}}}\over\hbox{\hskip
36.43607pt\vbox{\vbox{}\hbox{\hskip-36.43607pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\pi
U.S\leqslant_{n}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\pi
U.T$}}}}}}$ [f-tag-in] $\displaystyle\displaystyle{\hbox{\hskip
75.33511pt\vbox{\hbox{\hskip-75.3351pt\hbox{\hbox{$\displaystyle\displaystyle\forall
i\in I:S_{i}\leqslant_{n_{i}}T_{i}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall i\in I:n_{i}\leq
n$}}}}\vbox{}}}\over\hbox{\hskip
63.09538pt\vbox{\vbox{}\hbox{\hskip-63.09538pt\hbox{\hbox{$\displaystyle\displaystyle\textstyle\sum_{i\in
I}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.S_{i}\leqslant_{n}\sum_{i\in
I\cup
J}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.T_{i}$}}}}}}$
[f-tag-out-1] $\displaystyle\displaystyle{\hbox{\hskip
75.33511pt\vbox{\hbox{\hskip-75.3351pt\hbox{\hbox{$\displaystyle\displaystyle\forall
i\in I:S_{i}\leqslant_{n_{i}}T_{i}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall i\in I:n_{i}\leq
n$}}}}\vbox{}}}\over\hbox{\hskip
57.46233pt\vbox{\vbox{}\hbox{\hskip-57.46233pt\hbox{\hbox{$\displaystyle\displaystyle\textstyle\sum_{i\in
I}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.S_{i}\leqslant_{n}\sum_{i\in
I}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.T_{i}$}}}}}}$
[f-tag-out-2] $\displaystyle\displaystyle{\hbox{\hskip
75.33511pt\vbox{\hbox{\hskip-75.3351pt\hbox{\hbox{$\displaystyle\displaystyle\forall
i\in I:S_{i}\leqslant_{n_{i}}T_{i}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\exists i\in
I:n_{i}<n$}}}}\vbox{}}}\over\hbox{\hskip
61.15094pt\vbox{\vbox{}\hbox{\hskip-61.15094pt\hbox{\hbox{$\displaystyle\displaystyle\textstyle\sum_{i\in
I\cup
J}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.S_{i}\leqslant_{n}\sum_{i\in
I}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.T_{i}$}}}}}}$

Consider the relation $\leqslant_{n}$ coinductively defined by the inference
system in Table 5, where $n$ ranges over natural numbers. The characterization
of fair subtyping that we consider is the relation
${\leqslant}\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\bigcup_{n\in\mathbb{N}}{\leqslant_{n}}$. The rules for deriving
$S\leqslant_{n}T$ are quite similar to those of the standard subtyping
relation for session types [22]: [f-end] states reflexivity of subtyping on
terminated session types; [f-channel] relates higher-order session types with
the same polarity and payload type; [f-tag-in] is the usual covariant rule for
the input of tags (the set of tags in the larger session type includes those
in the smaller one); [f-tag-out-2] is the usual contravariant rule for the
output of tags (the set of tags in the smaller session type includes those in
the larger one). Overall, these rules entail a “simulation” between the
behaviors described by $S$ and $T$ whereby all inputs offered by $S$ are also
offered by $T$ and all outputs performed by $T$ are also performed by $S$. The
main differences between $\leqslant$ and the subtyping relation of Gay and
Hole [22] are the presence of an invariant rule for outputs [f-tag-out-1] and
the natural number $n$ annotating each subtyping judgment $S\leqslant_{n}T$.
Intuitively, this number estimates how much $S$ and $T$ differ in terms of
performed outputs. In all rules but [f-tag-out-2], the annotation in the
conclusion of the rule is just an upper bound of the annotations found in the
premises. In [f-tag-out-2], where the sets of output tags in related session
types may differ, the annotation $n$ is required to be a _strict_ upper bound
for at least one of the premises. That is, there must be at least one premise
in which the annotation strictly decreases, while no restriction is imposed on
the others. Intuitively, this ensures the existence of a tag shared by the two
related session types whose corresponding continuations are slightly less
different. So, the annotation $n$ provides an upper bound to the number of
applications of [f-tag-out-2] along any path (_i.e._ any sequence of actions)
shared by $S$ and $T$ that leads to termination. In the particular case when
$n=0$, the rule [f-tag-out-2] cannot be applied, so that $T$ may perform all
the outputs also performed by $S$.

######  Example 4.5.

Consider the session type
$S=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.S+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}pay}.{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$,
which describes the behavior of the buyer in Equation 1 purchasing an
arbitrary number of items,
$T=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.T+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}pay}.{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$,
which describes the behavior of the buyer in Example 3.1 always purchasing an
even number of items, and
$U=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.U$,
which describes the behavior of a buyer attempting to purchase an infinite
number of items without ever paying the seller. We have $S\leqslant T$ and
$S\not\leqslant U$. Indeed, we can derive

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
5.71005pt\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
9.89824pt\hbox{$\displaystyle\penalty 1\mathstrut\smash{\vdots}$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=27.29648pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle S\leqslant_{1}T$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=72.93541pt\hbox{\kern
3.00003pt$\hyperlink{rule:f-tag-out-2}{\textup{{\small[f-tag-
out-2]}}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
S\leqslant_{2}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.T$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
23.62227pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=47.24454pt\hbox{\kern
3.00003pt$\hyperlink{rule:f-end}{\textup{{\small[f-end]}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}\leqslant_{0}{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=394.50249pt\hbox{\kern
3.00003pt$\hyperlink{rule:f-tag-out-2}{\textup{{\small[f-tag-
out-2]}}}$}}}\hbox{\kern 183.603pt\hbox{$\displaystyle S\leqslant_{1}T$}}}}$

but there is no derivation for $S\leqslant_{n}U$ no matter how large $n$ is
chosen. Note that there are infinitely many sequences of actions of $S$ that
cannot be performed by both $T$ and $U$. In particular, $T$ cannot perform any
sequence of actions consisting of an odd number of add outputs followed by a
pay output, whereas $U$ cannot perform any sequence of add outputs followed by
a pay output. Nonetheless, there is a path shared by $S$ and $T$ that leads
into a region of $S$ and $T$ in which no more differences are detectable. The
annotations in the derivation tree measures the distance of each judgment from
such region. In the case of $S$ and $U$, there is no shared path that leads to
a region where no differences are detectable. $\lrcorner$

######  Example 4.6.

Consider the session types
$S=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}player}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}play}.(\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}player}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}win}.S+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}player}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}lose}.S)+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}player}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}quit}.{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$
and
$T=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}player}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}play}.\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}player}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}lose}.T+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}player}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}quit}.{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$
describing the behavior of two slot machines, an unbiased one in which the
player may win at every play and a biased one in which the player never wins.
If we try to build a derivation for $S\leqslant_{n}T$ we obtain

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
63.31424pt\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
12.51222pt\hbox{$\displaystyle\penalty 1\mathstrut\smash{\vdots}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=32.52444pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle S\leqslant_{n-1}T$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=193.37177pt\hbox{\kern
3.00003pt$\hyperlink{rule:f-tag-out-1}{\textup{{\small[f-tag-
out-1]}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}player}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}win}.S+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}player}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}lose}.S\leqslant_{n}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}player}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}lose}.T$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
23.90292pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=47.80585pt\hbox{\kern
3.00003pt$\hyperlink{rule:f-end}{\textup{{\small[f-end]}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}\leqslant_{n}{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=510.50015pt\hbox{\kern
3.00003pt$\hyperlink{rule:f-tag-in}{\textup{{\small[f-tag-
in]}}}$}}}\hbox{\kern 241.32118pt\hbox{$\displaystyle S\leqslant_{n}T$}}}}$

which would contain an infinite branch with strictly decreasing annotations.
Therefore, we have $S\not\leqslant T$. In this case there exists a shared path
leading into a region of $S$ and $T$ in which no more differences are
detectable between the two protocols, but this path starts from an input. The
fact that $S$ is _not_ a fair subtype of $T$ has a semantic justification.
Think of a
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}player}$
that deliberately insists on playing until it wins. This is possible when
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}player}$
interacts with the unbiased slot machine $S$ but not with the biased one $T$.
$\lrcorner$

In the rest of this section we study the fundamental properties of
$\leqslant$, starting from the non-obvious fact that it is a preorder.

######  Theorem 4.7.

$\leqslant$ is a preorder.

While reflexivity of $\leqslant$ is trivial to prove (since [f-tag-out-2] is
never necessary, it suffices to only consider judgments with a $0$
annotation), transitivity is surprisingly complex. The challenging part of
proving that from $S\leqslant_{m}U$ and $U\leqslant_{n}T$ we can derive
$S\leqslant_{k}T$ is to come up with a feasible annotation $k$. As it turns
out, such $k$ depends not only on $m$ and $n$, but also on annotations found
in different regions of the derivation trees that prove $S\leqslant_{m}U$ and
$U\leqslant_{n}T$. In particular, the “difference” of $S$ and $T$ is not
simply the “maximum difference” or “the sum of the differences” of $S$ and $U$
and of $U$ and $T$. More in detail, we first show that we can always find a
derivation of $S\leqslant_{m}U$ where the rank annotations of all judgements
occurring in it are below some $h\geq m$; then, the judgement
$S\leqslant_{k}T$ is provable for $k=m+(1+h)n$. For previous characterizations
of fair subtyping [39, 41, 12, 13], transitivity has been established
indirectly by relating the inference system of fair subtyping (Table 5) with
its semantic definition (Definition 4.4). For Theorem 4.7 we are able to
provide a direct proof (cf. Section B.1).

Now we establish the connection between $\leqslant$ and $\sqsubseteq$
(Definition 4.4). First of all, we prove that $\leqslant$ is coherence-
preserving just like $\sqsubseteq$ is.

######  Theorem 4.8 (soundness).

If $S\leqslant T$ then $S\sqsubseteq T$.

The proof of this result relies on a key property of $\leqslant$ not enjoyed
by the usual subtyping relation on session types [22]: when $S\leqslant T$ and
$M\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright
S$ is coherent, the session map
$M\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright
T$ can successfully terminate. The rank annotation on subtyping judgements is
used to set up an appropriate inductive argument for proving this property.

Theorem 4.8 alone suffices to justify the adoption of $\leqslant$ as fair
subtyping relation, but we are interested in understanding to which extent
$\leqslant$ covers $\sqsubseteq$. In this respect, it is quite easy to see
that there exist session types that are related by $\sqsubseteq$ but not by
$\leqslant$. For example, consider
$S=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}a}.S$
and
$T=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}b}.T$
and observe that these two session types describe completely different
protocols (the output of infinitely many a’s in the case of $S$ and the input
of infinitely many b’s in the case of $T$). In particular, we have
$S\not\leqslant T$ and $T\not\leqslant S$ but also $S\sqsubseteq T$ and
$T\sqsubseteq S$. That is, $S$ and $T$ are _unrelated_ according to
$\leqslant$ but they are _equivalent_ according to $\sqsubseteq$. This
equivalence is justified by the fact that there exists no coherent session map
in which $S$ and $T$ could play any role, because none of them can ever
terminate.

This discussion hints at the possibility that, if we restrict the attention to
those session types that _can_ terminate, which are the interesting ones as
far as this work is concerned, then we can establish a tighter correspondence
between $\leqslant$ and $\sqsubseteq$. We call such session types _bounded_ ,
because they describe protocols for which termination is always within reach.

######  Definition 4.9 (bounded session type).

We say that a session type is _bounded_ if all of its subtrees contain a
$\pi\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$
leaf.

Note that a _finite_ session type is always bounded but not every bounded
session type is finite. If we consider the reduction system in which states
are session types and we have $S\rightarrow T$ if $T$ is an immediate subtree
of $S$, then $S$ is bounded if and only if $S$ is fairly terminating. Now, for
the family of bounded session types we can prove a _relative completeness_
result for $\leqslant$ with respect to $\sqsubseteq$.

######  Theorem 4.10 (relative completeness).

If $S$ is bounded and $S\sqsubseteq T$ then $S\leqslant T$.

The proof of Theorem 4.10 is done by contradiction. We show that, for any
bounded $S$, if $S\leqslant T$ does not hold then we can build a session map
$M$ called _discriminator_ such that
$M\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright
S$ is coherent and
$M\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright
T$ is not, which contraddicts the hypothesis $S\sqsubseteq T$. The boundedness
of $S$ is necessary to make sure that it is always possible to find a session
map $N$ such that
$N\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright
S$ is coherent.

##  5 Type System

In this section we describe the type system for the calculus of multiparty
sessions of Section 3. The typing judgments have the form $\Gamma\vdash^{n}P$,
meaning that the process $P$ is well typed in the typing context $\Gamma$ and
has rank $n$. As usual, the _typing context_ is a map associating channels
with session types and is meant to contain an association for each name in
$\mathsf{fn}(P)$. We write $u_{1}:S_{1},\dots,u_{n}:S_{n}$ for the map with
domain $\\{u_{1},\dots,u_{n}\\}$ that associates $u_{i}$ with $S_{i}$.
Occationally we write $\overline{u:S}$ for the same context, when the number
and the specific associations are unimportant. We also assume that endpoints
occurring in a typing context have different session names. That is,
$s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}],s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\in\mathsf{dom}(\Gamma)$
implies
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}$.
This constraint makes sure that each well-typed process plays exactly one role
in each of the sessions in which it participates. It is also a common
assumption made in all multiparty session calculi. We use $\Gamma$ and
$\Delta$ to range over typing contexts, we write $\emptyset$ for the empty
context and $\Gamma,\Delta$ for the union of $\Gamma$ and $\Delta$ when they
have disjoint domains and disjoint sets of session names. The _rank_ $n$ in a
typing judgment estimates the number of sessions that $P$ has to create and
the number of casts that $P$ has to perform in order to terminate. The fact
that the rank is finite suggests that so is the effort required by $P$ to
terminate.

Table 6: Typing rules.
$\displaystyle{\vbox{\hbox{\hypertarget{rule:t-done}{{{\small[t-done]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
18.90288pt\vbox{\vbox{}\hbox{\hskip-18.90288pt\hbox{\hbox{$\displaystyle\displaystyle\emptyset\vdash^{n}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:t-call}{{{\small[t-call]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
23.64078pt\vbox{\hbox{\hskip-23.64078pt\hbox{\hbox{$\displaystyle\displaystyle\overline{u:S}\vdash^{n}P\\{\overline{u}/\overline{x}\\}$}}}\vbox{}}}\over\hbox{\hskip
22.01137pt\vbox{\vbox{}\hbox{\hskip-22.01135pt\hbox{\hbox{$\displaystyle\displaystyle\overline{u:S}\vdash^{n+m}A\langle\overline{u}\rangle$}}}}}}$}}}\leavevmode\nobreak\
A:[\overline{S};n],A(\overline{x})\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}P\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:t-wait}{{{\small[t-wait]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
13.1546pt\vbox{\hbox{\hskip-13.15459pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash^{n}P$}}}\vbox{}}}\over\hbox{\hskip
43.60141pt\vbox{\vbox{}\hbox{\hskip-43.6014pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,u:{?}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}\vdash^{n}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,u.{P}$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:t-close}{{{\small[t-close]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
32.15526pt\vbox{\vbox{}\hbox{\hskip-32.15524pt\hbox{\hbox{$\displaystyle\displaystyle
u:{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}\vdash^{n}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,u$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:t-channel-in}{{{\small[t-channel-
in]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
37.78929pt\vbox{\hbox{\hskip-37.78928pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,u:T,x:S\vdash^{n}P$}}}\vbox{}}}\over\hbox{\hskip
54.54059pt\vbox{\vbox{}\hbox{\hskip-54.54059pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,u:\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{?}{S}.T\vdash^{n}u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{?}(x).P$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:t-channel-out}{{{\small[t-channel-
out]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
25.46646pt\vbox{\hbox{\hskip-25.46646pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,u:T\vdash^{n}P$}}}\vbox{}}}\over\hbox{\hskip
60.52081pt\vbox{\vbox{}\hbox{\hskip-60.5208pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,u:\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{!}{S}.T,v:S\vdash^{n}u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{!}v.P$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:t-tag}{{{\small[t-tag]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
44.77962pt\vbox{\hbox{\hskip-44.77962pt\hbox{\hbox{$\displaystyle\displaystyle\forall
i\in I:\Gamma,u:S_{i}\vdash^{n}P_{i}$}}}\vbox{}}}\over\hbox{\hskip
76.1892pt\vbox{\vbox{}\hbox{\hskip-76.1892pt\hbox{\hbox{$\displaystyle\displaystyle\textstyle\Gamma,u:\sum_{i\in
I}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\pi\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.S_{i}\vdash^{n}u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\pi\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.P_{i}\\}_{i\in
I}$}}}}}}$}}}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:t-choice}{{{\small[t-choice]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
40.70921pt\vbox{\hbox{\hskip-40.70921pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash^{n_{1}}P_{1}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash^{n_{2}}P_{2}$}}}}\vbox{}}}\over\hbox{\hskip
25.74243pt\vbox{\vbox{}\hbox{\hskip-25.74243pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash^{n_{k}}P_{1}\oplus
P_{2}$}}}}}}$}}}\leavevmode\nobreak\ k\in\\{1,2\\}\penalty 50\hskip 20.00003pt
plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:t-cast}{{{\small[t-cast]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
25.46646pt\vbox{\hbox{\hskip-25.46646pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,u:T\vdash^{n}P$}}}\vbox{}}}\over\hbox{\hskip
37.14725pt\vbox{\vbox{}\hbox{\hskip-37.14725pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,u:S\vdash^{m+n}\lceil
u\rceil{P}$}}}}}}$}}}\leavevmode\nobreak\ S\leqslant_{m}T\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hypertarget{rule:t-par}{{{\small[t-par]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
66.05995pt\vbox{\hbox{\hskip-66.05995pt\hbox{\hbox{$\displaystyle\displaystyle\forall
i\in\\{1,\dots,h\\}:\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vdash^{n_{i}}P_{i}$}}}\vbox{}}}\over\hbox{\hskip
63.10136pt\vbox{\vbox{}\hbox{\hskip-63.10136pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1},\dots,\Gamma_{h}\vdash^{1+n_{1}+\cdots+n_{h}}(s)(P_{1}\mathrel{|}\cdots\mathrel{|}P_{h})$}}}}}}$}}}\leavevmode\nobreak\
{\\#}\\{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright
S_{i}\\}_{i=1..h}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{{\vbox{\hbox{\hypertarget{rule:co-tag}{{{\small[co-
tag]}}}}\hbox{\hbox{$\displaystyle\displaystyle{\hbox{\raise
1.83437pt\hbox{$\displaystyle\hbox{\hskip
26.9071pt\vbox{\hbox{\hskip-26.90709pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,u:S_{k}\vdash^{n}P_{k}$}}}\vbox{}}}$}}\atop\hbox{\lower
2.78159pt\hbox{$\displaystyle\hbox{\hskip
76.1892pt\vbox{\vbox{}\hbox{\hskip-76.1892pt\hbox{\hbox{$\displaystyle\displaystyle\textstyle\Gamma,u:\sum_{i\in
I}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\pi\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.S_{i}\vdash^{n}u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\pi\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.P_{i}\\}_{i\in
I}$}}}}}$}}}$}\hskip-152.37839pt\hbox
to152.37839pt{$\displaystyle\mathrel{=}\joinrel\xleaders\hbox{\hbox{$\displaystyle\mkern-3.0mu=\mkern-3.0mu$}}\hfil\joinrel\mathrel{=}$}}}}}\leavevmode\nobreak\
k\in I\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{{\vbox{\hbox{\hypertarget{rule:co-choice}{{{\small[co-
choice]}}}}\hbox{\hbox{$\displaystyle\displaystyle{\hbox{\raise
1.83437pt\hbox{$\displaystyle\hbox{\hskip
14.70042pt\vbox{\hbox{\hskip-14.70042pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash^{n}P_{k}$}}}\vbox{}}}$}}\atop\hbox{\lower
2.78159pt\hbox{$\displaystyle\hbox{\hskip
24.8591pt\vbox{\vbox{}\hbox{\hskip-24.8591pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash^{n}P_{1}\oplus
P_{2}$}}}}}$}}}$}\hskip-49.7182pt\hbox
to49.7182pt{$\displaystyle\mathrel{=}\joinrel\xleaders\hbox{\hbox{$\displaystyle\mkern-3.0mu=\mkern-3.0mu$}}\hfil\joinrel\mathrel{=}$}}}}}\leavevmode\nobreak\
k\in\\{1,2\\}$

The typing rules are shown in Table 6 as a _generalized inference system_ [3,
16, 10, 17] in which, roughly speaking, the singly-lined rules are interpreted
coinductively and the doubly-lined rules – called _corules_ – are interpreted
inductively. We will come back with a more detailed intuition later on
(Definition 5.1), although we will not provide a formal definition of the
interpretation of a generalized inference system in this paper. The interested
reader may refer to the cited literature for details. We type check a program
$\\{A_{i}(\overline{x_{i}})\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}P_{i}\\}_{i\in
I}$ under a global set of assignments
$\\{A_{i}:[\overline{S_{i}};n_{i}]\\}_{i\in I}$ associating each process name
$A_{i}$ with a tuple of session types $\overline{S_{i}}$, one for each of the
variables in $\overline{x_{i}}$, and a rank $n_{i}$. The program is well typed
if $\overline{x_{i}:S_{i}}\vdash^{n_{i}}P_{i}$ is derivable for every $i\in
I$, establishing that the tuple $\overline{S_{i}}$ corresponds to the way the
variables $\overline{x_{i}}$ are used by $P_{i}$ and that $n_{i}$ is a
feasible rank annotation for $P_{i}$. We now describe the typing rules in
detail.

The rule [t-done] states that the terminated process is well typed in the
empty context, to make sure that no unused channels are left behind. Note that
done can be given any rank, since it performs no casts and it creates no new
sessions. The rule [t-call] checks that a process invocation
$A\langle\overline{u}\rangle$ is well typed by unfolding $A$ into the process
associated with $A$. The types associated with $\overline{u}$ must match those
of the global assignment $A:[\overline{S};n]$ and the rank of the process must
be no greater than that of the invocation. The potential mismatch between the
two ranks improves typeability in some corner cases. The rules [t-wait] and
[t-close] concern processes that exchange termination signals. The channel
being closed is consumed and, in the case of [t-wait], no longer available in
the continuation $P$. Again,
$\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,u$
can be typed with any rank whereas the rank of
$\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,u.P$
coincides with that of $P$. The rules [t-channel-in] and [t-channel-out] deal
with the exchange of channels in a quite standard way. Note that the actual
type of the exchanged channel is required to coincide with the expected one.
In particular, no covariance or contravariance of input and output
respectively is allowed. Relaxing the typing rule in this way would introduce
implicit applications of subtyping that may compromise fair termination [13].
In our type system, each application of subtyping must be explicitly accounted
for as we will see when discussing [t-cast]. Rule [t-tag] deals with the
exchange of tags. Channels that are not used for such communication must be
used in the same way in all branches, whereas the type of the channel on which
the message is exchanged changes accordingly. All branches are required to
have the same rank, which also corresponds to the rank of the process. Unlike
other presentations of this typing rule [22], we require the branches in the
process to be matched exactly by those in the type. Again, this is to avoid
implicit application of subtyping, which might jeopardize fair termination.
The rule [t-choice] deals with non-deterministic choices and requires both
continuations to be well typed in the same typing context. The judgment in the
conclusion inherits the rank of one of the processes, typically the one with
minimum rank. As we will see in Example 6.3, this makes it possible to model
finite-rank processes that may create an unbounded number of sessions or that
perform an unbounded number of casts.

The rule [t-cast] models the substitution principle induced by fair subtyping:
when $S\leqslant_{m}T$, a channel of type $S$ can be used where a channel of
type $T$ is expected or, in dual fashion [21], a process using $u$ according
to $T$ can be used in place of a process using $u$ according to $S$. To keep
track of this cast, the rank in the conclusion is augmented by the weight $m$
of the subtyping relation between $S$ and $T$. Note that the typing rule
guesses the target type of the cast.

Finally, the rule [t-par] deals with session creation and parallel
composition. This rule is inspired to the _multiparty cut_ rule found in
linear logic interpretations of multiparty session types [8, 9] and provides a
straightforward way for enforcing deadlock freedom. Each process in the
composition must be well typed in a slice of the typing context augmented with
the endpoint corresponding to its role. The session map of the new session
must be coherent, implying that it fairly terminates. The rank of the
composition is one plus the aggregated rank of the composed processes, to
account for the fact that one more session has been created. Recall that
coherence is a property expressed on the LTS of session maps (Definition 4.2)
in line with the approach of Scalas and Yoshida [45].

The typing rules described so far are interpreted _coinductively_. That is, in
order for a rank $n$ process $P$ to be well typed in $\Gamma$ there must be a
_possibly infinite_ derivation tree built with these rules and whose
conclusion is the judgment $\Gamma\vdash^{n}P$. But in a generalized inference
system like the one we are defining, this is not enough to establish that $P$
is well typed. In addition, it must be possible to find _finite_ derivation
trees for all of the judgments occurring in this possibly infinite derivation
tree using the discussed rules _and possibly_ the corules, which we are about
to describe. Since the additional derivation trees must be finite, all of
their branches must end up with an application of [t-done] or [t-close], which
are the only axioms in Table 6 corresponding to the only terminated processes
in Table 1. So, the purpose of these finite typing derivations is to make sure
that in every well-typed (sub-)process there exists a path that leads to
termination. On the one hand, this is a sensible condition to require as our
type system is meant to enforce fair process termination. On the other hand,
insisting that these finite derivations can be built using only the typing
rules discusses thus far is overly restrictive, for a process might have _one_
path that leads to termination, but also alternative paths that lead to
(recursive) process invocations. In fact, all of the processes we have
discussed in Examples 3.1, 3.2 and 3.3 are structured like this. The two
corules [co-choice] and [co-tag] in Table 6 establish that, whenever a multi-
branch process is dealt with, it suffices for _one_ of the branches to lead to
termination. A key detail to note in the case of [co-choice] is that the rank
of the non-deterministic choice coincides with that of the branch that leads
to termination. This makes sense recalling that the rank associated with a
process represents the overall effort required for that process to terminate.

Let us recap the notion of well-typed process resulting from the typing rules
of Table 6.

######  Definition 5.1 (well-typed process).

We say that $P$ is _well typed_ in the context $\Gamma$ and has rank $n$ if
(1) there exists an arbitrary (possibly infinite) derivation tree obtained
using the (singly-lined) rules in Table 6 and whose conclusion is
$\Gamma\vdash^{n}P$ and (2) for each judgment in such tree there is a finite
derivation obtained using the rules and the (doubly-lined) corules.

######  Remark 5.2.

The term “ _co_ rule” seems to suggest that the rule should be _co_
inductively interpreted. As we have seen above (Definition 5.1), corules are
interpreted inductively. We have chosen to stick with the terminology used in
the works that introduced generalized inference systems [3, 16]. $\lrcorner$

######  Example 5.3.

Let us show some typing derivations for fragments of Example 3.1 using the
types $S_{b}$, $S_{s}$ and $S_{c}$ from Example 4.3. Concerning Buyer, we
obtain the infinite derivation

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
32.03218pt\hbox{$\displaystyle\penalty 1\mathstrut\smash{\vdots}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=71.56436pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-call}{\textup{{\small[t-call]}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle x:S_{b}\vdash^{0}\textit{Buyer}\langle
x\rangle$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=179.27528pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-tag}{\textup{{\small[t-tag]}}}$}}}\hbox{\kern
4.80327pt\hbox{$\displaystyle
x:\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.S_{b}\vdash^{0}x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.\textit{Buyer}\langle
x\rangle$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
33.25414pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=66.50827pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-close}{\textup{{\small[t-close]}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle
x:{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}\vdash^{0}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,x$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=464.03082pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-tag}{\textup{{\small[t-tag]}}}$}}}\hbox{\kern
110.60464pt\hbox{$\displaystyle
x:S_{b}\vdash^{0}x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}]\mathsf{!}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}add}.\textit{Buyer}\langle
x\rangle,\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}pay}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,x\\}$}}}}$

and, for each judgment in it, it is easy to find a finite derivation possibly
using [co-tag]. Concerning Main we obtain

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
61.03226pt\hbox{$\displaystyle\penalty 1\mathstrut\smash{\vdots}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=129.56451pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-call}{\textup{{\small[t-call]}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}buyer}]:S_{b}\vdash^{0}\textit{Buyer}\langle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}buyer}]\rangle$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
57.93471pt\hbox{$\displaystyle\penalty 1\smash{\vdots}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=123.36942pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-call}{\textup{{\small[t-call]}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}]:S_{s}\vdash^{0}\textit{Seller}\langle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}]\rangle$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\vdots$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=463.35577pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-par}{\textup{{\small[t-par]}}}$}}}\hbox{\kern
105.80548pt\hbox{$\displaystyle\emptyset\vdash^{1}(s)(\textit{Buyer}\langle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}buyer}]\rangle\mathbin{\mid}\textit{Seller}\langle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}]\rangle\mathbin{\mid}\textit{Carrier}\langle
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}carrier}]\rangle)$}}}}$

where the application of [t-par] is justified by the fact that
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}buyer}\triangleright{S_{b}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}seller}\triangleright{S_{s}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}carrier}\triangleright{S_{c}}$
is coherent (Example 4.3). No participant creates new sessions or performs
casts, so they all have zero rank. The rank of Main is 1 since it creates the
session $s$. $\lrcorner$

We can prove a strong soundness result for our type system, stating that well-
typed, closed processes can always successfully terminate no matter how they
reduce.

######  Theorem 5.4 (soundness).

If $\emptyset\vdash^{n}P$ and $P\Rightarrow Q$, then
$Q\Rightarrow\preccurlyeq\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$.

There are several valuable implications of Theorem 5.4 on a well-typed, closed
process $P$:

Deadlock freedom.

If $Q$ cannot reduce any further, then it must be (structurally precongruent
to) done, namely there are no residual input/output actions.

Fair termination.

Under the fairness assumption, Theorem 2.5 assures that $P$ eventually reduces
to done. This also implies that every session created by $P$ eventually
terminates.

Progress.

If $Q$ contains a sub-process with pending input/output actions, the fact that
$Q$ may reduce to done means that these actions are eventually performed.

The proof of Theorem 5.4 is essentially composed of a standard subject
reduction result showing that typing is preserved by reductions and a proof
that every well-typed process other than done may always reduce in such a way
that a suitably defined _well-founded measure_ strictly decreases. The measure
is a lexicographically ordered pair of natural numbers with the following
meaning: the first component measures the number of sessions that must be
created and the total weight of casts that must be performed in order for the
process to terminate (this information is essentially the rank we associate
with typing judgments); the second component measures the overall effort
required to terminate every session that has already been created (these
sessions are identified by the fact that their restriction occurs unguarded in
the process). We account for this effort by measuring the shortest reduction
that terminates a coherent session map (Definition 4.2). The reason why we
need two quantities in the measure is that in general every application of
fair subtyping may _increase_ the length of the shortest reduction that
terminates a coherent session map. So, when casts are performed the second
component of the measure may increase, but the first component reduces. As a
final remark, it should be noted that the overall measure associated with a
well-typed process _may also increase_ , for example if new sessions are
created (Example 3.3). However, one particular reduction that decreases the
measure is always guaranteed to exist.

We conclude this section discussing a few more examples that motivate the
features of the type system that are key for ensuring fair program
termination.

######  Example 5.5.

To see simple examples of processes whose ill/well typing crucially depends on
the fact that we use a generalized inference system consider the definitions

$A\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}A\qquad
B\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}B\oplus B\qquad
C\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}C\oplus\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$

which define a stuck process $A$, a diverging process $B$ and a fairly
terminating process $C$ that admits an infinite reduction. For them we can
find the infinite typing derivations below:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
8.34442pt\hbox{$\displaystyle\penalty 1\mathstrut\smash{\vdots}$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=24.18884pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-call}{\textup{{\small[t-call]}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\emptyset\vdash^{0}A$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=131.89977pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-call}{\textup{{\small[t-call]}}}$}}}\hbox{\kern
53.85545pt\hbox{$\displaystyle\emptyset\vdash^{0}A$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip
5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\mathstrut\smash{\vdots}\qquad\hskip
5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 8.63782pt\hbox{$\displaystyle\penalty
1\mathstrut\smash{\vdots}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=24.77563pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-call}{\textup{{\small[t-call]}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\emptyset\vdash^{0}B$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=159.98659pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-choice}{\textup{{\small[t-choice]}}}$}}}\hbox{\kern
57.45099pt\hbox{$\displaystyle\emptyset\vdash^{0}B\oplus B$}}}}\hskip 5.0pt
plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=289.31047pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-call}{\textup{{\small[t-call]}}}$}}}\hbox{\kern
132.26741pt\hbox{$\displaystyle\emptyset\vdash^{0}B$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip
5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
8.52567pt\hbox{$\displaystyle\penalty 1\mathstrut\smash{\vdots}$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=24.55133pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-call}{\textup{{\small[t-call]}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\emptyset\vdash^{0}C$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 18.62222pt\hbox{$\displaystyle\penalty
1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=37.24445pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-done}{\textup{{\small[t-done]}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\emptyset\vdash^{0}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=286.95377pt\hbox{\kern
3.00003pt$\hyperlink{rule:t-choice}{\textup{{\small[t-choice]}}}$}}}\hbox{\kern
115.92343pt\hbox{$\displaystyle\emptyset\vdash^{0}C\oplus\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=416.27765pt\hbox{}}}\hbox{\kern
195.86316pt\hbox{$\displaystyle\emptyset\vdash^{0}C$}}}}$

However, only for $C$ it is possible to find a finite typing derivation using
the corule [co-choice]. So, $A$ and $B$ are ill typed, whereas $C$ is well
typed. This is consistent with the fact that only $C$ can always reduce to the
successfully terminated process done. $\lrcorner$

######  Example 5.6 (infinitely ranked processes).

The mere existence of a path that leads to termination ensured by the
generalized interpretation of the typing rules in Table 6 does not always
guarantee that the process is actually able to terminate. An example where
this is the case is shown by the process $A$ defined as

$A\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}(s)(s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\mathsf{!}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}a}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}],\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}b}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}].{A}\\}\mathrel{|}s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{?}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}a}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}].{A},\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}b}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\\})$

which creates a session $s$ and splits as two parallel sub-processes connected
by $s$. Each sub-process has a path that leads to termination but, because of
the way they synchronize, when one sub-process terminates the other one
restarts $A$. For $A$ it would be possible to build a finite typing derivation
with the help of [co-tag], but $A$ is ill typed because it cannot be assigned
a finite rank, since it creates a new session at each recursive invocation.

Further examples of infinitely ranked processes, including ones where the rank
is affected by the presence of casts, are discussed by Ciccone and Padovani
[13] for binary sessions and can be easily reframed in our multiparty setting.
$\lrcorner$

##  6 Advanced Examples

######  Example 6.1.

In this example we show that the process $\textit{Buyer}_{1}$ playing the role
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{1}$
in the inner session of Example 3.2 is well typed. For clarity, we recall its
definition here:

$Buyer_{1}(x,y)\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}y[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{2}]\mathsf{!}\\{\begin{array}[t]{@{}l@{}}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}split}.y[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{2}]\mathsf{?}\\{\begin{array}[t]{@{}l@{}}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}yes}.\lceil
x\rceil
x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}s}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}ok}.x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}c}]\mathsf{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}box}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,x.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,y.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done},\\\
\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}no}.Buyer_{1}\langle
x,y\rangle\\},\end{array}\\\
\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}giveup}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,y.\lceil
x\rceil
x[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}s}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}cancel}.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,x.\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}\\}\end{array}$

We wish to build a typing derivation showing that $Buyer_{1}$ has rank $1$ and
uses $x$ and $y$ respectively according to $S$ and $T$, where
$S=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}s}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}ok}.\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}c}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}box}.{?}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}s}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}cancel}.{?}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$
and
$T=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{2}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}split}.(\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{2}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}yes}.{?}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{2}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}no}.T)+\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{2}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}giveup}.{?}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$.
As it has been noted previously, what makes this process interesting is that
it uses the endpoint $x$ differently depending on the messages it exchanges
with
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}b}_{2}$
on $y$. Since rule [t-tag] requires any endpoint other than the one on which
messages are exchanged to have the same type, the only way
$\textit{Buyer}_{2}$ can be declared well typed is by means of the casts that
occur in its body. For the branch in which $\textit{Buyer}_{1}$ proposes to
split the payment we obtain the following derivation tree:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
18.62222pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus