$F_{1}={\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{|}}\
F_{2}\\}$ with $F_{1}\vdash^{\mathsf{B}}\Delta_{1},x{:}B;\Gamma$ and
$q_{1}=\overline{d_{l}}$. By Lemma 1,
$Q^{\prime}\vdash^{\mathsf{B}}\Delta_{Q},z{:}A;\Gamma$,
$\Gamma;\Delta^{\prime}_{j}\vdash d_{j}{:}F_{j}$ and
$\overline{B}=\mathbf{F}_{l};\overline{A}$ and
$\Delta_{1}=\Delta^{\prime}_{1},\ldots,\Delta^{\prime}_{l},\Delta_{Q}$. By
Lemma 1 we get
${\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{|}}z{:}A\;[q_{2}@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$.

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, cut) and $Q$ is an action process. We first show that a live process
either reduces or offers an interaction on a free name. The observability
predicate defined in Fig. 9 (cf. [62]) characterises interactions of a process
with the environment.

$\begin{array}[]{c}\displaystyle\prooftree\infer
0[\text{[fwd]}]{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y\downarrow_{x}}\quad\prooftree\infer[norule]0{s(\mathcal{A})=x}\infer
1[\text{[$\mathcal{A}$]}]{\mathcal{A}\downarrow_{x}}\quad\prooftree\infer[norule]0{P\equiv
Q\quad Q\downarrow_{x}}\infer
1[\text{[$\equiv$]}]{P\downarrow_{x}}\quad\prooftree\infer[norule]0{P\downarrow_{x}}\infer
1[\text{[mix]}]{(P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
Q)\downarrow_{x}\vspace{2pt}}\\\
\prooftree\infer[norule]0{P\downarrow_{x}\quad x\neq y}\infer
1[\text{[cut]}]{(P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}y[q]x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q)\downarrow_{x}}\quad\prooftree\infer[norule]0{Q\downarrow_{x}\quad x\neq
y}\infer 1[\text{[cut!]}]{(z.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{|}}\
Q)\downarrow_{x}}\end{array}$ Figure 9:  Observability Predicate
$P\downarrow_{x}$.

######  Lemma 4 (Liveness)

Let $P\vdash^{\mathsf{B}}\Delta;\Gamma$ be live. Either $P\downarrow_{x}$ or
$P\to^{\mathsf{B}}$.

###### Proof

By induction on the derivation for $P\vdash\Delta;\Gamma$, and case analysis
on the last typing rule. We illustrate with one rule.

(Case of [TCut$\otimes$]) We have
$P={\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{|}}\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{|}}\
P_{2}\\} \vdash^{\mathsf{B}}\Delta;\Gamma$ where
$q=r@\mathsf{clos}(z_{k};R_{k})$ derived from
$P_{1}\vdash^{\mathsf{B}}x:A,\Delta_{P_{1}};\Gamma$. By i.h. $P_{1}\to$ or
$P_{1}\downarrow_{x_{1}}$. If $x\neq x_{1}$ then $P_{1}\downarrow_{x_{1}}$ and
$P\downarrow_{x_{1}}$. If $A$ is positive, by the same reasoning as above for
$P_{2}$ we conclude that $P\to$ or $P\downarrow_{w}$.

Otherwise, $A$ is negative. By i.h. $P_{2}\to$ or $P_{2}\downarrow_{z}$. If
$z\neq y$ then $P\downarrow_{x}$. Otherwise, $P_{2}\downarrow_{y}$. By Lemma
1, $B=\overline{T}\mathbin{\bindnasrepma}C$. By Lemma 10 (2,6), either
$P_{2}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
y\ v\
{\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{|}}\
Q^{\prime}$ (a) or
$P_{2}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w);Q^{\prime}\
{\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{|}}\
Q^{\prime\prime}$ (b). For case (a) we conclude as in [TCutB] above that
$P\to$ or $P\downarrow_{v}$, for case (b) $P\to$ by
[$\mathbin{\bindnasrepma}$].

######  Theorem 4.2 (Progress)

Let $P\vdash\emptyset;\emptyset$ be a live process. Then, $P\to^{\mathsf{B}}$.

###### Proof

Follows from Lemma 4 since $\Delta=\emptyset$.

###  4.2 Correspondence between $\mathsf{CLL}$ and $\mathsf{CLLB}$

In this section we establish the correspondence between reduction in
$\mathsf{CLL}$ and $\mathsf{CLLB}$, proving that the two languages simulate
each other in a tight sense. Intuitively, the correspondence shows that
$\mathsf{CLLB}$ allows some positive actions to be buffered ahead of
reception, while in $\mathsf{CLL}$ a single positive action synchronises with
the corresponding dual in one step, or a forward reduction takes place.

We write a reduction $P{\to^{\mathsf{B}}}Q$ as
$P{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}p}\;}Q$ if the
reduced action is positive,
$P{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}\;}Q$ if the
reduced action is negative (we consider [call] negative),
$P{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;{}Q$ if the
reduced action is a forwarder, and
$P{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}Q$ if the
reduced action is positive or a forwarder. We also write
$P\to^{\mathsf{Br}}{}Q$ for positive action followed by a matching negative
action on the same cut with an initially empty queue.

######  Lemma 5 ()

The following commutations of reductions hold.

  1. 1.

Let
$P_{1}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}p}\;}S{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;P_{2}$.
Either $P_{1}\to^{\mathsf{Br}}{}P_{2}$, or
$P_{1}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;S^{\prime}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}p}\;}P_{2}$
for some $S^{\prime}$.

  2. 2.

Let
$P_{1}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;{}S{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;P_{2}$.
Then
$P_{1}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;S^{\prime}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;{}P_{2}$
for some $S^{\prime}$.

  3. 3.

If
$P_{1}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}S{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;P_{2}$,
either $P_{1}\to^{\mathsf{Br}}{}P_{2}$, or
$P_{1}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;S^{\prime}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}P_{2}$
for some $S^{\prime}$.

  4. 4.

