11institutetext: Técnico Lisboa / INESC-ID 11email:
<EMAIL_ADDRESS>22institutetext: NOVA FCT / NOVA LINCS 22email:
<EMAIL_ADDRESS>
# The Session Abstract Machine
(Extended Version)

Luís Caires 11 Bernardo Toninho 22

###### Keywords:

Abstract machine Session Types Linear Logic

> Abstract. We build on a fine-grained analysis of session-based interaction
> as provided by the linear logic typing disciplines to introduce the SAM, an
> abstract machine for mechanically executing session-typed processes. A
> remarkable feature of the SAM’s design is its ability to naturally segregate
> and coordinate sequential with concurrent session behaviours. In particular,
> implicitly sequential parts of session programs may be efficiently executed
> by deterministic sequential application of SAM transitions, amenable to
> compilation, and without concurrent synchronisation mechanisms. We provide
> an intuitive discussion of the SAM structure and its underlying design, and
> state and prove its correctness for executing programs in a session calculus
> corresponding to full classical linear logic $\mathsf{CLL}$. We also discuss
> extensions and applications of the SAM to the execution of linear and
> session-based programming languages.

##  1 Introduction

In this work, we build on the linear logic based foundation for session types
[13, 15, 71] to construct SAM, an abstract machine specially designed for
executing session processes typed by (classical) linear logic $\mathsf{CLL}$.
Although motivated by the session type discipline, which originally emerged in
the realm of concurrency and distribution [30, 32, 27, 33], a basic motivation
for designing the SAM was to provide an efficient deterministic execution
model for the implicitly sequential session-typed program idioms that often
proliferate in concurrent session-based programming. It is well-known that in
a world of fine-grained concurrency, building on many process-based encodings
of concepts such as (abstract) data types, functions, continuations, and
effects [48, 69, 64, 65, 10, 67, 53], large parts of the code turn out to be
inherently sequential, further justifying the foundational and practical
relevance of our results. A remarkable feature of the SAM’s design is
therefore its potential to efficiently coordinate sequential with full-fledged
concurrent behaviours in session-based programming.

Leveraging early work relating linear logic with the semantics of linear and
concurrent computation [1, 6, 2], the proposition-as-types (PaT)
interpretation [72] of linear logic proofs as a form of well-behaved session-
typed nominal calculus has motivated many developments since its inception
[12, 5, 67, 66]. We believe that, much how the $\lambda$-calculus is deemed a
canonical typed model for functional (sequential) computation with pure
values, the session calculus can be accepted as a fairly canonical typed model
for stateful concurrent computation with linear resources, well-rooted in the
trunk of “classical” Type Theory. The PaT interpretation of session processes
also establishes a bridge between more classical theories of computation and
process algebra via logic. It also reinstates Robin Milner’s view of
computation as interaction [47], “data-as-processes” [48] and “functions-as-
processes” [46], now in the setting of a tightly typed world, based on linear
logic, where types may statically ensure key properties like deadlock-freedom,
termination, and correct resource usage in stateful programs. Session calculi
are motivating novel programming language design, bringing up new insights on
typeful programming [17] with linear and behavioral types, e.g., [23, 60, 19,
5]. Most systems of typed session calculi have been formulated in process
algebraic form [30, 32, 27], or on top of concurrent $\lambda$-calculi with an
extra layer of communication channels (e.g., [28]), logically inspired systems
such as the those discussed in this paper (e.g., [13, 15, 71, 22, 38, 58, 26,
60]) are defined by a logical proof / type system where proof rules are seen
as witnesses for the typing of process terms, proofs are read as processes,
structural equivalence is proof conversion and computation corresponds to cut
reduction. These formulations provide a fundamental semantic foundation to
study the model’s expressiveness and meta-theory, but of course do not
directly support the concrete implementation of programming languages based on
them.

Although several programming language implementations of nominal calculi based
languages have been proposed for some time (e.g. [56]), with some introducing
abstract machines as the underlying technology (e.g., [68, 45]), we are not
aware of any prior design proposal for an abstract machine for reducing
session processes exploiting deep properties of a source session calculus, as
e.g., the CAM [20] the LAM [40], or the KM [39], which also explore the Curry-
Howard correspondences, may reclaim to be, respectively for call-by-value
cartesian-closed structures, linear logic, and the call-by-name
$\lambda$-calculus.

The SAM reduction strategy explores a form of “asynchronous” interaction that
essentially expresses that, for processes typed by the logical discipline,
sessions are always pairwise causally independent, in the sense that immediate
communication on some session is never blocked by communication on a different
session. This property is captured syntactically by prefix commutation
equations, valid commuting conversions in the underlying logic: adding
equations for such laws explicitly to process structural congruence keeps
observational equivalence of $\mathsf{CLL}$ processes untouched [52]. Combined
with insights related to focalisation and polarisation in linear logic [4, 55,
43], we realize that all communication in any session may be operationally
structured as the exchange of bundles of positive actions from sender to
receiver, where the roles sender/receiver flip whenever the session type swaps
polarity. Communication may then be mediated by message buffers, first filled
up by the sender (“write-biased” scheduling), and at a later time emptied by
the receiver. Building on these observations and on key properties of linear
logic proofs leveraged in well-known purely structural proofs of progress [13,
15, 60], we identify a sequential and deterministic reduction strategy for
$\mathsf{CLL}$ typed processes, based on a form of co-routining where
continuations are associated to session queues, and “context switching” occurs
whenever polarity flips. That such strategy works at all, preserving all the
required correctness properties of the $\mathsf{CLL}$ language does not seem
immediately obvious, given that each processes may sequentially perform
multiple actions on many different sessions, meaning that multiple context
switches must be interleaved. The bulk of our paper is then devoted to
establishing all such properties in a precise technical sense. We believe that
the SAM may provide a principled foundation for safe execution environments
for programming languages combining functional, imperative and concurrent
idioms based on session and linear types, as witnessed in practice for Rust
[36], (Linear) Haskell [44, 8, 37], Move [9], and in research languages [59,
35, 23]. To further substantiate these views we have developed an
implementation of the SAM, integrated in a language for realistic session-
based shared-state programs [16].

Outline and Contributions. In Section 2 we briefly review the session-typed
calculus $\mathsf{CLL}$, which exactly corresponds to (classical) Linear Logic
with mix. In Section 3 we discuss the motivation and design principles of the
core SAM, gradually presenting its structure for the language fragment
corresponding to session types without the exponentials, which will be
introduced later. Even if the core SAM structure and transition rules are
fairly simple, the proofs of correctness are more technically involved, and
require progressive build up. Therefore, we first bridge between
$\mathsf{CLL}$ and SAM via a intermediate logical language $\mathsf{CLLB}$,
introducing explicit queues in cuts, presented in Section 4. We show
preservation (Theorem 4.1) and progress (Theorem 4.2) for $\mathsf{CLLB}$, and
prove that there is two way simulation between $\mathsf{CLLB}$ and
$\mathsf{CLL}$ via a strong operational correspondence (Theorem 4.3). Given
this correspondence, in Section 5 we state and prove the adequacy of the SAM
for executing $\mathsf{CLL}$ processes, showing soundness wrt. $\mathsf{CLLB}$
(Theorem 5.1) and $\mathsf{CLL}$ (Theorem 5.2), and progress / deadlock
absense (Theorem 5.3). In Section 6 modularly extend the previous results to
the exponentials and mix, and revise the core SAM by introducing explicit
environments, stating the associated adequacy results (Theorem 6.1 and Theorem
6.2). We also discuss how to accommodate concurrency, and other extensions in
the SAM. We conclude by a discussion of related work and additional remarks.
Appendix 0.A includes additional lemmas and proofs.

##  2 Background on $\mathsf{CLL}$, the core language and type system

We start by revisiting the language and type system of $\mathsf{CLL}{}$, and
its operational semantics. The system is based on a PaT interpretation of
classical linear logic (we follow the presentations of [15, 11, 59]).

######  Definition 1 (Types)

Types $A,B$ are defined by

$\begin{array}[]{lllllllllllll}A,B::=&{\mathbf{1}}&\;|\;\bot&\;|\;A\mathbin{\bindnasrepma}B&\;|\;A\otimes
B&\;|\;\mathbin{\binampersand}_{\ell\in L}{A_{\ell}}&\;|\;\oplus_{\ell\in
L}{A_{\ell}}&\;|\;!A&\;|\;?A\\\ \end{array}$

