11institutetext: IT University of Copenhagen, 2300 Copenhagen S, Denmark
11email<EMAIL_ADDRESS>
22institutetext: School of Computer Science, University of Birmingham, B15 2TT
Birmingham, United Kingdom
22email<EMAIL_ADDRESS>
# A Logical Interpretation of Asynchronous Multiparty Compatibility

Marco Carbone 11 0000-1111-2222-3333 Sonia Marin 22 1111-2222-3333-4444
Carsten Schürmann 11 2222–3333-4444-5555

###### Abstract

Session types are types for specifying the protocols that communicating
processes must follow in a concurrent system. When composing two or more well-
typed processes, a session typing system must check whether such processes are
multiparty compatible, a property that guarantees that all sent messages are
eventually received and no deadlock ever occurs. Previous work has shown that
duality and the more general notion of coherence are sufficient syntactic
conditions for guaranteeing the multiparty compatibility property.

In this paper, following a propositions-as-types fashion which relates session
types to linear logic, we generalise coherence to forwarders. Forwarders are
processes that act as middleware by forwarding messages according to a given
protocol. Our main result shows that forwarders not only generalise coherence,
but fully capture all well-typed multiparty compatible processes.

###### Keywords:

Linear Logic Session Types Process Compatibility.

##  1 Introduction

Session types, originally proposed by Honda et al. [18], are type annotations
that ascribe protocols to processes in a concurrent system and determine how
they behave when communicating together. _Binary session types_ found a
logical justification in _linear logic_ , identified by Caires and Pfenning
[4, 3] and later by Wadler [31, 32], which establishes the following
correspondences: session types _as_ linear logic propositions, processes _as_
proofs, reductions in the operational semantics _as_ cut reductions in linear
logic, and dualilty _as_ a notion of compatibility ensuring that two processes
communication pattern match.

In binary session types, a sufficient condition for two protocols to be
_compatible_ is that their type annotations are dual: the send action of one
party must match a corresponding receive action of the other party, and vice
versa. Because of asynchronous interleavings, however, there are protocols
that are compatible but not dual. The situation is even more complex for
_multiparty session types_ [20], which generalise binary session types to
types for protocols with more than two participants. A central observation is
that compatibility of sessions requires a property stronger than duality,
ensuring that all messages sent by any participating party will eventually be
collected by another. In [12], Deniélou and Yoshida proposed the semantic
notion of _multiparty compatibility_. The concept has then found many
successful applications in the literature [12, 24, 14]. The question whether
this notion “would be applicable to extend other theoretical foundations such
as the correspondence with linear logic to multiparty communications” has
however not been answered since Deniélou and Yoshida’s original work.

As a first step in defining a logical correspondent to multiparty
compatibility, Carbone et al. [9, 6] extended Wadler’s embedding of binary
session types into classical linear logic (CLL) to the multiparty setting by
generalising logical duality to the notion of coherence [20]. Coherence is a
compatibility condition: coherent processes are multiparty compatible, which
ensures that their execution never leads to a communication error. Coherence
is characterised proof-theoretically, and each coherence proof corresponds
precisely to a multiparty protocol specification (_global type_). An
interesting observation is that coherence proofs correspond to a definable
subset of the processes typable in linear logic, so-called arbiters [6]. In
retrospect, the concept of coherence has sharpened our proof-theoretic
understanding of how to characterise compatibility in multiparty session
types. However, coherence, similarly to duality, cannot capture completely the
notion of multiparty compatibility.

In this paper, we show that coherence can be generalised to a more expressive
logic of asynchronous forwarders. _Forwarders_ are processes that forward
messages between endpoints according to a protocol specification. Forwarders
are more general than arbiters (every arbiter corresponds to a forwarder but
not vice versa) but still can be used to guide the communication of multiple
processes and guarantee they communicate safely, as done by coherence in [6].
Our main result is that forwarders fully capture multiparty compatibility
which let us answer Deniélou and Yoshida’s original question positively. In
this work, we show that i) any possible interleaving of a set of multiparty
compatible processes can be represented as a forwarder, and, conversely, ii)
if a set of processes can be composed by a forwarder (describing a possible
execution), then such processes are indeed multiparty compatible.

Operationally, forwarders are a central process that decide how to dispatch
messages between peers, providing a global description of a multiparty
protocol (hence they can be seen as a generalisation of global types). They
capture the message flow by preventing messages from being duplicated, as
superfluous messages would not be accounted for, and by preventing messages
from being lost, otherwise a process might get stuck, awaiting a message.
However, when data-dependencies allow, forwarders can choose to receive
messages from different endpoints and forward such messages at a later point,
or decide to buffer a certain number of messages from a given sender.
Eventually, they simply re-transmit messages after receiving them, without
computing with them. Intuitively, this captures an interleaving of the
communications between the given endpoints.

Besides showing that they precisely capture multiparty compatibility, this
paper shows that forwarders can also replace duality or coherence for
composing well-typed processes. We achieve this logically: we replace the
linear logic cut rule with a new rule called MCutF which allows to compose two
or more processes (proofs) using a forwarder as a condition, instead of
duality [4] or coherence [6]. Our second main result is that MCutF can be
eliminated by proof reductions that correspond to asynchronous process
communications.

Although most of this paper’s interest is on their logical properties,
forwarders have other interesting features related to explaining communication
patterns as they occur in practice, including message routing, proxy services,
and runtime monitors for message flows [22].

Outline and key contributions. The key contributions of this paper include

  * •

a definition of multiparty compatibility for classical linear logic (§ 4);

  * •

a logical characterisation of _forwarders_ that enjoys a sound and complete
correspondence with multiparty compatibility (§ 5);

  * •

a composition mechanism (MCutF) for processes with asynchronous communication
that uses forwarders instead of coherence, and guarantees lack of
communication errors (§ 6).

Additionally, § 2 introduces the main concepts on an example and § 3 recaps
types, processes, and CP-typing. § 7 discusses related and future work.
Finally, concluding remarks are in § 8.

##  2 Preview

We start with a gentle introduction to asynchronous forwarders by informally
describing the classic _2-buyer protocol_ [19, 20], where two buyers intend to
buy a book jointly from a seller. The first buyer sends the title of the book
to the seller, who, in turn, sends a quote to both buyers. Then, the first
buyer decides how much she wishes to contribute and informs the second buyer,
who either pays the rest or cancels the transaction by informing the seller.
If the decision was made to buy the book, the second buyer will provide the
seller with an address, where to ship the book to.

The three participants are connected through endpoints
${\color[rgb]{0.8,0.25,0.33}{b_{1}}}$, ${\color[rgb]{0.8,0.25,0.33}{b_{2}}}$,
and ${\color[rgb]{0.8,0.25,0.33}{s}}$ respectively: an endpoint acts like a
socket where processes can write/read messages to/from. Each endpoint must be
used according to its respective session type which gives a precise
description of how each endpoint has to act. For example,
${\color[rgb]{0.8,0.25,0.33}{b_{1}}}:\mathbf{name}\otimes\mathbf{cost}^{\perp}\parr\mathbf{cost}\otimes\mathbf{1}$
says that buyer ${\color[rgb]{0.8,0.25,0.33}{b_{1}}}$ first sends (expressed
by $\otimes$) a value of type $\mathbf{name}$ (the book title), then receives
(expressed by $\parr$) a value of type $\mathbf{cost}^{\bot}$ (the price of
the book), then sends a value of type $\mathbf{cost}$ (the amount of money she
wishes to contribute), and finally terminates. Here, following classical
linear logic, the annotation ⊥ stands for dual. The behaviour of buyer
${\color[rgb]{0.8,0.25,0.33}{b_{2}}}$ and seller
${\color[rgb]{0.8,0.25,0.33}{s}}$ can similarly be specified by session types,
respectively
${\color[rgb]{0.8,0.25,0.33}{b_{2}}}:\mathbf{cost}^{\perp}\parr\mathbf{cost}^{\perp}\parr((\mathbf{addr}\otimes\mathbf{1})\oplus\mathbf{1})$
and
${\color[rgb]{0.8,0.25,0.33}{s}}:\mathbf{name}^{\perp}\parr\mathbf{cost}\otimes\mathbf{cost}\otimes((\,\mathbf{addr}\parr\perp\,)\
\&\perp)$.

Any well-typed processes with respective endpoints
${\color[rgb]{0.8,0.25,0.33}{b_{1}}}$, ${\color[rgb]{0.8,0.25,0.33}{b_{2}}}$,
and ${\color[rgb]{0.8,0.25,0.33}{s}}$ are going to execute this protocol
correctly because their type specifications are _compatible_ , meaning that
they match. In a multiparty setting, such compatibility can be expressed as
_coherence_ [6] and more generally with the semantic notion of _multiparty
compatibility_ [12]. Our theory of forwarders logically captures this notion
of multiparty compatibility precisely, namely that i) anything that has been
received is eventually sent, ii) anything that is sent must have been
previously received, and iii) the order of messages between any two points
must be preserved. A _forwarder_ captures the message flows between two or
more different endpoints. In the example above, a forwarder process may
receive a name from ${\color[rgb]{0.8,0.25,0.33}{b_{1}}}$, forward it to
${\color[rgb]{0.8,0.25,0.33}{s}}$, and then proceed to receiving the price
from ${\color[rgb]{0.8,0.25,0.33}{s}}$, forward it to
${\color[rgb]{0.8,0.25,0.33}{b_{1}}}$ and
${\color[rgb]{0.8,0.25,0.33}{b_{2}}}$, and so on. A forwarder acts as a medium
that, according to a prescribed protocol, dispatches messages processes send.
In the 2-buyers case, for ${\color[rgb]{0.8,0.25,0.33}{P_{s}}}$,
${\color[rgb]{0.8,0.25,0.33}{P_{b_{1}}}}$,
${\color[rgb]{0.8,0.25,0.33}{P_{b_{2}}}}$ respectively implementing the seller
and the two buyers, we can depict this with the following diagram:

In order to capture the message flows between several processes, forwarders
need to support buffering, reordering and other properties, which are not
necessarily coherent. Consider for example two endpoints
${\color[rgb]{0.8,0.25,0.33}{x}}$ and ${\color[rgb]{0.8,0.25,0.33}{y}}$
willing to communicate with the following protocol – called a _criss-cross_ :
they both send a message to each other, and then the messages are received,
according to the following types
${\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{name}\otimes\mathbf{cost}\parr\mathbf{1}$
and
${\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{cost}^{\perp}\otimes\mathbf{name}^{\perp}\parr\bot$.
Such protocol leads to no error (assuming processes implement an asynchronous
semantics), still the two types above are not coherent [6] and not even dual
to each other. On the other hand, we can easily write a forwarder typable in
the context
${\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{name}^{\perp}\parr\mathbf{cost}^{\perp}\otimes\bot,{\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{cost}\parr\mathbf{name}\otimes\mathbf{1}$
formed by their duals, i.e., a process that first receives on both
${\color[rgb]{0.8,0.25,0.33}{x}}$ and ${\color[rgb]{0.8,0.25,0.33}{y}}$ and
then forwards the received messages over to ${\color[rgb]{0.8,0.25,0.33}{y}}$
and ${\color[rgb]{0.8,0.25,0.33}{x}}$, respectively.

##  3 CP and Classical Linear Logic

In this section, we give an introduction to the proposition-as-sessions
approach [32]. This comprises the syntax of types and processes and the
interpretation of processes as sequent proofs in classical linear logic (CLL).

Types. Following the propositions-as-types approach, types, taken to be
propositions (formulas) of CLL, denote the way an endpoint (a channel end)
must be used at runtime. Their formal syntax is given by the following
grammar:

$\begin{array}[]{lrcl}\mbox{Types}&A&\mathrel{::=}&a\mid
a^{\perp}\mid\mathbf{1}\mid\bot\mid A\otimes A\mid A\parr A\mid A\oplus A\mid
A\with A\mid!A\mid?A\end{array}$ (1)

Atoms $a$ and negated atoms $a^{\bot}$ are basic dual types. Types
$\mathbf{1}$ and $\perp$ denote an endpoint that must close with a last
synchronisation. A type $A\otimes B$ is assigned to an endpoint that outputs a
message of type $A$ and then is used as $B$, and similarly, an endpoint of
type $A\parr B$, receives a message of type $A$ and continues as $B$. In the
situation of a branching choice, $A\oplus B$ is the type of an endpoint that
may select to go left or right and continues as $A$ or $B$, respectively, and
$A\with B$ is the type of an endpoint that offers two choices (left or right)
and then, based on such choice, continues as $A$ or $B$. Finally, $!A$ types
an endpoint offering an unbounded number of copies of a service of type $A$,
while $?A$ types an endpoint of a client invoking some replicated/unbounded
service with behaviour $A$.

Duality. Operators can be grouped in pairs of duals that reflect the input-
output duality. Consequently, standard duality $(\cdot)^{\perp}$ on types is
inductively defined as:

$(a^{\bot})^{\bot}=a\qquad\mathbf{1}^{\bot}=\perp\qquad(A\otimes
B)^{\bot}=A^{\bot}\parr B^{\bot}\quad(A\oplus B)^{\bot}=A^{\bot}\with
B^{\bot}\quad(!A)^{\bot}=?A^{\bot}$

In the remainder, for any binary operators
$\oslash,\odot\in\\{\otimes,\parr,\oplus,\with\\}$, we sometimes write
$A\oslash B\odot C$ to mean $A\oslash(B\odot C)$.

Processes. We use a standard language of processes to represent communicating
entities (including forwarders) which is a variant of the $\pi$-calculus [26]
with specific communication primitives as usually done for session calculi.
Moreover, given that the theory of this paper is based on the proposition-as-
sessions correspondence with CLL, we adopt a syntax akin to that of Wadler
[32]. Each process can be found on the left-hand side of the turnstyle
$\vdash$ in the conclusion of each rule in Figure 1. We briefly comment each
process term. A link ${\color[rgb]{0.8,0.25,0.33}{x\leftrightarrow y}}$ is a
binary forwarder, i.e., a process that forwards any communication between
endpoints ${\color[rgb]{0.8,0.25,0.33}{x}}$ and
${\color[rgb]{0.8,0.25,0.33}{y}}$. This yields a sort of equality relation on
names: it says that endpoints ${\color[rgb]{0.8,0.25,0.33}{x}}$ and
${\color[rgb]{0.8,0.25,0.33}{y}}$ are equivalent, and communicating something
over ${\color[rgb]{0.8,0.25,0.33}{x}}$ is like communicating it over
${\color[rgb]{0.8,0.25,0.33}{y}}$. Note that we use endpoints instead of
channels [30]. The difference is subtle: the restriction
${\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}xy)\,}}$ connects the two endpoints
${\color[rgb]{0.8,0.25,0.33}{x}}$ and ${\color[rgb]{0.8,0.25,0.33}{y}}$,
instead of referring to the channel between them. The terms
${\color[rgb]{0.8,0.25,0.33}{x().P}}$ and
${\color[rgb]{0.8,0.25,0.33}{{x}[]}}$ handle synchronisation (no message
passing); ${\color[rgb]{0.8,0.25,0.33}{x().P}}$ can be seen as an empty input
on ${\color[rgb]{0.8,0.25,0.33}{x}}$, while
${\color[rgb]{0.8,0.25,0.33}{{x}[]}}$ terminates the execution of the process.
The term ${\color[rgb]{0.8,0.25,0.33}{{x}[y\triangleright P].Q}}$ denotes a
process that creates a fresh name ${\color[rgb]{0.8,0.25,0.33}{y}}$ (hence a
new session), spawns a new process ${\color[rgb]{0.8,0.25,0.33}{P}}$, and then
continues as ${\color[rgb]{0.8,0.25,0.33}{Q}}$. The intuition behind this
communication operation is that ${\color[rgb]{0.8,0.25,0.33}{P}}$ uses
${\color[rgb]{0.8,0.25,0.33}{y}}$ as an interface for dealing with the
continuation of the dual primitive (denoted by term
${\color[rgb]{0.8,0.25,0.33}{{x}(y).R}}$, for some
${\color[rgb]{0.8,0.25,0.33}{R}}$). Note that output messages are always
fresh, as for the internal $\pi$-calculus [27], hence the output term
${\color[rgb]{0.8,0.25,0.33}{{x}[y\triangleright P].Q}}$ is a compact version
of the $\pi$-calculus term $(\nu y)\,\overline{x}y.(P\,|\,Q)$. Branching
computations are handled by
${\color[rgb]{0.8,0.25,0.33}{x.\mathsf{case}(P,Q)}}$,
${\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inl}].P}}$ and
${\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inr}].P}}$. The former denotes a
process offering two options (external choice) from which some other process
can make a selection with ${\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inl}].P}}$
or ${\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inr}].P}}$ (internal choice).
Finally, ${\color[rgb]{0.8,0.25,0.33}{\oc x(y).P}}$ denotes a persistently
available service that can be invoked by ${\color[rgb]{0.8,0.25,0.33}{\wn
x[z].Q}}$ which will spawn a new session to be handled by a copy of process
${\color[rgb]{0.8,0.25,0.33}{P}}$.