Let
$P_{1}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}N{\stackrel{{\scriptstyle\epsilon}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;S\to^{\mathsf{Br}}{}P_{2}$.
Either
$P_{1}{\stackrel{{\scriptstyle\epsilon}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;N$
or
$P_{1}\to^{\mathsf{Br}}{}S^{\prime}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}P_{2}$
for some $S^{\prime}$.

######  Lemma 6 (Simulation)

Let $P\vdash\emptyset;\emptyset$. If $P\to Q$ then
$P^{\dagger}\Rightarrow^{\mathsf{B}}Q^{\dagger}$.

###### Proof

Each cut reduction of $\mathsf{CLL}$ is either simulated by two reduction
steps of $\mathsf{B}$ in sequence or by a [fwd] reduction.

The following lemma identifies that in $\mathsf{CLLB}$, a sequence of positive
actions (or forwards) followed by a negative action can always be commuted
either by pulling out the negative action first, followed by the sequence of
positive actions and forwards; having the negative action follow a positive
action on the same channel and then performing the remaining actions; or by
first performing a sequence of forward actions, the output and input on the
relevant session and then the remaining actions.

######  Lemma 7 (Simulation)

Let $P\vdash^{\mathsf{B}}\emptyset;\emptyset$. If
$P{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;{}Q$
then (1) $P{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;R$
and
$R{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}Q$
for some $R$, or; (2) $P\to^{\mathsf{Br}}{}R$ and
$R{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}{\;}Q$
for some $R$, or; (3)
$P{\stackrel{{\scriptstyle\epsilon}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;\to^{\mathsf{Br}}{}R$
and
$R{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}Q$
for some $R$.

###### Proof

By induction on
$P({\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{})^{*}P^{\prime}$.

######  Theorem 4.3 (Operational correspondence
$\mathsf{CLL}$-$\mathsf{CLLB}$)

Let $P\vdash\emptyset;\emptyset$.

  1. 1.

If $P\Rightarrow R$ then $P^{\dagger}\Rightarrow^{\mathsf{B}}R^{\dagger}$.

  2. 2.

If
$P^{\dagger}({\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;)^{*}Q$
then there is $R$ such that $P\Rightarrow R$ and
$R^{\dagger}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}Q$.

Due to the progress property for $\mathsf{CLLB}$ (Theorem 4.2) and because
queues are bounded by the size of positive/negative sections in types, after a
sequence of positive or forwarder reductions a negative reduction consuming a
queue value must occur. Theorem 4.3(2) states that every reduction sequence in
$\mathsf{CLLB}$ is simulated by a reduction sequence in $\mathsf{CLL}$ up to
some anticipated forwarding and buffering of positive actions. Our results
imply that every reduction path in $\mathsf{CLLB}$ maps to a reduction path in
$\mathsf{CLL}$ in which every negative reduction step in the former is mapped,
in order, to a cut reduction step in the latter.

##  5 Correctness of the core SAM

We now prove that every execution trace of the core SAM defined in Fig. 5
represents a correct process reduction sequence $\mathsf{CLLB}$ (and therefore
of $\mathsf{CLL}$, in the light of Theorem 4.3), first for the language
without exponentials and mix, which will be treated in Section 6. In what
follows, we annotate endpoints of session records with their types (e.g. as
$x{:}A\\!\left<q,P\right>\\!y{:}B$), these annotations are not needed to guide
the operation of the SAM, but convenient for the proofs; they will be omitted
when not relevant or are obvious from the context. We first define a simple
encoding of well-typed $\mathsf{CLLB}$ processes to SAM states.

######  Definition 8 (Encode)

Given $P\vdash^{\mathsf{B}}\emptyset$ we define $enc(P)=\mathcal{C}$ as
$enc(P,\emptyset)\stackrel{{\scriptstyle\mathsf{cut}*}}{{\Mapsto}}\mathcal{\mathcal{C}}$
where
$enc(P,H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}\mathcal{\mathcal{C}}$
is defined by the rules

$\begin{array}[]{clll}\displaystyle\frac{enc(P(x),H[x{:}A\\!\left<q,Q\right>\\!y{:}B])\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}\mathcal{C}}{enc({\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\\},H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}\mathcal{C}}&\mbox{\rm($A+$
)}\vspace{6pt}\\\
\displaystyle\frac{enc(Q(y),H[x{:}A\\!\left<q,P\right>\\!y{:}B])\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}\mathcal{C}}{enc({\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\\},H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}\mathcal{C}}&\mbox{\rm($A-$
or
$P={{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$
)}\vspace{6pt}\\\
enc(\mathcal{A},H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}(\mathcal{A},H)&\mbox{\rm($A\in\mathcal{A}$)}\end{array}$

Notice that $enc(P)$ maximally applies the SAM execution rule for cut to
$(P,\emptyset)$ until an action is reached. Clearly, for any
$P\vdash^{\mathsf{B}}\emptyset$, if $enc(P)=\mathcal{C}$ then
$P\Mapsto^{*}\mathcal{C}$. Also, if all cuts in a state $C$ have empty queues
then there is a process $Q$ of $\mathsf{CLL}$ such that $enc(Q^{\dagger})=C$.
We then have

######  Theorem 5.1 (Soundness wrt $\mathsf{CLLB}$)

Let $P\vdash^{\mathsf{B}}\emptyset$.

If $enc(P)\Mapsto
D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}\mathcal{C}$ then there is
$Q$ such that $P\to\cup\equiv Q$ and $\mathcal{C}=enc(Q)$.

###### Proof

Let $enc(P)\Mapsto\mathcal{B}$. Let $enc(P)=(\mathcal{A},H)$ for some action
$\mathcal{A}$. Then $P\equiv E[\mathcal{A}]$ for some cut context $E[-]$. We
illustrate one case.

(Case of [S${\mathbf{1}}$]) Let
$enc(P)=({\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,R\right>\\!y])\Mapsto(R,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])=D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$.
Therefore, $P\equiv
E[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x] \equiv
E^{\prime}[{\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{|}}\
R\\}]$ and $P\to
Q=E^{\prime}[{\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@\checkmark]\;y]{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}]$ and $enc(Q)=C$.

We can then combine soundness with the operational correspondence between
$\mathsf{CLL}$ and $\mathsf{CLLB}$ (Theorem 4.3) to obtain an overall
soundness result for the SAM with respect to $\mathsf{CLL}$:

######  Theorem 5.2 (Soundness wrt $\mathsf{CLL}$)

Let $P\vdash^{\mathsf{B}}\emptyset$.

1\. If
$enc(P)\stackrel{{\scriptstyle*}}{{\Mapsto}}\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$
there is $Q$ such that $P\Rightarrow\cup\equiv Q$ and $\mathcal{C}=enc(Q)$.

2\. Let $P\vdash\emptyset$. If
$enc(P^{\dagger})\stackrel{{\scriptstyle*}}{{\Mapsto}}enc(Q^{\dagger})$ then
$P\Rightarrow Q$.

In Definition 9 we identify readiness, the fundamental invariant property of
SAM states, key to prove progress of its execution strategy. Readiness means
that any running process holding an endpoint of negative type, and thus
attempting to execute a negative action (e.g., a receive or offer action) on
it, will always find an appropriate value (resp. a closure or a label) to be
read in the appropriate session queue. No busy waiting or context switching
will be necessary since the sequential execution semantics of the SAM enforces
that all actions corresponding to a positive section of a session type have
always been enqueued by the “caller” process before the ”callee” takes over.
As discussed in Section 3 it might not seem obvious whether all such input
endpoints, (including endpoints moved around via send / receive interactions),
always refer to non-empty queues.

Readiness must also be maintained by processes suspended in session records,
even if a suspended process waiting on a read endpoint will not necessarily
have the corresponding queue already populated. Intuitively, a process $P$ is
$(H,N)$-ready if all its “reads” in the input channels (except those in $N$)
will be matched by values already stored in the corresponding session queue.

######  Definition 9 (Ready)

Process $P$ is $H,N$-ready if for all $y\in\mathsf{fn}(P)\setminus N$ and
${x:A}\\!\left<q,R\right>\\!{y}\in H$ then $A$ is negative or void. We
abbreviate $H,\emptyset$-ready by $H$-ready. Heap $H$ is ready if, for all
$x\\!\left<q,R\right>\\!y\in H$, the following conditions hold:

  1. 1.

if $R(y)$ then $R$ is $H,\\{y\\}$-ready

  2. 2.

if $R(x)$ then $R$ is $H$-ready

  3. 3.

if
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z:-,R)\in
q$, $R$ is $H,\\{z\\}$-ready.

  4. 4.

if
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z:+,R)\in
q$, $R$ is $H$-ready.

State $C=(P,H)$ is ready if $H$ is ready and $P$ is $H$-ready.

######  Lemma 8 (Readiness)

Let $P\vdash\emptyset$ and
$(P,\emptyset)\stackrel{{\scriptstyle*}}{{\Mapsto}}S$. Then $\mathcal{S}$ is
ready.

###### Proof

The property trivially holds for $(P,\emptyset)$ for
$\mathsf{fn}(P)=\emptyset$ and $H=\emptyset$. We proceed by transition
induction, assuming that $S=(P,H)$ is ready, and
$\mathcal{S}\Mapsto\mathcal{S}^{\prime}=(P,H^{\prime})$, we check that
$S^{\prime}$ is ready. We illustrate one case.

(Case of [SCut]) Let
$R={\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}:T\;[q]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}$ and $S=(R,H)\Mapsto S^{\prime}=(P,H^{\prime})$, where
$H^{\prime}=H[x\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},Q\right>\\!y]$
and $T$ positive. By i.h., $R$ is $H$-ready hence $P(x)$ is $H,\\{x\\}$-ready
and $Q(y)$ is $H,\\{y\\}$-ready. Then $P(x)$ is $H^{\prime}$-ready, and
$H^{\prime}$ is ready. We conclude that $S^{\prime}$ is ready.

######  Theorem 5.3 (Progress)

Let $P\vdash^{\mathsf{B}}\emptyset$ and $P$ live. Then $enc(P)\Mapsto
S^{\prime}$.

###### Proof

Since $P$ is live then $enc(P)=S=({\mathcal{A}},H)$ for some action
$\mathcal{A}$.

(Case of [$\bot$])
$\mathcal{A}={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
y;R^{\prime}$. If $H=H^{\prime}[y{:}A\\!\left<q,Q\right>\\!x]$, then $S\Mapsto
S^{\prime}$ by [S$-$]. Otherwise,
$H=H^{\prime}[x{:}A\\!\left<q,\mathcal{A}\right>\\!y]$. By Lemma 8,
$\mathcal{A}$ is $H^{\prime}$-ready, so $A$ is negative or void. By Lemma 3
$q\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$.
By Lemma 2, $q=\checkmark$. So $S\Mapsto S^{\prime}$ by [S$\bot$].

##  6 The SAM for full $\mathsf{CLL}$

$\begin{array}[]{llll}S&::=&(\mathcal{E},P,H)&\mbox{State}\vspace{6pt}\\\
H&::=&\mathit{Ref}\to\mathit{SessionRec}&\mbox{Heap}\vspace{6pt}\\\
\mathit{SessionRec}&::=&x\\!\left<q,\mathcal{E},P\right>\\!y\vspace{6pt}\\\
\mathit{q}&::=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}\;|\;\mathit{Val}@q&\mbox{Queue}\vspace{8pt}\\\
\mathit{Val}&::=&\checkmark&\mbox{Close token}\\\
&|&\\#\mathsf{l}&\mbox{Choice label}\\\
&|&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(x,\mathcal{E},P)&\mbox{Linear
Closure}\\\
&|&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(x,\mathcal{E},P)&\mbox{Exponential
Closure}\vspace{6pt}\\\
\mathcal{E},\mathcal{G},\mathcal{F}&::=&\mathit{Name}\to(\mathit{Ref}\cup\mathit{Val})&\mbox{Environment}\end{array}$
Figure 10: The SAM

In this section, we complete our initial presentation of the SAM, in
particular, we introduce support for the exponentials, allowing the machine to
compute with non-linear values, and a selective concurrency semantics. We have
delayed the introduction of an environment structure for the SAM, to make the
presentation easier to follow. However, this was done at the expense of a more
abstract formalisation of the operational semantics, making use of
$\alpha$-conversion, and overloading language syntax names as heap references
for allocated session records.

The SAM actually relies on environment-based implementation of name
management, presented in Fig. 10. A SAM state is then a triple
$(\mathcal{E},P,H)$ where $\mathcal{E}$ is an environment that maps each free
name of the code $P$ into either a closure or a heap record endpoint. These
heap references are freshly allocated and unique, thus avoiding any clashes
and enforcing proper static scoping. Closures, representing suspended linear
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,\mathcal{E},P)$)
and exponential behaviour
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{E},P)$),
pair the code in its environment, and we expect the following structural
safety conditions for name biding in configurations to hold.

######  Definition 10 (Closure)

A process $P$ is $(\mathcal{E},N)$-closed if $\mathsf{fn}(P)\setminus
N\subseteq dom(\mathcal{E})$, and $\mathcal{E}$-closed if
$(\mathcal{E},\emptyset)$-closed.

Environment $\mathcal{E}$ is $H$-closed if for all $x\in dom(\mathcal{E})$ if
$\mathcal{E}(x)$ is a reference then $x\in H$, if
$\mathcal{E}(x)={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{F},R)$
then $\mathcal{F}$ is $H$-closed and $R$ is $(\mathcal{F},\\{z\\})$-closed.

Heap $H$ is closed if for all $x\\!\left<q,\mathcal{G},Q\right>\\!y\in H$,
$\mathcal{G}$ is $H$-closed, $Q$ is $\mathcal{G}$-closed, and for all
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,\mathcal{F},R)\in
q$ and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{F},R)\in
q$, $\mathcal{F}$ is $H$ closed and $R$ is $(\mathcal{F},\\{z\\})$-closed.
State $(\mathcal{E},P,H)$ is closed if $H$ is closed, $\mathcal{E}$ is
$H$-closed, and $P$ is $\mathcal{E}$-closed.