Types comprise of the units (${\mathbf{1}}$, $\bot$), multiplicatives
($\otimes$, $\mathbin{\bindnasrepma}$), additives ($\oplus_{\ell\in
L}{A_{\ell}}$, $\mathbin{\binampersand}_{\ell\in L}{A_{\ell}}$) and
exponentials ($!$, $?$). We adopt here a labeled version of the additives,
where the linear logic sum type $A_{\\#\mathsf{inl}}\oplus
A_{\\#\mathsf{inr}}$ is defined by
$\oplus_{\ell\in\\{\\#\mathsf{inl},\\#\mathsf{inr}\\}}{A_{\ell}}$. The
_positive types_ are ${\mathbf{1}}$, $\otimes$, $\oplus$, and $!$, while the
_negative types_ are $\bot$, $\mathbin{\bindnasrepma}$,
$\mathbin{\binampersand}$ and $?$. We abbreviate
$\overline{A}\mathbin{\bindnasrepma}B$ by $A\multimap B$. We write $A^{+}$
(resp. $A^{-}$) to assert that $A$ is a positive (resp. negative) type. Type
_duality_ $\overline{A}$ corresponds to negation:

$\begin{array}[]{llllllllllllllll}\overline{{\mathbf{1}}}&=&\bot&&&\hskip
15.0pt\overline{A\otimes
B}&=&\overline{A}\mathbin{\bindnasrepma}\overline{B}&&&\hskip
15.0pt\overline{\oplus_{\ell\in
L}{A_{\ell}}}&=&\mathbin{\binampersand}_{\ell\in
L}{\overline{A}_{\ell}}&\hskip 15.0pt\overline{!A}&=&?\overline{B}\end{array}$

Duality captures the symmetry of behaviour in binary process interaction, as
manifest in the cut rule.

######  Definition 2 (Processes)

The syntax of processes $P,Q$ is given by:

$\begin{array}[]{lcl}P,Q&::=&{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\mid
P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
Q\mid{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\
y\mid{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{:}A{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\mid{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x\mid{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
x;P\\\
&\mid&{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{case}}\
x\ \\{|{\\#\mathsf{\ell}\in
L}{:}P_{\ell}\\}\mid\\#{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{inr}}\
x;P\mid{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(y.P);Q\mid{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
x(z);P\\\
&\mid&{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(y);P\mid{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{?}}x;P\mid{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x:A{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\mid{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{call}}\
x(z);Q\end{array}$

_Typing judgements_ have the form $P\vdash\Delta;\Gamma$, where $P$ is a
process and the _typing context_ $\Delta;\Gamma$ is dyadic [4, 7, 54, 13]:
both $\Delta$ and $\Gamma$ assign types to names, the context $\Delta$ is
handled linearly (no implicit contraction or weakening) while the exponential
context $\Gamma$ is unrestricted. The type system exactly corresponds, via a
propositions-as-types correspondence, to the canonical proof system of
Classical Linear Logic with Mix. When a cut type annotation is easily
inferred, we may omit it and write
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}$. The typing rules of $\mathsf{CLL}{}$ are given in Fig. 1.

The process
${{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$
denotes the inactive process, typed in the empty linear context (rule
[T${{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$]).
$P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
Q$ denotes independent parallel composition of processes $P$ and $Q$ (rule
[Tmix]), whereas
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{:}A{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}$ denotes interfering parallel composition of $P$ and $Q$, where $P$ and
$Q$ share exactly one channel name $x$, typed as $A$ in $P$ and $\overline{A}$
in $Q$ (rule [Tcut]). The construct
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y$ captures forwarding between dually typed names $x$ and $y$ (rule
[Tfwd]), which operationally consists in (globally) renaming $x$ for $y$.

Processes
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x$ and
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
x;P$ denote session termination and the dual action of waiting for session
termination, respectively (rules [T${\mathbf{1}}$] and [T$\bot$]). The
constructs
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{case}}\
x\ \\{|{\\#\mathsf{\ell}\in L}{:}P_{\ell}\\}$ and $\\#\mathsf{l}\ x;P$ denote
label input and output, respectively, where the input construct pattern
matches on the received label to select the process continuation that is to
run. Process
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(y.P_{1});P_{2}$ and
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
x(z);Q$ codify the output of (fresh) name $y$ on channel $x$ and the
corresponding input action, where the received name will be substituted for
$z$ in $Q$ (rules [T$\otimes$] and [T$\mathbin{\bindnasrepma}$]). Typing
ensures that the names used in $P_{1}$ and $P_{2}$ are disjoint.

Processes
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(y);P$,
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{?}}x;Q$
and
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{call}}\
x(z);Q$ embody replicated servers and client processes. Process
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(y);P$
consists of a process that waits for inputs on $x$, spawning a replica of $P$
(depending on no linear sessions – rule [T$!$]). Process
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{?}}x;Q$
and
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{call}}\
x(z);Q$ allow for replicated servers to be activated and subsequently used as
(fresh) linear sessions (rules [T$?$] and [Tcall]). Composition of
exponentials is achieved by the
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x:A{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}$ process, where $P$ cannot depend on linear sessions and so may be safely
replicated.

$\begin{array}[]{c}\prooftree\infer[norule]0{{}}\infer
1[\text{[T${{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$]}]{{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\vdash\emptyset;\Gamma}\quad\prooftree\infer[norule]0{{}}\infer[norule]1{P\vdash\Delta^{\prime};\Gamma\quad
Q\vdash\Delta;\Gamma}\infer 1[\text{[Tmix]}]{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
Q \vdash\Delta^{\prime},\Delta;\Gamma}\\\ \prooftree\infer[norule]0{{}}\infer
1[\text{[Tfwd]}]{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y \vdash
x:\overline{A},y:A;\Gamma}\quad\prooftree\infer[norule]0{{}}\infer[norule]1{P\vdash\Delta^{\prime},x:A;\Gamma\quad
Q\vdash\Delta,x:\overline{A};\Gamma}\infer
1{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x:A{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\} \vdash\Delta^{\prime},\Delta;\Gamma} \text{[Tcut]}\vspace{4pt}\\\
\prooftree\infer[norule]0{\;}\infer
1[\text{[T${\mathbf{1}}$]}]{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x\vdash
x:{\mathbf{1}};\Gamma}\quad\prooftree\infer[norule]0{Q\vdash\Delta;\Gamma}\infer
1[\text{[T$\bot$]}]{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
x;Q \vdash\Delta,x:\bot;\Gamma\vspace{4pt}}\\\
\prooftree\infer[norule]0{P_{\ell}\vdash\Delta,x:A_{\ell};\Gamma\quad(\mathit{all}\
\ell\in L)}\infer
1[\text{[T$\mathbin{\binampersand}$]}]{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{case}}\
x\ \\{|{\\#\mathsf{\ell}\in L}{:}P_{\ell}\\}
\vdash\Delta,x:\mathbin{\binampersand}_{\ell\in L}{A_{\ell}};\Gamma}
\quad\prooftree\infer[norule]0{Q\vdash\Delta^{\prime},x:A_{\\#\mathsf{l}};\Gamma\quad\\#\mathsf{l}\in
L} \infer 1[\text{[T$\oplus$]}]{\\#\mathsf{l}\ x;Q
\vdash\Delta^{\prime},x:\oplus_{\ell\in L}{A_{\ell}};\Gamma\vspace{4pt}}\\\
\prooftree\infer[norule]0{P_{1}\vdash\Delta_{1},y:A;\Gamma\quad
P_{2}\vdash\Delta_{2},x:B;\Gamma}\infer
1[\text{[T$\otimes$]}]{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(y.P_{1});P_{2} \vdash\Delta_{1},\Delta_{2},x:A\otimes
B;\Gamma\vspace{4pt}}\\\
\prooftree\infer[norule]0{Q\vdash\Delta,z:A,x:B;\Gamma} \infer
1[\text{[T$\mathbin{\bindnasrepma}$]}]{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
x(z);Q\vdash\Delta,x:A\mathbin{\bindnasrepma}B;\Gamma\vspace{4pt}}\\\
\prooftree\infer[norule]0{P\vdash y:A;\Gamma} \infer
1[\text{[T!]}]{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(y);P
\vdash x:!A;\Gamma}\quad\prooftree\infer[norule]0{Q\vdash\Delta;\Gamma,x:A}
\infer
1[\text{[T?]}]{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{?}}x;Q
\vdash\Delta,x:?A;\Gamma\vspace{4pt}}\\\
\prooftree\infer[norule]0{{}}\infer[norule]1{P\vdash y:A;\Gamma\quad
Q\vdash\Delta;\Gamma,x:\overline{A}} \infer
1[\text{[Tcut!]}]{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x:A{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\} \vdash\Delta;\Gamma}
\quad\prooftree\infer[norule]0{Q\vdash\Delta,z:A;\Gamma,x:A}\infer
1[\text{[Tcall]}]{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{call}}\
x(z);Q \vdash\Delta;\Gamma,x:A}\end{array}$ Figure 1: Typing Rules of
$\mathsf{CLL}$.

We call action any process that is either a forwarder or realizes an
introduction rule, and denote by $\mathcal{A}$ the set of all actions, by
$\mathcal{A}(x)$ the set of action with subject $x$ (the subject of an action
is the channel name in which it interacts [48]). An action is deemed
_positive_ (resp. _negative_) if its associated type is positive (resp.
negative) in the sense of _focusing_. The set of positive (resp. negative)
actions is denoted by $\mathcal{A}^{+}$ (resp. $\mathcal{A}^{-}$). We
sometimes use, e.g., $\mathcal{A}$ or $\mathcal{A}^{+}(x)$ to denote a process
in the set. The $\mathsf{CLL}$ operational semantics is given by a _structural
congruence_ relation $\equiv$ that captures static identities on processes,
corresponding to commuting conversions in the logic, and a _reduction_
relation $\to$ that captures process interaction, and corresponds to cut-
elimination steps.

$\begin{array}[]{ll}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y
\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
y\ x&\text{[fwd]}\vspace{6pt}\\\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x:A{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}
\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x:\overline{A}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P\\}&\text{[com]}\vspace{6pt}\\\ P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}
\equiv P\quad P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
Q\equiv Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
P\quad P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
(Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
R)\equiv(P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
Q)\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
R&\text{[par]}\vspace{6pt}\\\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
(Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
R)\\}\equiv({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\})\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
R&\text{[CM]}\vspace{6pt}\\\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\})\\}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\})\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}&\text{[CC]}\vspace{6pt}\\\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}z{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\})\\}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}z{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\})\\}&\text{[CC!]}\vspace{6pt}\\\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
(P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
R)\\}\equiv P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\})&\text{[C!M]}\vspace{6pt}\\\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{w.Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!z{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\})\\}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{w.Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!z{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\})\\}&\text{[C!C!]}\vspace{6pt}\\\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
(Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}*{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R)\\}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}*{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}&\text{[C!*]}\vspace{8pt}\\\ a(x);Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}*{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R \equiv a(x);{(Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}*{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R)}&\text{[C$+$*]}\vspace{6pt}\\\ a_{1}(x);a_{2}(y);P \equiv
a_{2}(y);a_{1}(x);P&\text{[C$i$]}\end{array}$

Provisos: in [CM] $x\in\mathsf{fn}(Q)$; in [CC] $x,y\in\mathsf{fn}(Q)$; in
[CC!], [C!M] $x\notin\mathsf{fn}(P)$; in [C!C!], $x\notin\mathsf{fn}(Q)$ and
$z\notin\mathsf{fn}(P)$. In [C$i$], $x\neq y$ and $bn(a_{1}(x))\cap
bn(a_{2}(y))=\emptyset$

Figure 2:  Structural congruence $P\equiv Q$.

######  Definition 3 ($P\equiv Q$)

Structural congruence $\equiv$ is the least congruence on processes closed
under $\alpha$-conversion and the $\equiv$-rules in Fig. 2.

The definition of $\equiv$ reflects expected static laws, along the lines of
the structural congruences / conversions in [13, 70]. The binary operators
forwarder, cut, and mix are commutative. The set of processes modulo $\equiv$
is a commutative monoid with operation the parallel composition $(-\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
-)$ and identity given by inaction
${{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$
([par]). Any static constructs commute, as expressed by the laws [CM]-[C!sC!].
The unrestricted cut distributes over all the static constructs by law [C*],
where $-\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}*{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
-$ stands for either a mix, linear or unrestricted cut. The laws [C$+*$] and
[C$+$] denote sound proof equivalences in linear logic and bring explicit the
independence of linear actions (noted $a(x)$), in different sessions $x$ [52].
These conversions are not required to obtain deadlock freedom. However, they
are necessary for full cut elimination (e.g., see [70]), and expose more
redexes, thus more non-determinism in the choice of possible reductions.
Perhaps surprisingly, this extra flexibility is important to allow the
deterministic sequential evaluation strategy for $\mathsf{CLL}$ programs
adopted by the SAM to be expressed.

######  Definition 4 (Reduction $\to$)

Reduction $\to$ is defined by the rules of Fig. 3.

We denote by $\Rightarrow$ the reflexive-transitive closure of $\to$.
Reduction includes the set of principal cut conversions, i.e. the redexes for
each pair of interacting constructs. It is closed by structural congruence
([$\equiv$]), in rule [cong] we consider that $\mathcal{C}$ is a static
context, i.e. a process context in which the single hole is covered only by
the static constructs mix or cut. The forwarding behaviour is implemented by
name substitution [fwd] [14]. All the other reductions act on a principal cut
between two dual actions, and eliminate it on behalf of cuts involving their
subprocesses.

$\begin{array}[]{ll}{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P\\}\to\\{x/y\\}P&\text{[fwd]}\vspace{6pt}\\\
{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
x;P\\}\to P&\text{[${\mathbf{1}}\bot$]}\vspace{6pt}\\\
{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(y.P);Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
x(z);R\\}\to Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
(P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
\\{y/z\\}R)&\text{[$\otimes\mathbin{\bindnasrepma}$]}\vspace{6pt}\\\
{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{case}}\
x\ \\{|{\\#\mathsf{\ell}\in L}{:}P_{\\#\mathsf{\ell}}\\}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
\\#\mathsf{l}\
{x};{R}\\}\to{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P_{\\#\mathsf{l}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}&\text{[$\mathbin{\binampersand}\oplus_{l}$]}\vspace{8pt}\\\
{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(y);P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{?}}x;Q\\}\to{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}&\text{[!?]}\vspace{6pt}\\\
{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{call}}\
x(z);Q\\}\to{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{\\{z/y\\}P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}z{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\})\\}&\text{[call]}\end{array}\vspace{-10pt}$ Figure 3:  Reduction $P\to
Q$.

$\mathsf{CLL}$ satisfies basic safety properties [13] listed below, and also
confluence, and termination [59, 60]. In particular we have:

######  Theorem 2.1 (Type Preservation)

Let $P\vdash\Delta;\Gamma$. (1) If $P\equiv Q$, then $Q\vdash\Delta;\Gamma$.
(2) If $P\to Q$, then $Q\vdash\Delta;\Gamma$.

A process $P$ is _live_ if and only if $P=\mathcal{C}[Q]$, for some static
context $\mathcal{C}$ (the hole lies within the scope of static constructs mix
and cut) and $Q$ is an active process (a process with a topmost action
prefix).

######  Theorem 2.2 (Progress)

Let $P\vdash\emptyset;\emptyset$ be live. Then $P\to Q$ for some $Q$.

##  3 A Core Session Abstract Machine

In this section we develop the key insights that guide the construction of our
session abstract machine (SAM) and introduce its operational rules in an
incremental fashion. We omit the linear logic exponentials for the sake of
clarity of presentation, postponing their discussion for Section 6.

One of the main observations that drives the design of the SAM is the nature
of proof dynamics in (classical) linear logic, and thus of process execution
dynamics in the $\mathsf{CLL}$ system of Section 2. The proof dynamics of
linear logic are derived from the computational content of the cut elimination
proof, which defines a proof simplification strategy that removes (all)
instances of the cut rule from a proof. However, the strategy induced by cut
elimination is _non-deterministic_ insofar as multiple simplification steps
may apply to a given proof. Transposing this observation to $\mathsf{CLL}$ and
other related systems, we observe that their operational semantics is does not
prescribe a rigid evaluation order for processes. For instance, in the process
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}$, reduction is allowed in both $P$ and $Q$. This is of course in line
with reduction in process calculi (e.g., [48]). However, in logical-based
systems this amounts to _don’t care_ non-determinism since, regardless of the
evaluation order, confluence ensures that the same outcomes are produced (in
opposition to _don’t know_ non-determinism which breaks confluence and is thus
disallowed in purely logical systems). The design of the SAM arises from
attempting to fix a purely sequential reduction strategy for $\mathsf{CLL}$
processes, such that only _one_ process is allowed to execute at any given
point in time, in the style of coroutines. To construct such a strategy, we
forego the use of purely synchronous communication channels, which require a
handshake between two concurrently executing processes, and so consider
session channels as a kind of _buffered_ communication medium (this idea has
been explored in the context of linear logic interpretations of sessions in
[24]), or queue, where one process can asynchronously write messages so that
another may, subsequently, read. To ensure the correct directionality of
communication, the queue has a write endpoint (on which a process may only
write) and a read endpoint (along which only reads may be performed), such
that at any given point in time a process can only hold one of two endpoints
of a queue. Moreover, our design takes inspiration from insights related to
polarisation and focusing in linear logic, grouping communication in sequences
of positive (i.e. write) actions.

$\begin{array}[]{llll}S&::=&(P,H)&\mbox{State}\vspace{4pt}\\\
H&::=&\mathit{SessionRef}\to\mathit{SessionRec}&\mbox{Heap}\vspace{4pt}\\\
\mathit{R}&::=&x\\!\left<q,P\right>\\!y&\mbox{Session Record}\vspace{4pt}\\\
\mathit{q}&::=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}\;|\;\mathit{Val}@q&\mbox{Queue}\vspace{4pt}\\\
\mathit{Val}&::=&\checkmark&\mbox{Close token}\\\
&|&\\#\mathsf{l}&\mbox{Choice label}\\\ &|&\mathsf{clos}(x,P)&\mbox{Process
Closure}\end{array}$ Figure 4: core SAM Components