$\begin{array}[]{c}{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{x\leftrightarrow
y}}}}\vdash{\color[rgb]{0.8,0.25,0.33}{x}}:a^{\bot},{\color[rgb]{0.8,0.25,0.33}{y}}:a\qquad{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}[]}}}}\vdash{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{1}\qquad{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{x().P}}}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:\bot{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta\\\\[4.30554pt]
{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}[y\triangleright
P].Q}}}}\vdash\Delta_{1},\Delta_{2},{\color[rgb]{0.8,0.25,0.33}{x}}:A_{1}\otimes
A_{2}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta_{1},{\color[rgb]{0.8,0.25,0.33}{y}}:A_{1}{\color[rgb]{0.8,0.25,0.33}{Q}}\vdash\Delta_{2},{\color[rgb]{0.8,0.25,0.33}{x}}:A_{2}\qquad{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}(y).P}}}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A_{1}\parr
A_{2}{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{y}}:A_{1},{\color[rgb]{0.8,0.25,0.33}{x}}:A_{2}\\\\[4.30554pt]
{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inl}].P}}}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A_{1}\oplus
A_{2}{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A_{1}\qquad{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inr}].P}}}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A_{1}\oplus
A_{2}{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A_{2}\qquad{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{x.\mathsf{case}(P,Q)}}}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A_{1}\with
A_{2}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A_{1}{\color[rgb]{0.8,0.25,0.33}{Q}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A_{2}\\\\[4.30554pt]
{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{\oc
x(y).P}}}}\vdash\,\wn\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:\oc
A{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\,\wn\Delta,{\color[rgb]{0.8,0.25,0.33}{y}}:A\qquad{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{\wn
x[y].P}}}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{y}}:A\qquad{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta\qquad{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn A\end{array}$ Figure 1: Sequent Calculus
for CP and Classical Linear Logic

###### Example 1

For some ${\color[rgb]{0.8,0.25,0.33}{P_{i}}}$ ,
${\color[rgb]{0.8,0.25,0.33}{Q_{j}}}$, ${\color[rgb]{0.8,0.25,0.33}{R_{k}}}$,
we provide possible implementations for processes
${\color[rgb]{0.8,0.25,0.33}{P_{s}}}$,
${\color[rgb]{0.8,0.25,0.33}{P_{b_{1}}}}$, and
${\color[rgb]{0.8,0.25,0.33}{P_{b_{2}}}}$ from the 2-buyer example.

$\begin{array}[]{rll}{\color[rgb]{0.8,0.25,0.33}{P_{s}}}\
=&{\color[rgb]{0.8,0.25,0.33}{{s}(book).}}\
{\color[rgb]{0.8,0.25,0.33}{{s}[price\triangleright P_{1}].}}\
{\color[rgb]{0.8,0.25,0.33}{{s}[price\triangleright P_{2}].}}\
{\color[rgb]{0.8,0.25,0.33}{s.\mathsf{case}({\color[rgb]{0.8,0.25,0.33}{{s}(addr).P_{3}}},P_{4})}}\\\
{\color[rgb]{0.8,0.25,0.33}{P_{b_{1}}}}\
=&{\color[rgb]{0.8,0.25,0.33}{{b_{1}}[book\triangleright Q_{1}].}}\
{\color[rgb]{0.8,0.25,0.33}{{b_{1}}(price).}}\
{\color[rgb]{0.8,0.25,0.33}{{b_{1}}[contr\triangleright Q_{2}].Q_{3}}}\\\
{\color[rgb]{0.8,0.25,0.33}{P_{b_{2}}}}\
=&{\color[rgb]{0.8,0.25,0.33}{{b_{2}}(price).}}\
{\color[rgb]{0.8,0.25,0.33}{{b_{2}}(contr).}}\
{\color[rgb]{0.8,0.25,0.33}{{b_{2}}[\mathsf{inl}].{\color[rgb]{0.8,0.25,0.33}{{b_{2}}[addr\triangleright
R_{1}].R_{2}}}}}\end{array}$

Note that the order the two buyers receive the price is not relevant.

CP-typing. As shown by Wadler [32], CLL proofs can be associated to a subset
of well-behaved processes, that satisfy deadlock freedom and session fidelity.

Judgements are defined as ${\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta$ with
$\Delta$ a set of named types, i.e.,
$\Delta\coloncolonequals\varnothing\mid{\color[rgb]{0.8,0.25,0.33}{x}}:A,\Delta$.
The system, called CP and reported in Figure 1, uses CLL to type processes.

CP can be extended with a structural rule for defining composition of
processes which corresponds to the Cut rule from classical linear logic:

${\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}xy)\,(P{\ \;\bm{|}\
\;}Q)}}\vdash\Sigma,\Delta\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:A{\color[rgb]{0.8,0.25,0.33}{Q}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{y}}:A^{\bot}$

In linear logic this rule is admissible, i.e., the CLL derivations of the two
premises can be combined into a derivation of the conclusion with no
occurrence of the Cut rule. Moreover, this is a constructive procedure, called
_cut-elimination_ , meaning that the proof with cut is inductively transformed
into a proof without cut. The strength of the proposition-as-type
correspondence stems from the fact that it carries on to the proof level, as
it was shown that the cut-elimination steps correspond to reductions in the
$\pi$-calculus [4, 31].

##  4 Multiparty Compatibility

Duality is a condition that guarantees composed processes (proofs) to be well-
behaved. This can be seen in rule Cut which composes two processes through
endpoints that are dual: cut elimination guarantees that such processes can
communicate with each other without getting stuck or reaching an error.
Multiparty compatibility [12, 24, 14], a semantic notion that allows for the
composition of multiple processes while guaranteeing the same properties, uses
session types as an abstraction of process behaviours and simulates their
execution. If no error occurs during any such simulation then the composition
is considered compatible.

Extended types and queues. In order to define multiparty compatibility to our
logical setting with CLL formulas, we extend the syntax of types (formulas)
with annotations that make explicit where messages should be forwarded from
and to. This is similar to local types $!{\mathsf{p}}.T$ and $?{\mathsf{p}}.T$
[11] expressing an output and an input to and from role $\mathsf{p}$
respectively. The meaning of each operator and the definition of duality
remains the same as in CP.

$\begin{array}[]{lrcl}\mbox{Types}&A&\mathrel{::=}&a\mid
a^{\perp}\mid\mathbf{1}\mid\bot\mid A\otimes A\mid A\parr A\mid A\oplus A\mid
A\with A\mid!A\mid?A\\\ \mbox{Local types}&B&\mathrel{::=}&a\mid
a^{\perp}\mid\mathbf{1}^{\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}\mid\bot^{\color[rgb]{0.8,0.25,0.33}{u}}\mid(A\otimes^{\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}B)\mid(A\parr^{\color[rgb]{0.8,0.25,0.33}{u}}B)\\\
&&&\quad\mid\oc^{\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}B\mid\wn^{\color[rgb]{0.8,0.25,0.33}{u}}B\mid(B\oplus^{\color[rgb]{0.8,0.25,0.33}{u}}B)\mid(B\with^{\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}B)\end{array}$

Annotations are either single endpoints ${\color[rgb]{0.8,0.25,0.33}{x}}$ or a
set of endpoints ${\color[rgb]{0.8,0.25,0.33}{u_{1},\ldots,u_{n}}}$. The left-
hand side $A$ of $\otimes$ and $\parr$ are not annotated (they will become
dynamically labelled when needed). We will see that units demonstrate some
_gathering_ behaviour which explains the need to annotate $\mathbf{1}$ with a
non-empty list of an arbitrary number of distinct names. We may write
${\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}$ for
${\color[rgb]{0.8,0.25,0.33}{u_{1},\ldots,u_{n}}}$ when the size of the list
is irrelevant.

Additionally to annotated types, in order to give a semantics to types, we
introduce queues defined by as
$\begin{array}[]{rcl}{\Psi}&\coloncolonequals&\epsilon\mid
A\cdot\Psi\mid{{\color[rgb]{0,0,1}\ast}}\cdot\Psi\mid{{\color[rgb]{0,0,1}\mathcal{L}}}\cdot\Psi\mid{{\color[rgb]{0,0,1}\mathcal{R}}}\cdot\Psi\mid{{\color[rgb]{0,0,1}\mathcal{Q}}}\cdot\Psi\end{array}$.
Intuitively, a queue (FIFO) is a standard ordered list of messages. A message
can be a proposition $A$, a session termination ${\color[rgb]{0,0,1}\ast}$, a
choice ${\color[rgb]{0,0,1}\mathcal{L}}$ or ${\color[rgb]{0,0,1}\mathcal{R}}$,
or an exponential ${\color[rgb]{0,0,1}\mathcal{Q}}$. Since every ordered pair
of endpoints has an associated queue, we define a queue environment $\sigma$
as a mapping from ordered pairs of endpoints to queues:
$\sigma:(x,y)\mapsto\Psi$. In the sequel, $\sigma_{\epsilon}$ denotes the
queue environment with only empty queues. The notation
$\sigma[({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y}})\mapsto\Psi]$
denotes a new environment where the entry for
$({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y}})$ has been
updated to $\Psi$. Finally, we are ready to define type-context semantics for
an annotated environment, i.e., an environment $\Delta$ where each formula has
been annotated (with a slight abuse of notation, we overload the category
$\Delta$):

######  Definition 1 (Type-Context Semantics)

We define $\xrightarrow{\alpha}$ as the minimum relation on annotated $\Delta$
satisfying the following rules:

$\begin{array}[]{lc@{\quad}l}\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:\perp^{{\color[rgb]{0.8,0.25,0.33}{y}}}\bullet\sigma[({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y}})\mapsto\Psi]&\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{x}}\perp{\color[rgb]{0.8,0.25,0.33}{y}}}&\Delta\bullet\sigma[({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y}})\mapsto\Psi\cdot{{\color[rgb]{0,0,1}\ast}}]\\\
{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{1}^{{\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}}\bullet\
\sigma_{\epsilon}[\\{({\color[rgb]{0.8,0.25,0.33}{y_{i},}}{\color[rgb]{0.8,0.25,0.33}{x}})\mapsto{\color[rgb]{0,0,1}\ast}\\}_{i}]&\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}\mathbf{1}{\color[rgb]{0.8,0.25,0.33}{x}}}&\varnothing\bullet\sigma_{\epsilon}\\\
{\color[rgb]{0.8,0.25,0.33}{x}}:a^{\bot},{\color[rgb]{0.8,0.25,0.33}{y}}:a\bullet\sigma_{\epsilon}&\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{x}}{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{\leftrightarrow}}y}}}&\varnothing\bullet\sigma_{\epsilon}\\\
\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A\parr^{{\color[rgb]{0.8,0.25,0.33}{y}}}B\bullet\sigma[({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y}})\mapsto\Psi]&\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{x}}\parr{\color[rgb]{0.8,0.25,0.33}{y}}}&\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:B\bullet\sigma[({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y}})\mapsto\Psi\cdot
A]\\\
\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A\otimes^{{\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}}B\bullet\sigma[\\{({\color[rgb]{0.8,0.25,0.33}{y_{i}}},{\color[rgb]{0.8,0.25,0.33}{x}})\mapsto
A_{i}\cdot\Psi_{i}\\}_{i}]&\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}\otimes{\color[rgb]{0.8,0.25,0.33}{x}}[A,\\{A_{i}\\}_{i}]}&\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:B\bullet\sigma[\\{({\color[rgb]{0.8,0.25,0.33}{y_{i}}},{\color[rgb]{0.8,0.25,0.33}{x}})\mapsto\Psi_{i}\\}_{i}]\\\
\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A\with^{{\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}}B\bullet\sigma[\\{({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y_{i}}})\mapsto\Psi_{i}\\}_{i}]&\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{x}}\with_{{\color[rgb]{0,0,1}\mathcal{L}}}{\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}}&\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A\bullet\sigma[\\{({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y_{i}}})\mapsto\Psi_{i}\cdot{{\color[rgb]{0,0,1}\mathcal{L}}}\\}_{i}]\\\
\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A\with^{{\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}}B\bullet\sigma[\\{({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y_{i}}})\mapsto\Psi_{i}\\}_{i}]&\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{x}}\with_{{\color[rgb]{0,0,1}\mathcal{R}}}{\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}}&\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:B\bullet\sigma[\\{({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y_{i}}})\mapsto\Psi_{i}\cdot{{\color[rgb]{0,0,1}\mathcal{R}}}\\}_{i}]\\\
\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A\oplus^{{\color[rgb]{0.8,0.25,0.33}{y}}}B\bullet\sigma[({\color[rgb]{0.8,0.25,0.33}{y}},{\color[rgb]{0.8,0.25,0.33}{x}})\mapsto{{\color[rgb]{0,0,1}\mathcal{L}}}\cdot\Psi]&\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{y}}\oplus_{{\color[rgb]{0,0,1}\mathcal{L}}}{\color[rgb]{0.8,0.25,0.33}{x}}}&\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A\bullet\sigma[({\color[rgb]{0.8,0.25,0.33}{y}},{\color[rgb]{0.8,0.25,0.33}{x}})\mapsto\Psi]\\\
\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A\oplus^{{\color[rgb]{0.8,0.25,0.33}{y}}}B\bullet\sigma[({\color[rgb]{0.8,0.25,0.33}{y}},{\color[rgb]{0.8,0.25,0.33}{x}})\mapsto{{\color[rgb]{0,0,1}\mathcal{R}}}\cdot\Psi]&\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{y}}\oplus_{{\color[rgb]{0,0,1}\mathcal{R}}}{\color[rgb]{0.8,0.25,0.33}{x}}}&\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:B\bullet\sigma[({\color[rgb]{0.8,0.25,0.33}{y}},{\color[rgb]{0.8,0.25,0.33}{x}})\mapsto\Psi]\\\
\\{{\color[rgb]{0.8,0.25,0.33}{y_{i}}}:\wn
A_{i}\\}_{i},{\color[rgb]{0.8,0.25,0.33}{x}}:\oc^{{\color[rgb]{0.8,0.25,0.33}{y}}}A\bullet\sigma_{\epsilon}&\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{x}}\mathbin{!}{\color[rgb]{0.8,0.25,0.33}{y}}}&\\{{\color[rgb]{0.8,0.25,0.33}{y_{i}}}:\wn
A_{i}\\}_{i},{\color[rgb]{0.8,0.25,0.33}{x}}:A\bullet\sigma_{\epsilon}[\\{({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y_{i}}})\mapsto{\color[rgb]{0,0,1}\mathcal{Q}}\\}_{i}]\\\
\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn^{{\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}}A\bullet\sigma[({\color[rgb]{0.8,0.25,0.33}{y}},{\color[rgb]{0.8,0.25,0.33}{x}})\mapsto{\color[rgb]{0,0,1}\mathcal{Q}}\cdot\Psi]&\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{y}}\mathbin{?}{\color[rgb]{0.8,0.25,0.33}{x}}}&\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A\bullet\sigma[({\color[rgb]{0.8,0.25,0.33}{y}},{\color[rgb]{0.8,0.25,0.33}{x}})\mapsto\Psi]\end{array}$

The rules above capture an asynchronous semantics for typing contexts. We
clarify further with an example of how the semantics above works. Assume we
wish to compose three CP proofs through endpoints
$\Delta={\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot}\parr
B,{\color[rgb]{0.8,0.25,0.33}{y}}:A^{\bot}\parr A\otimes
C,{\color[rgb]{0.8,0.25,0.33}{z}}:A\otimes D$. The context says that
${\color[rgb]{0.8,0.25,0.33}{x}}$ is receiving something of type $A^{\bot}$,
${\color[rgb]{0.8,0.25,0.33}{y}}$ is receiving something of type $A^{\bot}$
and then sending something of type $A$, and, finally,
${\color[rgb]{0.8,0.25,0.33}{z}}$ is sending something of type $A$. In order
to obtain an execution of $\Delta$, we first dualise and annotate $\Delta$
(for some annotation) to, e.g.,
$\Delta^{\bot}={\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot}\otimes^{{\color[rgb]{0.8,0.25,0.33}{y}}}B^{\bot},{\color[rgb]{0.8,0.25,0.33}{y}}:A\otimes^{{\color[rgb]{0.8,0.25,0.33}{z}}}A^{\bot}\parr^{{\color[rgb]{0.8,0.25,0.33}{x}}}C^{\bot},{\color[rgb]{0.8,0.25,0.33}{z}}:A^{\bot}\parr^{{\color[rgb]{0.8,0.25,0.33}{y}}}D^{\bot}$.
Then, obtain an execution, e.g.,:

$\begin{array}[]{rl}\Delta^{\bot}\bullet\sigma_{\epsilon}\quad\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{z}}\parr{\color[rgb]{0.8,0.25,0.33}{y}}}&{\color[rgb]{0.8,0.25,0.33}{x}}:A\otimes^{{\color[rgb]{0.8,0.25,0.33}{y}}}B,{\color[rgb]{0.8,0.25,0.33}{y}}:A\otimes^{{\color[rgb]{0.8,0.25,0.33}{z}}}A^{\bot}\parr^{{\color[rgb]{0.8,0.25,0.33}{x}}}C^{\bot},{\color[rgb]{0.8,0.25,0.33}{z}}:D\
\bullet\
\sigma_{\epsilon}[({\color[rgb]{0.8,0.25,0.33}{z}},{\color[rgb]{0.8,0.25,0.33}{y}})\mapsto
A^{\bot}]\\\
\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{z}}\otimes{\color[rgb]{0.8,0.25,0.33}{y}}[A,A^{\bot}]}&{\color[rgb]{0.8,0.25,0.33}{x}}:A\otimes^{{\color[rgb]{0.8,0.25,0.33}{y}}}B,{\color[rgb]{0.8,0.25,0.33}{y}}:A^{\bot}\parr^{{\color[rgb]{0.8,0.25,0.33}{x}}}C^{\bot},{\color[rgb]{0.8,0.25,0.33}{z}}:D\
\bullet\ \sigma_{\epsilon}\\\
\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{y}}\parr{\color[rgb]{0.8,0.25,0.33}{x}}}&{\color[rgb]{0.8,0.25,0.33}{x}}:A\otimes^{{\color[rgb]{0.8,0.25,0.33}{y}}}B,{\color[rgb]{0.8,0.25,0.33}{y}}:C^{\bot},{\color[rgb]{0.8,0.25,0.33}{z}}:D\
\bullet\
\sigma_{\epsilon}[({\color[rgb]{0.8,0.25,0.33}{y}},{\color[rgb]{0.8,0.25,0.33}{x}})\mapsto
A^{\bot}]\\\
\xrightarrow{{\color[rgb]{0.8,0.25,0.33}{y}}\otimes{\color[rgb]{0.8,0.25,0.33}{x}}[A,A^{\bot}]}&{\color[rgb]{0.8,0.25,0.33}{x}}:B,{\color[rgb]{0.8,0.25,0.33}{y}}:C,{\color[rgb]{0.8,0.25,0.33}{z}}:D\
\bullet\ \sigma_{\epsilon}\end{array}$