$\begin{array}[]{lrr}(\mathcal{E},{\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:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\},H)\Mapsto(\mathcal{G},P,H[a\\!\left<q,\mathcal{F},Q\right>\\!b])&\text{\rm[SCut]}\\\
a,b=\mathsf{new},\mathcal{G}=\mathcal{E}\\{a/x\\},\mathcal{F}=\mathcal{E}\\{b/y\\}\vspace{6pt}\\\
(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x,H[a\\!\left<q,\mathcal{F},P\right>\\!b])\Mapsto(\mathcal{F},P,H[a\\!\left<q@{\checkmark},\emptyset,{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!b])&\text{\rm[S${\mathbf{1}}$]}\\\
a=\mathcal{E}(x)\vspace{6pt}\\\
(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\
y,H[c\\!\left<q_{1},\mathcal{G},Q\right>\\!a][b\\!\left<q_{2},\mathcal{F},P\right>\\!d])\Mapsto(\mathcal{F},P,H[c\\!\left<q_{2}@{q_{1}},\mathcal{G},Q\right>\\!d])&\text{\rm[Sfwd]}\\\
a=\mathcal{E}(x),b=\mathcal{E}(y)\vspace{6pt}\\\
(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
y;P,H[a\\!\left<{\checkmark},\emptyset,{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!b])\Mapsto(\mathcal{E},P,H)&\text{\rm[S$\bot$]}\\\
b=\mathcal{E}(y)\vspace{6pt}\\\
(\mathcal{E},\mathcal{A}^{-}(x),H[a\\!\left<{q},\mathcal{G},Q\right>\\!b])\Mapsto(\mathcal{G},Q,H[a\\!\left<{q},\mathcal{E},\mathcal{A}^{-}(x)\right>\\!b])&\text{\rm[S$-$]}\\\
a=\mathcal{E}(x)\vspace{6pt}\\\
(\mathcal{E},{\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[a\\!\left<q,P\right>\\!b])\Mapsto\\\
\quad\quad\quad\quad\quad\quad\quad\quad(\mathcal{E},Q,H[a\\!\left<q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,\mathcal{E},R),P\right>\\!b])&\text{\rm[S$\otimes$]}\\\
a=\mathcal{E}(x)\vspace{6pt}\\\
(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w{:}+);Q,H[a\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,\mathcal{F},R)@q,\mathcal{G},P\right>\\!b])\Mapsto\\\
\quad\quad\quad\quad\quad\quad\quad\quad(\mathcal{E}^{\prime},Q,H[e\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},\mathcal{F}^{\prime},R\right>\\!f][a\\!\left<q\right>^{s}\\!b])&\text{\rm[S$\mathbin{\bindnasrepma}+$]}\\\
e,f=\mathsf{new},b=\mathcal{E}(y),\mathcal{E}^{\prime}=\mathcal{E}\\{e/w\\},\mathcal{F}^{\prime}=\mathcal{F}\\{f/z\\}\vspace{6pt}\\\
(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w{:}-);Q,H[a\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,\mathcal{F},R)@q,\mathcal{G},P\right>\\!b])\Mapsto\\\
\quad\quad\quad\quad\quad\quad\quad\quad(\mathcal{F}^{\prime},R,H[e\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},\mathcal{E}^{\prime},Q\right>\\!f][a\\!\left<q\right>^{s}\\!b])&\text{\rm[S$\mathbin{\bindnasrepma}-$]}\\\
e,f=\mathsf{new},b=\mathcal{E}(y),\mathcal{F}^{\prime}=\mathcal{F}\\{e/z\\},\mathcal{E}^{\prime}=\mathcal{E}\\{f/w\\}\vspace{6pt}\\\
(\mathcal{E},\\#\mathsf{l}\;x;Q,H[a\\!\left<q,\mathcal{G},P\right>\\!b])\Mapsto(\mathcal{E},Q,H[a\\!\left<q@\\#\mathsf{l},\mathcal{G},P\right>\\!b])&\text{\rm[S$\oplus$]}\\\
a=\mathcal{E}(x)\vspace{6pt}\\\
(\mathcal{E},{\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[a\\!\left<\\#\mathsf{l}@q,\mathcal{G},P\right>\\!b])\Mapsto(\mathcal{E},Q_{\\#\mathsf{l}},H[a\\!\left<q\right>^{s}\\!b])&\text{\rm[S$\mathbin{\binampersand}$]}\\\
b=\mathcal{E}(y)\vspace{6pt}\\\
(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(z);Q,H[a\\!\left<q,\mathcal{G},P\right>\\!b])\Mapsto(\mathcal{G},P,H[a\\!\left<q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,\mathcal{E},Q),\emptyset,{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!b])&\text{\rm[S$!$]}\\\
a=\mathcal{E}(x)\vspace{6pt}\\\
(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{?}}y;Q,H[a\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,\mathcal{F},R),\emptyset,{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!b])\Mapsto(\mathcal{E}^{\prime},Q,H)&\text{\rm[S$?$]}\\\
b=\mathcal{E}(y),\mathcal{E}^{\prime}=\mathcal{E}\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,\mathcal{F},R)/y\\}\vspace{6pt}\\\
(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{call}}\
y(w{:}+);Q,H)\Mapsto(\mathcal{E}^{\prime},Q,H[a\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},\mathcal{F}^{\prime},R\right>\\!b])&\text{\rm[Scall+]}\\\
a,b=\mathsf{new},\mathcal{E}^{\prime}=\mathcal{E}\\{a/w\\},\mathcal{F}^{\prime}=\mathcal{F}\\{b/z\\}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,\mathcal{F},R)=\mathcal{E}(y)\vspace{6pt}\\\
(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{call}}\
y(w{:}-);Q,H)\Mapsto(\mathcal{F}^{\prime},R,H[a\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},\mathcal{E}^{\prime},Q\right>\\!b])&\text{\rm[Scall-]}\\\
a,b=\mathsf{new},\mathcal{E}^{\prime}=\mathcal{E}\\{b/w\\},\mathcal{F}^{\prime}=\mathcal{F}\\{a/z\\}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,\mathcal{F},R)=\mathcal{E}(y)\vspace{6pt}\\\
\\\ a\\!\left<q\right>^{s}\\!b\triangleq\mbox{if
}(q={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}})\mbox{
then }b\\!\left<q,\mathcal{G},P\right>\\!a\mbox{ else
}a\\!\left<q,\mathcal{G},P\right>\\!b\end{array}$ Figure 11: SAM Transition
Rules for the complete $\mathsf{CLL}$

In Figure 11 we present the environment-based execution rules for the SAM. All
rules except those for exponentials have already been essentially presented in
Fig. 5 and discussed in previous sections. The only changes to those rules are
due to the presence of environments, which at all times record the bindings
for free names in the code. Overall, we have

###### Lemma 9

Let $P\vdash^{\mathsf{B}}\emptyset;\emptyset$. For all $S$ such that
$(P,\emptyset,\emptyset)\stackrel{{\scriptstyle*}}{{\Mapsto}}S$, $S$ is
closed.

We discuss the SAM rules for the exponentials. Values of exponential type are
represented by exponential closures
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{F},R)$.
Recall that a session type may terminate in either type ${\mathbf{1}}$, type
$\bot$ or in an exponential type $!A/?A$ (cf. 2). So, the (positive) execution
rule [S$!$] is similar to rule [S${\mathbf{1}}$]: it enqueues the closure
representing the replicated process, and switches context, since the session
terminates (cf. [!] Fig. 8). The execution rule [S$?$] is similar to rule
[S$\mathbin{\bindnasrepma}$]: it pops a closure from the queue (which, in this
case, always becomes empty), and instead of using it immediately, adds it to
the environment to become persistently available to client code (cf. reduction
rule [S$?$] Fig. 8). Any such closure representing a replicated process may be
called by client code with transition rule [Scall], which essentially creates
a new linear session composed by cut with the client code, similarly to
[S$\mathbin{\bindnasrepma}$]. Rule [SCall] operates with some similarity to
rule [S$\mathbin{\bindnasrepma}$]: instead of activating a linear closure
popped from the queue, it activate an exponential closure fetched from the
environment.

We extend the $enc$ map to the exponential cut and environment states
$(\mathcal{E},P,H)$ by adapting Definition 8, and adding the clause:

$\displaystyle\frac{enc(\mathcal{E}\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(y,\mathcal{E},R)/x\\},P),H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}{enc(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.R\
{\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\\},H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}$

We now update our meta-theoretical results for the complete SAM.

######  Theorem 6.1 (Soundness)

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

If $enc(P)\Mapsto D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$ then
there is $Q$ such that $P\to\cup\equiv Q$ and $C=enc(Q)$.

######  Theorem 6.2 (Progress)

Let $P\vdash^{\mathsf{B}}\emptyset;\emptyset$ and $P$ live. Then
$enc(P)\Mapsto C$.

###  6.1 Concurrent Semantics of Cut and Mix

Intuitively, the execution of mix $P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
Q$ consists in the parallel execution of (non-interfering) processes $P$ and
$Q$. We may execute $P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
Q$ by sequentialising $P$ and $Q$ in some arbirary way, and this actually may
be useful in some cases.

However, much more interesting is the accommodation in the SAM of interfering
concurrency, as required to support full-fledged concurrent languages for
session-based programming. First, we evolve the SAM from single threaded to
multithreaded, where states now expose a multiset of processes $P_{i}$ ready
for execution by the basic SAM sequential transitions:
$(\\{P_{1},P_{2},\ldots,P_{n}\\},H)$ and introduce an annotated variant
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{pcut}}$
of the cut. It has the same $\mathsf{CLL}/\mathsf{CLLB}$ semantics, but to be
implemented as a fork construct where $P$ and $Q$ spawn concurrently, their
interaction mediated by an atomic _concurrent session record_
$x\left<q\right>y$. The type system ensuring that concurrent channels may be
forwarded only to concurrent channels. We extend the SAM with transition rule
for multisets:

$\begin{array}[]{c}\displaystyle\frac{(P,H)\Mapsto(P^{\prime},H^{\prime})}{(P\uplus
T,H)\Mapsto(P^{\prime}\uplus T,H^{\prime})}\;\text{\rm[Srun]}\vspace{6pt}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{pcut}}\;\\{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\\}\uplus T,H)\Mapsto(\\{P,Q\\}\uplus
T\\},H[x\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}\right>y])\quad\text{\rm[SCutp]}\vspace{6pt}\\\
((P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
Q)\uplus T,H)\Mapsto(\\{P,Q\\}\uplus
T\\},H[x\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}\right>y])\quad\text{\rm[SMixp]}\end{array}$

Each individual thread executes locally according to the SAM sequential
transitions presented before, until an action on a concurrent queue is
reached. Concurrent process actions on concurrent queues are atomic, and
defined as expected. Positive actions always progress by pushing a value into
the queue, while negative actions will either pop off a value from the queue
or block, waiting for a value to become available. We illustrate with the
rules for ${\mathbf{1}}$,$\bot$ typed actions.

$\begin{array}[]{ll}({\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\right>y])\Mapsto({{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}},H[x\left<q@{\checkmark}\right>y])&\text{\rm[S${\mathbf{1}}$c]}\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},y\right>\\!])\Mapsto(P,H)&\text{\rm[S$\bot$c]}\end{array}$

Notice that, as in the case for
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
y;P$ above, any negative action in the thread queue is unable to progress if
the corresponding queue is empty. It should be clear how to define transition
rules for all other pairs of dual actions. Given an appropriate encoding
$enc^{c}$ of annotated $\mathsf{CLLB}$ processes in concurrent SAM states, and
as consequence of typing and leveraging the proof scheme for progress in
$\mathsf{CLLB}$ (Theorem 4.2), we have:

######  Theorem 6.3 (Soundness-c)

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

If $enc^{c}(P)\Mapsto D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$
then there is $Q$ such that $P\to\cup\equiv Q$ and $C=enc^{c}(Q)$.

######  Theorem 6.4 (Progress-c)

Let $P\vdash^{\mathsf{B}}\emptyset;\emptyset$ and $P$ live. Then
$enc_{c}(P)\Mapsto C$.

The extended SAM executes concurrent session programs, consisting in an
arbitrary number of concurrent threads. Each thread deterministically executes
sequential code, but can at any moment spawn new concurrent threads. The whole
model is expressed in the common language of (classical) linear logic,
statically ensuring safety, proper resource usage, termination, and deadlock
absence by static typing.

##  7 Concluding Remarks and Related Work

We introduce the Session Abstract Machine, or SAM, an abstract machine for
executing session processes typed by (classical) linear logic $\mathsf{CLL}$,
deriving a deterministic, sequential evaluation strategy, where exactly one
process is executing at any given point in time. In the SAM, session channels
are implemented as single queues with a write and a read endpoint, which are
written to, and read by executing processes. Positive actions are non-
blocking, giving rise to a degree of asynchrony. However, processes in a
session synchronise at polarity inversions, where they alternate execution,
according to a fixed co-routining strategy. Despite its specific strategy, the
SAM semantics is sound wrt $\mathsf{CLL}$ and satisfies the correctness
properties of logic-based session type systems. We also present a conservative
concurrent extension of the SAM, allowing the degrees of concurrency to be
modularly expressed at a fine grain, ranging from fully sequential to fully
concurrent execution. Indeed, a practical concern with the SAM design lies in
providing a principled foundation for an execution environment for multi-
paradigm languages, combining concurrent, imperative and functional
programming. The overall SAM design as presented here may be uniformly
extended to cover any other polarised language constructs that conservatively
extend the PaT paradigm, such as polymorphism, affine types, recursive and co-
recursive types, and shared state [55, 60]. We have implemented a SAM-based
version [16] of an open-source implementation of $\mathsf{CLL}$ [61].

A machine model provides evidence of the algorithmic feasibility of a
programming language abstract semantics, and illuminates its operational
meaning from certain concrete semantic perspective. Since the seminal work of
Landin on the SECD [42], several machines to support the execution of programs
for a given programming language have been proposed. The SAM is then proposed
herein in this same spirit of Cousineau, Curien and Mauny’s Categorical
Abstract Machine for the call-by-value $\lambda$-calculus [20], Lafont’s
Linear Abstract Machine for the linear $\lambda$-calculus [40], and Krivine’s
Machine for the call-by-name $\lambda$-calculus [39] ; these works explored
Curry-Howard correspondences to propose provably correct solutions. In [21],
Danvy developed a deconstruction of the SECD based on a sequence of program
transformations. The SAM is also derived from Curry-Howard correspondences for
linear logic $\mathsf{CLL}$ [15, 71], and we also rely on program conversions,
via the intermediate buffered language $\mathsf{CLLB}$, as a key proof
technique. We believe that the SAM is the first proposal of its kind to tackle
the challenges of a process language, while building on several deep
properties of its type structure towards a principled design. Among those,
focusing [4] and polarisation [43, 31, 55] played an important role to achieve
a deterministic sequential reduction strategy for session-based programming,
perhaps our main initial motivation. That allows the SAM to naturally and
efficiently integrate the execution of sequential and concurrent session
behaviours, and suggests effective compilation schemes for mainstream virtual
machines or compiler frameworks.

The adoption of session and linear types is clearly increasing in research
(e.g., [25, 3, 57, 23, 73, 65, 55, 60]) and general purpose languages (e.g.,
Haskell [8, 37], Rust [41, 19] Ocaml [34, 51], F# [50], Move [9], among many
others), which either require sophisticated encodings of linear typing via
type-level computation or forego of some static correctness properties for
usability purposes. Such developments typically have as a main focus the
realization of the session typing discipline (or of a particular refinement of
such typing), with the underlying concurrent execution model often offloaded
to existing language infrastructure.

We highlight the work [18], which studies the relationship between synchronous
session types and game semantics, which are fundamentally asynchronous. Their
work proposes an encoding of synchronous strategies into asynchronous
strategies by so-called call-return protocols. While their focus differs
significantly from ours, the encoding via asynchrony is reminiscent of our
own.

We further note the work [49] which develops a polarized variant of the
$\overline{\lambda}\mu\tilde{\mu}$ suitable for sequent calculi like that of
linear logic. While we draw upon similar inspirations in the design of the
SAM, there are several key distinctions: the work [49] presents
$\lambda\mu$-calculi featuring values and substitution of terms for variables
(potentially deep within the term structure). Our system, being based on
processes calculus, features neither -– there is no term representing the
outcome of a computation, since computation is the interactive behavior of
processes (cf. game semantics); nor does computation rely on substitution in
the same sense. Another significant distinction is that our work materializes
a heap-based abstract machine rather than a stack-based machine. Finally, our
type and term structure is not itself polarized. Instead, we draw inspiration
from focusing insofar as we extract from focusing the insights that drive
execution in the SAM.

In future work, we plan to study the semantics of the SAM in terms of games
(and categories), along the lines of [18, 20, 40]. We also plan to investigate
the ways in which the evaluation strategy of the SAM can be leveraged to
develop efficient compilation of fine-grained session-based programming, and
its relationship with effect handlers, coroutines and delimited continuations.
Linearity plays a key role in programming languages and environments for smart
contracts in distributed ledgers [23, 63] manipulating linear resources
(assets); it would be interesting to investigate how linear abstract machines
like the SAM would provide a basis for certifying resource sensitive computing
infrastructures [74, 9].

#### Acknowledgments.

This work was supported by NOVA LINCS (UIDB/ 04516/ 2020), INESC ID (UIDB/
50021/ 2020), BIG (Horizon EU 952226 BIG).