Allowing session channels to buffer message sequences, we may then model
process execution by alternating between writer processes (that inject
messages into the respective queues) and corresponding reader processes. Thus,
the SAM must maintain a _heap_ that tracks the queue contents of each session
(and its endpoints), as well as the suspended processes. The construction of
the core of the SAM is given in Figure 4. An execution state is simply a pair
consisting of _the_ running process $P$ and the heap $H$. For technical
reasons that are made clear in Sections 4 and 5, the process language used in
the SAM differs superficially from that of $\mathsf{CLL}$, but for the
purposes of this overview we will use $\mathsf{CLL}$ process syntax. Later we
show the two languages are equivalent in a strong sense.

A heap is a mapping between session identifiers and _session records_ of the
form $x\\!\left<q,Q\right>\\!y$, denoting a session with write endpoint $x$
and read endpoint $y$, with queue contents $q$ and a suspended process $Q$,
holding one of the two endpoints. If $Q$ holds the read endpoint then it is
suspended waiting for the process holding the write endpoint to fill the queue
with data for it to read. If $Q$ holds the write endpoint, then $Q$ has been
suspended _after_ filling the queue and is now waiting for the reader process
on $y$ to empty the queue.

We adopt the convention of placing the write endpoint on the left and the read
endpoint on the right. In general, session records in the SAM support a form
of coroutines through their contained processes, which are called on and
returned from multiple times over the course of the execution of the machine.
A queue can either be empty
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$)
or holding a sequence of values. A value is either a close session token
($\checkmark$), identifying the last output on a session; a choice label
$\\#\mathsf{l}$ or a process closure $\mathsf{clos}(x,P)$, used to model
session send and receive. We overload the $@$ notation to also denote
concatenation of queues.