Note the general rule for the multiplicative connectors $\otimes$ and $\parr$.
In their multiparty interpretation [6], they implement a gathering
communication, where many $A_{i}\otimes B_{i}$ can communicate with a single
$A\parr B$. As a consequence, the $A_{i}$’s are enqueued to a single endpoint
which will consume such messages. The effect of a gathering communication with
such connectives is to spawn a new session with the environment
$\\{{A_{i}}\\}_{i}$ shown in the label. Ideally, we could have enriched the
semantics so that it can work on different contexts running in parallel, where
$\\{{A_{i}}\\}_{i}$ would be added to. However, since the need for the
semantics is to define compatibility we decided to just observe in the label.
Units also have a similar gathering behaviour. On the other hand, additives
and exponentials use broadcasting.

Using the relation on contexts above, we can define when a set of endpoints
successfully progresses without reaching an error. This can be formalised by
the concept of live path. In the sequel, let $\alpha$ range over all the
possible labels of the relation above. Moreover, let
$\alpha_{1},\ldots,\alpha_{n}$ be a path for some annotated $\Delta$ whenever
there exist $\Delta_{1},\sigma_{1},\ldots\Delta_{n},\sigma_{n}$ such that
$\Delta\bullet\sigma_{\epsilon}\xrightarrow{\alpha_{1}}\Delta_{1}\bullet\sigma_{1}\ldots\xrightarrow{\alpha_{n}}\Delta_{n}\bullet\sigma_{n}$.
This path is maximal if there is no $\Delta_{n+1},\sigma_{n+1},\alpha_{n+1}$
such that
$\Delta_{n}\bullet\sigma_{n}\xrightarrow{\alpha_{n+1}}\Delta_{n+1}\bullet\sigma_{n+1}$.

######  Definition 2 (Live Path)

A path $\tilde{\alpha}$ for an environment $\Delta\bullet\sigma$ is live if
$\Delta\bullet\sigma\xrightarrow{\alpha_{1}}\ldots\xrightarrow{\alpha_{n}}\varnothing\bullet\sigma_{\epsilon}$.

Intuitively, a maximal path is live whenever we can consume all sends and
receives specified in the type context and all queues are empty, i.e., an
error is never reached. With this notion, we are ready to define multiparty
compatibility:

######  Definition 3 (Multiparty Compatibility)

An environment $\Delta\bullet\sigma$ is executable if all maximal paths
$\alpha_{1},\ldots,\alpha_{n}$ for $\Delta$ are live and such that
$\alpha_{i}={\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}\otimes{\color[rgb]{0.8,0.25,0.33}{x}}[A,\mathopen{}\left\\{A_{i}\right\\}_{i}\mathclose{}]$
implies
${\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot},\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{y_{i}}}:A_{i}^{\bot}\right\\}_{i}\mathclose{}$
is multiparty compatible for some annotation. A context
$\Delta\not=\varnothing$ is multiparty compatible if there exists an
annotation such that $\Delta^{\bot}\bullet\sigma_{\epsilon}$ is executable.

Multiparty compatibility states that all maximal paths are live, i.e., an
error is never reached. Note that the definition above is well-founded since
propositions get smaller when reduced.

Relationship to Previous Definitions. Definition 1 is an adaptation to CLL of
the typing environment reduction (Definition 4.3, [14]) with a little twist:
in order not to overload notation (cf. § 5), we are defining it on the dual of
formulas. For example, following an approach as that of [14], a process with
an endpoint ${\color[rgb]{0.8,0.25,0.33}{x}}$ of type
$A\otimes^{{\color[rgb]{0.8,0.25,0.33}{y}}}B$ is meant to store something of
type $A$ in the queue from ${\color[rgb]{0.8,0.25,0.33}{x}}$ to
${\color[rgb]{0.8,0.25,0.33}{y}}$. In our notation, we dualise the type of
${\color[rgb]{0.8,0.25,0.33}{x}}$ to
$A^{\bot}\parr^{{\color[rgb]{0.8,0.25,0.33}{y}}}B^{\bot}$ but keep the same
behaviour, i.e., storing something of type $A^{\bot}$ in the queue from
${\color[rgb]{0.8,0.25,0.33}{x}}$ to ${\color[rgb]{0.8,0.25,0.33}{y}}$.
Moreover, for the sake of simplicity, we are using a single queue environment
$\sigma$ as a function from pairs of endpoints to a FIFO, while Ghilezan et
al. [14] use labelled queues attached to each endpoint of the typing context:
the two approaches are equivalent. Finally, our definition being an adaptation
to CLL, uses different language constructs. In particular, we do not combine
value passing and branching, and our $\otimes$ and $\parr$ cases spawn new
sessions (hence the well-founded recursive definition). The original
definition of compatibility given by Deniélou and Yoshida is for communicating
automata. Therefore, our starting point is the adaptation to local types given
by Ghilezan et al. [14].

Properties of Multiparty Compatibility. As a consequence of multiparty
compatibility, we can formalise the lack of errors with the following

######  Proposition 1 (No Error)

Let $\Delta$ be multiparty compatible and $\alpha_{1},\ldots,\alpha_{n}$ be a
maximal path for an annotated $\Delta^{\bot}$ such that
$\Delta^{\bot}\bullet\sigma_{\epsilon}\xrightarrow{\alpha_{1}}\Delta_{1}\bullet\sigma_{1}\ldots\xrightarrow{\alpha_{n}}\varnothing\bullet\sigma_{\epsilon}$.
Then, for $i<n$,

  1. 1.

    1. (a)

$\sigma_{i}({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y}})={\color[rgb]{0,0,1}\ast}\cdot\Psi$
implies that
$\alpha_{n}={\color[rgb]{0.8,0.25,0.33}{x\tilde{z}}}\mathbf{1}{\color[rgb]{0.8,0.25,0.33}{y}}$;

    2. (b)

$\sigma_{i}({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y}})=A\cdot\Psi$
implies that there exists $k>i$ such that
$\alpha_{k}={\color[rgb]{0.8,0.25,0.33}{x\tilde{z}}}\otimes{\color[rgb]{0.8,0.25,0.33}{y}}[A,\\{A_{i}\\}_{i}]$;

    3. (c)

$\sigma_{i}({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y}})={\color[rgb]{0,0,1}\mathcal{L}}\cdot\Psi$
implies that there exists $k>i$ such that
$\alpha_{k}={\color[rgb]{0.8,0.25,0.33}{x}}\oplus_{{\color[rgb]{0,0,1}\mathcal{L}}}{\color[rgb]{0.8,0.25,0.33}{y}}$;

    4. (d)

$\sigma_{i}({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y}})={\color[rgb]{0,0,1}\mathcal{R}}\cdot\Psi$
implies that there exists $k>i$ such that
$\alpha_{k}={\color[rgb]{0.8,0.25,0.33}{x}}\oplus_{{\color[rgb]{0,0,1}\mathcal{R}}}{\color[rgb]{0.8,0.25,0.33}{y}}$;

    5. (e)

$\sigma_{i}({\color[rgb]{0.8,0.25,0.33}{x}},{\color[rgb]{0.8,0.25,0.33}{y}})={\color[rgb]{0,0,1}\mathcal{Q}}\cdot\Psi$
implies that there exists $k>i$ such that
$\alpha_{k}={\color[rgb]{0.8,0.25,0.33}{x}}\mathbin{?}{\color[rgb]{0.8,0.25,0.33}{y}}$;

  2. 2.

    1. (a)

$\Delta_{i}=\Delta_{i}^{\prime},{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{1}^{{\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}}$,
then
$\alpha_{n}={\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}\mathbf{1}{\color[rgb]{0.8,0.25,0.33}{x}}$;

    2. (b)

$\Delta_{i}=\Delta_{i}^{\prime},{\color[rgb]{0.8,0.25,0.33}{x}}:A\otimes^{{\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}}B$,
then there exists $k>i$ such that
$\alpha_{k}={\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}\otimes{\color[rgb]{0.8,0.25,0.33}{x}}[\\{A_{i}\\}_{i}]$;

    3. (c)

$\Delta_{i}=\Delta_{i}^{\prime},{\color[rgb]{0.8,0.25,0.33}{x}}:A\oplus^{{\color[rgb]{0.8,0.25,0.33}{y}}}B$,
then there exists $k>i$ such that
$\alpha_{k}={\color[rgb]{0.8,0.25,0.33}{y}}\oplus_{{\color[rgb]{0,0,1}\mathcal{L}}}{\color[rgb]{0.8,0.25,0.33}{x}}$
or
$\alpha_{k}={\color[rgb]{0.8,0.25,0.33}{y}}\oplus_{{\color[rgb]{0,0,1}\mathcal{R}}}{\color[rgb]{0.8,0.25,0.33}{x}}$;

    4. (d)

$\Delta_{i}=\Delta_{i}^{\prime},{\color[rgb]{0.8,0.25,0.33}{x}}:\wn^{{\color[rgb]{0.8,0.25,0.33}{y}}}A$,
then there exists $k>i$ such that
$\alpha_{k}={\color[rgb]{0.8,0.25,0.33}{y}}\mathbin{?}{\color[rgb]{0.8,0.25,0.33}{x}}$.

Conditions in (1) state that every message that has been enqueued is
eventually consumed. On the other hand, conditions in (2) state that every
input instruction is eventually executed. Note also that since we have no
infinite computations, we do not need to consider fairness.

Are annotations important? A careful reader may be wondering why the
definitions of type-context semantics and multiparty compatibility are not
given for annotation-free contexts. Unfortunately, doing so would make
multiparty compatibility too strong since we would have to allow for messages
to be sent to different endpoints in different paths. As an example,
${\color[rgb]{0.8,0.25,0.33}{x}}:A\otimes
B^{\bot},{\color[rgb]{0.8,0.25,0.33}{y}}:A\otimes A^{\bot}\parr
C^{\bot},{\color[rgb]{0.8,0.25,0.33}{z}}:A^{\bot}\parr D^{\bot}$ can get stuck
if ${\color[rgb]{0.8,0.25,0.33}{z}}$ communicates with
${\color[rgb]{0.8,0.25,0.33}{x}}$ first, violating property (2b) in
Proposition 1. Note that previous definitions of multiparty compatibility for
multiparty session types [24, 14] do indeed use annotations.

##  5 Asynchronous Forwarders

Forwarders form a subclass of processes with some special features but that
are also typable in classical linear logic. I.e., our goal is to identify all
those CP processes that are also forwarders. In order to do so, we must add
further information in the standard CP contexts.

Contexts. What we need is to be able to enforce the main features that
characterise a forwarder, namely i) anything received must be forwarded, ii)
anything that is going to be sent must be something that has been previously
received, and iii) the order of such messages between any two points must be
preserved. In order to enforce these requirements, we add more information to
the standard CP judgement. For example, let us consider the input process
${\color[rgb]{0.8,0.25,0.33}{{x}(y).P}}$. In CP, the typing environment for
such process must be such that endpoint ${\color[rgb]{0.8,0.25,0.33}{x}}$ has
type $A\parr B$ such that ${\color[rgb]{0.8,0.25,0.33}{P}}$ has type
${\color[rgb]{0.8,0.25,0.33}{y}}:A$ and ${\color[rgb]{0.8,0.25,0.33}{x}}:B$.
However, the context is not telling us at all that
${\color[rgb]{0.8,0.25,0.33}{y}}$ is actually a message that has been received
and, as such, it should not be used by ${\color[rgb]{0.8,0.25,0.33}{P}}$ for
further communications but just forwarded over some other channel. In order to
remember this fact when we type the subprocess
${\color[rgb]{0.8,0.25,0.33}{P}}$, we actually insert
${\color[rgb]{0.8,0.25,0.33}{y}}:A$ into a queue that belongs to endpoint
${\color[rgb]{0.8,0.25,0.33}{x}}$ where we put all the types of messages
received over it. I.e., when typing ${\color[rgb]{0.8,0.25,0.33}{P}}$, the
context will contain
$[\\![\Psi]\\!][^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0.8,0.25,0.33}{y}}:A]{\color[rgb]{0.8,0.25,0.33}{x}}:B$.
That still means that ${\color[rgb]{0.8,0.25,0.33}{x}}$ must have type $B$ and
${\color[rgb]{0.8,0.25,0.33}{y}}$ must have type $A$ in
${\color[rgb]{0.8,0.25,0.33}{P}}$, but also that
${\color[rgb]{0.8,0.25,0.33}{y}}:A$ has been received over
${\color[rgb]{0.8,0.25,0.33}{x}}$ (it is in
${\color[rgb]{0.8,0.25,0.33}{x}}$’s queue) and we are intending to forward it
to endpoint ${\color[rgb]{0.8,0.25,0.33}{u}}$. Moreover, $\Psi$ contains the
types of messages that have been previously received over
${\color[rgb]{0.8,0.25,0.33}{x}}$. The forwarders behave asynchronously. They
can input arbitrarily many messages, which are enqueued at the arrival point,
without blocking the possibility of producing an output from the same
endpoint. This behaviour is captured by the notion of queues of _boxed_
messages, i.e. messages that are in-transit.

$\begin{array}[]{rcllllllll}[\\![\Psi]\\!]&\coloncolonequals&\varnothing&\mid\quad[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\ast}][\\![\Psi]\\!]&\mid\quad[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0.8,0.25,0.33}{y}}:A][\\![\Psi]\\!]&\mid\quad[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\mathcal{Q}}][\\![\Psi]\\!]&\mid\quad[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\mathcal{L}}][\\![\Psi]\\!]&\mid\quad[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\mathcal{R}}][\\![\Psi]\\!]\end{array}$

A queue element
$[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0.8,0.25,0.33}{x}}:A]$
expresses that ${\color[rgb]{0.8,0.25,0.33}{x}}$ of type $A$ has been received
and will need to later be forwarded to endpoint
${\color[rgb]{0.8,0.25,0.33}{u}}$. Similarly,
$[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\ast}]$ indicates that
a request for closing a session has been received and must be forwarded to
${\color[rgb]{0.8,0.25,0.33}{u}}$.
$[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\mathcal{L}}]$ (or
$[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\mathcal{R}}]$) and
$[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\mathcal{Q}}]$ indicate
that a branching request and server invocation, respectively, has been
received and must be forwarded.

The order of messages needing to be forwarded to _independent_ endpoints is
irrelevant. Hence, we consider queue
$[\\![\Psi_{1}]\\!][^{{\color[rgb]{0.8,0.25,0.33}{x}}}\ldots][^{{\color[rgb]{0.8,0.25,0.33}{y}}}\ldots][\\![\Psi_{2}]\\!]$
equivalent to queue
$[\\![\Psi_{1}]\\!][^{{\color[rgb]{0.8,0.25,0.33}{y}}}\ldots][^{{\color[rgb]{0.8,0.25,0.33}{x}}}\ldots][\\![\Psi_{2}]\\!]$
whenever
${\color[rgb]{0.8,0.25,0.33}{x}}\not={\color[rgb]{0.8,0.25,0.33}{y}}$. For a
given endpoint ${\color[rgb]{0.8,0.25,0.33}{x}}$ however the order of two
messages
$[^{{\color[rgb]{0.8,0.25,0.33}{x}}}\ldots][^{{\color[rgb]{0.8,0.25,0.33}{x}}}\ldots]$
is crucial and must be maintained throughout the forwarding. This follows the
idea of having a queue for every ordered pair of endpoints in the type-context
semantics in Definition 1. By attaching a queue to each endpoint we get a
typing context