## References

  * [1] Abramsky, S.: Computational Interpretations of Linear Logic. Theoret. Comput. Sci. 111(1–2), 3–57 (1993)
  * [2] Abramsky, S., Gay, S.J., Nagarajan, R.: Interaction categories and the foundations of typed concurrent programming. In: NATO ASI DPD. pp. 35–113 (1996)
  * [3] Almeida, B., Mordido, A., Thiemann, P., Vasconcelos, V.T.: Polymorphic lambda calculus with context-free session types. Inf. Comput. 289(Part), 104948 (2022)
  * [4] Andreoli, J.M.: Logic Programming with Focusing Proofs in Linear Logic. J. Log. Comput. 2(3), 297–347 (1992)
  * [5] Balzer, S., Pfenning, F.: Manifest sharing with session types. Proc. ACM Program. Lang. 1(ICFP) (2017)
  * [6] Bellin, G., Scott, P.: On the $\pi$-calculus and linear logic. Theoret. Comput. Sci. 135(1), 11–65 (1994)
  * [7] Benton, P.N.: A mixed linear and non-linear logic: Proofs, terms and models. In: International Workshop on Computer Science Logic. pp. 121–135. Springer (1994)
  * [8] Bernardy, J., Boespflug, M., Newton, R.R., Jones, S.P., Spiwack, A.: Linear haskell: practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang. 2(POPL), 5:1–5:29 (2018)
  * [9] Blackshear, S., Cheng, E., Dill, D.L., Gao, V., Maurer, B., Nowacki, T., Pott, A., Qadeer, S., Russi, D., Sezer, D., Zakian, T., Zhou, R.: Move: A Language with Programmable Resources (2019)
  * [10] Caires, L., Pérez, J.A.: Linearity, control effects, and behavioral types. In: Yang, H. (ed.) Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017. Lecture Notes in Computer Science, vol. 10201, pp. 229–259. Springer (2017)
  * [11] Caires, L., Pérez, J.A.: Linearity, control effects, and behavioral types. In: Proceedings of the 26th European Symposium on Programming Languages and Systems - Volume 10201. p. 229–259. Springer-Verlag, Berlin, Heidelberg (2017)
  * [12] Caires, L., Pérez, J.A., Pfenning, F., Toninho, B.: Behavioral polymorphism and parametricity in session-based communication. In: Proceedings of the 22nd European Conference on Programming Languages and Systems. p. 330–349. ESOP’13, Springer-Verlag, Berlin, Heidelberg (2013)
  * [13] Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010 - Concurrency Theory. pp. 222–236. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)
  * [14] Caires, L., Pfenning, F., Toninho, B.: Towards concurrent type theory. In: Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation. p. 1–12. TLDI ’12, Association for Computing Machinery, New York, NY, USA (2012)
  * [15] Caires, L., Pfenning, F., Toninho, B.: Linear logic propositions as session types. Mathematical Structures in Computer Science 26(3), 367–423 (2016)
  * [16] Caires, L., Toninho, B.: The Session Abstract Machine (Artifact) (2024). https://doi.org/10.5281/zenodo.10459455
  * [17] Cardelli, L.: Typeful Programming. IFIP State-of-the-Art Reports: Formal Description of Programming Concepts pp. 431–507 (1991)
  * [18] Castellan, S., Yoshida, N.: Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side. Proc. ACM Program. Lang. 3(POPL), 27:1–27:29 (2019)
  * [19] Chen, R., Balzer, S., Toninho, B.: Ferrite: A Judgmental Embedding of Session Types in Rust. In: Ali, K., Vitek, J. (eds.) 36th European Conference on Object-Oriented Programming, ECOOP 2022. LIPIcs, vol. 222, pp. 22:1–22:28 (2022)
  * [20] Cousineau, G., Curien, P., Mauny, M.: The Categorical Abstract Machine. Sci. Comput. Program. 8(2), 173–202 (1987)
  * [21] Danvy, O.: A Rational Deconstruction of Landin’s SECD Machine. In: Grelck, C., Huch, F., Michaelson, G., Trinder, P.W. (eds.) Implementation and Application of Functional Languages, 16th International Workshop, IFL 2004. LNCS, vol. 3474, pp. 52–71. Springer (2004)
  * [22] Dardha, O., Gay, S.J.: A new linear logic for deadlock-free session-typed processes. In: Baier, C., Lago, U.D. (eds.) Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018. LNCS, vol. 10803, pp. 91–109. Springer (2018)
  * [23] Das, A., Pfenning, F.: Rast: A language for resource-aware session types. Log. Methods Comput. Sci. 18(1) (2022)
  * [24] DeYoung, H., Caires, L., Pfenning, F., Toninho, B.: Cut reduction in linear logic as asynchronous session-typed communication. In: Computer Science Logic (2012)
  * [25] Franco, J., Vasconcelos, V.T.: A concurrent programming language with refined session types. In: Counsell, S., Núñez, M. (eds.) Software Engineering and Formal Methods - SEFM 2013. LNCS, vol. 8368, pp. 15–28. Springer (2013)
  * [26] Frumin, D., D’Osualdo, E., van den Heuvel, B., Pérez, J.A.: A bunch of sessions: a propositions-as-sessions interpretation of bunched implications in channel-based concurrency. Proc. ACM Program. Lang. 6(OOPSLA2), 841–869 (2022)
  * [27] Gay, S., Hole, M.: Subtyping for Session Types in the Pi Calculus. Acta Informatica 42(2-3), 191–225 (2005)
  * [28] Gay, S., Vasconcelos, V.: Linear Type Theory for Asynchronous Session Types. Journal of Functional Programming 20(1), 19–50 (2010)
  * [29] Girard, J.: A new constructive logic: Classical logic. Math. Struct. Comput. Sci. 1(3), 255–296 (1991)
  * [30] Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR’93. pp. 509–523. Springer Berlin Heidelberg, Berlin, Heidelberg (1993)
  * [31] Honda, K., Laurent, O.: An exact correspondence between a typed pi-calculus and polarised proof-nets. Theor. Comput. Sci. 411(22-24), 2223–2238 (2010)
  * [32] Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) Programming Languages and Systems. pp. 122–138. Springer (1998)
  * [33] Hüttel, H., Lanese, I., Vasconcelos, V.T., Caires, L., et al.: Foundations of Session Types and Behavioural Contracts. ACM Comput. Surv. 49(1), 3 (2016)
  * [34] Imai, K., Neykova, R., Yoshida, N., Yuen, S.: Multiparty session programming with global protocol combinators. In: Hirschfeld, R., Pape, T. (eds.) 34th European Conference on Object-Oriented Programming, ECOOP 2020. LIPIcs, vol. 166, pp. 9:1–9:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
  * [35] Jacobs, J., Balzer, S.: Higher-order leak and deadlock free locks. Proc. ACM Program. Lang. 7(POPL), 1027–1057 (2023)
  * [36] Klabnik, S., Nichols, C.: The Rust Programming Language (2021)
  * [37] Kokke, W., Dardha, O.: Deadlock-free session types in linear Haskell. In: Hage, J. (ed.) Haskell 2021: Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell. pp. 1–13. ACM (2021)
  * [38] Kokke, W., Montesi, F., Peressotti, M.: Better late than never: a fully-abstract semantics for classical processes. Proc. ACM Program. Lang. 3(POPL), 24:1–24:29 (2019)
  * [39] Krivine, J.: A call-by-name Lambda-calculus Machine. High. Order Symb. Comput. 20(3), 199–207 (2007)
  * [40] Lafont, Y.: The Linear Abstract Machine. Theor. Comput. Sci. 59, 157–180 (1988)
  * [41] Lagaillardie, N., Neykova, R., Yoshida, N.: Implementing Multiparty Session Types in Rust. In: Coordination Models and Languages Coordination 2020. Lecture Notes in Computer Science, vol. 12134, pp. 127–136. Springer (2020)
  * [42] Landin, P.J.: The Mechanical Evaluation of Expressions. The Computer Journal, Volume 6, Issue 4, January 1964 6(4), 308–320 (1964)
  * [43] Laurent, O.: Polarized Proof-Nets: Proof-Nets for LC. In: Girard, J. (ed.) Typed Lambda Calculi and Applications, 4th International Conference, TLCA’99. LNCS, vol. 1581, pp. 213–227. Springer (1999)
  * [44] Lindley, S., Morris, J.G.: Embedding session types in Haskell. In: Mainland, G. (ed.) Proceedings of the 9th International Symposium on Haskell, Haskell 2016, Nara, Japan, September 22-23, 2016. pp. 133–145. ACM (2016)
  * [45] Lopes, L.M.B., Silva, F.M.A., Vasconcelos, V.T.: A virtual machine for a process calculus. In: Nadathur, G. (ed.) Principles and Practice of Declarative Programming, International Conference PPDP’99. Lecture Notes in Computer Science, vol. 1702, pp. 244–260. Springer (1999)
  * [46] Milner, R.: Functions as processes. Math. Struct. Comput. Sci. 2(2), 119–141 (1992)
  * [47] Milner, R.: Elements of interaction: Turing award lecture. Communications of the ACM 36(1), 78–89 (1993)
  * [48] Milner, R.: Communicating and mobile systems - the Pi-calculus. Cambridge University Press (1999)
  * [49] Munch-Maccagnoni, G.: Focalisation and classical realisability. In: Grädel, E., Kahle, R. (eds.) Computer Science Logic, 23rd international Workshop, CSL 2009. LNCS, vol. 5771, pp. 409–423. Springer (2009)
  * [50] Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: compile-time API generation of distributed protocols with refinements in f#. In: Dubach, C., Xue, J. (eds.) Proceedings of the 27th International Conference on Compiler Construction, CC 2018, February 24-25, 2018, Vienna, Austria. pp. 128–138. ACM (2018)
  * [51] Padovani, L.: A simple library implementation of binary sessions. J. Funct. Program. 27, e4 (2017)
  * [52] Pérez, J.A., Caires, L., Pfenning, F., Toninho, B.: Linear logical relations and observational equivalences for session-based concurrency. Information and Computation 239, 254–302 (2014)
  * [53] Pfenning, F., Pruiksma, K.: Relating message passing and shared memory, proof-theoretically. In: Jongmans, S., Lopes, A. (eds.) Coordination Models and Languages - COORDINATION 2023. LNCS, vol. 13908, pp. 3–27. Springer (2023)
  * [54] Pfenning, F.: Structural cut elimination. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science. p. 156. LICS ’95, IEEE Computer Society, USA (1995)
  * [55] Pfenning, F., Griffith, D.: Polarized Substructural Session Types. In: Proc. of FoSSaCS 2015. LNCS, vol. 9034, pp. 3–22. Springer (2015)
  * [56] Pierce, B.C., Turner, D.N.: Pict: a programming language based on the pi-calculus. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, Essays in Honour of Robin Milner. pp. 455–494. The MIT Press (2000)
  * [57] Poças, D., Costa, D., Mordido, A., Vasconcelos, V.T.: System f${}^{\mbox{{$\mu$}}}$ ${}_{\mbox{{\o}mega}}$ with context-free session types. In: Wies, T. (ed.) Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023. LNCS, vol. 13990, pp. 392–420. Springer (2023)
  * [58] Qian, Z., Kavvos, G., Birkedal, L.: Client-server sessions in linear logic. Proceedings of the ACM on Programming Languages 5(ICFP), 1–31 (2021)
  * [59] Rocha, P., Caires, L.: Propositions-as-types and Shared State. Proceedings of the ACM on Programming Languages 5(ICFP), 1–30 (2021)
  * [60] Rocha, P., Caires, L.: Safe session-based concurrency with shared linear state. In: Wies, T. (ed.) Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023. LNCS, vol. 13990, pp. 421–450. Springer (2023)
  * [61] Rocha, P., Caires, L.: Safe session-based concurrency with shared linear state (artifact) (January 2023). https://doi.org/10.5281/zenodo.7506064
  * [62] Sangiorgi, D., Walker, D.: PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, USA (2001)
  * [63] Sergey, I., Nagaraj, V., Johannsen, J., Kumar, A., Trunov, A., Hao, K.: Safer smart contract programming with Scilla. Proc. ACM Program. Lang. 3(OOPSLA), 185:1–185:30 (2019)
  * [64] Toninho, B., Caires, L., Pfenning, F.: Functions as Session-Typed Processes. In: FoSSaCS’12. No. 7213 in LNCS (2012)
  * [65] Toninho, B., Caires, L., Pfenning, F.: Higher-order processes, functions, and sessions: A monadic integration. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. pp. 350–369. Springer (2013)
  * [66] Toninho, B., Caires, L., Pfenning, F.: A decade of dependent session types. In: Veltri, N., Benton, N., Ghilezan, S. (eds.) PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming. pp. 3:1–3:3. ACM (2021)
  * [67] Toninho, B., Yoshida, N.: On polymorphic sessions and functions: A tale of two (fully abstract) encodings. ACM Trans. Program. Lang. Syst. 43(2) (Jun 2021)
  * [68] Turner, D.N.: The polymorphic Pi-calculus : theory and implementation. Ph.D. thesis, University of Edinburgh, UK (1996)
  * [69] Vasconcelos, V.T.: Lambda and pi calculi, CAM and SECD machines. J. Funct. Program. 15(1), 101–127 (2005)
  * [70] Wadler, P.: Propositions as sessions. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming. p. 273–286. ICFP ’12, Association for Computing Machinery, New York, NY, USA (2012)
  * [71] Wadler, P.: Propositions as Sessions. Journal of Functional Programming 24(2-3), 384–418 (2014)
  * [72] Wadler, P.: Propositions as Types. Commun. ACM 58(12), 75–84 (2015)
  * [73] Willsey, M., Prabhu, R., Pfenning, F.: Design and implementation of concurrent C0. In: Cervesato, I., Fernández, M. (eds.) Proceedings Fourth International Workshop on Linearity, LINEARITY 2016. EPTCS, vol. 238, pp. 73–82 (2016)
  * [74] Wood, G.: Ethereum: A Secure Decentralised Generalised Transaction Ledger. Ethereum project yellow paper 151(2014), 1–32 (2014)