Cut. We begin by considering how to execute a cut of the form
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x:A^{+}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}$ where $x$ is a positive type (in the sense of polarized logic [29]) in
$P$. A positive type corresponds to a type denoting an _output_ (or write)
action, whereas a negative type denotes an _input_ (or read) action. We
maintain the invariant that in such a cut, $P$ holds the write endpoint and
$Q$ the read endpoint. This means that the next action performed by $P$ on the
session will be to push some value onto the queue and, dually, the next action
performed by $Q$ on the session will be to read a value from the queue. In
general, the holder of the write and read endpoint can change throughout
execution.

Given the choice of either scheduling $P$ or $Q$, we are effectively _forced_
to schedule $P$ _before_ $Q$. Given that the cut introduces the (unique)
session that is shared between the two processes, the only way for $Q$ to
exercise its read capability on the session successfully is to wait for $P$ to
have exercised (at least some of) its write capability. If we were to schedule
$Q$ before $P$, the process might attempt to read a value from an empty queue,
resulting in a stuck state of the SAM. Thus, the SAM execution rule for cut
is:

$({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x:A^{+}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\},H)\Mapsto(P,H[x\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},\\{y/x\\}Q\right>\\!y])\qquad\text{\rm[SCut]}$

The rule states that $P$ is the process that is to be scheduled, adding the
session record
$x\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},Q\right>\\!y$
to the heap, which effectively suspends the execution of $Q$ until $P$ has
exercised some of its write capabilities on the new session. Note that, in
general, both $P$ and $Q$ can interact along many different sessions as both
readers and writers before exercising any action on $x$ (resp. $y$). However,
they alone hold the freshly created endpoints $x$ and $y$ and so the next
value sent along the session must come from $P$ and $Q$ is its intended
receiver.

Channel Output. To execute an output of the form
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(z.R);Q$ in the SAM we simply lookup the session record for $x$ and add to
the queue a _process closure_ containing $R$ (which interacts along $z$),
continuing with the execution of $Q$:

$({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(z.R);Q,H[x\\!\left<q,P\right>\\!y])\Mapsto(Q,H[x\\!\left<q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,R),P\right>\\!y])\qquad\text{\rm[S$\otimes$]}$

Note that the SAM _eagerly_ continues to execute $Q$ instead of switching to
$P$, the holder of the read endpoint of the queue. This allows for the running
process to perform all available writes before a context switch occurs.

Session Closure. Executing a
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
\\!\\!$ follows a similar spirit, but no continuation process exists and so
execution switches to the process $P$ holding the _read_ endpoint $y$ of the
queue:

$({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x,H[x\\!\left<q,P\right>\\!y])\Mapsto(P,H[x\\!\left<q@{\checkmark},{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!y])\qquad\text{\rm[S${\mathbf{1}}$]}$

The process $P$ will eventually read the termination mark from the queue
(triggering the deallocation of the session record from the heap):

$({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
y;P,H[x\\!\left<{\checkmark},{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!y])\Mapsto(P,H)\qquad\text{\rm[S$\bot$]}$

Note the requirement that $\checkmark$ be the final element of the queue.

Negative Action on Write Endpoint. As hinted above for the case of executing a
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}$,
the SAM has a kind of _write bias_ insofar as the process chosen to execute in
a cut is that which holds the write endpoint for the newly created session.
Since $\mathsf{CLL}$ processes use channels bidirectionally, the role of
writer and reader on a channel (and thus the holder of the write and read
endpoints of the queue) may be exchanged during execution. For instance, a
process $P$ may wish to send a value $v$ to $Q$ and then receive a response on
the same channel. However, when considering a queue-based semantics, the
execution of the input action _must not_ obtain the value $v$, intended for
$Q$. Care is therefore needed to ensure that $v$ is received by the holder of
the read endpoint of the queue _before_ $P$ is allowed to execute its input
action (and so taking over the read endpoint). This notion is captured by the
following rule, where $\mathcal{A}^{-}$ denotes any process performing a
negative polarity action (i.e., a
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}$,
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}$,
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{case}}$
or, as we discuss later, a
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y$ when $x$ is a write endpoint with a negative polarity type):

$(\mathcal{A}^{-}(x),H[x\\!\left<{q},Q\right>\\!y])\Mapsto(Q,H[x\\!\left<{q},\mathcal{A}^{-}(x)\right>\\!y])\qquad\text{\rm[S$-$]}$

If the executing process is to perform a negative polarity action on a write
endpoint $x$, the SAM context switches to $Q$, the holder of the read endpoint
$y$ of the session, and suspends the previously running process. This will now
allow for $Q$ to perform the appropriate inputs before execution of the action
$\mathcal{A}^{-}$ resumes.

Channel Input. The rules for
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}$
actions are as follows:

$\begin{array}[]{l}({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w{:}+);Q,H[x\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,R)@q,P\right>\\!y])\Mapsto(Q,H[w\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},R\right>\\!z][x\\!\left<q\right>^{s}\\!y])\;\;\text{\rm[S$\mathbin{\bindnasrepma}_{+}$]}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w{:}-);Q,H[x\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,R)@q,P\right>\\!y])\Mapsto(R,H[z\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},Q\right>\\!w][x\\!\left<q\right>^{s}\\!y])\;\;\text{\rm[S$\mathbin{\bindnasrepma}_{-}$]}\end{array}$

where $x\\!\left<q\right>^{s}\\!y\triangleq\mbox{if
}(q={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}})\mbox{
then }y\\!\left<q,P\right>\\!x\mbox{ else }x\\!\left<q,P\right>\\!y$. The
execution of an input action requires the corresponding queue to contain a
process closure, denoting the process that interacts along the received
channel $w$. In order to ensure that no inputs attempt to read from an empty
queue, we must _branch_ on the polarity of the communicated session (written
$w{:}+$ and $w{:}-$ in the rules above): if the session has a _positive_ type,
then $Q$ must take the _write_ endpoint $w$ of the newly generated queue
(since $Q$ uses the session with a dual type) and thus we execute $Q$ and
allocate a session record in the heap for the new session, with read endpoint
$z$; if the exchanged session has a _negative_ type, the converse holds and
$Q$ must take the _read_ endpoint of the newly generated queue. In this
scenario, we must execute $R$ so that it may exercise its write capability on
the queue and suspend $Q$ in the new session record.