$\begin{array}[]{rcllllllll}\Gamma&\coloncolonequals&\quad\varnothing&\quad\mid\quad\Gamma,[\\![\Psi]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:B&\quad\mid\quad\Gamma,[\\![\Psi]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:\cdot\end{array}$

The element $[\\![\Psi]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:B$ of a context
$\Gamma$ indicates that the messages in $[\\![\Psi]\\!]$ have been received at
endpoint ${\color[rgb]{0.8,0.25,0.33}{x}}$. The special case
$[\\![\Psi]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:\cdot$ is denoting the
situation when endpoint ${\color[rgb]{0.8,0.25,0.33}{x}}$ no longer needs to
be used for communication, but still has a non-empty queue of messages to
forward.

When forwarding to many endpoints, we use
$[^{{\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}}{\color[rgb]{0,0,1}\mathcal{X}}]$
for denoting
$[^{{\color[rgb]{0.8,0.25,0.33}{u_{1}}}}{\color[rgb]{0,0,1}\mathcal{X}}]\ldots[^{{\color[rgb]{0.8,0.25,0.33}{u_{n}}}}{\color[rgb]{0,0,1}\mathcal{X}}]$,
with
${\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}={\color[rgb]{0.8,0.25,0.33}{u_{1}}},\ldots,{\color[rgb]{0.8,0.25,0.33}{u_{n}}}$.
In this case, we also assume the implicit rewriting
$[^{{\color[rgb]{0.8,0.25,0.33}{\varnothing}}}{\color[rgb]{0,0,1}\mathcal{X}}][\\![\Psi]\\!]\equiv[\\![\Psi]\\!]$.

Judgements and rules. A judgement denoted by
${\color[rgb]{0.8,0.25,0.33}{P}}\Vdash\Gamma$ types the forwarder processes
${\color[rgb]{0.8,0.25,0.33}{P}}$ that connects the endpoints in $\Gamma$. The
rules enforce the asynchronous forwarding behaviour by adding elements to
queues using rules for $\bot$ and $\parr$, which forces them to be later
removed from queues by the corresponding rules for $\mathbf{1}$ and $\otimes$.
The rules are reported in Fig. 2.

$\small\begin{array}[]{c}{\color[rgb]{0.8,0.25,0.33}{x\leftrightarrow
y}}\Vdash{\color[rgb]{0.8,0.25,0.33}{x}}:a^{\bot},{\color[rgb]{0.8,0.25,0.33}{y}}:a\qquad{\color[rgb]{0.8,0.25,0.33}{x().P}}\Vdash\Gamma,[\\![\Psi]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:\bot^{\color[rgb]{0.8,0.25,0.33}{u}}{\color[rgb]{0.8,0.25,0.33}{P}}\Vdash\Gamma,[\\![\Psi]\\!][^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\ast}]{\color[rgb]{0.8,0.25,0.33}{x}}:\cdot\qquad{\color[rgb]{0.8,0.25,0.33}{{x}[]}}\Vdash\mathopen{}\left\\{[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0,0,1}\ast}]{\color[rgb]{0.8,0.25,0.33}{u_{i}}}:\cdot\right\\}_{i}\mathclose{},{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{1}^{\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}\\\
\\\
{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}(y).P}}}}\Vdash\Gamma,[\\![\Psi]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A\parr^{\color[rgb]{0.8,0.25,0.33}{u}}B{\color[rgb]{0.8,0.25,0.33}{P}}\Vdash\Gamma,[\\![\Psi]\\!][^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0.8,0.25,0.33}{y}}:A]{\color[rgb]{0.8,0.25,0.33}{x}}:B\qquad{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}[y\triangleright
P].Q}}}}\Vdash\Gamma,\big{\\{}[^{{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{x}}}}}{\color[rgb]{0.8,0.25,0.33}{y_{i}}}:A_{i}][\\![\Psi_{i}]\\!]{\color[rgb]{0.8,0.25,0.33}{u_{i}}}:C_{i}\big{\\}}_{i},[\\![\Psi]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A\otimes^{\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}B\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{P}}\Vdash\big{\\{}{\color[rgb]{0.8,0.25,0.33}{y_{i}}}:A_{i}\big{\\}}_{i},{\color[rgb]{0.8,0.25,0.33}{y}}:A{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\Gamma,\big{\\{}[\\![\Psi_{i}]\\!]{\color[rgb]{0.8,0.25,0.33}{u_{i}}}:A_{i}\big{\\}}_{i},[\\![\Psi]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:B\\\
\\\
{\color[rgb]{0.8,0.25,0.33}{x.\mathsf{case}(P,Q)}}\Vdash\Gamma,[\\![\Psi]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A\with^{\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}B\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{P}}\Vdash\Gamma,[\\![\Psi]\\!][^{{\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}}{\color[rgb]{0,0,1}\mathcal{L}}]{\color[rgb]{0.8,0.25,0.33}{x}}:A{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\Gamma,[\\![\Psi]\\!][^{{\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}}{\color[rgb]{0,0,1}\mathcal{R}}]{\color[rgb]{0.8,0.25,0.33}{x}}:B\\\
\\\
{\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inl}].P}}\Vdash\Gamma,[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0,0,1}\mathcal{L}}][\\![\Psi_{z}]\\!]{\color[rgb]{0.8,0.25,0.33}{z}}:C,[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A\oplus^{\color[rgb]{0.8,0.25,0.33}{z}}B{\color[rgb]{0.8,0.25,0.33}{P}}\Vdash\Gamma,[\\![\Psi_{z}]\\!]{\color[rgb]{0.8,0.25,0.33}{z}}:C,[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A\qquad{\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inr}].P}}\Vdash\Gamma,[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0,0,1}\mathcal{R}}][\\![\Psi_{z}]\\!]{\color[rgb]{0.8,0.25,0.33}{z}}:C,[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A\oplus^{\color[rgb]{0.8,0.25,0.33}{z}}B{\color[rgb]{0.8,0.25,0.33}{P}}\Vdash\Gamma,[\\![\Psi_{z}]\\!]{\color[rgb]{0.8,0.25,0.33}{z}}:C,[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:B\\\
\\\ {\color[rgb]{0.8,0.25,0.33}{\oc
x(y).P}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{u_{i}}}:\wn
B_{i}\right\\}_{i}\mathclose{},{\color[rgb]{0.8,0.25,0.33}{x}}:\oc^{\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}A{\color[rgb]{0.8,0.25,0.33}{P}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{u_{i}}}:\wn
B_{i}\right\\}_{i}\mathclose{},[^{{\color[rgb]{0.8,0.25,0.33}{\tilde{u}}}}{\color[rgb]{0,0,1}\mathcal{Q}}]{\color[rgb]{0.8,0.25,0.33}{y}}:A\qquad{\color[rgb]{0.8,0.25,0.33}{\wn
x[y].P}}\Vdash\Gamma,[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0,0,1}\mathcal{Q}}][\\![\Psi_{z}]\\!]{\color[rgb]{0.8,0.25,0.33}{z}}:C,[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:\wn^{\color[rgb]{0.8,0.25,0.33}{z}}A{\color[rgb]{0.8,0.25,0.33}{P}}\Vdash\Gamma,[\\![\Psi_{z}]\\!]{\color[rgb]{0.8,0.25,0.33}{z}}:C,[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{y}}:A\end{array}$
Figure 2: Proof System for Forwarders

Rule Ax is identical to the one of CP. Rules $\mathbf{1}$ and $\bot$ forward a
request to close a session. Rule $\bot$ receives the request on endpoint
${\color[rgb]{0.8,0.25,0.33}{x}}$ and enqueues it as
$[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\ast}]$ if it needs to
forward it to ${\color[rgb]{0.8,0.25,0.33}{u}}$. Note that in the premiss of
$\bot$ the endpoint is terminated pending the remaining messages in the
corresponding queue being dispatched. Eventually all endpoints but one will be
terminated in the same manner. Rule $\mathbf{1}$ will then be applicable. Note
that the behaviour of ${\color[rgb]{0.8,0.25,0.33}{x().P}}$ and
${\color[rgb]{0.8,0.25,0.33}{{x}[]}}$ work as gathering, several terminated
endpoints connect to the last active endpoint typed with a $\mathbf{1}$. Rules
$\otimes$ and $\parr$ forward a message. Rule $\parr$ receives the message
${\color[rgb]{0.8,0.25,0.33}{y}}:A$ and enqueues it as
$[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0.8,0.25,0.33}{y}}:A]$ to be
forwarded to endpoint ${\color[rgb]{0.8,0.25,0.33}{u}}$. Dually, rule
$\otimes$ applied to a $\otimes$ sends the messages at the top of the queues
of endpoints ${\color[rgb]{0.8,0.25,0.33}{u_{i}}}$’s, meaning that several
messages are sent at the same time. Messages will be picked from queues
belonging to distinct endpoints, as a consequence, the left premiss of
$\otimes$ rule spawns a new forwarder consisting of the gathered messages.

In the case of additives and exponentials, the behaviour is actually
_broadcasting_ , that is, an external choice
$[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\mathcal{L}}]$ or
$[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\mathcal{R}}]$, or a
server opening
$[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\mathcal{Q}}]$, resp.,
is received and can be used several (at least one) times to guide internal
choices or server requests, resp., later on.

Note how annotations put constraints on how the proof is constructed, e.g.,
annotating ${\color[rgb]{0.8,0.25,0.33}{x}}:A\parr B$ with
${\color[rgb]{0.8,0.25,0.33}{u}}$ ensures us that the proof will contain a
$\otimes$-rule application on endpoint ${\color[rgb]{0.8,0.25,0.33}{u}}$.

######  Example 2 (Multiplicative Criss-cross)

${\color[rgb]{0.8,0.25,0.33}{P}}\colonequals{\color[rgb]{0.8,0.25,0.33}{{x}(u).{\color[rgb]{0.8,0.25,0.33}{{y}(v).{\color[rgb]{0.8,0.25,0.33}{{y}[u^{\prime}\triangleright{\color[rgb]{0.8,0.25,0.33}{u\leftrightarrow
u^{\prime}}}].{\color[rgb]{0.8,0.25,0.33}{{x}[v^{\prime}\triangleright{\color[rgb]{0.8,0.25,0.33}{v^{\prime}\leftrightarrow
v}}].{\color[rgb]{0.8,0.25,0.33}{x().{\color[rgb]{0.8,0.25,0.33}{{y}[]}}}}}}}}}}}}$
is one of the forwarders that can prove the compatibility of the types
involved in the criss-cross protocol (in § 2), as illustrated by the
derivation below.