##  Appendix 0.A Appendix - Supplementary Material

###  0.A.1 Proofs of Section 4.1: Preservation and Progress for
$\mathsf{CLLB}$

See 1

###### Proof

To check that the rule is admissible, directly derive the conclusion using $k$
applications of [TCut$\otimes$] or [TCut$\oplus$]. To check inversion, we
proceed by induction in the derivation of
${\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\;[\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;\Gamma$.

(Case [TCutB]) We have $k=0$ so
$q={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$,
$A$ positive and $B$ negative.

(Case [TCut-${\mathbf{1}}$]) Not applicable, since $c_{k}\neq\checkmark$.

(Case [TCut-$\otimes$]) We have
${\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\;[\overline{c_{k-1}}@\mathsf{clos}(z_{k};R_{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;\Gamma$ derived from
${\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_{k}.R_{k});P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:T_{k}{\otimes}A\;[\overline{c_{k-1}}]\;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$. By i.h.
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(z_{k}.R_{k});P\vdash^{\mathsf{B}}\Sigma_{k},x{:}T_{k}\otimes A$ and
$Q\vdash\Delta_{Q},y{:}B$ where
$B=\mathbf{E}_{k-1};{\overline{(T_{k}\otimes{A})}}$ and
$\Delta_{i}\vdash^{\mathsf{B}}c_{i}:E_{i}$ for $i\leq k-1$. By inversion
([T$\otimes$]) $P\vdash^{\mathsf{B}}\Delta_{P},x:A$,
$\Sigma_{k}=\Delta_{k},\Delta_{P}$ and
$R_{k}\vdash^{\mathsf{B}}\Delta_{k},z_{k}{:}T_{k}$, so
$\Delta_{k}\vdash^{\mathsf{B}}c_{k}{:}E_{k}$ where
$E_{k}=\overline{T_{k}}\mathbin{\bindnasrepma}\Box$. We conclude
$P\vdash^{\mathsf{B}}\Delta_{P},x:A$, $Q\vdash\Delta_{Q},y{:}B$,
$B=\mathbf{E}_{k};\overline{A}$ and $\Delta_{i}\vdash c_{i}{:}E_{i}$ for
$i\leq k$.

(Case [TCut-$\oplus$]) We have
${\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}}\;[\overline{c_{k-1}}@\\#\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$ derived from
${\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}}\;[\overline{c_{k-1}}]\;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,\Delta^{\prime};\Gamma$. We proceed by the i.h.
as with [T$\otimes$] above, considering
$B=\mathbf{E}_{k-1};{\overline{(\oplus_{\ell\in L}{A_{\ell}})}}$ and
$\Delta_{k}\vdash^{\mathsf{B}}c_{k}:E_{k}$ where
$E_{k}=\mathbin{\binampersand}_{\ell\in L}{E_{\ell}}$ and
$E_{\\#\mathsf{l}}=\Box$, so that $B=\mathbf{E}_{k};\overline{A}$ and
$\Delta_{i}\vdash c_{i}:E_{i}$ for $i\leq k$.

See 2

###### Proof

We have
${\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;\Gamma$ derived from [TCut${\mathbf{1}}$] (a) or
[TCut$!$] (b). In case (a)
${\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}}\;[{\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;\Gamma$ with
$c_{k}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\checkmark}$.
We conclude by Lemma 1 . In case (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{!}}x(z);R\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:!A\;[{\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;\Gamma$ with
$c_{k}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,R)$.
By Lemma 1,
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(z);R\vdash
z:!A;\Gamma$, so $\Gamma;\vdash
c_{k}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,R):?\overline{A}$
and we conclude with $B=\mathbf{E}_{k-1};C$ and $C=?\overline{A}$.

See 3

###### Proof

If $A$ is void then immediate by Lemma 2. If $A$ is negative, 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}}$.

See 4.1

###### 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.

(Case [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
$F_{1}={\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{|}}\
F_{2}\\}$ with $F_{1}\vdash^{\mathsf{B}}\Delta_{1},x{:}B;\Gamma$ and
$q_{1}=\overline{d_{l}}$. By Lemma 1,
$Q^{\prime}\vdash^{\mathsf{B}}\Delta_{Q},z{:}A;\Gamma$,
$\Gamma;\Delta^{\prime}_{j}\vdash d_{j}:F_{j}$ and
$\overline{B}=\mathbf{F}_{l};\overline{A}$ and
$\Delta_{1}=\Delta^{\prime}_{1},\ldots,\Delta^{\prime}_{l},\Delta_{Q}$. By
Lemma 1 we get
${\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{|}}z{:}A\;[q_{2}@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$.

(Case of [$\otimes$]) Let
${\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}:A\otimes
C\;[q]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}\vdash^{\mathsf{B}}\Delta;\Gamma$. By Lemma 1,
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(z.P);Q\vdash^{\mathsf{B}}\Delta_{P},x:A$ and $R\vdash\Delta_{R},y:B$ and
$\Delta_{i}\vdash c_{i}:E_{i}$ for $1\leq i\leq k$, and
$B=\mathbf{E}_{k};\overline{(}A\otimes C)$. By inversion [T$\otimes$],
$\Delta_{P}=\Delta^{\prime}_{P},\Delta^{\prime\prime}_{P}$ and
$Q\vdash^{\mathsf{B}}\Delta^{\prime\prime}_{P},x:C;\Gamma$ and
$P\vdash^{\mathsf{B}}\Delta^{\prime}_{P},z:A,\Gamma$. So
$\Gamma;\Delta^{\prime}_{P}\vdash
c_{k+1}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,P):\overline{A}\mathbin{\bindnasrepma}\overline{C}$.
Let $E_{k+1}=\overline{A}\mathbin{\bindnasrepma}\Box$ so
$B=\mathbf{E}_{k+1};\overline{C}$. By Lemma 1,
${\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}:C\;[q@\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{|}}\
R\\}\vdash^{\mathsf{B}}\Delta;\Gamma$.

(Case [$\mathbin{\bindnasrepma}$]) 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\;[\overline{c_{k}}]\;y: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{recv}}\
y(w);Q\\}\vdash^{\mathsf{B}}\Delta$ where
$\overline{c_{k}}=\mathsf{clos}(z,R)@q$. By Lemma 1, $P\vdash\Delta_{P},x:A$
and
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w);Q\vdash^{\mathsf{B}}\Delta_{Q},y:B$ and
$\Delta_{1}\vdash\mathsf{clos}(z,R):T_{1}\mathbin{\bindnasrepma}\Box$ and
$\Delta_{i}\vdash^{\mathsf{B}}c_{i}:E_{i}$ for $2\leq i\leq k$, and
$B=\overline{T}_{1}\mathbin{\bindnasrepma}E_{2}[..E_{k}[\overline{A}]..]$. We
then have $R\vdash^{\mathsf{B}}\Delta_{1},z:T_{1}$. By inversion on
[T$\mathbin{\bindnasrepma}$], $Q\vdash\Delta_{Q},w:\overline{T}_{1},y:C$ where
$C=E_{2}[..E_{k}[\overline{A}]..]$. We consider the case where $T_{1}$ and $A$
are positive, and check that
${\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:C{\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}}\;\\{R_{1}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{z}_{1}:T_{1}\;[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}]\;w:\overline{T}_{1}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\})\\}\vdash^{\mathsf{B}}\Delta$ by [TCutB] on $R_{1}$ and $Q$ and Lemma 1.
Other cases are handled in a similar way.

######  Lemma 10 (Barbs inversion)

Let $P\vdash\Delta;\Gamma$ and $P\downarrow_{x}$.

  1. 1.

If $x\in\Gamma$ then
$P\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{call}}\
x(y);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$, Otherwise $x:A\in\Delta$ and

  2. 2.

$P\equiv{\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{|}}*{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q$, or

  3. 3.

If $A={\mathbf{1}}$ then
$P\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x$.

  4. 4.

If $A=B\otimes C$ then
$P\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(y.Q);R$.

  5. 5.

If $A=\bot$ then
$P\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
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$.

  6. 6.

If $A=B\mathbin{\bindnasrepma}C$ then
$P\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
x(y);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$.

  7. 7.

If $A=?B$ then
$P\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{?}}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$.

  8. 8.

If $A=!B$ then
$P\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(y);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$.

See 4

###### Proof

By induction on the derivation for $P\vdash\Delta;\Gamma$, and case analysis
on the last typing rule.