In either case, the session record for the original session is updated by
removing the received message from the queue. Crucially, since processes are
well-typed, if the resulting queue is empty then it must be the case that $Q$
has no more reads to perform on the session, and so we _swap_ the read and
write endpoints of the session. This swap serves two purposes: first, it
enables $Q$ to perform writes if needed; secondly, and more subtly, it allows
for the process, say, $P$, that holds the other endpoint of the queue to be
resumed to perform its actions accordingly. To see how this is the case,
consider that such a process will be suspended (due to rule [S$-$]) attempting
to perform a negative action on the write endpoint of the queue. After the
swap, the endpoint of the suspended process now matches its intended action.
Since $Q$ now holds the write endpoint, it will perform some number of
positive actions on the session which end either in a
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}$,
which context switches to $P$, or until it attempts to perform a negative
action on the write endpoint, triggering rule [S$-$] and so context switching
to $P$.

Choice and Selection. The treatment of the additive constructs in the SAM is
straightforward:

$\begin{array}[]{ll}(\\#\mathsf{l}\;x;Q,H[x\\!\left<q,P\right>\\!y])\Mapsto(Q,H[x\\!\left<q@\\#\mathsf{l},P\right>\\!y])&\quad\text{\rm[S$\oplus$]}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{case}}\
y\ \\{|{\\#\mathsf{\ell}\in
L}{:}Q_{\ell}\\},H[x\\!\left<\\#\mathsf{l}@q,P\right>\\!y])\Mapsto(Q_{\\#\mathsf{l}},H[x\\!\left<q\right>^{s}\\!y])&\quad\text{\rm[S$\mathbin{\binampersand}$]}\end{array}$

Sending a label $\\#\mathsf{l}$ simply adds the $\\#\mathsf{l}$ to the
corresponding queue and proceeds with the execution, whereas executing a
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{case}}$
reads a label from the queue and continues execution of the appropriate
branch. Since removing the label may empty the queue, we perform the same
adjustment as in rules [S$\mathbin{\bindnasrepma}_{+}$] and
[S$\mathbin{\bindnasrepma}_{-}$].

Forwarding. Finally, let us consider the execution of a forwarder (we overload
the $@$ notation to also denote concatenation of queues):

$({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x^{-}\
y^{+},H[z\\!\left<q_{1},Q\right>\\!x][y\\!\left<q_{2},P\right>\\!w])\Mapsto(P,H[z\\!\left<q_{2}@{q_{1}},Q\right>\\!w])\qquad\text{\rm[Sfwd]}$

A forwarder denotes the merging of two sessions $x$ and $y$. Since the
forwarder holds the read and write endpoints $x$ and $y$, respectively, $Q$
has written (through $z$) the contents of $q_{1}$, whereas the previous steps
of the currently running process have written $q_{2}$. Thus, $P$ is waiting to
read $q_{2}@q_{1}$, justifying the rule above.

The reader may then wonder about other possible configurations of the SAM heap
and how they interact with the forwarder. Specifically, what happens if $y$ is
of a positive type but a read endpoint of a queue, or, dually, if $x$ is of a
negative type but a write endpoint. The former case is _ruled out_ by the SAM
since the heap satisfies the invariant that any session record of the form
$x{:}A\\!\left<q,P\right>\\!y{:}A\in H$ is such that $A$ must be of negative
polarity or $P$ is the inert process (which cannot be forwarded). The latter
case is possible and is handled by rule [S$-$], since such a forward
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x^{-}\ y^{+}$ stands for a process that wants to perform a _negative polarity_
action on a _write_ endpoint (or a positive action on a read endpoint).

###  3.1 On the Write-Bias of the SAM

Consider the following $\mathsf{CLL}$ process:

$P\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P_{1}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}a:{\mathbf{1}}\otimes{\mathbf{1}}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
\\{a/b\\}Q_{1}\\}$

$\begin{array}[]{ll}P_{1}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
a(y.P_{2});P_{3}&\qquad
Q_{1}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
b(x);Q_{2}\\\
P_{2}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
y&\qquad
Q_{2}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
x;Q_{3}\\\
P_{3}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
a&\qquad
Q_{3}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
b;{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\\\\[10.00002pt]
\end{array}$

Let us walk through the execution trace of $P$:

(1) $(P,\emptyset)\Mapsto$ by [SCut]
---
(2)
$(P_{1},a\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},Q_{1}\right>\\!b)\Mapsto$
by [S$\otimes$]
(3)
$(P_{3},a\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(y,P_{2}),Q_{1}\right>\\!b)\Mapsto$
by [S${\mathbf{1}}$]
(4)
$(Q_{1},a\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(y,P_{2})@\checkmark,{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!b)\Mapsto$
by [S$\mathbin{\bindnasrepma}_{-}$]
(5)
$(P_{2},y\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},Q_{2}\right>\\!x,a\\!\left<\checkmark,{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!b)\Mapsto$
by [S${\mathbf{1}}$]
(6)
$(Q_{2},y\\!\left<\checkmark,{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!x,a\\!\left<\checkmark,{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!b)\Mapsto$
by [S$\bot$]
(7)
$(Q_{3},a\\!\left<\checkmark,{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!b)\Mapsto$
by [S$\bot$]
(8)
$({{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}},\emptyset)$

The SAM begins in the state on line (1) above, executing the cut. Since the
type of $a$ is positive, we execute $P_{1}$, and allocate the session record,
suspending $Q_{1}$, resulting in the state on line (2). Since $P_{1}$ is a
write action on a write endpoint, we proceed via the [S$\otimes$] rule,
resulting in the SAM configuration in line (3), executing $P_{3}$ and adding a
closure containing $P_{2}$ to the session queue with write endpoint $a$.
Executing $P_{3}$ (3), a
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}$
action, requires adding the $\checkmark$ to the queue and context switching to
the process $Q_{1}$, now ready to receive the sent value. The applicable rule
is now (4) [S$\mathbin{\bindnasrepma}_{-}$], and so execution will context
switch to $P_{2}$ after creating the session record for the new session with
endpoints $y$ and $x$. $P_{2}$ will execute and the machine ends up in state
(6) followed by (7), which consume the appropriate $\checkmark$ and deallocate
the session records.

Note how after executing the send action of $P_{1}$ we eagerly execute the
positive action in $P_{3}$ rather than context switching to $Q_{1}$. While in
this particular process it would have been safe to execute the negative action
in $Q_{1}$, switch to $P_{2}$ and then back to $Q_{2}$, we would now need to
somehow context switch to $P_{3}$ _before_ continuing with the execution of
$Q_{3}$, or execution would be stuck. However, the relationship between
$P_{3}$ and $Q_{2}$ is unclear at best. Moreover, if the continuation of
$Q_{1}$ were of the form
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
b;{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
x;{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$,
the context switch after the execution of $P_{2}$ would have to execute
$P_{3}$, or the machine would also be in a stuck state.

###  3.2 Illustrating Forwarding

To better illustrate the way in which
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x^{-}\ y^{+}$ effectively stands for a negative action, consider the following
$\mathsf{CLL}$ process (to simplify the execution trace we assume the
existence of output and input of integers typed as $\mathsf{int}\otimes A$ and
$\overline{\mathsf{int}}\mathbin{\bindnasrepma}A$, respectively, eliding the
need for process closures in this example):

$P\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P_{1}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}b:\overline{\mathsf{int}}\mathbin{\bindnasrepma}\overline{\mathsf{int}}\mathbin{\bindnasrepma}{\mathbf{1}}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
\\{b/c\\}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q_{1}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}a:{\mathsf{int}}\otimes\overline{\mathsf{int}}\mathbin{\bindnasrepma}{\mathbf{1}}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
\\{a/d\\}R_{1}\\}\\}$
$\begin{array}[]{lll}P_{1}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
b(x);P_{2}&\qquad
Q_{1}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\,a(1);{Q_{2}}&\qquad
R_{1}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
d(y);R_{2}\\\
P_{2}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
b(z);P_{3}&\qquad
Q_{2}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\,c(3);{Q_{3}}&\qquad
R_{2}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\,d(2);{R_{3}}\\\
P_{3}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
b&\qquad
Q_{3}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
a\ c&\qquad
R_{3}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
d;{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\\\\[9.00002pt]
\end{array}$

If we consider the execution of $P$ we observe:

(1) $(P,\emptyset)\Mapsto$ by [SCut]
---
(2)
$({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q_{1}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}a{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
\\{a/d\\}R_{1}\\},c\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},P_{1}\right>\\!b)\Mapsto$
by [SCut]
(3)
$(Q_{1},a\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},R_{1}\right>\\!d,c\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},P_{1}\right>\\!b)\Mapsto$
by [S$\otimes$]
(4)
$(Q_{2},a\\!\left<1,R_{1}\right>\\!d,c\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},P_{1}\right>\\!b)\Mapsto$
by [S$\otimes$]
(5)
$({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
a\ c,a\\!\left<1,R_{1}\right>\\!d,c\\!\left<3,P_{1}\right>\\!b)\Mapsto$ by
[S$-$]
(6) $(R_{1},a\\!\left<1,Q_{3}\right>\\!d,c\\!\left<3,P_{1}\right>\\!b)\Mapsto$
by [S$\mathbin{\bindnasrepma}$]
(7)
$(R_{2},d\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},Q_{3}\right>\\!a,c\\!\left<3,P_{1}\right>\\!b)\Mapsto$
by [S$\otimes$]
(8) $(R_{3},d\\!\left<2,Q_{3}\right>\\!a,c\\!\left<3,P_{1}\right>\\!b)\Mapsto$
by [S$-$]
(9)
$({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
a\ c,d\\!\left<2,R_{3}\right>\\!a,c\\!\left<3,P_{1}\right>\\!b)\Mapsto$ by
[Sfwd]
(10) $(P_{1},d\\!\left<3@2,R_{3}\right>\\!b)\Mapsto$ by
[S$\mathbin{\bindnasrepma}$]
(11) $(P_{2},b\\!\left<2,R_{3}\right>\\!d)\Mapsto$ by
[S$\mathbin{\bindnasrepma}$]
(12)
$(P_{3},b\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},R_{3}\right>\\!d)\Mapsto$
by [S${\mathbf{1}}$]
(13) $(R_{3},b\\!\left<\checkmark,R_{3}\right>\\!d)\Mapsto$ by [S$\bot$]
(14)
$({{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}},\emptyset)$