${\color[rgb]{0.8,0.25,0.33}{P}}\Vdash{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{name}^{\perp}\parr^{\color[rgb]{0.8,0.25,0.33}{y}}\mathbf{cost}^{\perp}\otimes^{\color[rgb]{0.8,0.25,0.33}{y}}\bot^{\color[rgb]{0.8,0.25,0.33}{y}},{\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{cost}\parr^{\color[rgb]{0.8,0.25,0.33}{x}}\mathbf{name}\otimes^{\color[rgb]{0.8,0.25,0.33}{x}}\mathbf{1}^{\color[rgb]{0.8,0.25,0.33}{x}}{\color[rgb]{0.8,0.25,0.33}{{y}(v).{\color[rgb]{0.8,0.25,0.33}{{y}[u^{\prime}\triangleright
F_{1}].{\color[rgb]{0.8,0.25,0.33}{{x}[v^{\prime}\triangleright
F_{2}].F_{3}}}}}}}\Vdash[^{{\color[rgb]{0.8,0.25,0.33}{y}}}{\color[rgb]{0.8,0.25,0.33}{u}}:\mathbf{name}^{\perp}]{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{cost}^{\perp}\otimes^{\color[rgb]{0.8,0.25,0.33}{y}}\bot^{\color[rgb]{0.8,0.25,0.33}{y}},{\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{cost}\parr^{\color[rgb]{0.8,0.25,0.33}{x}}\mathbf{name}\otimes^{\color[rgb]{0.8,0.25,0.33}{x}}\mathbf{1}^{\color[rgb]{0.8,0.25,0.33}{x}}{\color[rgb]{0.8,0.25,0.33}{{y}[u^{\prime}\triangleright
F_{1}].{\color[rgb]{0.8,0.25,0.33}{{x}[v^{\prime}\triangleright
F_{2}].F_{3}}}}}\Vdash[^{{\color[rgb]{0.8,0.25,0.33}{y}}}{\color[rgb]{0.8,0.25,0.33}{u}}:\mathbf{name}^{\perp}]{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{cost}^{\perp}\otimes^{\color[rgb]{0.8,0.25,0.33}{y}}\bot^{\color[rgb]{0.8,0.25,0.33}{y}},[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0.8,0.25,0.33}{v}}:\mathbf{cost}]{\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{name}\otimes^{\color[rgb]{0.8,0.25,0.33}{x}}\mathbf{1}^{\color[rgb]{0.8,0.25,0.33}{x}}\lx@proof@logical@and\Vdash{\color[rgb]{0.8,0.25,0.33}{u}}:\mathbf{name}^{\perp},{\color[rgb]{0.8,0.25,0.33}{u^{\prime}}}:\mathbf{name}{\color[rgb]{0.8,0.25,0.33}{F_{1}}}\colonequals{\color[rgb]{0.8,0.25,0.33}{u\leftrightarrow
u^{\prime}}}{\color[rgb]{0.8,0.25,0.33}{{x}[v^{\prime}\triangleright
F_{2}].F_{3}}}\Vdash{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{cost}^{\perp}\otimes^{\color[rgb]{0.8,0.25,0.33}{y}}\bot^{\color[rgb]{0.8,0.25,0.33}{y}},[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0.8,0.25,0.33}{v}}:\mathbf{cost}]{\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{1}^{\color[rgb]{0.8,0.25,0.33}{x}}\lx@proof@logical@and\Vdash{\color[rgb]{0.8,0.25,0.33}{v^{\prime}}}:\mathbf{cost}^{\perp},{\color[rgb]{0.8,0.25,0.33}{v}}:\mathbf{cost}{\color[rgb]{0.8,0.25,0.33}{F_{2}}}\colonequals{\color[rgb]{0.8,0.25,0.33}{v^{\prime}\leftrightarrow
v}}{\color[rgb]{0.8,0.25,0.33}{F_{3}}}\Vdash{\color[rgb]{0.8,0.25,0.33}{x}}:\bot^{\color[rgb]{0.8,0.25,0.33}{y}},{\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{1}^{\color[rgb]{0.8,0.25,0.33}{x}}{\color[rgb]{0.8,0.25,0.33}{{y}[]}}\Vdash[^{{\color[rgb]{0.8,0.25,0.33}{y}}}{\color[rgb]{0,0,1}\ast}]{\color[rgb]{0.8,0.25,0.33}{x}}:\cdot,{\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{1}{\color[rgb]{0.8,0.25,0.33}{F_{3}}}\colonequals{\color[rgb]{0.8,0.25,0.33}{x().{\color[rgb]{0.8,0.25,0.33}{{y}[]}}}}$

###### Example 3

The following is a forwarder for the 2-buyer protocol, for some
${\color[rgb]{0.8,0.25,0.33}{T_{i}}}$’s.

$\begin{array}[]{l}{\color[rgb]{0.8,0.25,0.33}{{b_{1}^{\prime}}(book).}}\
{\color[rgb]{0.8,0.25,0.33}{{s^{\prime}}[book\triangleright T_{1}].}}\
{\color[rgb]{0.8,0.25,0.33}{{s^{\prime}}(price).}}\
{\color[rgb]{0.8,0.25,0.33}{{s^{\prime}}(price).}}\
{\color[rgb]{0.8,0.25,0.33}{{b_{1}^{\prime}}[price\triangleright T_{2}].}}\
{\color[rgb]{0.8,0.25,0.33}{{b_{2}^{\prime}}[price\triangleright T_{3}].}}\\\
{\color[rgb]{0.8,0.25,0.33}{{b_{1}^{\prime}}(contr).}}\
{\color[rgb]{0.8,0.25,0.33}{{b_{2}^{\prime}}[contr\triangleright
T_{4}].}}\quad{\color[rgb]{0.8,0.25,0.33}{b_{2}^{\prime}.\mathsf{case}({\color[rgb]{0.8,0.25,0.33}{{s^{\prime}}[\mathsf{inl}].}}\
{\color[rgb]{0.8,0.25,0.33}{{b_{2}^{\prime}}(addr).}}\
{\color[rgb]{0.8,0.25,0.33}{{s}[addr\triangleright T_{5}].\ T_{6}}}\quad,\quad
T_{7})}}\end{array}$

Properties of Forwarders. We write $\llcorner{B}\lrcorner$ for the formula
obtained from any $B$ by removing all the annotations. We state that every
forwarder is also a CP process, the embedding $\llcorner{\cdot}\lrcorner$
being extended to contexts and queus as:

$\begin{array}[]{l@{\qquad\qquad}l@{\qquad}l}\llcorner{[\\![\Psi]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:B,\Gamma}\lrcorner=\llcorner{[\\![\Psi]\\!]}\lrcorner,{\color[rgb]{0.8,0.25,0.33}{x}}:\llcorner{B}\lrcorner,\llcorner{\Gamma}\lrcorner&\llcorner{[\\![\Psi]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:\cdot,\Gamma}\lrcorner=\llcorner{[\\![\Psi]\\!]}\lrcorner,\llcorner{\Gamma}\lrcorner\\\\[3.87498pt]
\llcorner{[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0.8,0.25,0.33}{y}}:A][\\![\Psi]\\!]}\lrcorner={\color[rgb]{0.8,0.25,0.33}{y}}:A,\llcorner{[\\![\Psi]\\!]}\lrcorner&\llcorner{[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\mathcal{X}}][\\![\Psi]\\!]}\lrcorner~=\llcorner{[^{{\color[rgb]{0.8,0.25,0.33}{u}}}{\color[rgb]{0,0,1}\ast}][\\![\Psi]\\!]}\lrcorner=\llcorner{[\\![\Psi]\\!]}\lrcorner\\\
&\text{where
${\color[rgb]{0,0,1}\mathcal{X}}\in\mathopen{}\left\\{{\color[rgb]{0,0,1}\mathcal{L}},{\color[rgb]{0,0,1}\mathcal{R}},{\color[rgb]{0,0,1}\mathcal{Q}}\right\\}\mathclose{}$}\end{array}$

###### Proposition 2

Any forwarder is typable in CP, i.e., if
${\color[rgb]{0.8,0.25,0.33}{P}}\Vdash\Gamma$, then
${\color[rgb]{0.8,0.25,0.33}{P}}\vdash\llcorner{\Gamma}\lrcorner$.

Moreover, forwarders enjoy an invertibility property, i.e., all its rules are
invertible. In CLL, the rules $\otimes$ or $\oplus$ are not invertible because
of the choice involved either in splitting the context in the conclusion of
$\otimes$ into the two premisses or the choice of either disjuncts for
$\oplus$. In our case on the other hand, the annotations put extra syntactic
constraints on what can be derived and hence are restricting these choices to
a unique one and as a result the rules are invertible. This is formalised by
the following.

###### Proposition 3

All the forwarder rules are invertible, that is, for any rule if there exists
a forwarder ${\color[rgb]{0.8,0.25,0.33}{F}}$ such that
${\color[rgb]{0.8,0.25,0.33}{F}}\Vdash\Gamma$, the conclusion of the rule,
there is a forwarder ${\color[rgb]{0.8,0.25,0.33}{F_{i}}}\Vdash\Gamma_{i}$,
for each of its premiss, $i=1$ or $2$.

###### Proof

For each rule, the proof is standard and follows by induction on
${\color[rgb]{0.8,0.25,0.33}{F}}$. For example, for $\oplus_{l}$, let us
suppose that
${\color[rgb]{0.8,0.25,0.33}{F}}\Vdash\Gamma,[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0,0,1}\mathcal{L}}][\\![\Psi_{z}]\\!]{\color[rgb]{0.8,0.25,0.33}{z}}:C,[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A\oplus^{\color[rgb]{0.8,0.25,0.33}{z}}B$.
If
${\color[rgb]{0.8,0.25,0.33}{F}}={\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inl}].F_{1}}}$,
then we directly get that
${\color[rgb]{0.8,0.25,0.33}{F_{1}}}\Vdash\Gamma,[\\![\Psi_{z}]\\!]{\color[rgb]{0.8,0.25,0.33}{z}}:C,[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A$.

Otherwise, if ${\color[rgb]{0.8,0.25,0.33}{F}}$ starts with any other process
operator, we apply an inductive step. E.g., let
${\color[rgb]{0.8,0.25,0.33}{F}}={\color[rgb]{0.8,0.25,0.33}{{u}(v).F^{\prime}}}$,
meaning that
$\Gamma=\Gamma^{\prime},[\\![\Psi_{u}]\\!]{\color[rgb]{0.8,0.25,0.33}{u}}:A\parr^{\color[rgb]{0.8,0.25,0.33}{w}}B$
and that
${\color[rgb]{0.8,0.25,0.33}{F^{\prime}}}\Vdash\Gamma^{\prime},[\\![\Psi_{u}]\\!][^{{\color[rgb]{0.8,0.25,0.33}{w}}}{\color[rgb]{0.8,0.25,0.33}{v}}:A]{\color[rgb]{0.8,0.25,0.33}{u}}:B,[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0,0,1}\mathcal{L}}][\\![\Psi_{z}]\\!]{\color[rgb]{0.8,0.25,0.33}{z}}:C,[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A\oplus^{\color[rgb]{0.8,0.25,0.33}{z}}B$.
By induction hypothesis (given that ${\color[rgb]{0.8,0.25,0.33}{F^{\prime}}}$
is a subprocess of ${\color[rgb]{0.8,0.25,0.33}{F}}$), we know there exists
${\color[rgb]{0.8,0.25,0.33}{F_{1}^{\prime}}}$ such that
${\color[rgb]{0.8,0.25,0.33}{F_{1}^{\prime}}}\Vdash\Gamma^{\prime},[\\![\Psi_{u}]\\!][^{{\color[rgb]{0.8,0.25,0.33}{w}}}{\color[rgb]{0.8,0.25,0.33}{v}}:A]{\color[rgb]{0.8,0.25,0.33}{u}}:B,[\\![\Psi_{z}]\\!]{\color[rgb]{0.8,0.25,0.33}{z}}:C,[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A$.
From there we can derive
${\color[rgb]{0.8,0.25,0.33}{F_{1}}}={\color[rgb]{0.8,0.25,0.33}{{u}(v).F_{1}^{\prime}}}$.
The rest of the cases follow in a similar way.

A Note on Compositionality and Cut Elimination. The sequent calculus we
presented enjoys cut elimination. That means that forwarders can be composed,
and their composition is still a forwarder. The way we compose forwarders
follows a standard cut rule augmented with extra machinery to deal with
annotations. Additionally, the cut elimination proof provides a semantics for
forwarders, in the proposition-as-types style. For space reasons, we have not
included its technical development, but it can be found in our extended note
[7].

Relation to Multiparty Compatibility. Forwarders relate to transitions in the
type-context semantics introduced in the previous section. In order to
formalise this, we first give a translation from type-contexts into forwarder
contexts:

  * •

$\mathsf{tr}(\varnothing\bullet\sigma_{\epsilon})=\varnothing$.

  * •

$\mathsf{tr}(\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:A\bullet\sigma\cup\mathopen{}\left\\{({\color[rgb]{0.8,0.25,0.33}{y_{i},}}{\color[rgb]{0.8,0.25,0.33}{x}})\mapsto\Psi_{i}\right\\}_{i}\mathclose{})\colonequals[\\![^{{\color[rgb]{0.8,0.25,0.33}{y_{1}}}}\Psi_{1}]\\!]\ldots[\\![^{{\color[rgb]{0.8,0.25,0.33}{y_{n}}}}\Psi_{n}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A,\mathsf{tr}(\Delta\bullet\sigma)$
for a type environment
$\Delta=\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{y_{i}}}:\Psi_{i}\right\\}_{i}\mathclose{}$
and a queue environment $\sigma$ mapping the endpoints
${\color[rgb]{0.8,0.25,0.33}{y_{i}}}$;

We use the extended notation
$[\\![^{{\color[rgb]{0.8,0.25,0.33}{u}}}\Psi]\\!]$ to signify that all the
brackets in $[\\![\Psi]\\!]$ are labelled by
${\color[rgb]{0.8,0.25,0.33}{u}}$.

###### Lemma 1

Let $\Delta\bullet\sigma$ be a type-context and
$\Gamma=\mathsf{tr}(\Delta\bullet\sigma)$.

  1. 1.

if there exists $\alpha$ and $\Delta^{\prime}\bullet\sigma^{\prime}$ such that
$\Delta\bullet\sigma\xrightarrow{\alpha}\Delta^{\prime}\bullet\sigma^{\prime}$
then there exists a rule from forwarders such that $\Gamma$ is an instance of
its conclusion and
$\Gamma^{\prime}=\mathsf{tr}(\Delta^{\prime}\bullet\sigma^{\prime})$ is an
instance of (one of) the premiss(es);

  2. 2.

otherwise, either $\Delta=\varnothing$ and $\sigma=\sigma_{\epsilon}$ or there
is no forwarder ${\color[rgb]{0.8,0.25,0.33}{F}}$ such that
${\color[rgb]{0.8,0.25,0.33}{F}}\Vdash\Gamma$.

###### Proof

Follows from a simple inspection of the transitions in Def. 1 and the rules in
Fig. 2.

Thus, we can conclude this section by proving that forwarders are actually
characterising multiparty compatibility for CP processes (processes that are
well-typed in CLL).

######  Theorem 5.1 ()

$\Delta$ is multiparty compatible iff there exists a forwarder
${\color[rgb]{0.8,0.25,0.33}{F}}$ such that
${\color[rgb]{0.8,0.25,0.33}{F}}\Vdash\Delta^{\bot}$ where each connective in
$\Delta^{\bot}$ is annotated.

######  Proof (Proof Sketch)

See Appendix 0.A for the full proof. From left to right, we need to prove more
generally that if $\Delta\bullet\sigma$ is executable, then there exists a
forwarder ${\color[rgb]{0.8,0.25,0.33}{F}}$ such that
${\color[rgb]{0.8,0.25,0.33}{F}}\Vdash\mathsf{tr}(\Delta\bullet\sigma)$, by
induction on the size of $\Delta$, defined as the sum of the formula sizes in
$\Delta$. From right to left can be proven by contrapositive, using Lemma 1
and Proposition 3.

##  6 Composing Processes with Asynchronous Forwarders

In this section, we show how to use forwarders for logically composing CP
processes.

Multiparty Process Composition. We start by focusing on the structural rule
that can be added to CP, namely the Cut, as seen in Section 3. Rule Cut
corresponds to parallel composition of processes. The implicit side condition
that this rule uses is _duality_ , i.e., we can compose two processes if
endpoints ${\color[rgb]{0.8,0.25,0.33}{x}}$ and
${\color[rgb]{0.8,0.25,0.33}{y}}$ have a dual type. Carbone et al. [6]
generalise the concept of duality to that of coherence. Coherence, denoted by
$\vDash$, generalises duality to many endpoints, allowing for a cut rule that
composes many processes in parallel

${\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}\tilde{x}:G)\,(R_{1}{\ \;\bm{|}\
\;}\ldots{\ \;\bm{|}\
\;}R_{n})}}\vdash\mathopen{}\left\\{\Sigma_{i}\right\\}_{i\leq
n}\mathclose{}\lx@proof@logical@and\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{R_{i}}}\vdash\Sigma_{i},{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:A_{i}\right\\}_{i\leq
n}\mathclose{}{\color[rgb]{0.8,0.25,0.33}{G}}\vDash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:A_{i}\right\\}_{i\leq
n}\mathclose{}$

The judgement
${\color[rgb]{0.8,0.25,0.33}{G}}\vDash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:A_{i}\right\\}_{i\leq
n}\mathclose{}$ intuitively says that the
${\color[rgb]{0.8,0.25,0.33}{x_{i}}}:A_{i}$’s are compatible and the execution
of the ${\color[rgb]{0.8,0.25,0.33}{R_{i}}}$ will proceed without any error.
Such a result is formalised by an MCut elimination theorem analogous to the
one of CP. We leave ${\color[rgb]{0.8,0.25,0.33}{G}}$ abstract here: it is a
proof term and it corresponds to a global type (see [6]).

Our goal here is to replace the notion of coherence with an asynchronous
forwarder ${\color[rgb]{0.8,0.25,0.33}{Q}}$, yielding the rule

${\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}\tilde{x}:Q)\,(R_{1}{\ \;\bm{|}\
\;}\ldots{\ \;\bm{|}\
\;}R_{n})}}\vdash\mathopen{}\left\\{\Sigma_{i}\right\\}_{i\leq
n}\mathclose{}\lx@proof@logical@and\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{R_{i}}}\vdash\Sigma_{i},{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:A_{i}\right\\}_{i\leq
n}\mathclose{}{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:A_{i}^{\bot}\right\\}_{i\leq
n}\mathclose{}$

Asynchronous forwarders are more general than coherence: every coherence proof
can be transformed into an _arbiter_ process [6], which is indeed a forwarder,
while there are judgements that are not coherent but are provable in our
forwarders (see Example 2). In the rule MCutF, the role of a forwarder
(replacing coherence) is to be a middleware that decides whom to forward
messages to. This means that when a process
${\color[rgb]{0.8,0.25,0.33}{R_{i}}}$ sends a message to the middleware, the
message must be stored by the forwarder, who will later forward it to the
right receiver. Since our goal is to show that MCutF is admissible (and hence
we can eliminate it from any correct proof), we extend such rule to account
for messages in transit that are temporarily held by the forwarder. In order
to do so, we use the forwarders queues and some extra premises and define
MCutQ as:

${\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}\tilde{x}:Q[\tilde{y}\lhd
P_{1},\ldots,P_{m}])\,(R_{1}{\ \;\bm{|}\ \;}\ldots{\ \;\bm{|}\
\;}R_{n})}}\vdash\mathopen{}\left\\{\Delta_{j}\right\\}_{j\leq
m}\mathclose{},\mathopen{}\left\\{\Sigma_{i}\right\\}_{i\leq
n}\mathclose{}\lx@proof@logical@and\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{P_{j}}}\vdash\Delta_{j},{\color[rgb]{0.8,0.25,0.33}{y_{j}}}:A_{j}\right\\}_{j\leq
m}\mathclose{}\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{R_{i}}}\vdash\Sigma_{i},{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:B_{i}\right\\}_{i\leq
n}\mathclose{}{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\mathopen{}\left\\{[\\![\Psi_{i}]\\!]{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:B_{i}^{\bot}\right\\}_{i\leq
n}\mathclose{},\mathopen{}\left\\{[\\![\Psi_{i}]\\!]{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\cdot\right\\}_{n<i\leq
p}\mathclose{}$

We have three types of process terms: ${\color[rgb]{0.8,0.25,0.33}{P_{j}}}$’s,
${\color[rgb]{0.8,0.25,0.33}{R_{i}}}$’s and ${\color[rgb]{0.8,0.25,0.33}{Q}}$.
Processes ${\color[rgb]{0.8,0.25,0.33}{R_{i}}}$’s are the processes that we
are composing, implementing a multiparty session.
${\color[rgb]{0.8,0.25,0.33}{Q}}$ is the forwarder whose role is to certify
compatibility and to determine, at run time, who talks to whom. Finally,
processes ${\color[rgb]{0.8,0.25,0.33}{P_{i}}}$’s must be linked to messages
in the forwarder queue. Such processes are there because of the way $\otimes$
and $\parr$ work in linear logic. This will become clearer when we look at the
reduction steps that lead to cut admissibility. This imposes a side condition
on the rule, namely that

$\bigcup_{i\leq
p}{\Psi_{i}}\setminus\mathopen{}\left\\{{\color[rgb]{0,0,1}\ast}\right\\}\mathclose{}=\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{y_{j}}}:A_{j}^{\bot}\right\\}_{j\leq
m}\mathclose{}$

Note that we need to introduce a new syntax for this new structural rule: in
the process ${\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}\tilde{x}:Q[\tilde{y}\lhd
P_{1},\ldots,P_{m}])\,(R_{1}{\ \;\bm{|}\ \;}\ldots{\ \;\bm{|}\ \;}R_{n})}}$,
the list ${\color[rgb]{0.8,0.25,0.33}{P_{1},\ldots,P_{m}}}$ denotes those
messages (processes) in transit that are going to form a new session after the
communication has taken place. In the remainder we (slightly abusively)
abbreviate both
${\color[rgb]{0.8,0.25,0.33}{\mathopen{}\left\\{P_{1},\ldots,P_{m}\right\\}\mathclose{}}}$
and ${\color[rgb]{0.8,0.25,0.33}{(R_{1}{\ \;\bm{|}\ \;}\ldots{\ \;\bm{|}\
\;}R_{n})}}$ as ${\color[rgb]{0.8,0.25,0.33}{\tilde{P}}}$ and
${\color[rgb]{0.8,0.25,0.33}{\tilde{R}}}$ respectively.

Semantics and MCutF-admissibility. We now formally show that MCutF is
admissible, yielding a semantics for our extended CP (with MCutF) in a
proposition-as-types fashion. In order to do so, we consider some cases from
the multiplicative fragment (see appendix for all cases). In the sequel,
$\Gamma=\mathopen{}\left\\{[\\![\Psi_{i}]\\!]{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:B_{i}^{\bot}\right\\}_{i\leq
n}\mathclose{},\mathopen{}\left\\{[\\![\Psi_{i}]\\!]{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\cdot\right\\}_{n<i\leq
p}\mathclose{}$ and
$\Gamma{-k}=\Gamma\setminus\mathopen{}\left\\{[\\![\Psi_{k}]\\!]{\color[rgb]{0.8,0.25,0.33}{x_{k}}}:B_{k}^{\bot}\right\\}\mathclose{}$.
Also, we omit (indicated as “$\ldots$”) the premises of the MCutQ that do not
play a role in the reduction at hand, and assume that they are always the same
as above, that is,
$\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{P_{j}}}\vdash\Delta_{j},{\color[rgb]{0.8,0.25,0.33}{y_{j}}}:A_{j}\right\\}_{j\leq
m}\mathclose{}$ and
$\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{R_{i}}}\vdash\Sigma_{i},{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:B_{i}\right\\}_{i\leq
n}\mathclose{}$.

Send Message ($\otimes$). This is the case when a process intends to send a
message, which corresponds to a $\otimes$ rule. As a consequence, the
forwarder has to be ready to receive the message (to then forward it later):

${\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:{\color[rgb]{0.8,0.25,0.33}{{x}(y).Q}}[{\tilde{y}}\lhd\tilde{P}])\,({\color[rgb]{0.8,0.25,0.33}{{x}[y\triangleright
P].R}}{\ \;\bm{|}\
\;}\tilde{R})}}\vdash\Delta,\Sigma,\mathopen{}\left\\{\Delta_{j}\right\\}_{j\leq
m}\mathclose{},\mathopen{}\left\\{\Sigma_{i}\right\\}_{i\leq
n}\mathclose{}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}[y\triangleright
P].R}}}}\vdash\Delta,\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:A\otimes
B\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{y}}:A{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:B\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}(y).Q}}}}\Vdash[\\![\Psi]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot}\parr^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}B^{\bot},\Gamma{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi]\\!][^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}{\color[rgb]{0.8,0.25,0.33}{y}}:A^{\bot}]{\color[rgb]{0.8,0.25,0.33}{x}}:B^{\bot},\Gamma$