(Case of [TcutB]) we have
$P={\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{|}}y:\overline{A}\;[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}]\;\overline{z}:A{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P_{2}\\}\vdash^{\mathsf{B}}\Delta^{\prime},\Delta;\Gamma$, derived from
$P_{1}\vdash^{\mathsf{B}}\Delta^{\prime},y:\overline{A};\Gamma$ and
$P_{2}\vdash^{\mathsf{B}}\Delta,z:A;\Gamma$, where $A$ is positive. By the
i.h. we conclude that $P_{2}\to$ or $P_{2}\downarrow_{x_{2}}$. So if
$P_{2}\to$, then $P\to$ . Otherwise, $P_{2}\downarrow_{x_{2}}$. If $x_{2}\neq
z$ then $P\downarrow_{x_{2}}$ with $x_{2}\in\Delta$.

Otherwise $x_{2}=z$. By Lemma 10 (1,2,3), either
$P_{2}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
z\ v\
{\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$ (a), or since $A$ is positive,
$P_{2}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
z$ (b) or
$P_{2}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
z(w.Q);R$ (c).

In case (a) if $v\not\in\Delta$, then $P$ reduces by [fwdp] (both $x_{2}$ and
$v$ are bound in $P$ by cuts), otherwise $v\in\Delta$ and
$P_{2}\downarrow_{v}$ and $P\downarrow_{v}$. In case (b) $P\to$ by
[${\mathbf{1}}$] and in case (c) by [$\otimes$]).

(Case of [TCut$!$]) Let
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.R\
{\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^{\mathsf{B}}\Delta;\Gamma$ derived from
$R\vdash^{\mathsf{B}}y:A;\Gamma$ and
$Q\vdash^{\mathsf{B}}\Delta;\Gamma,x:\overline{A}$. By i.h. either $Q\to$ or
$Q\downarrow_{z}$. If $z\neq x$ then $P\to$ or $P\downarrow_{z}$. If $z=x$
then by Lemma 10
$Q\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{call}}\
x(y);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$ and $P\to$ by [call].

(Case of [TCut$\otimes$]) We have
$P={\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{|}}\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{|}}\
P_{2}\\} \vdash^{\mathsf{B}}\Delta;\Gamma$ where
$q=r@\mathsf{clos}(z_{k};R_{k})$ derived from
$P_{1}\vdash^{\mathsf{B}}x:A,\Delta_{P_{1}};\Gamma$. By i.h. $P_{1}\to$ or
$P_{1}\downarrow_{x_{1}}$. If $x\neq x_{1}$ then $P_{1}\downarrow_{x_{1}}$ and
$P\downarrow_{x_{1}}$. If $A$ is positive, by the same reasoning as above for
$P_{2}$ we conclude that $P\to$ or $P\downarrow_{w}$.

Otherwise, $A$ is negative. By i.h. $P_{2}\to$ or $P_{2}\downarrow_{z}$. If
$z\neq y$ then $P\downarrow_{x}$. Otherwise, $P_{2}\downarrow_{y}$. By Lemma
1, $B=\overline{T}\mathbin{\bindnasrepma}C$. By Lemma 10 (2,6), either
$P_{2}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
y\ v\
{\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{|}}\
Q^{\prime}$ (a) or
$P_{2}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w);Q^{\prime}\
{\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{|}}\
Q^{\prime\prime}$ (b). For case (a) we conclude as in [TCutB] above that
$P\to$ or $P\downarrow_{v}$, for case (b) $P\to$ by
[$\mathbin{\bindnasrepma}$].

(Case of [TCut$\oplus$]) Similar to [TCut$\otimes$]

(Case of [TCut${\mathbf{1}}$]) Let
$P={\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]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P_{2}\\} \vdash^{\mathsf{B}}\Delta;\Gamma$ where
$q=r@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\checkmark}$
derived from
${\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}}\;[{r}]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P_{2}\\} \vdash^{\mathsf{B}}\Delta;\Gamma$. By i.h. $P_{2}\to$ or
$P_{2}\downarrow_{z}$. If $z\neq y$ then $P\downarrow_{x}$. Otherwise,
$P_{2}\downarrow_{y}$. By Lemma 2, either
$B=\overline{T}\mathbin{\bindnasrepma}C$ (a) or $B=\bot$ (b). If
$P_{2}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
y\ v\
{\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{|}}\
Q^{\prime}$, then as for [TCutB] we conclude that $P\to$ or $P\downarrow_{v}$.
For (a), by Lemma 10 (6),
$P_{2}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w);Q^{\prime}\
{\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{|}}\
Q^{\prime\prime}$, and $P\to$ by [$\mathbin{\bindnasrepma}$]. For (b), by
Lemma 10 (5),
$P_{2}\equiv{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
y;Q^{\prime}\
{\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{|}}\
Q^{\prime\prime}$, and $P\to$ by [$\bot$].

###  0.A.2 Proofs of Section 4.2: Correspondence between $\mathsf{CLL}$ and
$\mathsf{CLLB}$

We give some examples of commutations used in the proofs, those for other
pairs
${\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}p}\;}/{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;{}$
are checked in a similar way.

###### Lemma 11

Commutation (pos-neg-promote):

$\begin{array}[]{lll}{\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.R);P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[c@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);Q\\}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}p}}\\\
{\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}\;[c@q@v]\;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);Q\\}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}{}}\\\
{\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}\;[q@v]\;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}}\;\\{S\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}u[]w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\\}\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{send}}\
x(z.R);P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[c@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);Q\\}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}{}}\\\
{\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.R);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{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{R\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}s[]u{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\\}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}p}}\\\
{\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}\;[q@v]\;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}}\;\\{S\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}u[]w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\\}\end{array}$

###### Lemma 12

Commutation (pos-neg-seq-commute):

$\begin{array}[]{lll}E_{1}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{X\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}c\;[q_{1}]\;\overline{a}{\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{send}}\
a(z.R);{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
b(w);Q\\}]{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}p}}\\\
E_{2}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{Y}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{d}\;[c@q_{2}]\;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{recv}}\
b(w);Q\\}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;{}E_{3}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Y\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[q@v]\;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}}\;\\{S\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}u[]w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\\}]\vspace{8pt}\\\
E_{1}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{X\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}c\;[q_{1}]\;\overline{a}{\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{send}}\
a(z.R);{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
b(w);Q\\}]\equiv\\\
E_{2}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{X\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{d}\;[c@q_{2}]\;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{recv}}\
b(w);{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
a(z.R);Q\\}]{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}{}}\\\
F_{3}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Z\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}c\;[q_{1}]\;\overline{a}{\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}}\;\\{S\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}u[]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{send}}\
a(z.R);Q\\}\\}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}p}}\\\
E_{3}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{Y\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[q@v]\;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}}\;\\{S\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}u[]w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\\}]\end{array}$

###### Lemma 13

Commutation (fwd-neg-comm):

$\begin{array}[]{lll}E[{\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{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}\;[c@q_{2}]\;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{recv}}\
b(w);Q\\}]{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}a}{}}\\\
E[{\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{z}\;[c@q_{2}@q_{1}]\;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{recv}}\
b(w);Q\\}]{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}{}}\\\
E[{\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{z}\;[q_{2}@q_{1}]\;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}}\;\\{S\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}u[]w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\\}]\\\ \\\
E[{\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{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}\;[c@q_{2}]\;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{recv}}\
b(w);Q\\}]{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}{}}\\\
E[{\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{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}]\;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}}\;\\{S\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}u[]w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\\}]{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}a}{}}\\\
E[{\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{z}\;[q_{2}@q_{1}]\;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}}\;\\{S\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}u[]w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\\}]\end{array}$

See 5

###### Proof

(1) Either (a) the reductions are in the same cut, or (b) the reductions are
in different cuts. For (a), if reductions match we conclude. Otherwise they
commute (by Lemma 11 ) so
$P_{1}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;S{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}p}\;}P_{2}$
for some $S$. For (b), if reductions are independent (different threads),
commute, and we conclude. If the reductions are dependent (same thread), they
commute (by Lemma 12) and we conclude.

(2) We consider two cases: either (a) the reductions are in the same cut, or
(b) the reductions are in different cuts. For (a), the reductions commute (by
Lemma 13), so we have
$P{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;{}S{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;Q$
for some $S$. For (b), the reductions are independent and commute.

(3) By (1) and (2).

(4) Assume
$P_{1}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}p}\;}N$. Since
the reductions in $S\to^{\mathsf{Br}}{}P_{2}$ must act on the same cut with an
initially empty queue, and all reductions
$N{\stackrel{{\scriptstyle\epsilon}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;S$
are on empty cuts, the reduction
$P_{1}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}p}\;}N$ must
act on a different cut of all those involved and thus commutes with
$N{\stackrel{{\scriptstyle\epsilon}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;S\to^{\mathsf{Br}}{}P_{2}$,
and we conclude (b). If
$P_{1}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;{}S$ then
either this redex generates one empty cut, so
$P_{1}{\stackrel{{\scriptstyle\epsilon}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;S$,
and we conclude (a), or ,as in (b), it must be independent of
$N{\stackrel{{\scriptstyle\epsilon}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;S\to^{\mathsf{Br}}{}P_{2}$.

See 6

###### Proof

Each cut reduction of $\mathsf{CLL}$ is simulated by two reduction steps of
$\mathsf{B}$ in sequence: [$\otimes\mathbin{\bindnasrepma}$] by [$\otimes$]
followed by [$\mathbin{\bindnasrepma}$]; [${\mathbf{1}}\bot$] by
[${\mathbf{1}}$] followed by [$\bot$]; [$!?$] by [$!$] followed by [$?$]. In a
closed $\mathsf{CLL}$ process a [fwd] reduction has the form
${\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:A{\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{|}}y:{A}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P}\\}\to{\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:A{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
\\{x/y\\}P\\}$, which, for $A{+}$, reduces by [fwdB] as
${\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}{:}{A}\;[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}]\;z{:}\overline{A}{\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}}\
z\ w\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{w}\;[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}]\;y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P\\}\to_{a}{\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}{:}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{|}}\
P\\}$.