The first four steps of the execution of $P$ allocate the two session records
and the writes by $Q_{1}$ and $Q_{2}$ takes place. We are now in configuration
(5), where
$Q_{3}={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
a^{-}\ c^{+}$ is to execute and $a$ is a write endpoint of a queue assigned a
negative type ($\overline{\mathsf{int}}\mathbin{\bindnasrepma}{\mathbf{1}}$).
This forwarder stands for a process performing a negative action on a write
endpoint (i.e., $P_{1}$) and so context switching is required, rule [S$-$]
applies and the SAM context switches to $R_{1}$, suspending $Q_{3}$ until the
forward can be performed. After $R_{1}$ receives (6) and the queue endpoints
$a$ and $d$ are swapped (7), $R_{2}$ executes and then rule [S$-$] applies
(8), context switching back to $Q_{3}$. Since the queue endpoints are now
flipped, rule [Sfwd] now applies (9), collapsing the two session records (via
queue concatenation) and proceeding with the execution of $P_{1}$, $P_{2}$,
$P_{3}$ and $R_{3}$ (10-14). Note the correct ordering in which the sent
values are dequeued, where $3$ is read before $2$, as intended.

Discussion. The core execution rules for the SAM are summarized in Figure 5.
At this point, the reader may wonder just how reasonable the SAM’s evaluation
strategy is. Our evaluation strategy is devised to be a deterministic,
sequential strategy, where exactly one process is executing at any given point
in time, supported by a queue-based buffer structure for channels and a heap
for session records. Moreover, taking inspiration from focusing and polarized
logic, we adopt a write-biased stance and prioritize (bundles of) write
actions over reads, where suspended processes hold the read endpoint of queues
while waiting for the writer process to fill the queue, and hold write
endpoints of queues _after_ filling them, waiting for the reader process to
empty the queue.

While this latter point seems like a reasonable way to ensure that inputs
never get stuck, it is not immediately obvious that the strategy is sound wrt
the more standard (asynchronous) semantics of $\mathsf{CLL}$ and related
languages, given that processes are free to act on multiple sessions. Thus,
the write-bias of the cut rule (and the overall SAM) does not necessarily mean
that the process that is chosen to execute will immediately perform a write
action on the freshly cut session $x$. In general, such a process may perform
multiple write or read actions on many other sessions before performing the
write on $x$, meaning that multiple context switches may occur. Given this, it
is not obvious that this strategy is adequate insofar as preserving the
correctness properties of $\mathsf{CLL}$ in terms of soundness, progress and
type preservation. The remainder of this paper is devoted to establishing this
correspondence in a precise technical sense.

$\begin{array}[]{lll}({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x:A^{+}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\},H)\Mapsto(P,H[x\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},\\{y/x\\}Q\right>\\!y])&\text{\rm[SCut]}\vspace{6pt}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\
y,H[z\\!\left<q_{1},Q\right>\\!x][y\\!\left<q_{2},P\right>\\!w])\Mapsto(P,H[z\\!\left<q_{2}@{q_{1}},Q\right>\\!w])&\text{\rm[Sfwd]}\vspace{6pt}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x,H[x\\!\left<q,P\right>\\!y])\Mapsto(P,H[x\\!\left<q@{\checkmark},{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!y])&\text{\rm[S${\mathbf{1}}$]}\vspace{6pt}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
y;P,H[x\\!\left<{\checkmark},{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!y])\Mapsto(P,H)&\text{\rm[S$\bot$]}\vspace{6pt}\\\
(\mathcal{A}^{-}(x),H[x\\!\left<{q},Q\right>\\!y])\Mapsto(Q,H[x\\!\left<{q},\mathcal{A}^{-}(x)\right>\\!y])&\text{\rm[S$-$]}\vspace{6pt}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(z.R);Q,H[x\\!\left<q,P\right>\\!y])\Mapsto(Q,H[x\\!\left<q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,R),P\right>\\!y])&\text{\rm[S$\otimes$]}\vspace{6pt}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w:+);Q,H[x\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,R)@q,P\right>\\!y])\Mapsto(Q,H[w\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},R\right>\\!z][x\\!\left<q\right>^{s}\\!y])&\text{\rm[S$\mathbin{\bindnasrepma}$]}\vspace{6pt}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w:-);Q,H[x\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,R)@q,P\right>\\!y])\Mapsto(R,H[z\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},Q\right>\\!w][x\\!\left<q\right>^{s}\\!y])&\text{\rm[S$\mathbin{\bindnasrepma}$]}\vspace{6pt}\\\
(\\#\mathsf{l}\;x;Q,H[x\\!\left<q,P\right>\\!y])\Mapsto(Q,H[x\\!\left<q@\\#\mathsf{l},P\right>\\!y])&\text{\rm[S$\oplus$]}\vspace{6pt}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{case}}\
y\ \\{|{\\#\mathsf{\ell}\in
L}{:}Q_{\ell}\\},H[x\\!\left<\\#\mathsf{l}@q,P\right>\\!y])\Mapsto(Q_{\\#\mathsf{l}},H[x\\!\left<q\right>^{s}\\!y])&\text{\rm[S$\mathbin{\binampersand}$]}\vspace{6pt}\\\
N.B.:x\\!\left<q\right>^{s}\\!y\triangleq\mbox{if
}(q={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}})\mbox{
then }y\\!\left<q,P\right>\\!x\mbox{ else
}x\\!\left<q,P\right>\\!y\end{array}$ Figure 5: The core SAM Transition Rules

##  4  $\mathsf{CLLB}$: A Buffered Formulation of $\mathsf{CLL}$

There is a substantial gap between the language $\mathsf{CLL}$, presented in
an abstract algebraic style, and its operational semantics, defined by
equational and rewriting systems, and an abstract machine as the SAM, a
deterministic state machine manipulating several low level structures.
Therefore, even if the core SAM structure and transition rules are fairly
simple, proving its correctness is more challenging and technically involved,
and require progressive build up. Therefore, we first bridge between
$\mathsf{CLL}$ and SAM via a intermediate logical language $\mathsf{CLLB}$,
which extends $\mathsf{CLL}$ with a buffered cut construct.

$\begin{array}[]{c}\prooftree\infer[norule]0{{}}\infer[norule]1{P\vdash^{\mathsf{B}}\Delta^{\prime},x:\overline{A};\Gamma\quad
Q\vdash^{\mathsf{B}}\Delta,y:A;\Gamma}\infer
1{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x:\overline{A}\;[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}]\;\overline{y}:A{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\} \vdash^{\mathsf{B}}\Delta^{\prime},\Delta;\Gamma} \quad\mbox{(A
positive)}\quad \text{[TcutB] }\vspace{6pt}\\\
\prooftree\infer[norule]0{{}}\infer[norule]1{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:{\mathbf{1}}\;[{q}]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\} \vdash^{\mathsf{B}}\Delta;\Gamma}\infer
1{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:\emptyset[q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\checkmark}]y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\} \vdash^{\mathsf{B}}\Delta;\Gamma}
\text{[Tcut-${\mathbf{1}}$]}\vspace{6pt}\\\
\prooftree\infer[norule]0{{}}\infer[norule]1{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(y.R);P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:T{\otimes}A\;[q]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\} \vdash^{\mathsf{B}}\Delta;\Gamma}\infer
1{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:A\;[q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(y,R)]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\} \vdash^{\mathsf{B}}\Delta;\Gamma} \text{[Tcut-$\otimes$]}\vspace{6pt}\\\
\prooftree\infer[norule]0{{}}\infer[norule]1{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{\\#\mathsf{l}\
x;P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:\oplus_{\ell\in
L}{A_{\ell}}\;[q]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\} \vdash^{\mathsf{B}}\Delta;\Gamma}\infer
1{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:A_{\\#\mathsf{l}}\;[q@\\#\mathsf{l}]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\} \vdash^{\mathsf{B}}\Delta;\Gamma} \text{[Tcut-$\oplus$]}\vspace{6pt}\\\
\prooftree\infer[norule]0{{}}\infer[norule]1{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(z);P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:!A\;[q]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\} \vdash^{\mathsf{B}}\Delta;\Gamma}\infer
1{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:\emptyset\;[q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,P)]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\} \vdash^{\mathsf{B}}\Delta;\Gamma} \text{[Tcut$!$]}\end{array}$ Figure 6:
Additional typing rules for $\mathsf{CLLB}$.