The process on the left is ready to send the message to the forwarder. By the
annotation on the forwarder, it follows that the message will have to be
forwarded to endpoint ${\color[rgb]{0.8,0.25,0.33}{x_{k}}}$, at a later stage.
Observe that the nature of $\otimes$ forces us to deal with the process
${\color[rgb]{0.8,0.25,0.33}{P}}$: the idea is that when the forwarder will
finalise the communication (by sending to a process
${\color[rgb]{0.8,0.25,0.33}{R^{\prime}}}$ owning endpoint
${\color[rgb]{0.8,0.25,0.33}{x_{k}}}$) process
${\color[rgb]{0.8,0.25,0.33}{P}}$ will be composed with
${\color[rgb]{0.8,0.25,0.33}{R^{\prime}}}$. For now, we obtain the reductum:

${\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:Q[{y,\tilde{y}}\lhd
P,\tilde{P}])\,(R{\ \;\bm{|}\
\;}\tilde{R})}}\vdash\Delta,\Sigma,\mathopen{}\left\\{\Delta_{j}\right\\}_{j\leq
m}\mathclose{},\mathopen{}\left\\{\Sigma_{i}\right\\}_{i\leq
n}\mathclose{}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{y}}:A{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:B\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi]\\!][^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}{\color[rgb]{0.8,0.25,0.33}{y}}:A^{\bot}]{\color[rgb]{0.8,0.25,0.33}{x}}:B^{\bot},\Gamma$

Receive Message ($\parr$). At a later point, the forwarder will be able to
complete the forwarding operation by connecting with a process ready to
receive ($\parr$ rule):

${\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:{\color[rgb]{0.8,0.25,0.33}{{x}[y\triangleright
S].Q}}[z,\tilde{y}\lhd
P,\tilde{P}])\,({\color[rgb]{0.8,0.25,0.33}{{x}(y).R}}{\ \;\bm{|}\
\;}\tilde{R})}}\vdash\Delta,\Sigma,\mathopen{}\left\\{\Delta_{j}\right\\}_{j\leq
m}\mathclose{},\mathopen{}\left\\{\Sigma_{i}\right\\}_{i\leq
n}\mathclose{}\begin{array}[]{c}{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{z}}:A^{\bot}\hskip
56.9055pt\ldots\\\
{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}(y).R}}}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:A\parr
B{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{y}}:A,{\color[rgb]{0.8,0.25,0.33}{x}}:B\quad{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}[y\triangleright
S].Q}}}}\Vdash[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot}\otimes^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}B^{\bot},[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0.8,0.25,0.33}{z}}:A][\\![\Psi_{k}]\\!]{\color[rgb]{0.8,0.25,0.33}{x_{k}}}:B_{k}^{\bot},\Gamma-k\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{S}}\Vdash{\color[rgb]{0.8,0.25,0.33}{z}}:A,{\color[rgb]{0.8,0.25,0.33}{y}}:A^{\bot}{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:B^{\bot},\Gamma\end{array}$

Key ingredients are process ${\color[rgb]{0.8,0.25,0.33}{P}}$ with endpoint
${\color[rgb]{0.8,0.25,0.33}{z}}$ of type $A^{\bot}$, endpoint
${\color[rgb]{0.8,0.25,0.33}{x_{k}}}$ in the forwarder with a boxed endpoint
${\color[rgb]{0.8,0.25,0.33}{z}}$ with type $A$, and process
${\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}(y).R}}}}$ ready
to receive.

After reduction, we obtain the following:

${\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:Q[\tilde{y}\lhd\tilde{P}])\,((\bm{\nu}yz:S)\,(R{\
\;\bm{|}\ \;}P){\ \;\bm{|}\
\;}\tilde{R})}}\vdash\Delta,\Sigma,\mathopen{}\left\\{\Delta_{j}\right\\}_{j\leq
m}\mathclose{},\mathopen{}\left\\{\Sigma_{i}\right\\}_{i\leq
n}\mathclose{}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}yz:S)\,(R{\
\;\bm{|}\
\;}P)}}\vdash\Sigma,\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:B\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:B^{\bot},\Gamma$

Where the left premiss is obtained as follows:

${\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}yz:S)\,(R{\ \;\bm{|}\
\;}P)}}\vdash\Sigma,\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:B\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{y}}:A,{\color[rgb]{0.8,0.25,0.33}{x}}:B{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{z}}:A^{\bot}{\color[rgb]{0.8,0.25,0.33}{S}}\Vdash{\color[rgb]{0.8,0.25,0.33}{z}}:A,{\color[rgb]{0.8,0.25,0.33}{y}}:A^{\bot}$

meaning that now the message (namely process
${\color[rgb]{0.8,0.25,0.33}{P}}$) has finally been delivered and it can be
directly linked to ${\color[rgb]{0.8,0.25,0.33}{R}}$ with a new (but smaller)
MCutQ.

These reductions (the full set can be found in Appendix 0.B) allow us to prove
the key lemma of this section.

######  Lemma 2 (MCutQ Admissibility)

If
$\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{P_{j}}}\vdash\Delta_{j},{\color[rgb]{0.8,0.25,0.33}{y_{j}}}:A_{j}\right\\}_{j\leq
m}\mathclose{}$ and

$\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{R_{i}}}\vdash\Sigma_{i},{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:B_{i}\right\\}_{i\leq
n}\mathclose{}$ and
${\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\mathopen{}\left\\{[\\![\Psi_{i}]\\!]{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:B_{i}^{\bot}\right\\}_{i\leq
n}\mathclose{},\mathopen{}\left\\{[\\![\Psi_{i}]\\!]{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\cdot\right\\}_{n<i\leq
p}\mathclose{}$ then there exists a process ${\color[rgb]{0.8,0.25,0.33}{S}}$
such that
${\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}\tilde{x}:Q[\tilde{y}\lhd\tilde{P}])\,\tilde{R}}}\Rightarrow^{*}{\color[rgb]{0.8,0.25,0.33}{S}}$
and
${\color[rgb]{0.8,0.25,0.33}{S}}\vdash\mathopen{}\left\\{\Delta_{j}\right\\}_{j\leq
m}\mathclose{},\mathopen{}\left\\{\Sigma_{i}\right\\}_{i\leq n}\mathclose{}$.

######  Proof (Proof Sketch)

By lexicographic induction on ($i$) the sum of sizes of the $B_{i}$’s and
($ii$) the sum of sizes of the ${\color[rgb]{0.8,0.25,0.33}{R_{i}}}$’s. Some
of the key and base cases have been detailed above; the others can be found in
Appendix 0.B. The commutative cases are straightforward and only need to
consider the possible last rule applied to a premiss of the form
${\color[rgb]{0.8,0.25,0.33}{R_{i}}}\vdash\Sigma_{i},{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:B_{i}$.

We can finally conclude with the following theorem as a special case.

######  Theorem 6.1 (MCutF Admissibility)

If
$\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{R_{i}}}\vdash\Sigma_{i},{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:A_{i}\right\\}_{i\leq
n}\mathclose{}$ and
${\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:A_{i}^{\bot}\right\\}_{i\leq
n}\mathclose{}$ then there exists a process ${\color[rgb]{0.8,0.25,0.33}{S}}$
such that ${\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}\tilde{x}:Q)\,(R_{1}{\
\;\bm{|}\ \;}\ldots{\ \;\bm{|}\
\;}R_{n})}}\Rightarrow^{*}{\color[rgb]{0.8,0.25,0.33}{S}}$ and
${\color[rgb]{0.8,0.25,0.33}{S}}\vdash\mathopen{}\left\\{\Delta_{j}\right\\}_{j\leq
m}\mathclose{},\mathopen{}\left\\{\Sigma_{i}\right\\}_{i\leq n}\mathclose{}$.

##  7 Related Work

Our work takes [6] as a starting point. Guided by CLL, we set out to explore
if coherence can be broken down into more elementary logical rules which led
us to introduce forwarders. As a result, forwarders provide a more general
notion of compatibility. An earlier unpublished version of this work [8]
proposes synchronous forwarders, i.e., the restriction of forwarders with only
buffers of size one. In that case, we show that we can always construct a
coherence proof from a synchronous forwarder. However, synchronous forwarders
fail to capture all the possible interleaving of an arbiter (encoding of
coherence to processes).

Caires and Perez [3] also study multiparty session types in the context of
intuitionistic linear logic by translating global types to processes, called
_mediums_. Their work does not start from a logical account of global types
(their global types are just syntactic terms). But, as previous work [6], they
do generate arbiters as linear logic proofs, which are special instances of
forwarders. In this work, we generalise this approach to characterise exactly
which processes can justify the compatibility of several processes. In a more
recent work, van den Heuvel and Pérez [29] use routers in order to provide a
decentralised analysis of multiparty protocols. Routers act as point-to-point
forwarders but their types, called relative types, carry extra information on
causality of events that are not local. As in [3], this approach is confined
to global types and is therefore not complete wrt multiparty compatibility.

Another logical interpretation of multiparty compatibility is proposed by
Horne [21]. It uses the additonal expressivity of BV, a generalisation of CLL
with a non-commutative sequential operator, but only considers a fragment that
is expressible in the sequent calculus, unlike their previous work which
relied on the full strength of deep inference [10]. It also allows one to
consider compatible processes beyond duality but only for simply typed
processes, which cannot spawn other processes. The main advantage of this
approach is the fact that annotations are not needed (but can be recovered in
the typing).

Sangiorgi [27], probably the first to treat forwarders for the $\pi$-calculus,
uses binary forwarders, i.e., processes that only forward between two
channels, which are equivalent to our
${\color[rgb]{0.8,0.25,0.33}{x\leftrightarrow y}}$. We attribute our result to
the line of work that originated in 2010 by Caires and Pfenning [4], where
forwarders _à la Sangiorgi_ were introduced as processes to be typed by the
axiom rule in linear logic. Van den Heuvel and Perez [17] have recently
developed a version of linear logic that encompasses both classical and
intuitionistic logic, presenting a unified view on binary forwarders in both
logics.

Gardner et al. [13] study the expressivity of the linear forwarder calculus,
by encoding the asynchronous $\pi$-calculus (since it can encode distributed
choice). The linear forwarder calculus is a variant of the (asynchronous)
$\pi$-calculus that has binary forwarders and a restriction on the input
$x(y).P$ such that $y$ cannot be used for communicating (but only for
forwarding). Such a restriction is similar to the intuition behind our
forwarders, with the key difference that their methodology would not apply to
some of our session-based primitives.

Barbanera and Dezani [2] study multiparty session types as _gateways_ that
work as a medium among many interacting parties, forwarding communications
between two multiparty sessions. Such mechanism reminds us of our forwarder
composition: indeed, in their related work discussion they do mention that
their gateways could be modelled by a “connection-cut”.

Recent work [22, 15] proposes a variant of linear logic that models identity
providers, monitors that are like our forwarders but restricted to between two
channels. Identity providers are asynchronous, i.e., they allow unbounded
buffering of messages before forwarding. Our forwarders can be seen as a
generalisation to multiparty monitors. Multiparty monitors are also addressed
by Hamers and Jongmans [16], but not in a linear logic context.

Our forwarding mechanism may be confused with that of locality [25], which is
addressed logically by Caires et al. [5]. Locality requires that received
channels cannot be used for inputs (which must occur at the location where the
channel was created). In our case, we do not allow received channels to be
used at all until a new forwarder is spawned.

##  8 Conclusions and Future Work

We showed that forwarders are a logical characterisation of multiparty
compatibility and they can safely replace coherence for composing all well-
typed compatible communicating processes. Below, we discuss some aspects of
forwarders and identify possible future extensions.

Improving Multiparty Compatibility? Multiparty compatibility concerns the
error-free composition of processes that communicate by enqueueing/dequeueing
messages into/from pair-wise distinct FIFO queues. This work is not about
improving multiparty compatibility, unlike, e.g., [14]. In this paper, we take
the definition of multiparty compatibility and give it a logical
characterisation, in the spirit of the research line started in [4].
Forwarders are derived from our logical characterisation, this is our novel
contribution.

Are Forwarders Centralised? Following the approach taken for arbiters [6] and
mediums [3], forwarders provide an orchestration of the message flows between
the composed processes. In order to step to a fully decentralised setting, it
is necessary to redefine rule MCut such that i) queues are no longer embedded
in forwarders and ii) annotations in the forwarders are transferred to the
composed processes. This two steps are immediate and the correctness of this
follows, also immediately, by Theorem 5.1, since the type-context semantics in
Definition 1 is indeed fully decentralised. Note that a similar
decentralisation approach is also done for coherence in [6].

Cut Elimination for Forwarders. An unpublished longer version of this work [7]
addresses forwarder composition through a CUT rule for forwarders. Due to
annotations, such rule requires some subtle technical details for which there
was no space in this paper. This CUT rule for forwarders is proven to be
admissible through an algorithm of CUT elimination which mimics how messages
are transferred from one forwarder to another.

Process Language. Our process language is based Wadler’s CP [32], without
polymorphic communications. We conjecture that our forwarders can be smoothly
extended to polymorphic types $\exists X.A$ and $\forall X.A$. As future work,
we plan to consider a further extension to support recursion in the style of
Toninho et al. [28]. That will require an extended notion of multiparty
compatibility dealing with infinite paths as done by Ghilezan et al. [14].

Variants of Linear Logic. In this paper, we have chosen to base our theory on
CLL for two main reasons. Coherence is indeed defined by Carbone et al. [6] in
terms of CLL and therefore our results can immediately be related to theirs
without further investigations. An earlier version of forwarders was based on
intuitionistic linear logic, but moving to CLL required fewer rules and
greatly improved the presentation. Nevertheless, our results should be easily
reproducible in intuitionistic linear logic. A different approach could be to
include non-commutative operators which could encode our FIFO queues, e.g.,
using the work on non-commutative subexponentials by Kanovich et al. [23]. We
leave this as future work.

Beyond Linear Logic. Another interesting avenue would be to understand how the
queueing mechanism of forwarders can be treated within the graphical proof
system of [1]. Indeed, they observed that queues of length greater than 3
could not be expressed as linear logic formulas so they designed a proof
system that works not only on LL formulas (or even its generalisation with a
sequential operator called BV) but on more general graphs.

Variants of Coherence. Our results show that forwarders are a generalisation
of coherence proofs. Indeed, coherence would correspond to the notion of
_synchronous forwarders_ [8], the restriction of forwarders with only buffers
of size one. As a follow-up, we would like to investigate, whether other
syntactic restrictions of forwarders also induce interesting generalised
notions of coherence, and, as a consequence, generalisations of global types.

###  8.0.1 Acknowledgements

We would like to thank Frank Pfenning for initially suggesting the idea of
characterising arbiters as linear logic proofs, and Nobuko Yoshida and Ross
Horne for stimulating discussions.