See 7

###### Proof

By induction on
$P({\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{})^{*}P^{\prime}$.

(Base) We have $P\equiv
P^{\prime}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;Q$,
hence (1).

(Inductive) Case
$P{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}P^{\prime}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;Q$.
Let (r0)
$P{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}P^{\prime}$.

By i.h. for $P^{\prime}$ there is $R^{\prime}$ so that (c1)
$P^{\prime}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;R^{\prime}$
and
$R^{\prime}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}Q$,
or (c2) $P^{\prime}\to^{\mathsf{Br}}{}R^{\prime}$ and
$R^{\prime}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}{\;}Q$,
or (c3)
$P^{\prime}{\stackrel{{\scriptstyle\epsilon}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;\to^{\mathsf{Br}}{}R^{\prime}$
and
$R^{\prime}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}Q$
.

Case (c1). We have
$P{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}P^{\prime}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;R^{\prime}$
and
$R^{\prime}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}{\;}Q$.

By Lemma 5 (3) on
$P{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}P^{\prime}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;R^{\prime}$,
either $P\to^{\mathsf{Br}}{}R^{\prime}$ and we conclude (2) ($R=R^{\prime}$)
or there is $R$ such that
$P{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;{}R{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;R^{\prime}$
and we conclude (1).

Case (c2). We have
$P{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}P^{\prime}\to^{\mathsf{Br}}{}R^{\prime}$
and
$R^{\prime}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}{\;}Q$.
By Lemma 5 (4) either (a)
$P{\stackrel{{\scriptstyle\epsilon}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;P^{\prime}\to^{\mathsf{Br}}{}R^{\prime}$
or (b)
$P\to^{\mathsf{Br}}{}R^{\prime\prime}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}R^{\prime}$
for some $R^{\prime\prime}$. In case (a) we conclude (3) ($R=R^{\prime}$), in
case (b) we conclude (2) ($R=R^{\prime\prime}$).

Case (c3). We have
$P{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}P^{\prime}{\stackrel{{\scriptstyle\epsilon}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;\to^{\mathsf{Br}}{}R^{\prime}$
and
$R^{\prime}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}Q$.
By Lemma 5 (4) either (a)
$P{\stackrel{{\scriptstyle\epsilon}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;P^{\prime}$
or (b)
$P\to^{\mathsf{Br}}{}R^{\prime\prime}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;R^{\prime}$.
In case (a)
$P{\stackrel{{\scriptstyle\epsilon}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;\to^{\mathsf{Br}}{}R^{\prime}$
we conclude (3) ($R=R^{\prime}$), in case (b) we conclude (2)
($R=R^{\prime\prime}$).

See 4.3

###### Proof

1\. Iterating Lemma 6. 2\. We first check (A) if
$P^{\dagger}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;Q$
then either there is $R$ such that $P\to R$ and
$R^{\dagger}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}Q$
or there is $R$ such that $P\to R$ and
$R^{\dagger}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;Q$.
Subproof: Assume
$P^{\dagger}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}{\stackrel{{\scriptstyle}}{{\to}}{\\!\\!\\!\;}^{\mathsf{B}n}}\;Q$.
By Lemma 7 either (2) $P^{\dagger}\to^{\mathsf{Br}}{}R^{\prime}$ and
$R^{\prime}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}{\;}Q$
for some $R^{\prime}$, or (3)
$P^{\dagger}{\stackrel{{\scriptstyle\epsilon}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;\to^{\mathsf{Br}}{}R^{\prime}$
and
$R^{\prime}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}Q$
for some $R^{\prime}$ ((1) cannot apply, since in $P^{\dagger}$ all queues are
empty). In case (a) we have $P\to R$ and
$R^{\prime}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}Q$
with $R^{\prime}=R^{\dagger}$ for some $R$ since all cuts are empty in
$R^{\prime}$. In case (b)
$P^{\dagger}{\stackrel{{\scriptstyle\epsilon}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{B}a}}\;P^{\prime}\to^{\mathsf{Br}}{}R^{\prime}$
and
$R^{\prime}{\stackrel{{\scriptstyle}}{{\Rightarrow}}{\\!\\!\\!\;}^{\mathsf{Bap}}}\;{}Q$.
Then $P\Rightarrow Q$ by [fwd] and $Q\to R^{\prime}$, for some $Q$ where
$Q^{\dagger}=P^{\prime}$. So $P\Rightarrow R^{\prime}$ and
$R^{\prime}=R^{\dagger}$ for some $R$ since all cuts are empty in
$R^{\prime}$. To conclude (2), we iterate (A).

###  0.A.3 Proofs of Section 5: Correctness of the core SAM

######  Lemma 14 (Sanity)

1\. Let $(P,H)\Mapsto(P^{\prime},H^{\prime})$. Then if
$\mathsf{fn}(P)\subseteq dom(H)$ then $\mathsf{fn}(P^{\prime})\subseteq
dom(H^{\prime})$.

Lemma 16 (2) below expresses a useful invariant of session records in machine
states encoding well-typed processes: The right (reader) endpoint is of
negative type. The left (writer) endpoint is of positive type unless
$P={{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$
or $x\in\mathsf{fn}(P)$.

######  Lemma 15 (Soundness)

Let $P\vdash^{\mathsf{B}}\emptyset$.

1\. If $enc(P)\Mapsto D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$
then there is $Q$ such that $P\to\cup\equiv Q$ and $C=enc(Q)$.

2\. Let $P(H)$ denote property: If $x{:}A\\!\left<q,P\right>\\!y{:}B\in H$
then $B-$ and if ($x\in\mathsf{fn}(P)$ or
$P={{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$)
then $A-$ else $A+$.

Then if $enc(P)=(\mathcal{A},H)\Mapsto(Q,H^{\prime})$ and $P(H)$ then
$P(H^{\prime})$.

###### Proof

(1) Let $enc(P)\Mapsto D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$.
Let $enc(P)=(\mathcal{A},H)$ for some action $\mathcal{A}$. Then $P\equiv
E[\mathcal{A}]$ for some cut context $E[-]$. We consider each reduction
$\Mapsto$.

(Case of [Sfwd]) Let
$enc(P)=({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\
y,H[z{:}A\\!\left<q_{1},P_{1}\right>\\!x][y\\!\left<q_{2},P_{2}\right>\\!w])\Mapsto
D$ where
$D=(P_{2},H[z\\!\left<q_{2}@q_{1},P_{1}\right>\\!w])\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$.
By (2) since $P_{1}(z)$, then $A^{-}$. Therefore $P\equiv
E[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y] \equiv
E^{\prime}[{\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{|}}\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{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}\;[q_{1}]\;w]{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P_{2}\\}\\}]$. Then $P\to Q\equiv
E^{\prime}[{\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{|}}\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_{2}\\}]$ and $enc(Q)=C$.

(Case of [S${\mathbf{1}}$]) Let
$enc(P)=({\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,R\right>\\!y])\Mapsto(R,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])=D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$.
Therefore, $P\equiv
E[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x] \equiv
E^{\prime}[{\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{|}}\
R\\}]$ and $P\to
Q=E^{\prime}[{\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@\checkmark]\;y]{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}]$ and $enc(Q)=C$.

(Case of [S$\bot$]) Let
$enc(P)=({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
y;R,{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
D$ and $D=(R,{H})$.

Hence, $P\equiv
E[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
y;R] \equiv
E^{\prime}[{\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\;[\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;R\\}]\to Q=E^{\prime}[R]$ and
$D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$ and $enc(Q)=C$.

(Case of [S$-$]) Let
$enc(P)=(\mathcal{A}^{-}(x),\mathcal{H}[x{:}A\\!\left<{q},R\right>\\!y])\Mapsto
D$ with

$D=(R,H[x\\!\left<{q},\mathcal{A}^{-}(x)\right>\\!y])$. By typing $A-$ and
$x\in\mathsf{fn}(\mathcal{A}^{-}(x))$. Hence (2).

Hence, $P\equiv E[A^{-}(x)] \equiv$

$E^{\prime}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{A^{-}(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{|}}\
R\\}]\equiv Q$ and $D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$ and
$enc(Q)=C$.

(Case of [S$\otimes$]) Let
$enc(P)=({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(z.R);U,H[x\\!\left<q,S\right>\\!y])\Mapsto D$

where
$D=(U,H[x\\!\left<q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,R),S\right>\\!y])$.

So $P\equiv
E[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(z.R);U] \equiv
E^{\prime}[{\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.R);U\
{\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{|}}\
S\\}]\to\\\
E^{\prime}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{U\
{\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,R)]\;y]{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
S\\}]\equiv Q$ and $D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$ and
$enc(Q)=C$.

(Case of [S$\mathbin{\bindnasrepma}$]) Let
$enc(P)=({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w{:}-);U,H[x\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,R)@q,S\right>\\!y])\Mapsto
D$ where
$D=(R,H[z\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},U\right>\\!w][x\\!\left<q\right>^{s}\\!y])$
and $S(x)$ with $x:A$ and $A-$ or
$S={{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$.

So, $P\equiv
E[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w{:}-);U]\equiv
E^{\prime}[{\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{recv}}\
y(w{:}-);U\
{\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}}(z,R)@q]\;y]{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
S\\}]\to Q$. If
$q\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$
then $Q=E^{\prime}[
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{S\
{\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}}\;\\{R\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{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{|}}\
U\\}\\}]$. If
$q={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$,
then $Q=E^{\prime}[
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{S\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x\;[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}]\;\overline{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}}\;\\{R\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{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{|}}\
U\\}\\}]$. In both cases,
$B\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$ and $enc(Q)=C$.

(Case of [S$\oplus$]) Let
$enc(P)=(\\#\mathsf{l};R,H[x\\!\left<q,S\right>\\!y])\Mapsto
D=(R,H[x\\!\left<q@\\#\mathsf{l},S\right>\\!y])$. So $P\equiv
E[\\#\mathsf{l};R] \equiv
E^{\prime}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{\\#\mathsf{l};R\
{\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{|}}\
S\\}]\to
E^{\prime}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{R\