${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}a:A\;[q]\;b:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}$

The buffered cut construct models interaction via a “message queue” with two
polarised endpoints $a$ and $b$, held respectively by the processes $P$ and
$Q$. A polarised endpoint has the form $x$ or $\overline{x}$. The endpoint
marked $\overline{x}$ is the only allowing writes, the unmarked $y$ is the
only one allowing reads, exactly one of the two endpoints is marked. The
endpoints types $A,B$ are of course related but do not need to be exact duals,
the type of the writer endpoint may be advanced in time wrt the type of the
reader endpoint, reflecting the messages already enqueued but not yet
consumed. If the queue is empty, we have $A=\overline{B}$. Thus a buffered cut
with empty queue corresponds to the basic cut of $\mathsf{CLL}$.

$\begin{array}[]{llllll}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x:A{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:{A}\;[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}]\;y:\overline{A}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
\\{y/x\\}Q\\}&\quad\mbox{($A+$)}\\\ \end{array}$

The queue $q$ stores values $V$ defined by

$\begin{array}[]{llllllllll}\mathit{V}&::=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\checkmark}&\mbox{(Close
token)}&|&\;\;\\#\mathsf{l}&\mbox{(Selection Label)}\\\
&|&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(x,P)&\mbox{(Linear
Closure)}&|&\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(x,P)&\mbox{(Exponential
Closure)}\end{array}$
$\begin{array}[]{llllllllll}\mathit{q}&::=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}\;|\;\mathit{V}\;|\;V@q&&\mbox{(Queue)}\end{array}$

We use $@$ to also denote (associative) concatenation operation of queues,
with unit
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$.
Enqueue and dequeue operations occur respectively on the lhs and rhs.

The type system $\mathsf{CLLB}$ is obtained from $\mathsf{CLL}$ by replacing
[TCut] with the typing rules (and symmetric ones) in Fig. 6. We distinguish
the type judgements as $P\vdash\Delta;\Gamma$ for $\mathsf{CLL}$ and
$P\vdash^{\mathsf{B}}\Delta;\Gamma$ for $\mathsf{CLLB}$. The [TCutB] rule sets
the endpoints mode based in the cut type polarity, applicable whenever the
queue is empty. The remaining rules relate queue contents with their
corresponding (positive action) processes. For instance, rule [Tcut-$\otimes$]
can be read bottom-up as stating that typing processes mediated by a queue
containing a process closure
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(y,R)$
amounts to typing the process that will emit the session $y$ (bound to $R$),
interacting with the queue with the closure removed. Rules [Tcut-$\oplus$] and
[Tcut!] apply a similar principle to the other possible queue contents. In
[Tcut-${\mathbf{1}}$] and [Tcut!] the write endpoint is typed $\emptyset$, as
the sender has terminated
(${{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$).

$\begin{array}[]{ll}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}a:A[q]b:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P\\}
\equiv^{\mathsf{B}}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}b:B[q]a:A{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P\\}&\text{[comm]}\vspace{6pt}\\\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x[q]y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
(Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
R)\\}\equiv^{\mathsf{B}}({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x[q]y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\})\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
R&\text{[CM]}\vspace{6pt}\\\ P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x[q]z{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}y[p]w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\})\equiv^{\mathsf{B}}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x[q]z{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\})\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}y[p]w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}&\text{[CC]}\vspace{6pt}\\\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}z[q]w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\})\\}\equiv^{\mathsf{B}}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}z[q]w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\})\\}&\text{[CC!]}\vspace{6pt}\\\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}z[q]w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\})\\}\equiv^{\mathsf{B}}\\\
\quad\quad\quad\quad\quad\quad{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{(y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q)\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}z[q]w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}\\})&\text{[D-C!]}\end{array}$ Figure 7:  Additional structural congruence
rules for $\mathsf{CLLB}$.

Structural congruence for $\mathsf{B}$ (noted $\equiv^{\mathsf{B}}$) is
obtained by extending $\equiv$ with commutative conversions for the buffered
cut, listed in Fig. 7. The following provisos apply: [CM]
$y\in\mathsf{fn}(Q)$; in [CC] $y,z\in\mathsf{fn}(Q)$; in [CC!]
$x\notin\mathsf{fn}(P)$. Accordingly, reduction for $\mathsf{B}$ (noted
$\to^{\mathsf{B}}$) is obtained by replacing the $\to$ rules [fwd],
[${\mathbf{1}}\bot$], [$\otimes\mathbin{\bindnasrepma}]$ and
[$\oplus\mathbin{\binampersand}]$ by the rules in Fig. 8. Essentially each
principal cut reduction rule of $\mathsf{CLL}$ is replaced by a pair of
“positive” ($\to_{p}$) / “negative” ($\to_{n}$) reduction rules that allow
processes to interact asynchronously via the queue, that is, positive process
actions (corresponding to positive types) are non-blocking. For example, the
rule [$\otimes$] for send appends a session closure to the tail of the queue
(rhs) and the rule for receive pops a session closure from the head of the
queue (lhs). Notice that positive rules are enabled only if the relevant
endpoint is in write mode ($\overline{x}$), and negative rules are enabled
only if the relevant endpoint is in read mode ($y$). In
[$\mathbin{\bindnasrepma}$] above the target cuts endpoint polarities depends
on the types of the composed processes. To uniformly express the appropriate
marking of endpoint polarities we define some convenient abbreviations:

######  Definition 5 (Setting polarities)

$\begin{array}[]{llllll}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}a:A[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}]b:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P\\}^{\mathsf{p}}\triangleq\mbox{if }${+A}$\mbox{ then
}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{a}:A[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}]b:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P\\}\\\ \hskip 156.49014pt\mbox{ else
}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}a:A[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}]\overline{b}:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P\\}\\\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{a}:A[q]b:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P\\}^{\mathsf{p}}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{a}:A[q]b:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P\\}\quad(q\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}})\\\
\end{array}$

$\begin{array}[]{ll}{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{z}\;[q_{1}]\;x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{y}\;[q_{2}]\;w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P\\}\to^{\mathsf{B}}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{z}\;[q_{2}@q_{1}]\;w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P\\}&\text{[fwdp]}\vspace{6pt}\\\
{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}{}\;[q]\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\to^{\mathsf{B}}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\checkmark}]\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}&\text{[${\mathbf{1}}$]}\vspace{6pt}\\\
{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[\mathsf{\checkmark}]\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
y;P\\}\to^{\mathsf{B}}P&\text{[$\bot$]}\vspace{6pt}\\\
{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(z.P);Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[q]\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}\to^{\mathsf{B}}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[q@\mathsf{clos}(z,P)]|\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}&\text{[$\otimes$]}\vspace{6pt}\\\
{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[\mathsf{clos}(z,P)@q]\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w);R\\}\to^{\mathsf{B}}\\\
\quad\quad\quad\quad\quad\quad\quad\quad\quad{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[q]\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}z\;[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}]\;w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}^{\mathsf{p}}\\}^{\mathsf{p}}&\text{[$\mathbin{\bindnasrepma}$]}\vspace{6pt}\\\
{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{\\#{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{l}}\
x;P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[q]\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}\to^{\mathsf{B}}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[q@\\#\mathsf{l}]|\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}&\text{[$\oplus$]}\vspace{6pt}\\\
{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[\mathsf{l}@q]\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{case}}\
y\ \\{|{\\#\mathsf{\ell}\in L}{:}P_{\ell}\\}
\\}\to^{\mathsf{B}}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x\;[q]\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P_{\\#\mathsf{l}}\\}^{\mathsf{p}}&\text{[$\mathbin{\binampersand}$]}\vspace{6pt}\\\
{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(z);P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[q]\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\to^{\mathsf{B}}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,P)]|\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}&\text{[$!$]}\vspace{6pt}\\\
{}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(y,P)]\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{?}}y;Q\\}\to^{\mathsf{B}}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}&\text{[$?$]}\end{array}$ Figure 8:  Reduction $P\to^{\mathsf{B}}Q$.