## References

  * [1] Acclavio, M., Horne, R., Mauw, S., Straßburger, L.: A graphical proof theory of logical time. In: 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2022)
  * [2] Barbanera, F., Dezani-Ciancaglini, M.: Open multiparty sessions. In: Bartoletti, M., Henrio, L., Mavridou, A., Scalas, A. (eds.) Proceedings 12th Interaction and Concurrency Experience, ICE 2019, Copenhagen, Denmark, 20-21 June 2019. EPTCS, vol. 304, pp. 77–96 (2019). https://doi.org/10.4204/EPTCS.304.6, https://doi.org/10.4204/EPTCS.304.6
  * [3] Caires, L., Pérez, J.A.: Multiparty session types within a canonical binary theory, and beyond. In: Albert, E., Lanese, I. (eds.) Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9688, pp. 74–95. Springer (2016). https://doi.org/10.1007/978-3-319-39570-8_6, https://doi.org/10.1007/978-3-319-39570-8_6
  * [4] Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: CONCUR. pp. 222–236 (2010)
  * [5] Caires, L., Pfenning, F., Toninho, B.: Linear logic propositions as session types. Math. Struct. Comput. Sci. 26(3), 367–423 (2016). https://doi.org/10.1017/S0960129514000218, https://doi.org/10.1017/S0960129514000218
  * [6] Carbone, M., Lindley, S., Montesi, F., Schürmann, C., Wadler, P.: Coherence generalises duality: A logical explanation of multiparty session types. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada. LIPIcs, vol. 59, pp. 33:1–33:15. Schloss Dagstuhl \- Leibniz-Zentrum für Informatik, Germany (2016). https://doi.org/10.4230/LIPIcs.CONCUR.2016.33, https://doi.org/10.4230/LIPIcs.CONCUR.2016.33
  * [7] Carbone, M., Marin, S., Schürmann, C.: Forwarders as process compatibility, logically. CoRR abs/2112.07636 (2021), https://arxiv.org/abs/2112.07636
  * [8] Carbone, M., Marin, S., Schürmann, C.: Synchronous forwarders. CoRR abs/2102.04731 (2021), https://arxiv.org/abs/2102.04731
  * [9] Carbone, M., Montesi, F., Schürmann, C., Yoshida, N.: Multiparty session types as coherence proofs. In: CONCUR. pp. 412–426 (2015)
  * [10] Ciobanu, G., Horne, R.: Behavioural analysis of sessions using the calculus of structures. In: International Andrei Ershov Memorial Conference on Perspectives of System Informatics. pp. 91–106. Springer (2015)
  * [11] Coppo, M., Dezani-Ciancaglini, M., Yoshida, N., Padovani, L.: Global progress for dynamically interleaved multiparty sessions. MSCS 760, 1–65 (2015)
  * [12] Deniélou, P., Yoshida, N.: Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M.Z., Peleg, D. (eds.) Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II. Lecture Notes in Computer Science, vol. 7966, pp. 174–186. Springer (2013). https://doi.org/10.1007/978-3-642-39212-2_18, https://doi.org/10.1007/978-3-642-39212-2_18
  * [13] Gardner, P., Laneve, C., Wischik, L.: Linear forwarders. Inf. Comput. 205(10), 1526–1550 (2007). https://doi.org/10.1016/j.ic.2007.01.006, https://doi.org/10.1016/j.ic.2007.01.006
  * [14] Ghilezan, S., Pantovic, J., Prokic, I., Scalas, A., Yoshida, N.: Precise subtyping for asynchronous multiparty sessions. Proc. ACM Program. Lang. 5(POPL), 1–28 (2021). https://doi.org/10.1145/3434297, https://doi.org/10.1145/3434297
  * [15] Gommerstadt, H., Jia, L., Pfenning, F.: Session-typed concurrent contracts. In: Ahmed, A. (ed.) Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10801, pp. 771–798. Springer (2018). https://doi.org/10.1007/978-3-319-89884-1_27, https://doi.org/10.1007/978-3-319-89884-1_27
  * [16] Hamers, R., Jongmans, S.: Discourje: Runtime verification of communication protocols in clojure. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12078, pp. 266–284. Springer (2020). https://doi.org/10.1007/978-3-030-45190-5_15, https://doi.org/10.1007/978-3-030-45190-5_15
  * [17] van den Heuvel, B., Pérez, J.A.: Session type systems based on linear logic: Classical versus intuitionistic. In: Balzer, S., Padovani, L. (eds.) Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES@ETAPS 2020, Dublin, Ireland, 26th April 2020. EPTCS, vol. 314, pp. 1–11 (2020)
  * [18] Honda, K., Vasconcelos, V., Kubo, M.: Language primitives and type disciplines for structured communication-based programming. In: ESOP. pp. 22–138 (1998)
  * [19] Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008. pp. 273–284. ACM (2008)
  * [20] Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. JACM 63(1), 9 (2016), also: POPL, 2008, pages 273–284
  * [21] Horne, R.J.: Session subtyping and multiparty compatibility using circular sequents. In: In 31st International Conference on Concurrency Theory (CONCUR 2020). p. 12 (2020)
  * [22] Jia, L., Gommerstadt, H., Pfenning, F.: Monitors and blame assignment for higher-order session types. In: Bodík, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 582–594. ACM (2016). https://doi.org/10.1145/2837614.2837662, https://doi.org/10.1145/2837614.2837662
  * [23] Kanovich, M.I., Kuznetsov, S.L., Nigam, V., Scedrov, A.: A logical framework with commutative and non-commutative subexponentials. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10900, pp. 228–245. Springer (2018). https://doi.org/10.1007/978-3-319-94205-6_16, https://doi.org/10.1007/978-3-319-94205-6_16
  * [24] Lange, J., Yoshida, N.: Verifying asynchronous interactions via communicating session automata. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 97–117. Springer (2019). https://doi.org/10.1007/978-3-030-25540-4_6, https://doi.org/10.1007/978-3-030-25540-4_6
  * [25] Merro, M., Sangiorgi, D.: On asynchrony in name-passing calculi. Mathematical Structures in Computer Science 14(5), 715–767 (2004). https://doi.org/10.1017/S0960129504004323
  * [26] Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I and II. Information and Computation 100(1), 1–40,41–77 (Sep 1992)
  * [27] Sangiorgi, D.: pi-calculus, internal mobility, and agent-passing calculi. Theor. Comput. Sci. 167(1&2), 235–274 (1996), https://doi.org/10.1016/0304-3975(96)00075-8
  * [28] Toninho, B., Caires, L., Pfenning, F.: Corecursion and non-divergence in session-typed processes. In: Maffei, M., Tuosto, E. (eds.) Trustworthy Global Computing - 9th International Symposium, TGC 2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers. Lecture Notes in Computer Science, vol. 8902, pp. 159–175. Springer (2014). https://doi.org/10.1007/978-3-662-45917-1_11, https://doi.org/10.1007/978-3-662-45917-1_11
  * [29] van den Heuvel, B., Pérez, J.A.: A decentralized analysis of multiparty protocols. Science of Computer Programming p. 102840 (2022). https://doi.org/https://doi.org/10.1016/j.scico.2022.102840, https://www.sciencedirect.com/science/article/pii/S0167642322000739
  * [30] Vasconcelos, V.T.: Fundamentals of session types. Inf. Comput. 217, 52–70 (2012)
  * [31] Wadler, P.: Propositions as sessions. In: ICFP. pp. 273–286 (2012)
  * [32] Wadler, P.: Propositions as sessions. Journal of Functional Programming 24(2–3), 384–418 (2014), also: ICFP, pages 273–286, 2012

##  Appendix 0.A Compatiblity vs. Forwarders

See 5.1

###### Proof

Left to right: We will prove a slightly more general statement, namely that if
$\Delta\bullet\sigma$ is executable, then there exists a forwarder
${\color[rgb]{0.8,0.25,0.33}{F}}$ such that
${\color[rgb]{0.8,0.25,0.33}{F}}\Vdash\mathsf{tr}(\Delta\bullet\sigma)$.

Assume that $\Delta\bullet\sigma$ is executable, i.e., by Def. 3, all maximal
paths $\alpha_{1},\ldots,\alpha_{n}$ for $\Delta\bullet\sigma$ are live and
such that
$\alpha_{i}={\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}\otimes{\color[rgb]{0.8,0.25,0.33}{x}}[A,\\{A_{i}\\}_{i}]$
implies
${\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot},\\{{\color[rgb]{0.8,0.25,0.33}{y_{i}}}:A_{i}^{\bot}\\}_{i}$
is multiparty compatible (i.e., its dual is executable on $\sigma_{\epsilon}$
for some annotation).

We reason by induction on the size of $\Delta$, defined as the sum of the
formula sizes in $\Delta$. As $\Delta\not=\varnothing$ and any maximal path
for $\Delta\bullet\sigma$ is live, there must exist $\alpha_{1}$ such that
$\Delta\bullet\sigma\xrightarrow{\alpha_{1}}\Delta_{1}\bullet\sigma_{1}$. By
Lemma 1.1, there exists a rule $R_{\alpha_{1}}$ such that
$\Gamma=\mathsf{tr}(\Delta\bullet\sigma)$ is an instance of the conclusion of
$R_{\alpha_{1}}$ and $\Gamma_{1}=\mathsf{tr}(\Delta_{1}\bullet\sigma_{1})$ is
an instance of (one of) the premiss(es) of $R_{\alpha_{1}}$.

In the base case where $\Delta_{1}=\varnothing$ and
$\sigma_{1}=\sigma_{\epsilon}$, we must have
$\alpha_{1}={\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}\mathbf{1}{\color[rgb]{0.8,0.25,0.33}{x}}$
or
${\color[rgb]{0.8,0.25,0.33}{x}}{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{\leftrightarrow}}y}}$
and the associated rule $R_{\alpha_{1}}$(i.e., $\mathbf{1}$ or Ax resp.) does
not have any premisses giving us resp.
${\color[rgb]{0.8,0.25,0.33}{{x}[]}}\Vdash\Gamma$ or
${\color[rgb]{0.8,0.25,0.33}{x\leftrightarrow y}}\Vdash\Gamma$.

If the rule $R_{\alpha_{1}}$ has a single premiss, then by induction there
exists ${\color[rgb]{0.8,0.25,0.33}{F_{1}}}\Vdash\Gamma_{1}$ and by applying
the process operator that corresponds to $R_{\alpha_{1}}$ we obtain the
appropriate ${\color[rgb]{0.8,0.25,0.33}{F}}\Vdash\Gamma$.

If the rule $R_{\alpha_{1}}$ is branching, i.e., $\otimes$ or $\with$, we have
to treat each case separately:

  * •

If
$\alpha_{1}={\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}\otimes{\color[rgb]{0.8,0.25,0.33}{x}}[A,\\{A_{i}\\}_{i}]$,
then $R_{\alpha_{1}}$ is the $\otimes$-rule and $\Gamma_{1}$ is its right
premiss. Its left premiss would consist of
${\color[rgb]{0.8,0.25,0.33}{z}}:A,\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{z_{i}}}:A_{i}\right\\}_{i}\mathclose{}$
for some fresh endpoint names
${\color[rgb]{0.8,0.25,0.33}{z}},{\color[rgb]{0.8,0.25,0.33}{\tilde{z}}}$. We
know that
${\color[rgb]{0.8,0.25,0.33}{z}}:A^{\bot},\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{z_{i}}}:A_{i}^{\bot}\right\\}_{i}\mathclose{}$
form a multiparty compatible environment, and since
$\mathsf{size}({\color[rgb]{0.8,0.25,0.33}{z}}:A,\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{z_{i}}}:A_{i}\right\\}_{i}\mathclose{})<\mathsf{\Delta}$,
we have by induction that there exists a forwarder
${\color[rgb]{0.8,0.25,0.33}{F_{0}}}\Vdash{\color[rgb]{0.8,0.25,0.33}{z}}:A,\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{z_{i}}}:A_{i}\right\\}_{i}\mathclose{}$.
Hence, ${\color[rgb]{0.8,0.25,0.33}{{x}[z\triangleright
F_{0}].F_{1}}}\Vdash\Gamma$.

  * •

If
$\alpha_{1}={\color[rgb]{0.8,0.25,0.33}{x}}\with_{{\color[rgb]{0,0,1}\mathcal{L}}}{\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}$,
then $R_{\alpha_{1}}$ is the $\with$-rule and $\Gamma_{1}$ is its left
premiss. However, this means that the transition
$\alpha_{2}={\color[rgb]{0.8,0.25,0.33}{x}}\with_{{\color[rgb]{0,0,1}\mathcal{R}}}{\color[rgb]{0.8,0.25,0.33}{\tilde{y}}}$
was also possible as
$\Delta\bullet\sigma\xrightarrow{\alpha_{2}}\Delta_{2}\bullet\sigma_{2}$. By
Lemma 1.1, we get a rule $R_{\alpha_{2}}$ which is also a $\with$-rule and of
which $\Gamma_{2}=\mathsf{tr}(\Delta_{2}\bullet\sigma_{2})$ is the right
premiss. By induction applied to $\Delta_{1}\bullet\sigma_{1}$ we get
${\color[rgb]{0.8,0.25,0.33}{F_{1}}}\Vdash\Gamma_{1}$ and by induction applied
to $\Delta_{2}\bullet\sigma_{2}$ we get
${\color[rgb]{0.8,0.25,0.33}{F_{2}}}\Vdash\Gamma_{2}$. Hence,
${\color[rgb]{0.8,0.25,0.33}{x.\mathsf{case}(F_{1},F_{2})}}\Vdash\Gamma$.

Right to left: By contrapositive, suppose that $\Delta$ is not multiparty
compatible. There is then a maximal path $\alpha_{1},\ldots,\alpha_{n}$ for
any annotation of $\Delta^{\bot}$ (or for one of its sub-environments, in
which case the reasoning is easily adapted) which is not live. Fix an
annotation on $\Delta^{\bot}$, there is
$\Delta^{\bot}\bullet\sigma_{\epsilon}\xrightarrow{\alpha_{1}}\ldots\xrightarrow{\alpha_{n}}\Delta_{n}\bullet\sigma_{n}$
such that there is no available transition from $\Delta_{n}\bullet\sigma_{n}$
despite $\Delta_{n}\not=\varnothing$ or $\sigma_{n}\not=\sigma_{\epsilon}$. By
Lemma 1.1, we can construct a branch of a derivation in forwarders starting
from root $\Delta^{\bot}$, following $\tilde{\alpha}$ step-by-step and endinn
at the leaf on $\Gamma$ = translation of $\Delta_{n}\bullet\sigma_{n}$. By
Lemma 1.2, $\Gamma$ is not provable in our proof system for forwarders, i.e.,
there is no ${\color[rgb]{0.8,0.25,0.33}{F}}$ such that
${\color[rgb]{0.8,0.25,0.33}{F}}\Vdash\Gamma$. By Lemma 3 this means that
there is no correct derivation of $\Delta^{\bot}$ (as otherwise applying rules
bottom-up would preserve this property all the way to the leaf $\Gamma$).

##  Appendix 0.B MCutF admissibility

In this appendix, we display all cases for MCutF elimination that we need to
prove:

See 6.1

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}\tilde{x}:(\bm{\nu}\tilde{y})\,Q[\tilde{P}])\,\tilde{R}}}\vdash\tilde{\Delta},\tilde{\Sigma}\lx@proof@logical@and\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{P_{j}}}\vdash\Delta_{i},{\color[rgb]{0.8,0.25,0.33}{y_{j}}}:A_{j}\right\\}_{j\leq
m}\mathclose{}\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{R_{i}}}\vdash\Sigma_{i},{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:B_{i}\right\\}_{i\leq
n}\mathclose{}{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\mathopen{}\left\\{[\\![\Psi_{i}]\\!]{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:B_{i}^{\bot}\right\\}_{i\leq
n}\mathclose{},\mathopen{}\left\\{[\\![\Psi_{i}]\\!]{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\cdot\right\\}_{n<i\leq
p}\mathclose{}$

The rule has a developed side condition: $\bigcup_{i\leq
p}{\Psi_{i}}\setminus\mathopen{}\left\\{{\color[rgb]{0,0,1}\mathcal{L}},{\color[rgb]{0,0,1}\mathcal{R}},{\color[rgb]{0,0,1}\mathcal{Q}},{\color[rgb]{0,0,1}\ast}\right\\}\mathclose{}=\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{y_{j}}}:A_{j}^{\bot}\right\\}_{j\leq
m}\mathclose{}$.

Send Message ($\otimes$).

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{{x}(y).Q}}[\tilde{P}])\,({\color[rgb]{0.8,0.25,0.33}{{x}[y\triangleright
P].R}}{\ \;\bm{|}\
\;}\tilde{R})}}\vdash\Delta,\Sigma,\tilde{\Delta},\tilde{\Sigma}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}[y\triangleright
P].R}}}}\vdash\Delta,\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:A\otimes
B\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{y}}:A{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:B\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}(y).Q}}}}\Vdash[\\![\Psi]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot}\parr^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}B^{\bot},\Gamma{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi]\\!][^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}{\color[rgb]{0.8,0.25,0.33}{y}}:A^{\bot}]{\color[rgb]{0.8,0.25,0.33}{x}}:B^{\bot},\Gamma$

$\Longrightarrow$

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}y\tilde{y})\,Q[P,\tilde{P}])\,(R{\
\;\bm{|}\
\;}\tilde{R})}}\vdash\Delta,\Sigma,\tilde{\Delta},\tilde{\Sigma}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{y}}:A{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:B\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi]\\!][^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}{\color[rgb]{0.8,0.25,0.33}{y}}:A^{\bot}]{\color[rgb]{0.8,0.25,0.33}{x}}:B^{\bot},\Gamma$

Receive Message ($\parr$).

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}z\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{{x}[y\triangleright
S].Q}}[P,\tilde{P}])\,({\color[rgb]{0.8,0.25,0.33}{{x}(y).R}}{\ \;\bm{|}\
\;}\tilde{R})}}\vdash\Delta,\Sigma,\tilde{\Delta},\tilde{\Sigma}\lx@proof@logical@and\begin{array}[]{ll}{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{z}}:A^{\bot}\\\\[5.69054pt]
{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}(y).R}}}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:A\parr
B{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{y}}:A,{\color[rgb]{0.8,0.25,0.33}{x}}:B\end{array}\ldots{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}[y\triangleright
S].Q}}}}\Vdash[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot}\otimes^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}B^{\bot},[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0.8,0.25,0.33}{z}}:A][\\![\Psi_{k}]\\!]{\color[rgb]{0.8,0.25,0.33}{x_{k}}}:B_{k}^{\bot},\Gamma-k\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{S}}\Vdash{\color[rgb]{0.8,0.25,0.33}{z}}:A,{\color[rgb]{0.8,0.25,0.33}{y}}:A^{\bot}{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:B^{\bot},\Gamma$

$\Longrightarrow$

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,Q[\tilde{P}])\,((\bm{\nu}yz:S)\,(R{\
\;\bm{|}\ \;}P){\ \;\bm{|}\
\;}\tilde{R})}}\vdash\Delta,\Sigma,\tilde{\Delta},\tilde{\Sigma}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}yz:S)\,(R{\
\;\bm{|}\
\;}P)}}\Vdash\Sigma,\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:B\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{y}}:A,{\color[rgb]{0.8,0.25,0.33}{x}}:B{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{z}}:A^{\bot}{\color[rgb]{0.8,0.25,0.33}{S}}\Vdash{\color[rgb]{0.8,0.25,0.33}{z}}:A,{\color[rgb]{0.8,0.25,0.33}{y}}:A^{\bot}\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:B^{\bot},\Gamma$

Note that now the message (namely process ${\color[rgb]{0.8,0.25,0.33}{P}}$)
has finally been delivered and it can be directly linked with a new MCutF.

Internal choice ($\oplus$).

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{x.\mathsf{case}(Q,S)}}[\tilde{P}])\,({\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inl}].R}}{\
\;\bm{|}\
\;}\tilde{R})}}\vdash\Sigma,\tilde{\Delta},\tilde{\Sigma}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inl}].R}}}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:A\oplus
B{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:A\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{x.\mathsf{case}(Q,S)}}}}\Vdash[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot}\with^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}B^{\bot},\Gamma\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi_{x}]\\!][^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}{\color[rgb]{0,0,1}\mathcal{L}}]{\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot},\Gamma{\color[rgb]{0.8,0.25,0.33}{S}}\Vdash[\\![\Psi_{x}]\\!][^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}{\color[rgb]{0,0,1}\mathcal{R}}]{\color[rgb]{0.8,0.25,0.33}{x}}:B^{\bot},\Gamma$