The following definition then formalizes the intuition given above about how
to encode processes of $\mathsf{CLL}$ into processes of $\mathsf{CLLB}$.

######  Definition 6 (Embedding)

Let $P\vdash\Delta;\Gamma$. $P^{\dagger}$ is the $\mathsf{B}$ process such
that

$\begin{array}[]{llllll}({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x:A{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\})^{\dagger}\triangleq{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P^{\dagger}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x:{A}\;[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}]\;y:\overline{A}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
(\\{y/x\\}Q)^{\dagger}\\}^{\mathsf{p}}\\\ \end{array}$

homomorphically defined in the remaining constructs. Clearly
$P^{\dagger}\vdash^{\mathsf{B}}\Delta;\Gamma$.

###  4.1 Preservation and Progress for $\mathsf{CLLB}$

In this section, we prove basic safety properties of $\mathsf{CLLB}$:
Preservation (Theorem 4.1) and Progress (Theorem 4.2). To reason about type
derivations involving buffered cuts, we formulate some auxiliary inversion
principles that allow us, by aggregating sequences of application of
[TCut-$*$] rules of $\mathsf{CLLB}$, to talk in a uniform way about typing of
values in queues and typing of processes connected by queues. To assert typing
of queue values $c$ we use judgments the form $\Gamma;\Delta\vdash c{:}E$,
where $E$ is a either a type or a one hole type context, defined by

$E::=\Box\;|\;T\;|\;T\mathbin{\bindnasrepma}E\;|\;\mathbin{\binampersand}_{\ell\in
L}{E_{\ell}}$

where in $\mathbin{\binampersand}_{\ell\in L}{E_{\ell}}$ only branch type
$E_{\\#\mathsf{l}}$ for some selected label $\\#\mathsf{l}\in L$ is a one hole
context (to plug the continuation type); only the branch chosen by the
selected label in a queue is relevant to type next queue values. We identify
the selected branch in the type by tagging it with the corresponding label
$\\#\mathsf{l}$ thus $\mathbin{\binampersand}_{\ell\in
L}{E_{\ell}}[\\#\mathsf{l}]$. We then introduce the following typing rules for
queue values.

######  Definition 7 (Typing of Queue Values)

$\begin{array}[]{cccccccccccc}\displaystyle\frac{}{\Gamma;\vdash_{\mathtt{val}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\checkmark}:\bot}&&\displaystyle\frac{P\vdash^{\mathsf{B}}\Delta,z:T;\Gamma}{\Gamma;\Delta\vdash_{\mathtt{val}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,P):\overline{T}\mathbin{\bindnasrepma}E}\vspace{4pt}\\\
\displaystyle\frac{\mathbin{\binampersand}_{\ell\in
L}{E_{\ell}}[\\#\mathsf{l}]}{\Gamma;\Delta\vdash_{\mathtt{val}}\\#\mathsf{l}:\mathbin{\binampersand}_{\ell\in
L}{E_{\ell}}}&&\displaystyle\frac{P\vdash^{\mathsf{B}}z:A;\Gamma}{\Gamma;\vdash_{\mathtt{val}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,P):?\overline{A}}\end{array}$

Given a sequence of $k$ one hole queue value types $E_{i}$ and a type $A$, we
denote by $\mathbf{E}_{k};A$ the type $E_{1}[E_{2}[...E_{k}[A]]]$. Queue value
types allow us to talk in a uniform way about the type a receiver processes
compatible with the types of enqueued values, as characterized by the
following Lemma 1 and Lemma 2.

######  Lemma 1 (Non-full)

For
$P\neq{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$
the rule below is admissible and invertible:

$\frac{P\vdash^{\mathsf{B}}\Delta_{P},x{:}A;\Gamma\quad
Q\vdash^{\mathsf{B}}\Delta_{Q},y{:}B;\Gamma\quad q=\overline{c_{k}}\quad
B=\mathbf{E}_{k};\overline{A}\quad\Gamma;\Delta_{i}\vdash
c_{i}{:}E_{i}\quad{-}B}{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}{:}A\;[q]\;y{:}B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\vdash^{\mathsf{B}}\Delta_{P},\Delta_{Q},\Delta_{1},...,\Delta_{k};\Gamma}
$

Notice that a session type, as defined by a $\mathsf{CLL}$ proposition, may
terminate in either ${\mathbf{1}}$, $\bot$ or an exponential type $!A/?A$. We
then also have

######  Lemma 2 (Full)

The proof rules below are admissible:

$\frac{Q\vdash^{\mathsf{B}}\Delta_{Q},y:B;\Gamma\quad\Gamma;\Delta_{i}\vdash
c_{i}:E_{i}\quad B=\mathbf{E}_{k};\bot\quad
c_{k}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\checkmark}\quad{-}B}{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:\emptyset\;[\overline{c_{k}}]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\vdash^{\mathsf{B}}\Delta_{Q},\Delta_{1},\ldots,\Delta_{k};\Gamma} $
$\frac{Q\vdash^{\mathsf{B}}\Delta_{Q},y{:}B;\Gamma\quad\Gamma;\Delta_{i}\vdash
c_{i}{:}E_{i}\quad B=\mathbf{E}_{k-1};C\quad\Gamma\vdash
c_{k}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,R){:}C\quad{-}B}{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:\emptyset\;[\overline{c_{k}}]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\vdash^{\mathsf{B}}\Delta_{Q},\Delta_{1},\ldots,\Delta_{k},\Gamma} $

Moreover, one of them must apply for inverting the judgment in the conclusion.

######  Lemma 3 (Non-empty)

Let
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}{:}A\;[q]\;y{:}B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\vdash^{\mathsf{B}}\Delta;\Gamma$.

If $A$ is negative or void, then
$q\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$.

###### Proof

If $A$ is void then immediate by Lemma 2. If $-A$, suppose
$q={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$.
By Lemma 1 $k=0$ and $\overline{A}=B$. But then $B$ positive, contradiction.
So
$q\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$.

######  Theorem 4.1 (Preservation)

Let $P\vdash^{\mathsf{B}}\Delta;\Gamma$.

(1) If $P\equiv^{\mathsf{B}}Q$, then $Q\vdash^{\mathsf{B}}\Delta;\Gamma$. (2)
If $P\to^{\mathsf{B}}Q$, then $Q\vdash^{\mathsf{B}}\Delta;\Gamma$.

###### Proof

We verify that rules for $\stackrel{{\scriptstyle\mathsf{\tiny B}}}{{\equiv}}$
(Fig. 7) (resp. $\stackrel{{\scriptstyle\mathsf{B}}}{{\to}}$ (Fig. 8)) are
type preserving. We illustrate with (2) [fwdp].

(Case [fwdp])
$P={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q^{\prime}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{z}{:}A\;[q_{1}]\;x{:}\overline{B}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{y}{:}B\;[q_{2}]\;w{:}C{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P^{\prime}\\}\\}\vdash^{\mathsf{B}}\Delta;\Gamma$. If
$q_{2}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$
and $B=\overline{C}$, hence
$Q={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Q^{\prime}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{z}{:}A\;[q_{1}]\;w{:}C{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P^{\prime}\\}\vdash^{\mathsf{B}}\Delta;\Gamma$.

Otherwise
$q_{2}\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$.
Let
$F_{2}={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{y}{:}B\;[q_{2}]\;w{:}C{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P^{\prime}\\}$ where $F_{2}\vdash^{\mathsf{B}}\Delta_{2},x{:}\overline{B}$ and
$\Delta=\Delta_{1},\Delta_{2}$, and $q_{2}=\overline{c_{k}}$. By Lemma 1,
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y\vdash^{\mathsf{B}}x{:}\overline{B},y{:}B$, and
$C=\mathbf{E}_{k};\overline{B}$, $\Gamma;\Delta_{i}\vdash c_{i}{:}E_{i}$,
$P\vdash w{:}C,\Delta_{P};\Gamma$ and
$\Delta_{2}=\Delta_{1},\ldots,\Delta_{k},\Delta_{P}$.

Let