$\Longrightarrow$

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,Q[\tilde{P}])\,(R{\
\;\bm{|}\
\;}\tilde{R})}}\vdash\Sigma,\tilde{\Delta},\tilde{\Sigma}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:A\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi_{x}]\\!][^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}{\color[rgb]{0,0,1}\mathcal{L}}]{\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot},\Gamma$

External choice ($\with$).

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inl}].Q}}[\tilde{P}])\,({\color[rgb]{0.8,0.25,0.33}{x.\mathsf{case}(R,S)}}{\
\;\bm{|}\
\;}\tilde{R})}}\vdash\Sigma,\tilde{\Delta},\tilde{\Sigma}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{x.\mathsf{case}(R,S)}}}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:A\with
B\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{y}}:A{\color[rgb]{0.8,0.25,0.33}{S}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:B\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inl}].Q}}\Vdash[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot}\oplus^{x_{k}}B^{\bot},[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0,0,1}\mathcal{L}}][\\![\Psi_{k}]\\!]{\color[rgb]{0.8,0.25,0.33}{x_{k}}}:B_{k}^{\bot},\Gamma-k{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot},\Gamma$

$\Longrightarrow$

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{Q}[\tilde{P}])\,({R}{\
\;\bm{|}\
\;}\tilde{R})}}\vdash\Sigma,\tilde{\Delta},\tilde{\Sigma}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{y}}:A\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:A^{\bot},\Gamma$

Axiom.

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x_{1}x_{2}:{\color[rgb]{0.8,0.25,0.33}{x_{1}\leftrightarrow
x_{2}}})\,({\color[rgb]{0.8,0.25,0.33}{x_{1}\leftrightarrow z_{1}}}{\
\;\bm{|}\ \;}{\color[rgb]{0.8,0.25,0.33}{x_{2}\leftrightarrow
z_{2}}})}}\vdash{\color[rgb]{0.8,0.25,0.33}{z_{1}}}:a^{\bot},{\color[rgb]{0.8,0.25,0.33}{z_{2}}}:a\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{x_{1}\leftrightarrow
z_{1}}}\vdash{\color[rgb]{0.8,0.25,0.33}{x_{1}}}:a,{\color[rgb]{0.8,0.25,0.33}{z_{1}}}:a^{\bot}{\color[rgb]{0.8,0.25,0.33}{x_{2}\leftrightarrow
z_{2}}}\vdash{\color[rgb]{0.8,0.25,0.33}{x_{2}}}:a^{\bot},{\color[rgb]{0.8,0.25,0.33}{z_{2}}}:a{\color[rgb]{0.8,0.25,0.33}{x_{1}\leftrightarrow
x_{2}}}\Vdash{\color[rgb]{0.8,0.25,0.33}{x_{1}}}:a^{\bot},{\color[rgb]{0.8,0.25,0.33}{x_{2}}}:a$

$\Longrightarrow$

$\small{\color[rgb]{0.8,0.25,0.33}{z_{1}\leftrightarrow
z_{2}}}\vdash{\color[rgb]{0.8,0.25,0.33}{z_{1}}}:a^{\bot},{\color[rgb]{0.8,0.25,0.33}{z_{2}}}:a$

Close ($\mathbf{1}$).

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{x().Q}}[\tilde{P}])\,({\color[rgb]{0.8,0.25,0.33}{{x}[]}}{\
\;\bm{|}\
\;}\tilde{R})}}\vdash\tilde{\Delta},\tilde{\Sigma}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{{x}[]}}}}\vdash{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{1}\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{x().Q}}\Vdash[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:\bot^{x_{k}},\Gamma{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi_{x}]\\!][^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}{\color[rgb]{0,0,1}\ast}]{\color[rgb]{0.8,0.25,0.33}{x}}:\cdot,\Gamma$

$\Longrightarrow$

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,Q[\tilde{P}])\,(\tilde{R})}}\vdash\tilde{\Delta},\tilde{\Sigma}\lx@proof@logical@and\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash[\\![\Psi_{x}]\\!][^{{\color[rgb]{0.8,0.25,0.33}{x_{k}}}}{\color[rgb]{0,0,1}\ast}]{\color[rgb]{0.8,0.25,0.33}{x}}:\cdot,\Gamma$

Wait ($\bot$).

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x:{\color[rgb]{0.8,0.25,0.33}{{x}[]}})\,({\color[rgb]{0.8,0.25,0.33}{x().P}})}}\vdash\Delta\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{x().P}}}}\vdash\Delta,{\color[rgb]{0.8,0.25,0.33}{x}}:\bot{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta{\color[rgb]{0.8,0.25,0.33}{{x}[]}}\Vdash{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{1}^{\tilde{x}},\mathopen{}\left\\{[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0,0,1}\ast}]{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\cdot\right\\}_{i}\mathclose{}$

$\Longrightarrow$ ${{\color[rgb]{0.8,0.25,0.33}{P}}\vdash\Delta}$

Server query ($\oc$).

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{\wn
x[z].Q}}[\tilde{P}])\,({\color[rgb]{0.8,0.25,0.33}{\oc x(z).R}}{\ \;\bm{|}\
\;}\tilde{R})}}\vdash\wn\Sigma,\tilde{\Delta},\tilde{\Sigma}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).R}}}}\vdash\,\wn\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:\oc
A{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\,\wn\Sigma,{\color[rgb]{0.8,0.25,0.33}{z}}:A\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{\wn
x[z].Q}}\Vdash\Gamma-k,[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0,0,1}\mathcal{Q}}][\\![\Psi_{k}]\\!]{\color[rgb]{0.8,0.25,0.33}{x_{k}}}:B_{k}^{\bot},[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{x}}:\wn^{\color[rgb]{0.8,0.25,0.33}{x_{k}}}A^{\bot}{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\Gamma,[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{z}}:A^{\bot}$

$\Longrightarrow$

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}z\tilde{x}:(\bm{\nu}\tilde{y})\,{Q}[\tilde{P}])\,({R}{\
\;\bm{|}\
\;}\tilde{R})}}\vdash\wn\Sigma,\tilde{\Delta},\tilde{\Sigma}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\,\wn\Sigma,{\color[rgb]{0.8,0.25,0.33}{z}}:A\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\Gamma,[\\![\Psi_{x}]\\!]{\color[rgb]{0.8,0.25,0.33}{z}}:A^{\bot}$

Server opening ($\wn$).

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).Q}}[\tilde{P}])\,({\color[rgb]{0.8,0.25,0.33}{\wn x[z].R}}{\ \;\bm{|}\
\;}\tilde{R})}}\vdash\Sigma,\tilde{\Sigma}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{\wn
x[z].R}}}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{z}}:A\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).Q}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\wn
A_{i}^{\bot}\right\\}_{i}\mathclose{},{\color[rgb]{0.8,0.25,0.33}{x}}:\oc^{\color[rgb]{0.8,0.25,0.33}{\tilde{x}}}A{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\wn
A_{i}^{\bot}\right\\}_{i}\mathclose{},[^{{\color[rgb]{0.8,0.25,0.33}{\tilde{x}}}}{\color[rgb]{0,0,1}\mathcal{Q}}]{\color[rgb]{0.8,0.25,0.33}{z}}:A$

$\Longrightarrow$

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,Q[\tilde{P}])\,(R{\
\;\bm{|}\
\;}\tilde{R})}}\vdash\Sigma,\tilde{\Sigma}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{z}}:A\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\wn
A_{i}^{\bot}\right\\}_{i}\mathclose{},[^{{\color[rgb]{0.8,0.25,0.33}{\tilde{x}}}}{\color[rgb]{0,0,1}\mathcal{Q}}]{\color[rgb]{0.8,0.25,0.33}{z}}:A$

Server discarding (w).

${\color[rgb]{0.8,0.25,0.33}{{\color[rgb]{0.8,0.25,0.33}{\wn
x[z].R}}}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{y}}:A\qquad{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma\qquad{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn A$

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).Q}}[\tilde{P}])\,(R{\ \;\bm{|}\
\;}\tilde{R})}}\vdash\Sigma,\mathopen{}\left\\{\wn\Sigma_{i}\right\\}_{i}\mathclose{}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma\quad\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{R_{i}}}\vdash\wn\Sigma_{i},{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\oc
A_{i}\right\\}_{i}\mathclose{}\quad{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).Q}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\wn
A_{i}^{\bot}\right\\}_{i}\mathclose{},{\color[rgb]{0.8,0.25,0.33}{x}}:\oc^{\color[rgb]{0.8,0.25,0.33}{\tilde{x}}}A{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\wn
A_{i}^{\bot}\right\\}_{i}\mathclose{},[^{{\color[rgb]{0.8,0.25,0.33}{\tilde{x}}}}{\color[rgb]{0,0,1}\mathcal{Q}}]{\color[rgb]{0.8,0.25,0.33}{z}}:A$

$\Longrightarrow$

$\small{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,\mathopen{}\left\\{\wn\Sigma_{i}\right\\}_{i}\mathclose{}{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma$

Server duplicating (c).

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).Q}}[\tilde{P}])\,(R{\ \;\bm{|}\
\;}\tilde{R})}}\vdash\Sigma,\mathopen{}\left\\{\wn\Sigma_{i}\right\\}_{i}\mathclose{}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A\quad\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{R_{i}}}\vdash\wn\Sigma_{i},{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\oc
A_{i}\right\\}_{i}\mathclose{}\quad{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).Q}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\wn
A_{i}^{\bot}\right\\}_{i}\mathclose{},{\color[rgb]{0.8,0.25,0.33}{x}}:\oc^{\color[rgb]{0.8,0.25,0.33}{\tilde{x}}}A{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\wn
A_{i}^{\bot}\right\\}_{i}\mathclose{},[^{{\color[rgb]{0.8,0.25,0.33}{\tilde{x}}}}{\color[rgb]{0,0,1}\mathcal{Q}}]{\color[rgb]{0.8,0.25,0.33}{z}}:A$

$\Longrightarrow$

$\small{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).Q}}[\tilde{P}])\,((\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).Q}}[\tilde{P}])\,(R{\ \;\bm{|}\ \;}\tilde{R}){\ \;\bm{|}\
\;}\tilde{R})}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A,\mathopen{}\left\\{\wn\Sigma_{i}\right\\}_{i}\mathclose{}{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).Q}}[\tilde{P}])\,((\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).Q}}[\tilde{P}])\,(R{\ \;\bm{|}\ \;}\tilde{R}){\ \;\bm{|}\
\;}\tilde{R})}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A,\mathopen{}\left\\{\wn\Sigma_{i}\right\\}_{i}\mathclose{},\mathopen{}\left\\{\wn\Sigma_{i}\right\\}_{i}\mathclose{}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{(\bm{\nu}x\tilde{x}:(\bm{\nu}\tilde{y})\,{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).Q}}[\tilde{P}])\,(R{\ \;\bm{|}\
\;}\tilde{R})}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A,\mathopen{}\left\\{\wn\Sigma_{i}\right\\}_{i}\mathclose{}\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{R}}\vdash\Sigma,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A,{\color[rgb]{0.8,0.25,0.33}{x}}:\wn
A\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).Q}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\wn
A_{i}^{\bot}\right\\}_{i}\mathclose{},{\color[rgb]{0.8,0.25,0.33}{x}}:\oc^{\color[rgb]{0.8,0.25,0.33}{\tilde{x}}}A{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\wn
A_{i}^{\bot}\right\\}_{i}\mathclose{},[^{{\color[rgb]{0.8,0.25,0.33}{\tilde{x}}}}{\color[rgb]{0,0,1}\mathcal{Q}}]{\color[rgb]{0.8,0.25,0.33}{z}}:A\quad\ldots\quad{\color[rgb]{0.8,0.25,0.33}{\oc
x(z).Q}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\wn
A_{i}^{\bot}\right\\}_{i}\mathclose{},{\color[rgb]{0.8,0.25,0.33}{x}}:\oc^{\color[rgb]{0.8,0.25,0.33}{\tilde{x}}}A{\color[rgb]{0.8,0.25,0.33}{Q}}\Vdash\mathopen{}\left\\{{\color[rgb]{0.8,0.25,0.33}{x_{i}}}:\wn
A_{i}^{\bot}\right\\}_{i}\mathclose{},[^{{\color[rgb]{0.8,0.25,0.33}{\tilde{x}}}}{\color[rgb]{0,0,1}\mathcal{Q}}]{\color[rgb]{0.8,0.25,0.33}{z}}:A$

##  Appendix 0.C Example

######  Example 4 (Additive Criss-cross)

The process
${\color[rgb]{0.8,0.25,0.33}{P}}\colonequals{\color[rgb]{0.8,0.25,0.33}{x.\mathsf{case}({\color[rgb]{0.8,0.25,0.33}{y.\mathsf{case}(P_{1},P_{2})}},{\color[rgb]{0.8,0.25,0.33}{y.\mathsf{case}(P_{3},P_{4})}})}}$
is a variant of multiplicative criss-cross in Example 2 that uses branching
instead. As a derivation:

${\color[rgb]{0.8,0.25,0.33}{P}}\Vdash{\color[rgb]{0.8,0.25,0.33}{x}}:(\mathbf{name}\oplus^{\color[rgb]{0.8,0.25,0.33}{y}}\mathbf{name})\with^{\color[rgb]{0.8,0.25,0.33}{y}}(\mathbf{cost}\oplus^{\color[rgb]{0.8,0.25,0.33}{y}}\mathbf{cost}),{\color[rgb]{0.8,0.25,0.33}{y}}:(\mathbf{name}^{\bot}\oplus^{\color[rgb]{0.8,0.25,0.33}{x}}\mathbf{cost}^{\bot})\with^{\color[rgb]{0.8,0.25,0.33}{x}}(\mathbf{name}^{\bot}\oplus^{\color[rgb]{0.8,0.25,0.33}{x}}\mathbf{cost}^{\bot})\lx@proof@logical@and{\color[rgb]{0.8,0.25,0.33}{P_{1}}}\Vdash\Delta_{1}\qquad\qquad{\color[rgb]{0.8,0.25,0.33}{P_{2}}}\Vdash\Delta_{2}\qquad\qquad{\color[rgb]{0.8,0.25,0.33}{P_{3}}}\Vdash\Delta_{3}\qquad\qquad{\color[rgb]{0.8,0.25,0.33}{P_{4}}}\Vdash\Delta_{4}$

${\color[rgb]{0.8,0.25,0.33}{P_{1}}}={\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inl}].{\color[rgb]{0.8,0.25,0.33}{{y}[\mathsf{inl}].{\color[rgb]{0.8,0.25,0.33}{y\leftrightarrow
x}}}}}}\Vdash\Delta_{1}=[^{{\color[rgb]{0.8,0.25,0.33}{y}}}{\color[rgb]{0,0,1}\mathcal{L}}]{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{name}\oplus^{\color[rgb]{0.8,0.25,0.33}{y}}\mathbf{name},[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0,0,1}\mathcal{L}}]{\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{name}^{\bot}\oplus^{\color[rgb]{0.8,0.25,0.33}{x}}\mathbf{cost}^{\bot}{\color[rgb]{0.8,0.25,0.33}{{y}[\mathsf{inl}].{\color[rgb]{0.8,0.25,0.33}{y\leftrightarrow
x}}}}\Vdash[^{{\color[rgb]{0.8,0.25,0.33}{y}}}{\color[rgb]{0,0,1}\mathcal{L}}]{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{name},{\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{name}^{\bot}\oplus^{\color[rgb]{0.8,0.25,0.33}{x}}\mathbf{cost}^{\bot}{\color[rgb]{0.8,0.25,0.33}{y\leftrightarrow
x}}\Vdash{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{name},{\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{name}^{\bot}$

${\color[rgb]{0.8,0.25,0.33}{P_{2}}}={\color[rgb]{0.8,0.25,0.33}{{x}[\mathsf{inr}].{\color[rgb]{0.8,0.25,0.33}{{y}[\mathsf{inl}].{\color[rgb]{0.8,0.25,0.33}{y\leftrightarrow
x}}}}}}\Vdash\Delta_{2}=[^{{\color[rgb]{0.8,0.25,0.33}{y}}}{\color[rgb]{0,0,1}\mathcal{L}}]{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{name}\oplus^{\color[rgb]{0.8,0.25,0.33}{y}}\mathbf{name},[^{{\color[rgb]{0.8,0.25,0.33}{x}}}{\color[rgb]{0,0,1}\mathcal{R}}]{\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{name}^{\bot}\oplus^{\color[rgb]{0.8,0.25,0.33}{x}}\mathbf{cost}^{\bot}{\color[rgb]{0.8,0.25,0.33}{{y}[\mathsf{inl}].{\color[rgb]{0.8,0.25,0.33}{y\leftrightarrow
x}}}}\Vdash[^{{\color[rgb]{0.8,0.25,0.33}{y}}}{\color[rgb]{0,0,1}\mathcal{L}}]{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{name},{\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{name}^{\bot}\oplus^{\color[rgb]{0.8,0.25,0.33}{x}}\mathbf{cost}^{\bot}{\color[rgb]{0.8,0.25,0.33}{y\leftrightarrow
x}}\Vdash{\color[rgb]{0.8,0.25,0.33}{x}}:\mathbf{name},{\color[rgb]{0.8,0.25,0.33}{y}}:\mathbf{name}^{\bot}$