# Fault-Tolerant Multiparty Session Types with Global Escape Loops (Technical Report)

Lukas Bartl, Julian Linne, Kirstin Peters

► To cite this version:

Lukas Bartl, Julian Linne, Kirstin Peters. Fault-Tolerant Multiparty Session Types with Global Escape Loops (Technical Report). Universität Augsburg. 2025. hal-05283766

HAL Id: hal-05283766

https://hal.science/hal-05283766v1

Submitted on 25 Sep 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Fault-Tolerant Multiparty Session Types
with Global Escape Loops
(Technical Report)

Lukas Bartl ID

Julian Linne ID

Kirstin Peters ID

Universität Augsburg, Germany

September 25, 2025

Multiparty session types are designed to abstractly capture the structure of communication protocols and verify behavioural properties. One important such property is progress, i.e., the absence of deadlock. Distributed algorithms often resemble multiparty communication protocols. But proving their properties, in particular termination that is closely related to progress, can be elaborate. Since distributed algorithms are often designed to cope with faults, a first step towards using session types to verify distributed algorithms is to integrate fault-tolerance.

We extend FTMPST—a version of fault-tolerant multiparty session types with failure patterns to represent system requirements for system failures such as unreliable communication and process crashes—by a novel, fault-tolerant loop construct with global escapes that does not require global coordination. Each process runs its own local version of the loop. If a process finds a solution to the considered problem, it does not only terminate its own loop but also informs the other participants via **exit-messages**. Upon receiving an **exit-message**, a process immediately terminates its algorithm. To increase efficiency and model standard fault-tolerant algorithms, these messages are non-blocking, i.e., a process may continue until a possibly delayed **exit-message** is received. To illustrate our approach, we analyse a variant of the well-known rotating coordinator algorithm by Chandra and Toueg.

## 1 Introduction

This is a technical report that provides some additional material and the missing proofs of the paper [1]. Note that this technical report does not repeat the paper [1], but functions as an appendix of [1].

## 2 Fault-Tolerant Types and Processes

The syntax is given in Figure 1 and described in [1].

**Definition 1** (Well-Formedness, Global Type). A global type $G$ is *well-formed* if

(1) it neither contains free nor unguarded type variables,

(2) all loops eval($e$) in $G$ and all iterations of recursion or loops in $G$ are pairwise distinct,

(3) $R(G) = \{1, \dots, |R(G)|\},$

(4) for all its subterms of the form $r_1 \to_r r_2: \langle S \rangle.G'$ or $r_1 \to_u r_2: l\langle S \rangle.G'$, we have $r_1 \neq r_2$,

(5) for all its subterms of the form $r_1 \to_r r_2: \{l_i.G_i\}_{i \in I}$ or $r \to_w R: \{l_i.G_i\}_{i \in I, l_d}$, we have $r_1 \neq r_2$, $r \notin R$, $d \in I$, and the labels $l_i$ are pairwise distinct, and

(6) for all its subterms of the form $G_1 || G_2$, we have $R(G_1) \cap R(G_2) = \emptyset$.

We restrict our attention to well-formed global types.
<table><caption>Figure 1: Syntax of Fault-Tolerant MPST with Global Escape Loops.</caption><thead><tr><th>Global Types</th><th>Local Types</th><th>Processes</th></tr></thead><tbody><tr><td>G ::= r<sub>1</sub> →<sub>r</sub> r<sub>2</sub>:⟨S⟩.G</td><td>T ::= [r<sub>2</sub>]!<sub>r</sub>⟨S⟩.T<br>| [r<sub>1</sub>]?!<sub>r</sub>⟨S⟩.T<br>| [r<sub>2</sub>]!<sub>u</sub>l⟨S⟩.T<br>| [r<sub>1</sub>]?!<sub>u</sub>l⟨S⟩.T</td><td>P ::= <sup>a</sup>[n](s).P | <sup>a</sup>[r](s).P<br>| s[r<sub>1</sub>, r<sub>2</sub>]?!<sub>r</sub>⟨e⟩.P<br>| s[r<sub>2</sub>, r<sub>1</sub>]?!<sub>r</sub>(x).P<br>| s[r<sub>1</sub>, r<sub>2</sub>]?!<sub>u</sub>l⟨e⟩.P<br>| s[r<sub>2</sub>, r<sub>1</sub>]?!<sub>u</sub>l⟨v⟩(x).P</td></tr><tr><td>| r<sub>1</sub> →<sub>u</sub> r<sub>2</sub>:l⟨S⟩.G</td><td>| [r<sub>2</sub>]!<sub>r</sub>{l<sub>i</sub>.T<sub>i</sub>}<sub>i∈I</sub><br>| [r<sub>1</sub>]?!<sub>r</sub>{l<sub>i</sub>.T<sub>i</sub>}<sub>i∈I</sub><br>| [R]!<sub>w</sub>{l<sub>i</sub>.T<sub>i</sub>}<sub>i∈I</sub><br>| [r]?!<sub>w</sub>{l<sub>i</sub>.T<sub>i</sub>}<sub>i∈I,l<sub>d</sub></sub></td><td>| s[r<sub>1</sub>, r<sub>2</sub>]?!<sub>r</sub>.P<br>| s[r<sub>2</sub>, r<sub>1</sub>]?!<sub>r</sub>{l<sub>i</sub>.P<sub>i</sub>}<sub>i∈I</sub><br>| s[r, R]!<sub>w</sub>.P<br>| s[r<sub>j</sub>, r]?!<sub>w</sub>{l<sub>i</sub>.P<sub>i</sub>}<sub>i∈I,l<sub>d</sub></sub></td></tr><tr><td>| r →<sub>w</sub> R: {l<sub>i</sub>.G<sub>i</sub>}<sub>i∈I,l<sub>d</sub></sub></td><td>| (μt, c = n)T | t<br>| end<br>| [R]∞<sup>c</sup><sub>e</sub>{⟨S<sub>0</sub>⟩.G<sub>0</sub>; ⟨S<sub>2</sub>⟩.G<sub>2</sub></sub><br>| call⟨e⟩</td><td>| P<sub>1</sub> | P<sub>2</sub><br>| (μX, c = n)P | X<br>| 0<br>| s[r, R]∞<sup>c=n</sup><sub>e</sub>{⟨x⟩.P<sub>0</sub>}P<sub>1</sub>; (y).P<sub>2</sub><br>| call⟨e, e'⟩ | exit⟨e, e'⟩<br>| if b then P<sub>1</sub> else P<sub>2</sub><br>| (νx)P | ⊥</td></tr><tr><td>| G<sub>1</sub> || G<sub>2</sub></td><td>| [r<sub>2</sub>]!⟨s'[r]:T⟩.T'<br>| [r<sub>1</sub>]?!⟨s'[r]:T⟩.T'</td><td>| s[r<sub>1</sub>, r<sub>2</sub>]!⟨⟨s'[r]⟩⟩.P<br>| s[r<sub>2</sub>, r<sub>1</sub>]?!⟨⟨s'[r]⟩⟩.P<br>| s<sub>r<sub>1</sub>→r<sub>2</sub></sub>:M</td></tr><tr><td>| (μt, c)G | t</td><td>| (μt, c = n)T | t<br>| end<br>| [R]∞<sup>c=n</sup><sub>e</sub>{⟨S<sub>0</sub>⟩.T<sub>0</sub>}T<sub>1</sub>; ⟨S<sub>2</sub>⟩.T<sub>2</sub></td><td>| Messages<br>| m ::= ⟨v⟩<sup>r</sup> | l⟨v⟩<sup>u</sup> | l<sup>r</sup> | l<sup>w</sup><br>| exit⟨id, v⟩ | s[r]</td></tr><tr><td>| end<br>| [R]∞<sup>c=n</sup><sub>e</sub>{⟨S<sub>0</sub>⟩.G<sub>0</sub>; ⟨S<sub>2</sub>⟩.G<sub>2</sub></sub><br>| call⟨e⟩</td><td>| end<br>| [R]∞<sup>c=n</sup><sub>e</sub>{⟨S<sub>0</sub>⟩.T<sub>0</sub>}T<sub>1</sub>; ⟨S<sub>2</sub>⟩.T<sub>2</sub></td><td>| M ::= [] | m#M</td></tr><tr><td>| r<sub>1</sub> → r<sub>2</sub>:⟨s'[r]:T⟩.G</td><td>| [r<sub>2</sub>]!⟨s'[r]:T⟩.T'<br>| [r<sub>1</sub>]?!⟨s'[r]:T⟩.T'</td><td>|</td></tr></tbody></table>

**Definition 2** (Well-Formedness, Local Type). A local type $T$ is *well-formed* if

(1) it neither contains free nor unguarded type variables,

(2) all loops eval(e) in $T$ and all iterations of recursion or loops in $T$ are pairwise distinct, and

(3) for all its subterms of the form $[r]!_r\{l_i.T_i\}_{i \in I}$, $[r]?!_r\{l_i.T_i\}_{i \in I}$, $[R]!_w\{l_i.T_i\}_{i \in I, l_d}$, or $[R]?!_w\{l_i.T_i\}_{i \in I, l_d}$, we have $d \in I$ and the labels $l_i$ are pairwise distinct.

We restrict our attention to well-formed local types.

We denote a global type $G$ as *projectable* if for all $r \in R(G)$ the projection $G|_r$ is defined. We restrict our attention to projectable global types. Projection maps well-formed global types onto the respective local type for a given role $p$, where the results of projection—if defined—are again well-formed.

## 3 A Semantics with Failure Patterns for Global Escape Loops

The reduction semantics is given in Figure 2 and described in [1].

## 4 Typing Fault-Tolerant Processes

A type judgement is of the form $\Gamma, \Theta \vdash P \triangleright \Delta$, where $\Gamma$ is a global environment, $\Theta$ is a loop environment, $P \in \mathcal{P}$ is a process, and $\Delta$ is a session environment. A process $P$ is *well-typed* w.r.t. $\Gamma$ and $\Delta$ if $\Gamma \vdash P \triangleright \Delta$ can be derived from the rules in the Figures 3 and 4. We write $\text{nsr}(\Delta)$ (or $\text{unr}(\Delta)$) if for all types $T$ in $\Delta$ we have $\text{nsr}(T)$ (or $\text{unr}(T)$) and if $\Delta$ does not contain message queues. With $\Gamma \Vdash y:S$ we check that $y$ is an expression of the sort $S$ if all names $x$ in $y$ are replaced by arbitrary values of sort $S_x$ for $x:S_x \in \Gamma$.

We use *typing rules* to derive type judgements, where we assume that all mentioned global types are well-formed and projectable, all local types are well-formed, and all environments are linear. The new typing rules (highlighted in blue) in the Figures 3 and 4 are described in [1]. The remaining rules are described in [2].
(Init) $\overline{a[n]}(s).P_n \mid \prod_{1 \le i \le n-1} a[i](s).P_i \mapsto (\nu s) \left( \prod_{1 \le i \le n} P_i \mid \prod_{1 \le i,j \le n, i \ne j} s_i \to j \right)$ if $a \ne s$

(RSend) $s[r_1, r_2]!_r \langle e \rangle.P \mid s_{r_1 \to r_2}:M \mapsto P \mid s_{r_1 \to r_2}:M \# \langle v \rangle^r$ if $\text{eval}(e) = v$

(RGet) $s[r_1, r_2]?_r(x).P \mid s_{r_2 \to r_1}:\langle v \rangle^r \# M \mapsto P \{v/x\} \mid s_{r_2 \to r_1}:M$

(USend) $s[r_1, r_2]!_u l \langle e \rangle.P \mid s_{r_1 \to r_2}:M \mapsto P \mid s_{r_1 \to r_2}:M \# l \langle v \rangle^u$ if $\text{eval}(e) = v$

(UGet) $s[r_1, r_2]?_u l \langle dv \rangle(x).P \mid s_{r_2 \to r_1}:l' \langle v \rangle^u \# M \mapsto P \{v/x\} \mid s_{r_2 \to r_1}:M$ if $l \ne l'$, $\text{FP}_{\text{uget}}(s, r_1, r_2, l', \dots)$

(USkip) $s[r_1, r_2]?_u l \langle dv \rangle(x).P \mapsto P \{dv/x\}$ if $\text{FP}_{\text{uskip}}(s, r_1, r_2, l, \dots)$

(ML) $s_{r_1 \to r_2}:l \langle v \rangle^u \# M \mapsto s_{r_1 \to r_2}:M$ if $\text{FP}_{\text{ml}}(s, r_1, r_2, l, \dots)$

(RSel) $s[r_1, r_2]!_r l.P \mid s_{r_1 \to r_2}:M \mapsto P \mid s_{r_1 \to r_2}:M \# l^r$

(RBran) $s[r_1, r_2]?_r \{l_i.P_i\}_{i \in I} \mid s_{r_2 \to r_1}:l^r \# M \mapsto P_j \mid s_{r_2 \to r_1}:M$ if $l \ne l_j, j \in I$

(WSel) $s[r, R]!_w l.P \mid \prod_{r_i \in R} s_{r \to r_i}:M_i \mapsto P \mid \prod_{r_i \in R} s_{r \to r_i}:M_i \# l^w$

(WBran) $s[r_1, r_2]?_w \{l_i.P_i\}_{i \in I, l_q} \mid s_{r_2 \to r_1}:l^w \# M \mapsto P_j \mid s_{r_2 \to r_1}:M$ if $l \ne l_j, j \in I$

(WSkip) $s[r_1, r_2]?_w \{l_i.P_i\}_{i \in I, l_q} \mapsto P_d$ if $\text{FP}_{\text{wskip}}(s, r_1, r_2, \dots)$

(LStep) $s[r, R] \stackrel{c=n}{\to} [(x).P_0]P_1; (y).P_2 \mid Q \mapsto s[r, R] \stackrel{c=n}{\to} [(x).P_0]P'_1; (y).P_2 \mid Q'$ if $P_1 \mid Q \mapsto P'_1 \mid Q'$, only $MQ_{r \leftrightarrow R}(Q, Q')$

(LCall) $s[r, R] \stackrel{c=n}{\to} [(x).P_0] \text{call} \langle e_l, e_v \rangle; (y).P_2 \mapsto s[r, R] \stackrel{c=\text{eval}(n+1)}{\to} [(x).P_0] (P_0 \{n/c\}) \{v/x\}; (y).P_2$ if $\text{eval}(e) = \text{eval}(e_l), \text{eval}(e_v) = v$

(LExitS) $s[r, R] \stackrel{c=n}{\to} [(x).P_0] \text{exit} \langle e_l, e_v \rangle; (y).P_2 \mid \prod_{r_i \in R} s_{r \to r_i}:M_i \mapsto P_2 \{v/y\} \mid \prod_{r_i \in R} s_{r \to r_i}:M_i \# \text{exit} \langle id, v \rangle$ if $\text{eval}(e) = \text{eval}(e_l) = id, \text{eval}(e_v) = v$

(LExitG) $s[r, R] \stackrel{c=n}{\to} [(x).P_0]P_1; (y).P_2 \mid s_{r' \to r}:\text{exit} \langle id, v \rangle \# M \mapsto P_2 \{v/y\} \mid s_{r' \to r}:M$ if $\text{eval}(e) = id, r' \in R$

(EDrop) $s_{r_2 \to r_1}:\text{exit} \langle id, v \rangle \# M \mapsto s_{r_2 \to r_1}:M$ if $\text{FP}_{\text{drop}}(r, id)$

(Crash) $P \mapsto \perp$ if $\text{FP}_{\text{crash}}(P, \dots)$

(If-T) if $e$ then $P$ else $P' \mapsto P$ if $\text{eval}(e)$ is true

(If-F) if $e$ then $P$ else $P' \mapsto P'$ if $\text{eval}(e)$ is false

(Deleg) $s[r_1, r_2]!_l \langle s'[r] \rangle.P \mid s_{r_1 \to r_2}:M \mapsto P \mid s_{r_1 \to r_2}:M \# s'[r]$

(SRecv) $s[r_1, r_2]?(s'[r])'.P \mid s_{r_2 \to r_1}:s''[r'] \# M \mapsto P \{s''/s'\} \{r'/r\} \mid s_{r_1 \to r_2}:M$

(Par) $P_1 \mid P_2 \mapsto P'_1 \mid P_2$ if $P_1 \mapsto P'_1$

(Res) $(\nu x)P \mapsto (\nu x)P'$ if $P \mapsto P'$

(Rec) $(\mu X, c = n)P \mapsto (P \{n/c\}) \{(\mu X, c=\text{eval}(n+1))P/X\}$

(Struc) $P_1 \mapsto P'_1$ if $P_1 \equiv P_2, P_2 \mapsto P'_2, P'_2 \equiv P'_1$

<caption>Figure 2: Reduction Rules (↔) of Fault-Tolerant Processes with Global Escape Loops.</caption>

**Condition 1 (Failure Pattern).**

1. If $\text{FP}_{\text{crash}}(P, \dots)$ then $\text{nsr}(P)$.

2. The failure pattern $\text{FP}_{\text{uget}}(s, r_1, r_2, l, \dots)$ is always valid.

3. The pattern $\text{FP}_{\text{ml}}(s, r_1, r_2, l, \dots)$ is valid iff $\text{FP}_{\text{uskip}}(s, r_2, r_1, l, \dots)$ is valid.

4. If $\text{FP}_{\text{crash}}(P, \dots)$ and $s[r] \in A(P)$ is an actor then eventually the pattern $\text{FP}_{\text{uskip}}(s, r_2, r, l, \dots)$ and $\text{FP}_{\text{wskip}}(s, r_2, r, l, \dots)$ hold for all $r_2, l$.

5. If $\text{FP}_{\text{crash}}(P, \dots)$ and $s[r] \in A(P)$ then eventually $\text{FP}_{\text{ml}}(s, r_1, r, l, \dots)$ for all $r_1, l$ and $\text{FP}_{\text{drop}}(r, id)$.

6. If $\text{FP}_{\text{wskip}}(s, r_1, r_2, \dots)$ then $s[r_2]$ is crashed, i.e., the system does no longer contain an actor $s[r_2]$ and the message queue $s_{r_2 \to r_1}$ is empty.

7. If $s[r]$ terminated the loop id then eventually $\text{FP}_{\text{ml}}(s, r_1, r, l, \dots)$ for all $r_1, l$ and $\text{FP}_{\text{drop}}(r, id)$.

8. If $\text{FP}_{\text{drop}}(r, id)$ then $r$ terminated the loop id.

The combination of the 8 conditions in Condition 1 might appear quite restrictive. However, these conditions are minimal assumptions on the system requirements, as described in [2].

Let us have a closer look at the typing rules in the Figures 3 and 4. We observe that all typing rules are clearly distinguished by the outermost operator of the process in the conclusion except that there are two typing rules for restriction. With that, given a type judgement $\Gamma, \Theta \vdash P \triangleright \Delta$, we can use the structure of $P$—with a case split for restriction—to reason about the structure of the proof tree that was necessary to obtain $\Gamma, \Theta \vdash P \triangleright \Delta$ and from that derive conditions about the nature of the involved type environments. If $P$ is e.g. a parallel composition $P_1 \mid P_2$ then, since there is only one rule to type parallel compositions (the
<figure><img src="image_2.png" /><figcaption>Figure 3: Typing Rules for Fault-Tolerant Systems with Global Escape Loops.</figcaption></figure>

Rule (Par)), Γ, Θ ⊢ P₁ | P₂ ▷ Δ implies that there are Δ₁, Δ₂ such that Δ = Δ₁ · Δ₂, Γ, Θ ⊢ P₁ ▷ Δ₁, and Γ, Θ ⊢ P₂ ▷ Δ₂. In the following, we write 'by Rule (Par)' as short hand for 'by the clear distinction of the typing rules by the process in the conclusion and Rule (Par) in particular' and similar for the other rules.

In the following we prove some properties of our MPST variant. We start with an auxiliary result, proving that structural congruence preserves the validity of type judgements. The proof is by induction on P ≡ P'. In each case we can use the information about the structure of the process that is provided by the considered rule of structural congruence to conclude on the last few typing rules that had to be applied to derive the type judgement in the assumption. From these partial proof trees we obtain enough information to construct the proof tree for the conclusion. The proof is very similar to the respective proof in [2]. We highlight the differences in blue color.

**Lemma 2** (Subject Congruence). If Γ, Θ ⊢ P ▷ Δ and P ≡ P' then Γ, Θ ⊢ P' ▷ Δ.

*Proof.* The proof is by induction on P ≡ P'.

**Case** P | 0 ≡ P: Assume Γ, Θ ⊢ P | 0 ▷ Δ. By the Rule (Par), then there are Δ<sub>P</sub>, Δ<sub>0</sub> such that Δ = Δ<sub>P</sub> · Δ<sub>0</sub>, Γ, Θ ⊢ P ▷ Δ<sub>P</sub>, and Γ, Θ ⊢ 0 ▷ Δ<sub>0</sub>. Moreover, by Rule (End), Γ, Θ ⊢ 0 ▷ Δ<sub>0</sub> implies that Δ<sub>0</sub> = ∅ and, thus, Δ = Δ<sub>P</sub>. Then also Γ, Θ ⊢ P ▷ Δ.

For the opposite direction assume Γ, Θ ⊢ P ▷ Δ. By Rule (End), Γ, Θ ⊢ 0 ▷ ∅. With Rule (Par) and because Δ = Δ · ∅, then Γ, Θ ⊢ P | 0 ▷ Δ.

**Case** P₁ | P₂ ≡ P₂ | P₁: Assume Γ, Θ ⊢ P₁ | P₂ ▷ Δ. By Rule (Par), then there are Δ<sub>P₁</sub>, Δ<sub>P₂</sub> such that Δ = Δ<sub>P₁</sub> · Δ<sub>P₂</sub> and Γ, Θ ⊢ Pᵢ ▷ Δ<sub>Pᵢ</sub>. By Rule (Par) and since Δ = Δ<sub>P₁</sub> · Δ<sub>P₂</sub> implies Δ = Δ<sub>P₂</sub> · Δ<sub>P₁</sub>,
<figure><img src="image_3.png" /><figcaption>Figure 5: Reduction Rules for Session Environments.</figcaption></figure>
Moreover, types are preserved modulo substitution of names by values of the same sort. The proof is by induction on the typing rules. Again the proof is similar to the proof in [2]. Since we use expression to construct unique identifiers for loops in types, we have to apply the substitution to all parts of the type judgement. In the type environments substitution only affects names and expressions.

**Lemma 3 (Substitution).** If $\Gamma \cdot c:S_c, \Theta \vdash Q \triangleright \Delta$ and $\Gamma \Vdash d:S_c$, then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

*Proof.* The proof is by induction on the derivation of $\Gamma \cdot c:S_c, \Theta \vdash Q \triangleright \Delta$.

(Req) Then, $Q = \bar{a}[n](s).P, a:G \in \Gamma, |R(G)| = n$, and $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta \cdot s[n]:G|_n$. Without loss of generality, assume $s \neq c$. Because of linearity, $a:G \in \Gamma$ implies $a \neq c$. By the induction hypothesis, $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta \cdot s[n]:G|_n$ and $\Gamma \Vdash d:S_c$ imply $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta\{d/c\} \cdot s[n]: (G\{d/c\})|_n$. By (RReq), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(Acc) Then, $Q = a[r](s).P, a:G \in \Gamma, 0 < r < |R(G)|$, and $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta \cdot s[r]:G|_r$. Without loss of generality, assume $s \neq c$. Because of linearity, $a:G \in \Gamma$ implies $a \neq c$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta\{d/c\} \cdot s[r]:G|_r$. By (Acc), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(RSend) Then, $Q = s[r_1, r_2]!_r l\langle y \rangle.P, \Delta = \Delta' \cdot s[r_1]:[r_2]!_r \langle S \rangle.T, \Gamma \cdot c:S_c, \Theta \Vdash y:S$, and $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta' \cdot s[r_1]:T$. Because $\Gamma \cdot c:S_c \Vdash y:S, s \neq c$. With $\Gamma \Vdash d:S_c$, then $\Gamma \Vdash y\{d/c\}:S$ and $\Gamma\{d/c\} \Vdash y\{d/c\}:S$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta'\{d/c\} \cdot s[r_1]:T\{d/c\}$. By (RSend), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(RGet) Then, $Q = s[r_1, r_2]?_r(x).P, \Delta = \Delta' \cdot s[r_1]:[r_2]?_r \langle S \rangle.T, x \nvdash (\Gamma, c, \Delta', s)$, and $\Gamma \cdot c:S_c \cdot x:S, \Theta \vdash P_i \triangleright \Delta' \cdot s[r_1]:T$. Because $\Gamma \cdot c:S_c \cdot x:S, \Theta \vdash P_i \triangleright \Delta' \cdot s[r_1]:T, s \neq c$. By the induction hypothesis, $\Gamma\{d/c\} \cdot x:S, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta'\{d/c\} \cdot s[r_1]:T\{d/c\}$. By (RGet), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(USend) Then, $Q = s[r_1, r_2]!_u l\langle y \rangle.P, \Delta = \Delta' \cdot s[r_1]:[r_2]!_u l'\langle S \rangle.T, l \doteq l'$, $\Gamma \cdot c:S_c \Vdash y:S$, and $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta' \cdot s[r_1]:T$. Because of $\Gamma \cdot c:S_c \Vdash y:S, s \neq c$. With $\Gamma \Vdash d:S_c$, then $\Gamma \Vdash y\{d/c\}:S$ and $\Gamma\{d/c\} \Vdash y\{d/c\}:S$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta'\{d/c\} \cdot s[r_1]:T\{d/c\}$. By (USend), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(UGet) Then, $Q = s[r_1, r_2]?_u l\langle v \rangle(x).P, \Delta = \Delta' \cdot s[r_1]:[r_2]?_u l'\langle S \rangle.T, l \doteq l'$, $\Gamma \cdot c:S_c \Vdash v:S, x \nvdash (\Gamma, c, \Delta', s)$, and $\Gamma \cdot c:S_c \cdot x:S, \Theta \vdash P \triangleright \Delta' \cdot s[r_1]:T$. Because of $\Gamma \cdot c:S_c \Vdash v:S, s \neq c$. With $\Gamma \Vdash d:S_c$, then $\Gamma \Vdash v\{d/c\}:S$ and $\Gamma\{d/c\} \Vdash v\{d/c\}:S$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta'\{d/c\} \cdot s[r_1]:T\{d/c\}$. By (UGet), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(RSel) Then, $Q = s[r_1, r_2]!_r l.P, \Delta = \Delta' \cdot s[r_1]:[r_2]!_r \{l_i.T_i\}_{i \in I}, j \in I, l \doteq l_j$, and $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta' \cdot s[r_1]:T_j$. Because $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta' \cdot s[r_1]:T_j, s \neq c$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta'\{d/c\} \cdot s[r_1]:T_j\{d/c\}$. By (RSel), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(RBran) Then, $Q = s[r_1, r_2]?_w \{l_i.P_i\}_{i \in I_1}, \Delta = \Delta' \cdot s[r_1]:[r_2]?_w \{l_i.T_i\}_{i \in I_2}$, and, for all $j \in I_2$ exists some $i \in I_1$ such that $l_i \doteq l_j$ and $\Gamma \cdot c:S_c, \Theta \vdash P_i \triangleright \Delta' \cdot s[r_1]:T_j$. Fix $j$ and $i$. Because $\Gamma \cdot c:S_c, \Theta \vdash P_i \triangleright \Delta' \cdot s[r_1]:T_j, s \neq c$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P_i\{d/c\} \triangleright \Delta'\{d/c\} \cdot s[r_1]:T_j\{d/c\}$. By (RBran), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(WSel) Then, $Q = s[r, R]!_w l.P, \Delta = \Delta' \cdot s[r]:[R]!_w \{l_i.T_i\}_{i \in I, l_i}, j \in I, l \doteq l_j$, and $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta' \cdot s[r]:T_j$. Because $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta' \cdot s[r]:T_j, s \neq c$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta'\{d/c\} \cdot s[r]:T_j\{d/c\}$. By (WSel), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(W Bran) Then, $Q = s[r_1, r_2]?_w \{l_i.P_i\}_{i \in I_1, l_i}, \Delta = \Delta' \cdot s[r_1]:[r_2]?_w \{l_i.T_i\}_{i \in I_2, l'_i}$, $l_i \doteq l'_i$, and, for all $j \in I_2$ exists some $i \in I_1$ such that $l_i \doteq l_j$ and $\Gamma \cdot c:S_c, \Theta \vdash P_i \triangleright \Delta' \cdot s[r_1]:T_j$. Fix $j$ and $i$. Because $\Gamma \cdot c:S_c, \Theta \vdash P_i \triangleright \Delta' \cdot s[r_1]:T_j, s \neq c$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P_i\{d/c\} \triangleright \Delta'\{d/c\} \cdot s[r_1]:T_j\{d/c\}$. By (WBran), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(If) Then, $Q = \mathbf{if} \ e \ \mathbf{then} \ P \ \mathbf{else} \ P', \Gamma \cdot c:S_c \Vdash e:\mathbb{B}, \Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta$, and $\Gamma \cdot c:S_c, \Theta \vdash P' \triangleright \Delta$. With $\Gamma \Vdash d:S_c$, then $\Gamma \Vdash e\{d/c\}:\mathbb{B}$ and $\Gamma\{d/c\} \Vdash e\{d/c\}:\mathbb{B}$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta\{d/c\}$ and $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P'\{d/c\} \triangleright \Delta\{d/c\}$. By (If), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.
(Deleg) Then $Q = s[r_1, r_2]!\langle\langle s'[r] \rangle\rangle.P$, $\Delta = \Delta' \cdot s[r_1]:[r_2]!\langle s'[r]:T' \rangle.T \cdot s'[r]:T'$, and $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta' \cdot s[r_1]:T$. Because $\Gamma \cdot c:S_c, \Theta \vdash Q \triangleright \Delta, c \neq s$ and $c \neq s'$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta'\{d/c\} \cdot s[r_1]:T\{d/c\}$. By (Deleg), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(SRecv) Then $Q = s[r_1, r_2]?(\langle s'[r] \rangle).P$, $\Delta = \Delta' \cdot s[r_1]:[r_2]?\langle s'[r]:T' \rangle.T$, and $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta' \cdot s[r_1]:T \cdot s'[r]:T'$. Because $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta' \cdot s[r_1]:T \cdot s'[r]:T', c \neq s$ and $c \neq s'$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta'\{d/c\} \cdot s[r_1]:T\{d/c\} \cdot s'[r]:T'\{d/c\}$. By (SRecv), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(Par) Then, $Q = P \mid P'$, $\Delta = \Delta_1 \cdot \Delta_2$, $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta_1$, and $\Gamma \cdot c:S_c, \Theta \vdash P' \triangleright \Delta_2$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta_1\{d/c\}$ and $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P'\{d/c\} \triangleright \Delta_2\{d/c\}$. By (Par), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(Res1) Then, $Q = (\nu x)P, x\sharp(\Gamma, c, \Delta)$, and $\Gamma \cdot c:S_c \cdot x:S, \Theta \vdash P \triangleright \Delta$. By the induction hypothesis, $\Gamma\{d/c\} \cdot x:S, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta\{d/c\}$. By (Res1), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(Rec) Then, $Q = (\mu X, cnt = n)P$, $\Delta = s[r]:(\mu t, cnt = n)T$, $\Gamma \Vdash n:N$, and $\Gamma \cdot c:S_c \cdot cnt:N, \Theta \cdot X:s[r]t \vdash P \triangleright s[r]:T$. Without loss of generality, assume $cnt \neq c$. By the induction hypothesis, $\Gamma\{d/c\} \cdot cnt:N, \Theta\{d/c\} \cdot X:s[r]t \vdash P\{d/c\} \triangleright s[r]:T\{d/c\}$. By (Rec), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(Var) Then, $Q = X, \Theta = \Theta' \cdot X:s[r]:t$, and $\Delta = s[r]:t$. By (Var), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(End) Then, $Q = 0$, $\Delta = \emptyset$, and noLoop($\Theta$). Then noLoop($\Theta\{d/c\}$). By (End), then $\Gamma, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta$.

(Crash) Then, $Q = \perp$ and nsr($\Delta$). By (UCrash), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(Loop) Then, $Q = s[r, R]\infty_e^{cnt=n}[(x).P_0]P_1; (y).P_2$, $\Delta = \Delta' \cdot s[r]:[R]\infty_e^{cnt=n}[(S_0).T_0]T_1; \langle S_2 \rangle.T_2$, we have $x, y\sharp(\Gamma, c, \Delta, s)$, $\Gamma \Vdash n:N$, unr($T_0$), unr($T_1$), $\Gamma \cdot c:S_c \cdot x:S_0 \cdot c:N, e:s[r]\langle S_0, S_2 \rangle \vdash P_0 \triangleright s[r]:T_0$, $\Gamma \cdot c:S_c \cdot c:N, e:s[r]\langle S_0, S_2 \rangle \vdash P_1 \triangleright s[r]:T_1$, and $\Gamma \cdot c:S_c \cdot y:S_2, \Theta \vdash P_2 \triangleright \Delta \cdot s[r]:T_2$. Because of the judgement $\Gamma \cdot c:S_c \cdot x:S_0, e:s[r]\langle S_0, S_2 \rangle \vdash P_0 \triangleright s[r]:T_0$, $s \neq c$. By the induction hypothesis, we have $\Gamma\{d/c\} \cdot x:S_0 \cdot cnt:N, e\{d/c\}:s[r]\langle S_0, S_2 \rangle \vdash P_0\{d/c\} \triangleright s[r]:T_0\{d/c\}$ (program), $\Gamma\{d/c\} \cdot cnt:N, e\{d/c\}:s[r]\langle S_0, S_2 \rangle \vdash P_1\{d/c\} \triangleright s[r]:T_1\{d/c\}$ (loop body), and $\Gamma\{d/c\} \cdot y:S_2, \Theta\{d/c\} \vdash P_2\{d/c\} \triangleright \Delta\{d/c\} \cdot s[r]:T_2\{d/c\}$ (loop continuation). By (Loop), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(Call) Then, $Q = \text{call}\langle e, e_v \rangle$, $\Theta = \Theta' \cdot e:s[r]\langle S_0, S_2 \rangle$, $\Delta = s[r]:\text{call}\langle e \rangle$, and $\Gamma \cdot c:S_c \Vdash e_v:S_0$. With $\Gamma \Vdash d:S_c$, then $\Gamma \Vdash e_v\{d/c\}:S_0$ and $\Gamma\{d/c\} \Vdash e_v\{d/c\}:S_0$. By (Call), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(Exit) Then, $Q = \text{exit}\langle e, e_v \rangle$, $\Theta = \Theta' \cdot e:s[r]\langle S_0, S_2 \rangle$, $\Delta = s[r]:T_1$, and $\Gamma \cdot c:S_c \Vdash e_v:S_2$. With $\Gamma \Vdash d:S_c$, then $\Gamma \Vdash e_v\{d/c\}:S_2$ and $\Gamma\{d/c\} \Vdash e_v\{d/c\}:S_2$. By (Exit), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(Res2) Then, $\{s[r]:G|_r | r \in R(G)\} \cdot \{s_{r \to r'}:[] | r, r' \in R(G') \wedge r \neq r'\} \stackrel{s}{\rightleftharpoons} \Delta'$, $Q = (\nu s)P, s\sharp(\Gamma, c, \Delta)$, $a:G \in \Gamma$, and $\Gamma \cdot c:S_c, \Theta \vdash P \triangleright \Delta \cdot \Delta'$. Since Figure 5 does not pose any requirements on expressions except that they have to coincide on loops and matching exit-messages, $\{s[r]:G\{d/c\}|_r | r \in R(G\{d/c\})\} \cdot \{s_{r \to r'}:[] | r, r' \in R(G'\{d/c\}) \wedge r \neq r'\} \stackrel{s}{\rightleftharpoons} \Delta'\{d/c\}$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash P\{d/c\} \triangleright \Delta\{d/c\} \cdot \Delta'\{d/c\}$. By (ResS), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(MQComR) Then, $Q = s_{r_1 \to r_2}:\langle v \rangle^r \#M, \Delta = s_{r_1 \to r_2}:\langle S \rangle^r \#MT, \Gamma \cdot c:S_c \Vdash v:S$, and $\Gamma \cdot c:S_c, \Theta \vdash s_{r_1 \to r_2}:M \triangleright s_{r_1 \to r_2}:MT$. Because $\Gamma \cdot c:S_c \Vdash v:S, s \neq c$. With $\Gamma \Vdash d:S_c$, then $\Gamma \Vdash v\{d/c\}:S$ and $\Gamma\{d/c\} \Vdash v\{d/c\}:S$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash s_{r_1 \to r_2}:M\{d/c\} \triangleright s_{r_1 \to r_2}:MT\{d/c\}$. By (MQComR), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(MQComU) Then, $Q = s_{r_1 \to r_2}:l\langle v \rangle^u \#M, \Delta = s_{r_1 \to r_2}:l'\langle S \rangle^u \#MT, l \doteq l'$, $\Gamma \cdot c:S_c \Vdash v:S$, and $\Gamma \cdot c:S_c, \Theta \vdash s_{r_1 \to r_2}:M \triangleright s_{r_1 \to r_2}:MT$. Because $\Gamma \cdot c:S_c \Vdash v:S, s \neq c$. With $\Gamma \Vdash d:S_c$, then $\Gamma \Vdash v\{d/c\}:S$ and $\Gamma\{d/c\} \Vdash v\{d/c\}:S$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash s_{r_1 \to r_2}:M\{d/c\} \triangleright s_{r_1 \to r_2}:MT\{d/c\}$. By (MQComU), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(MQBranR) Then, $Q = s_{r_1 \to r_2}:^r \#M, \Delta = s_{r_1 \to r_2}:l'^r \#MT, l \doteq l'$, and $\Gamma \cdot c:S_c, \Theta \vdash s_{r_1 \to r_2}:M \triangleright s_{r_1 \to r_2}:MT$. Because $\Gamma \cdot c:S_c, \Theta \vdash s_{r_1 \to r_2}:M \triangleright s_{r_1 \to r_2}:MT, s \neq c$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash s_{r_1 \to r_2}:M\{d/c\} \triangleright s_{r_1 \to r_2}:MT\{d/c\}$. By (MQBranR), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.
(MQBranW) Then, $Q = s_{r_1 \to r_2}:l^w \# M, \Delta = s_{r_1 \to r_2}:l'^w \# MT, l \doteq l', \text{ and } \Gamma \cdot c:S_c, \Theta \vdash s_{r_1 \to r_2}:M \triangleright s_{r_1 \to r_2}:MT.$
Because $\Gamma \cdot c:S_c \vdash s_{r_1 \to r_2}:M \triangleright s_{r_1 \to r_2}:MT, s \neq c$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash s_{r_1 \to r_2}:M\{d/c\} \triangleright s_{r_1 \to r_2}:MT\{d/c\}$. By (MQBranW), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(MQDeleg) Then $Q = s_{r_1 \to r_2}:s'[r] \# M, \Delta = s_{r_1 \to r_2}:s'[r] \# MT$, and $\Gamma \cdot c:S_c, \Theta \vdash s_{r_1 \to r_2}:M \triangleright s_{r_1 \to r_2}:MT$.
Because $\Gamma \cdot c:S_c, \Theta \vdash s_{r_1 \to r_2}:M \triangleright s_{r_1 \to r_2}:MT, s \neq c$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash s_{r_1 \to r_2}:M\{d/c\} \triangleright s_{r_1 \to r_2}:MT\{d/c\}$. By (MQDeleg), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(MQNil) Then, $Q = s_{r_1 \to r_2}:[]$ and $\Delta = s_{r_1 \to r_2}:[]$. By (MQNil), then we have $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$.

(MQExit) Then, $Q = s_{r_1 \to r_2}:\text{exit}(e, v) \# M, \Delta = s_{r_1 \to r_2}:\text{exit}(e, S) \# MT, \Gamma \cdot c:S_c \Vdash v:S$, and $\Gamma \cdot c:S_c, \Theta \vdash s_{r_1 \to r_2}:M \triangleright s_{r_1 \to r_2}:MT$. Because $\Gamma \cdot c:S_c \Vdash v:S, s \neq c$. With $\Gamma \Vdash d:S_c$, then $\Gamma \Vdash v\{d/c\}:S$ and $\Gamma\{d/c\} \Vdash v\{d/c\}:S$. By the induction hypothesis, $\Gamma\{d/c\}, \Theta\{d/c\} \vdash s_{r_1 \to r_2}:M\{d/c\} \triangleright s_{r_1 \to r_2}:MT\{d/c\}$. By (MQExit), then $\Gamma\{d/c\}, \Theta\{d/c\} \vdash Q\{d/c\} \triangleright \Delta\{d/c\}$. $\square$

Subject reduction tells us that derivatives of well-typed systems are again well-typed. This ensures that our formalism can be used to analyse processes by static type checking. We extend subject reduction such that it provides some information on how the session environment evolves alongside reductions of the system using $\stackrel{s}{\rightleftharpoons}$. In Figure 5 we define the relation $\stackrel{s}{\rightleftharpoons}$ between session environments that emulates the reduction semantics.

**Definition 3 (Coherence).** The type environments $\Gamma, \Delta$ are coherent if, for all session channels $s$ in $\Delta$, there exists a global type $G$ in $\Gamma$ such that the restriction of $\Delta$ on assignments with $s$ is the set $\Delta'$ such that:

$$ \{s[r]:G|_r \mid r \in R(G)\} \cdot \{s_{r \to r'}:[\dots] \mid r, r' \in R(G)\} \stackrel{s}{\Longrightarrow} \Delta' $$

We use $\stackrel{s}{\Longrightarrow}$ in the above definition to define coherence for systems that already performed some steps.

**Theorem 4 (Subject Reduction).** If $\Gamma, \Delta$ are coherent, $\Gamma, \Theta \vdash P \triangleright \Delta$, and $P \mapsto P'$, then there is some $\Delta'$ such that $\Gamma, \Theta \vdash P' \triangleright \Delta'$.

For the proof of subject reduction (Theorem 4) we further strengthen its goal and show additionally that there is some $s$ such that $\Gamma, \Delta'$ is coherent and $\Delta \stackrel{s}{\Longrightarrow} \Delta'$, i.e., that the session environment evolves by mimicking the respective reduction step and that this emulation reduces the session environment modulo $\stackrel{s}{\Longrightarrow}$ w.r.t. a single session $s$. Moreover we use an additional goal—with weak coherence instead of coherence—to obtain a stronger induction hypothesis for the case of Rule (Par).

**Definition 4 (Weak Coherence).** The type environments $\Gamma, \Delta$ are weakly coherent if there exists some $\Delta'$ such that $\Gamma, \Delta \cdot \Delta'$ are coherent.

Ultimately, we are however interested into coherence. Note that obviously the coherent case implies the respective weakly coherent case. Our strengthened goal for subject reduction thus becomes:

$$
\begin{align*}
& \Gamma, \Theta \vdash P \triangleright \Delta \wedge \Gamma, \Delta \text{ are coherent } \wedge P \mapsto P' \longrightarrow \\
& \exists \Delta'. \Gamma, \Theta \vdash P' \triangleright \Delta' \wedge \Gamma, \Delta' \text{ are coherent } \wedge \Delta \stackrel{s}{\Longrightarrow} \Delta' \\
& \text{and} \\
& \Gamma, \Theta \vdash P \triangleright \Delta \wedge \Gamma, \Delta \text{ are weakly coherent } \wedge P \mapsto P' \longrightarrow \\
& \exists \Delta'. \Gamma, \Theta \vdash P' \triangleright \Delta' \wedge \Gamma, \Delta' \text{ are weakly coherent } \wedge \Delta \stackrel{s}{\Longrightarrow} \Delta'
\end{align*}
$$

The proof is again similar to the proof in [2] and we highlight the differences in blue colour.

*Proof of Theorem 4.* The proof is by induction on the reduction $P \mapsto P'$ that is derived from the rules of Figure 2.
**Case of Rule (Init)** In this case

$$P = \bar{a}[n](s) \cdot Q_n \mid \prod_{1 \le i \le n-1} a[i](s) \cdot Q_i$$

$$P' = (\nu s) P''$$

$$P'' = \prod_{1 \le i \le n} Q_i \mid \prod_{1 \le i,j \le n, i \ne j} s_{i \to j}$$

$a \neq s$, and we use alpha conversion to ensure that $s_{\#}^s(\Gamma, \Delta)$. By the typing Rules (Par), (Req), and (Acc), $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $G, \Delta_{Q_1}, \dots, \Delta_{Q_n}$ such that $\Delta = \Delta_{Q_1} \dots \Delta_{Q_n}$, $a:G \in \Gamma$, $\Gamma \vdash Q_i \triangleright \Delta_{Q_i} \cdot s[i]:G|_i$ for all $1 \le i \le n$, and $|R(G)| = n$. By Rule (MQNil), $\Gamma, \Theta \vdash s_{i \to j} : [] \triangleright s_{i \to j} : []$ for all $i, j \in R(G)$ with $i \neq j$. Since $s_{\#}^s \Delta$, the composition $\Delta \cdot \Delta_s$ for $\Delta_s = \{s[i]:G|_i, s_{i \to j} : [] | i, j \in R(G) \wedge i \neq j\}$ is defined. By Rule (Par), then $\Gamma, \Theta \vdash P'' \triangleright \Delta \cdot \Delta_s$. By Rule (T-Res2), where we use reflexivity to obtain $\Delta_s \iff \Delta_s$, then $\Gamma, \Theta \vdash P' \triangleright \Delta$.

Since $\Delta' = \Delta$, $\Gamma, \Delta'$ is coherent and, by reflexivity, $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$.

**Case of Rule (RSend)** Here $P = s[r_1, r_2]_!r \langle y \rangle \cdot Q \mid s_{r_1 \to r_2} : \mathbf{M}, \text{eval}(y) = v$, and $P' = Q \mid s_{r_1 \to r_2} : \mathbf{M} \# \langle v \rangle^r$. By the Rules (Par), (RSend), and the typing rules for message queues, $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $\Delta_Q, S, T, \mathbf{MT}$ such that $\Delta = \Delta_Q \cdot s[r_1]:[r_2]_!r \langle S \rangle \cdot T \cdot s_{r_1 \to r_2} : \mathbf{MT}, \Gamma \vdash y:S, \Gamma, \Theta \vdash Q \triangleright \Delta_Q \cdot s[r_1]:T$, and $\Gamma, \Theta \vdash s_{r_1 \to r_2} : \mathbf{M} \triangleright s_{r_1 \to r_2} : \mathbf{MT}$. By Rule (MQComR), then $\Gamma, \Theta \vdash s_{r_1 \to r_2} : \mathbf{M} \# \langle y \rangle^r \triangleright s_{r_1 \to r_2} : \mathbf{MT} \# \langle S \rangle^r$. Since $\Delta_Q \cdot s[r_1]:[r_2]_!r \langle S \rangle \cdot T \cdot s_{r_1 \to r_2} : \mathbf{MT}$ is defined, so is $\Delta' = \Delta_Q \cdot s[r_1]:T \cdot s_{r_1 \to r_2} : \mathbf{MT} \# \langle S \rangle^r$. By Rule (Par), then $\Gamma, \Theta \vdash P' \triangleright \Delta'$.

By Rule (T-RSend) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (RGet)** In this case $P = s[r_1, r_2]_?_r(x) \cdot Q \mid s_{r_2 \to r_1} : \langle v \rangle^r \# \mathbf{M}, P' = Q \{v/x\} \mid s_{r_2 \to r_1} : \mathbf{M}$, and we use alpha conversion to ensure that $x_{\#}^s(\Gamma, \Theta, \Delta, s)$. By (Par), (RGet), and the typing rules for message queues, $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $\Delta_Q, S_1, S_2, T, \mathbf{MT}$ such that $\Delta = \Delta_Q \cdot s[r_1]:[r_2]_?_r \langle S_1 \rangle \cdot T \cdot s_{r_2 \to r_1} : \langle S_2 \rangle^r \# \mathbf{MT}, \Gamma \cdot x:S_1, \Theta \vdash Q \triangleright \Delta_Q \cdot s[r_1]:T$, and $\Gamma, \Theta \vdash s_{r_2 \to r_1} : \mathbf{M} \triangleright s_{r_2 \to r_1} : \mathbf{MT}$. Since $\Gamma, \Delta$ are coherent, $S_1 = S_2$. By Lemma 3 and because $x_{\#}^s(\Gamma, \Theta, \Delta, s)$, then $\Gamma, \Theta \vdash Q \{v/x\} \triangleright \Delta_Q \cdot s[r_1]:T$. Since $\Delta_{Q_j} \cdot s[r_1]:[r_2]_?_r \langle S \rangle \cdot T \cdot s_{r_2 \to r_1} : \langle S_2 \rangle^r \# \mathbf{MT}$ is defined, so is $\Delta' = \Delta_Q \cdot s[r_1]:T \cdot s_{r_2 \to r_1} : \mathbf{MT}$. By Rule (Par), then $\Gamma, \Theta \vdash P' \triangleright \Delta'$.

By Rule (T-RGet) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (USend)** Here $P = s[r_1, r_2]_?_u l \langle v \rangle \cdot Q \mid s_{r_1 \to r_2} : \mathbf{M}, \text{eval}(y) = v$, and $P' = Q \mid s_{r_1 \to r_2} : \mathbf{M} \# l \langle v \rangle^u$. By the Rules (Par), (USend), and the typing rules for message queues, $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $\Delta_Q, l', S, T, \mathbf{MT}$ such that $\Delta = \Delta_Q \cdot s[r_1]:[r_2]_?_u l' \langle S \rangle \cdot T \cdot s_{r_1 \to r_2} : \mathbf{MT}, l \doteq l', l' : S \in \Gamma$, $\Gamma \vdash y:S, \Gamma, \Theta \vdash Q \triangleright \Delta_Q \cdot s[r_1]:T$, and $\Gamma, \Theta \vdash s_{r_1 \to r_2} : \mathbf{M} \triangleright s_{r_1 \to r_2} : \mathbf{MT}$. By Rule (MQComU), then $\Gamma, \Theta \vdash s_{r_1 \to r_2} : \mathbf{M} \# l \langle y \rangle^u \triangleright s_{r_1 \to r_2} : \mathbf{MT} \# l' \langle S \rangle^u$. Since $\Delta_Q \cdot s[r_1]:[r_2]_?_u l' \langle S \rangle \cdot T \cdot s_{r_1 \to r_2} : \mathbf{MT}$ is defined, so is $\Delta' = \Delta_Q \cdot s[r_1]:T \cdot s_{r_1 \to r_2} : \mathbf{MT} \# l' \langle S \rangle^u$. By Rule (Par), then $\Gamma, \Theta \vdash P' \triangleright \Delta'$.

By Rule (T-USend) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (UGet)** Here $P = s[r_1, r_2]_?_u l \langle dv \rangle(x) \cdot P \mid s_{r_2 \to r_1} : l' \langle v \rangle^u \# \mathbf{M}, P' = Q \{v/x\} \mid s_{r_2 \to r_1} : \mathbf{M}, l \doteq l'$, and (using alpha conversion) $x_{\#}^s(\Gamma, \Theta, \Delta, s)$. By (Par), (UGet), and the typing rules for message queues, $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $\Delta_Q, S_1, S_2, T, \mathbf{MT}$ such that $\Delta = \Delta_Q \cdot s[r_1]:[r_2]_?_u l'' \langle S_1 \rangle \cdot T \cdot s_{r_2 \to r_1} : l''' \langle S_2 \rangle^u \# \mathbf{MT}, l \doteq l'', l' \doteq l'', l'' : S_1 \in \Gamma, l''' : S_2 \in \Gamma, \Gamma \cdot x : S_1, \Theta \vdash Q \triangleright \Delta_Q \cdot s[r_1]:T, \Gamma \vdash v : S_2$, and $\Gamma, \Theta \vdash s_{r_2 \to r_1} : \mathbf{M} \triangleright s_{r_2 \to r_1} : \mathbf{MT}$. Since $l'' : S_1 \in \Gamma, l''' : S_2 \in \Gamma$, and $l'' \doteq l \doteq l' \doteq l''$, we have $l'' = l'''$ and $S_1 = S_2$. By Lemma 3 and because $x_{\#}^s(\Gamma, \Theta, \Delta, s)$, then $\Gamma, \Theta \vdash Q \{v/x\} \triangleright \Delta_Q \cdot s[r_1]:T$. By Rule (Par), then $\Gamma, \Theta \vdash P' \triangleright \Delta'$.

By Rule (T-UGet) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (USkip)** In this case $P = s[r_1, r_2]_?_u l \langle dv \rangle(x) \cdot P, P' = Q \{dv/x\}$, and we use alpha conversion to ensure that $x_{\#}^s(\Gamma, \Theta, \Delta, s)$. By (UGet), $\Gamma \vdash P \triangleright \Delta$ implies that there are $\Delta_Q, S, T$ such that
$\Delta = \Delta_Q \cdot s[r_1]:[r_2]?_w l'l'S\rangle^u \#M, P' = s_{r_1 \to r_2}:M$. By the typing rules for message queues, $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are S, MT such that $\Delta = s_{r_1 \to r_2}:l'S\rangle^u \#MT, l \doteq l', l':S \in \Gamma$, and $\Gamma, \Theta \vdash P' \triangleright \Delta'$ with $\Delta' = \Delta_Q \cdot s[r_1]:T$. By Lemma 3 and because $x'_d(\Gamma, \Theta, \Delta, s)$, then $\Gamma, \Theta \vdash P' \triangleright \Delta'$ with $\Delta' = \Delta_Q \cdot s[r_1]:T$.

By Rule (T-USkip) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (ML)** In this case $P = s_{r_1 \to r_2}:l\langle v\rangle^u \#M, P' = s_{r_1 \to r_2}:M$. By the typing rules for message queues, $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are S, MT such that $\Delta = s_{r_1 \to r_2}:l'S\rangle^u \#MT, l \doteq l', l':S \in \Gamma$, and $\Gamma, \Theta \vdash P' \triangleright \Delta'$ with $\Delta' = s_{r_1 \to r_2}:MT$.

By Rule (T-ML) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (RSel)** In this case $P = s[r_1, r_2]!_w l.Q \mid s_{r_1 \to r_2}:M$, and $P' = Q \mid s_{r_1 \to r_2}:M \#l^r$. By (Par), (RSel), and the typing rules for message queues, $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $\Delta_Q, I, j, MT$ and for all $i \in I$ there are $l_i, T_i$ such that $\Delta = \Delta_Q \cdot s[r_1]:[r_2]!_r\{l_i, T_i\}_{i \in I} \cdot s_{r_1 \to r_2}:MT, j \in I, l \doteq l_j, \Gamma, \Theta \vdash Q \triangleright \Delta_Q \cdot s[r_1]:T_j$, and $\Gamma, \Theta \vdash s_{r_1 \to r_2}:M \triangleright s_{r_1 \to r_2}:MT$. By Rule (MQBranR), then $\Gamma, \Theta \vdash s_{r_1 \to r_2}:M \#l^r \triangleright s_{r_1 \to r_2}:MT \#l_j^r$. Since $\Delta_Q \cdot s[r_1]:[r_2]!_r\{l_i, T_i\}_{i \in I} \cdot s_{r_1 \to r_2}:MT$ is defined, so is $\Delta' = \Delta_Q \cdot s[r_1]:T_j \cdot s_{r_1 \to r_2}:MT \#l_j^r$. By Rule (Par), then $\Gamma, \Theta \vdash P' \triangleright \Delta'$.

By Rule (T-RSel) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (RBran)** In this case $P = s[r_1, r_2]?_r\{l_i.Q_i\}_{i \in I_1} \mid s_{r_2 \to r_1}:l^r \#M, j \in I_1, l \doteq l_j$, and $P' = Q_j \mid s_{r_2 \to r_1}:M$. By the Rules (Par), (RBran), and the typing rules for message queues, $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $\Delta_Q, I_2, MT, l''$ and for all $i \in I_2$ there are $l'_i, T_i$ such that $\Delta = \Delta_Q \cdot s[r_1]:[r_2]?_r\{l'_i, T_i\}_{i \in I_2} \cdot s_{r_2 \to r_1}:l''^r \#MT, \Gamma, \Theta \vdash s_{r_2 \to r_1}:M \triangleright s_{r_2 \to r_1}:MT, l_j \doteq l'',$ and for all $k \in I_2$ exists some $m \in I_1$ such that $l_m \doteq l'_k, \Gamma, \Theta \vdash Q_m \triangleright \Delta_Q \cdot s[r_1]:T_k$. Since $l \doteq l_j \doteq l''$ and because $\Gamma, \Delta$ are coherent, there is some $n \in I_2$ such that $l_j \doteq l'' = l_n$ and $\Gamma, \Theta \vdash Q_j \triangleright \Delta_Q \cdot s[r_1]:T_n$. Since $\Delta_Q \cdot s[r_1]:[r_2]?_r\{l_i, T_i\}_{i \in I} \cdot s_{r_2 \to r_1}:l''^r \#MT$ is defined, so is $\Delta' = \Delta_Q \cdot s[r_1]:T_n \cdot s_{r_2 \to r_1}:MT$. By Rule (Par), then $\Gamma, \Theta \vdash P' \triangleright \Delta'$.

By Rule (T-RBran) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (WSel)** In this case $P = s[r, R]!_w l.Q \mid \prod_{r_i \in R} s_{r \to r_i}:M$ and $P' = Q \mid \prod_{r_i \in R} s_{r \to r_i}:M_i \#l^w$. Let $R = \{r_1, \dots, n\}$. By the Rules (Par), (WSel), and the typing rules for message queues, $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $\Delta_Q, I, j, MT_1, \dots, MT_n$ and for all $i \in I$ there are $l_i, T_i$ such that $\Delta = \Delta_Q \cdot s[r]:[R]!_w\{l_i, T_i\}_{i \in I} \cdot s_{r \to r_1}:MT \dots s_{r \to r_n}:MT, j \in I, l \doteq l_j, \Gamma, \Theta \vdash Q \triangleright \Delta_Q \cdot s[r]:T_j$, and $\Gamma, \Theta \vdash s_{r \to r_1}:M_1 \triangleright s_{r \to r_1}:MT_1, \dots, \Gamma, \Theta \vdash s_{r \to r_n}:M_n \triangleright s_{r \to r_n}:MT_n$. By Rule (MQBranW), then $\Gamma, \Theta \vdash s_{r \to r_1}:M_1 \#l^w \triangleright s_{r \to r_1}:MT_1 \#l_j^w, \dots, \Gamma, \Theta \vdash s_{r \to r_n}:M_n \#l^w \triangleright s_{r \to r_n}:MT_n \#l_j^w$. Since the session environment $\Delta_Q \cdot s[r]:[R]!_w\{l_i, T_i\}_{i \in I} \cdot s_{r \to r_1}:MT_1 \dots s_{r \to r_n}:MT_n$ is defined, so is $\Delta' = \Delta_Q \cdot s[r]:T_j \cdot s_{r \to r_1}:MT_1 \#l_j^w \dots s_{r \to r_n}:MT_n \#l_j^w$.

By Rule (T-WSel) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (WBran)** Here $P = s[r_1, r_2]?_w\{l_i.Q_i\}_{i \in I_1, l_d} \mid s_{r_2 \to r_1}:l^w \#M, j \in I_1, l \doteq l_j$, and $P' = Q_j \mid s_{r_2 \to r_1}:M$. By the Rules (Par), (WBran), and the typing rules for message queues, $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $\Delta_Q, l'_d, I_2, MT, l''$ and for all $i \in I_2$ there are $l'_i, T_i$ such that $\Delta = \Delta_Q \cdot s[r_1]:[r_2]?_w\{l'_i, T_i\}_{i \in I_2, l'_d} \cdot s_{r_2 \to r_1}:l''^w \#MT, l_d \doteq l'_d, \Gamma, \Theta \vdash s_{r_2 \to r_1}:M \triangleright s_{r_2 \to r_1}:MT, l_j \doteq l'',$ and for all $k \in I_2$ exists some $m \in I_1$ such that $l_m \doteq l'_k, \Gamma, \Theta \vdash Q_m \triangleright \Delta_Q \cdot s[r_1]:T_k$. Since $l \doteq l_j \doteq l''$ and because $\Gamma, \Delta$ are coherent, there is some $n \in I_2$ such that $l_j \doteq l'' = l_n$ and $\Gamma, \Theta \vdash Q_j \triangleright \Delta_Q \cdot s[r_1]:T_n$. Since $\Delta_Q \cdot s[r_1]:[r_2]?_w\{l_i, T_i\}_{i \in I_1, l'_d} \cdot s_{r_2 \to r_1}:l''^w \#MT$ is defined, so is $\Delta' = \Delta_Q \cdot s[r_1]:T_n \cdot s_{r_2 \to r_1}:MT$. By Rule (Par), then $\Gamma, \Theta \vdash P' \triangleright \Delta'$.

By Rule (T-WBran) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (WSkip)** In this case $P = s[r_1, r_2]?_w\{l_i.Q_i\}_{i \in I_1, l_d} \text{ and } P' = Q_d$. By the Rule (WSkip), $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $\Delta_Q, l'_d, I_2$ and for all $i \in I_2$ there are $l'_i, T_i$ such that $\Delta = \Delta_Q \cdot s[r_1]:[r_2]?_w\{l'_i, T_i\}_{i \in I_2, l'_d}, l_d \doteq l'_d$, and for all $k \in I_2$ exists some $m \in I_1$ such that $l_m \doteq l'_k$.
$\Gamma, \Theta \vdash Q_m \triangleright \Delta_Q \cdot s[r_1]:T_k$. Since $l_d \doteq l'_d$, there is some $n \in I_2$ such that $l_d \doteq l'_d = l_n$ and $\Gamma, \Theta \vdash P' \triangleright \Delta'$ with $\Delta' = \Delta_Q \cdot s[r_1]:T_d$.

By Rule (T-WSkip) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (LStep) In this case**

$$P = s[r, R] \infty_e^{c=n} [(x).Q_0] Q_1; (y).Q_2 | Q, \\ P' = s[r, R] \infty_e^{c=n} [(x).Q_0] Q'_1; (y).Q_2 | Q',$$

$Q_1 | Q \longmapsto Q'_1 | Q'$, and only $MQ_{r \leftrightarrow R}(Q, Q')$. By Rules (Par), (Loop), and the typing rules for message queues, $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $\Delta_Q, \Delta_{Q_2}, S_0, S_2, T_0, T_1, T_2$ such that $\Delta = \Delta_{Q_2} \cdot s[r]:[R] \infty_e^{c=n} [(\langle S_0 \rangle.T_0)T_1; \langle S_2 \rangle.T_2 \cdot \Delta_Q, x, y \nparallel (\Gamma, \Delta_{Q_2}, s, e, c, T_0, T_1, T_2)], \Gamma \Vdash n:N, \text{unr}(T_0), \text{unr}(T_1),$

$\Gamma \cdot x:S_0 \cdot c:N, e:s[r] \langle S_0, S_2 \rangle \vdash Q_0 \triangleright s[r]:T_0,$

$\Gamma \cdot c:N, e:s[r] \langle S_0, S_2 \rangle \vdash Q_1 \triangleright s[r]:T_1,$

$\Gamma \cdot y:S, \Theta \vdash Q_2 \triangleright \Delta_{Q_2} \cdot s[r]:T_2, \text{ and}$

$\Gamma, \Theta \vdash Q \triangleright \Delta_Q.$

By Rule (Par), then $\Gamma \cdot c:N, \Theta \cdot e:s[r] \langle S_0, S_2 \rangle \vdash Q_1 | Q \triangleright s[r]:T_1 \cdot \Delta_Q$. Since $\Gamma, \Delta$ are coherent, $\Gamma \cdot c:N, \Theta \cdot e:s[r] \langle S_0, S_2 \rangle$ are weakly coherent. By the induction hypothesis (for the weakly coherent case), $\Gamma \cdot c:N, \Theta \cdot e:s[r] \langle S_0, S_2 \rangle \vdash Q'_1 | Q' \triangleright \Delta'_1$ for some $\Delta'_1$ with $s[r]:T_1 \cdot \Delta_Q \stackrel{s}{\rightleftharpoons} \Delta'_1$. By Rule (Par) and global weakening, then there are $T'_1$ and $\Delta'_Q$ such that $\Delta'_1 = s[r]:T'_1 \cdot \Delta'_Q, \Gamma \cdot c:N, e:s[r] \langle S_0, S_2 \rangle \vdash Q'_1 \triangleright s[r]:T'_1$ and $\Gamma, \Theta \vdash Q' \triangleright \Delta'_Q$. By Rule (Loop), then $\Gamma, \Theta \vdash s[r, R] \infty_e^{c=n} [(x).Q_0] Q'_1; (y).Q_2 \triangleright \Delta_{Q_2} \cdot s[r]:[R] \infty_e^{c=n} [(\langle S_0 \rangle.T_0)T'_1; \langle S_2 \rangle.T_2]$. By Rule (Par), then $\Gamma, \Theta \vdash P' \triangleright \Delta'$ with the resulting session environment $\Delta' = \Delta_{Q_2} \cdot s[r]:[R] \infty_e^{c=n} [(\langle S_0 \rangle.T_0)T'_1; \langle S_2 \rangle.T_2 \cdot \Delta'_Q]$.

Since $s[r]:T_1 \cdot \Delta_Q \stackrel{s}{\rightleftharpoons} s[r]:T'_1 \cdot \Delta'_Q$ and by (T-LStep), then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (LCall) In this case**

$$P = s[r, R] \infty_e^{c=n} [(x).Q_0] \text{call} \langle e_l, e_v \rangle; (y).Q_2, \\ P' = s[r, R] \infty_e^{c=\text{eval}(n+1)} [(x).Q_0] (Q_0\{n/c\}) \{v/x\}; (y).Q_2,$$

$\text{eval}(e) = \text{eval}(e_l)$, and $\text{eval}(e_v) = v$. By the Rules (Loop) and (Call), $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are some $\Delta_{Q_2}, S_0, S_2, T_0, T_1, T_2$ such that $\Delta = \Delta_{Q_2} \cdot s[r]:[R] \infty_e^{c=n} [(\langle S_0 \rangle.T_0)\text{call}\langle e \rangle; \langle S_2 \rangle.T_2$, the variables $x, y, c$ are fresh, i.e., $x, y \nparallel (\Gamma, \Delta_{Q_2}, s, e, c, T_0, T_2)$, $\Gamma \Vdash n:N, \text{unr}(T_0),$

$\Gamma \cdot x:S_0 \cdot c:N, e:s[r] \langle S_0, S_2 \rangle \vdash Q_0 \triangleright s[r]:T_0, \\ \Gamma \cdot c:N, e:s[r] \langle S_0, S_2 \rangle \vdash \text{call} \langle e_l, e_v \rangle \triangleright s[r]:\text{call} \langle e \rangle, \\ \Gamma \cdot y:S, \Theta \vdash Q_2 \triangleright \Delta_{Q_2} \cdot s[r]:T_2,$

and $\Gamma \Vdash e_v:S_0$. Since $\text{eval}(e_v) = v$, then $\Gamma \Vdash v:S_0$. By Lemma 3 and $x \nparallel (\Gamma, \Delta_{Q_2}, s, e, c, T_0, T_2)$, then $\Gamma, e:s[r] \langle S_0, S_2 \rangle \vdash (Q_0\{n/c\}) \{v/x\} \triangleright s[r]:T_0\{n/c\}$. By Rule (Loop), then $\Gamma, \Theta \vdash P' \triangleright \Delta'$ with $\Delta' = \Delta_{Q_2} \cdot s[r]:[R] \infty_e^{c=\text{eval}(n+1)} [(\langle S_0 \rangle.T_0)T_0\{n/c\}; \langle S_2 \rangle.T_2]$.

By Rule (T-Call) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (LExitS) In this case** $P = s[r, R] \infty_e^{c=n} [(x).Q_0] \text{exit} \langle e_l, e_v \rangle; (y).Q_2 | \prod_{r_i \in R} s_{r \to r_i}:M_i, P' = Q_2\{v/y\} | \prod_{r_i \in R} s_{r \to r_i}:M_i \# \text{exit} \langle id, v \rangle, \text{eval}(e) = \text{eval}(e_l) = id$, and $\text{eval}(e_v) = v$. Let $R = \{r_1, \dots, r_n\}$. By the Rules (Par), (Loop), (Exit), and the typing rules for message queues, $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $\Delta_{Q_2}, S, S_0, T_0, T_1, T_2, \text{MT}_1, \dots, \text{MT}_n$ such that $\Delta = \Delta_{Q_2} \cdot s[r]:[R] \infty_e^{c=n} [(\langle S_0 \rangle.T_0)T_1; \langle S_2 \rangle.T_2 \cdot \prod_{r_i \in R} s_{r \to r_i}:\text{MT}_i$, we have $x, y \nparallel (\Gamma, \Delta_{Q_2}, s, e, c, T_0, T_1, T_2)$, $\Gamma \Vdash n:N, \text{unr}(T_0), \text{unr}(T_1),$

$\Gamma \cdot x:S_0 \cdot c:N, e:s[r] \langle S_0, S_2 \rangle \vdash Q_0 \triangleright s[r]:T_0, \\ \Gamma \cdot c:N, e:s[r] \langle S_0, S_2 \rangle \vdash \text{exit} \langle e_l, e_v \rangle \triangleright s[r]:T_1, \\ \Gamma \cdot y:S, \Theta \vdash Q_2 \triangleright \Delta_{Q_2} \cdot s[r]:T_2,$
Γ ⊩ e_v:S₂, and Γ ⊢ s_{r→r_i}:M_i ⊲ s_{r→r_i}:MT_i for all r_i ∈ R. Since eval(e_v) = v, then Γ ⊩ v:S₀. By Lemma 3 and because y♯(Γ, ΔQ₂, s, e, c, T₀, T₁, T₂), then Γ, Θ ⊢ Q₂{v/y} ▷ ΔQ₂ · s[r]:T₂. By Rule (MQExit), Γ, Θ ⊢ s_{r→r_i}:exit(l, v)♯M_i ⊢ s_{r→r_i}:exit(l, S)♯MT_i for all r_i ∈ R. Since the session environment Δ = ΔQ₂ · s[r]:[R]∞_e^{c=n}[(S₀)·T₀]T₁; (S₂)·T₂ · Π_{r_i∈R} s_{r→r_i}:MT_i is defined, so is the session environment Δ' = ΔQ₂ · s[r]:T₂ · Π_{r_i∈R} s_{r→r_i}:exit(l, S)♯MT_i. By Rule (Par), then Γ, Θ ⊢ P' ▷ Δ'. By Rule (T-LExitS), then Δ ⇌ Δ'. Since Γ, Δ are coherent and by transitivity of ⇌, then Γ, Δ' are coherent.

**Case of Rule (LExitG) In this case**

$$ P = s[r, R] \stackrel{c=n}{\propto} [(x).Q_0]Q_1; (y).Q_2 \mid s_{r_e \to r}:exit(id, v)♯M, \\ P' = Q_2\{v/y\} \mid s_{r_e \to r}:M, $$

eval(e) = id, and r_e ∈ R. By Rules (Par), (Loop), (MQExit), and the typing rules for message queues, the judgement Γ, Θ ⊢ P ▷ Δ implies that there are ΔQ, ΔQ₂, S₀, S₂, T₀, T₁, T₂, MT such that Δ = ΔQ₂ · s[r]:[R]∞_e^{c=n}[(S₀)·T₀]T₁; (S₂)·T₂ · s_{r_e \to r}:exit(e, S₂)♯MT, we have x, y♯(Γ, ΔQ₂, s, e, c, T₀, T₁, T₂), Γ ⊩ n:N, unr(T₀), unr(T₁),

$$ \Gamma \cdot x:S_0 \cdot c:N, e:s[r] \langle S_0, S_2 \rangle \vdash Q_0 \vdash s[r]:T_0, \\ \Gamma \cdot c:N, e:s[r] \langle S_0, S_2 \rangle \vdash Q_1 \vdash s[r]:T_1, \\ \Gamma \cdot y:S, \Theta \vdash Q_2 \vdash \Delta_{Q_2} \cdot s[r]:T_2, \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \Gamma, \Theta \vdash s_{r_e \to r}:M \vdash s_{r_e \to r}:MT, $$

and Γ ⊩ v:S₂. By Lemma 3 and because y♯(Γ, ΔQ₂, s, e, c, T₀, T₁, T₂), then Γ, Θ ⊢ Q₂{v/y} ▷ ΔQ₂ · s[r]:T₂. Since ΔQ₂ · s[r]:[R]∞_e^{c=n}[(S₀)·T₀]T₁; (S₂)·T₂ · s_{r_e \to r}:exit(e, S₂)♯MT is defined, so is Δ' = ΔQ₂ · s[r]:T₂ · s_{r_e \to r}:MT. By Rule (Par), then Γ, Θ ⊢ P' ▷ Δ'.

By Rule (T-LExitG), then Δ ⇌ Δ'. Since Γ, Δ are coherent and by transitivity of ⇌, then Γ, Δ' are coherent.

**Case of Rule (EDrop)** In this case $P = s_{r_2 \to r_1}:exit(id, v)♯M$ and $P' = s_{r_2 \to r_1}:M$. By the typing rules for message queues, Γ, Θ ⊢ P ▷ Δ implies that there are S, MT such that $\Delta = s_{r_2 \to r_1}:exit(e, S)♯MT$, eval(e) = id, and Γ, Θ ⊢ P' ▷ Δ' with $\Delta' = s_{r_2 \to r_1}:MT$. By Rule (T-EDrop) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since Γ, Δ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then Γ, Δ' are coherent.

**Case of Rule (Crash)** In this case $FP_{crash}$ and $P' = \perp$. By the typing rules and Condition 1.1, Γ, Θ ⊢ P ▷ Δ and $FP_{crash}$ imply $nsr(\Delta)$. By Rule (Crash), then Γ, Θ ⊢ ⊥ ▷ Δ. Since $\Delta' = \Delta$, Γ, $\Delta'$ is coherent and, by reflexivity, $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$.

**Case of Rule (If-T)** In this case $P = \mathit{if} e \mathit{ then} Q \mathit{ else} Q'$ and $P' = Q$. By Rule (If), Γ, Θ ⊢ P ▷ Δ implies Γ, Θ ⊢ P' ▷ Δ. Since $\Delta' = \Delta$, Γ, $\Delta'$ is coherent and, by reflexivity, $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$.

**Case of Rule (If-F)** In this case $P = \mathit{if} e \mathit{ then} Q \mathit{ else} Q'$ and $P' = Q'$. By Rule (If), Γ, Θ ⊢ P ▷ Δ implies Γ, Θ ⊢ P' ▷ Δ. Since $\Delta' = \Delta$, Γ, $\Delta'$ is coherent and, by reflexivity, $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$.

**Case of Rule (Deleg)** In this case $P = s[r_1, r_2]!\langle\langle s'[r] \rangle\rangle$. Q $|$ s_{r_1 \to r_2}:M$ and $P' = Q$ $|$ s_{r_1 \to r_2}:M\#s'[r]$. By the Rules (Par), (Deleg), and the typing rules for message queues, Γ, Θ ⊢ P ▷ Δ implies that there are ΔQ, T, T', MT such that $\Delta = \Delta_Q \cdot s[r_1]:[r_2]!\langle s'[r]:T' \rangle \cdot T \cdot s'[r]:T' \cdot s_{r_1 \to r_2}:MT$, Γ, Θ ⊢ Q ▷ ΔQ · s[r_1]:T, and Γ, Θ ⊢ s_{r_1 \to r_s}:MT ▷ s_{r_1 \to r_2}:MT. By Rule (MQDeleg), then Γ, Θ ⊢ s_{r_1 \to r_s}:MT\#s'[r] ▷ s_{r_1 \to r_2}:MT\#s'[r]. Since $\Delta = \Delta_Q \cdot s[r_1]:[r_2]!\langle s'[r]:T' \rangle \cdot T \cdot s'[r]:T' \cdot s_{r_1 \to r_2}:MT$ is defined, so is $\Delta' = \Delta_Q \cdot s[r_1]:T \cdot s_{r_1 \to r_2}:MT\#s'[r]$. By Rule (Par), then Γ, Θ ⊢ P' ▷ Δ'.

By Rule (T-Deleg) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since Γ, Δ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then Γ, Δ' are coherent.
**Case of Rule (SRecv)** In this case $P = s[r_1, r_2]?(s'[r])$. $Q$ | $s_{r_2 \to r_1}:s''[r]#M$ and $P' = Q\{s''/s'\}\{r'/r\}$ | M. We use alpha conversion to ensure that $s' = s''$ and $r = r'$. By the Rules (Par), (SRecv), and the typing rules for message queues, $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $\Delta_Q, T, T', \text{MT}$ such that $\Delta = \Delta_Q \cdot s[r_1]:[r_2]?\langle s'[r]:T'\rangle \cdot T \cdot s_{r_2 \to r_1}:s'[r]#\text{MT}, \Gamma, \Theta \vdash Q \triangleright \Delta_Q \cdot s[r_1]:T \cdot s'[r]:T'$, and $\Gamma, \Theta \vdash s_{r_2 \to r_1}:M \triangleright s_{r_2 \to r_1}:\text{MT}$. Since $\Delta = \Delta_Q \cdot s[r_1]:[r_2]?\langle s'[r]:T'\rangle \cdot T \cdot s_{r_2 \to r_1}:s''[r]#\text{MT}$ is defined, so is $\Delta' = \Delta_Q \cdot s[r_1]:T \cdot s'[r]:T' \cdot s_{r_2 \to r_1}:\text{MT}$. By Rule (Par), then $\Gamma, \Theta \vdash P' \triangleright \Delta'$.
By Rule (T-SRecv) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (Par)** In this case $P = Q_1 | Q_2$, $Q_1 \longmapsto Q'_1$, and $P' = Q'_1 | Q_2$. By Rule (Par), $\Gamma, \Theta \vdash P \triangleright \Delta$ implies that there are $\Delta_{Q_1}, \Delta_{Q_2}$ such that $\Delta = \Delta_{Q_1} \cdot \Delta_{Q_2}, \Gamma, \Theta \vdash Q_1 \triangleright \Delta_{Q_1}$, and $\Gamma, \Theta \vdash Q_2 \triangleright \Delta_{Q_2}$. Since $\Gamma, \Delta$ are coherent, $\Gamma, \Delta_{Q_1}$ is weakly coherent. By the induction hypothesis (for the weakly coherent case), $\Gamma, \Theta \vdash Q'_1 \triangleright \Delta'_{Q_1}$ with $\Delta_{Q_1} \stackrel{s}{\rightleftharpoons} \Delta'_{Q_1}$. Since $\Delta_{Q_1} \cdot \Delta_{Q_2}$ is defined, so is $\Delta' = \Delta_{Q_1} \cdot \Delta_{Q_2}$. By Rule (Par), then $\Gamma, \Theta \vdash P' \triangleright \Delta'$.
By $\Delta_{Q_1} \stackrel{s}{\rightleftharpoons} \Delta'_{Q_1}$, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (Res)** In this case $P = (\nu x)Q$, $Q \longmapsto Q'$, and $P' = (\nu x)Q'$. Then, one of the Rules (Res1) or (Res2) was used to type the restriction on $x$ in $P$.

**Case of (Res1)** Then there is some $S$ such that $x\sharp(\Gamma, \Delta)$ and $\Gamma \cdot x:S, \Theta \vdash Q \triangleright \Delta$. Since $\Gamma, \Delta$ are coherent, so are $\Gamma \cdot x:S, \Delta$. By the induction hypothesis, $\Gamma \cdot x:S, \Theta \vdash Q' \triangleright \Delta'$ for some $\Delta'$ such that $\Gamma, \Delta'$ is coherent and $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. With Rule (Res1), then $\Gamma, \Theta \vdash P' \triangleright \Delta'$.

**Case of (Res2)** In this case $x = s$ and there are $G, a, \Delta''$ such that $s\sharp(\Gamma, \Delta)$, $\{s[r]:G|_r | r \in R(G)\} \cdot \{s_{r \to r'}::[ ] | r, r' \in R(G') \wedge r \neq r'\} \stackrel{s}{\rightleftharpoons} \Delta''$, $a:G \in \Gamma$, and $\Gamma, \Theta \vdash Q \triangleright \Delta \cdot \Delta''$. Then $\Gamma, \Delta \cdot \Delta''$ are coherent. By the induction hypothesis, $\Gamma, \Theta \vdash Q' \triangleright \Delta'''$ for some $\Delta'''$ such that $\Delta \cdot \Delta'' \stackrel{s}{\rightleftharpoons} \Delta''$. By Rule (Res2), then $\Gamma, \Theta \vdash P' \triangleright \Delta$. Since $\Delta' = \Delta, \Gamma, \Delta'$ is coherent and, by reflexivity, $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$.

**Case of (Rec)** In this case $P = (\mu X, c = n)Q$ and $P' = (Q\{n/c\}) \{(\mu X, c=\text{eval}(n+1))Q/X\}$. We use alpha conversion to ensure that $c\sharp(\Gamma, \Theta, \Delta)$. By Rule (Rec), then there are $\Delta_Q, s, r, t, T$ such that $\Delta = \Delta_Q \cdot s[r]:(\mu t, c = n)T, \Gamma \Vdash n:N$, and $\Gamma \cdot c:N, \Theta \cdot X:s[r]:t \vdash Q \triangleright \Delta_Q \cdot s[r]:T$. Since $c\sharp(\Gamma, \Theta, \Delta)$ and because of Lemma 3, then $\Gamma, \Theta \cdot X:s[r]:t \vdash Q\{n/c\} \triangleright \Delta_Q \cdot s[r]:T\{n/c\}$. By replacing in the proof tree of $\Gamma, \Theta \cdot X:s[r]:t \vdash Q\{n/c\} \triangleright \Delta_Q \cdot s[r]:T\{n/c\}$ all occurrences of Rule (Var) by the proof tree, we obtain $\Gamma, \Theta \vdash P' \triangleright \Delta'$ with $\Delta' = \Delta_Q \cdot s[r]: (T\{n/c\}) \{(\mu t, c=\text{eval}(n+1))T/t\}$.
By Rule (T-Rec) of Figure 5, then $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. Since $\Gamma, \Delta$ are coherent and by transitivity of $\stackrel{s}{\rightleftharpoons}$, then $\Gamma, \Delta'$ are coherent.

**Case of Rule (Struc)** In this case $P \equiv Q$, $Q \longmapsto Q'$, $Q' \equiv P'$. By Lemma 2, $\Gamma, \Theta \vdash P \triangleright \Delta$ and $P \equiv Q$ imply $\Gamma, \Theta \vdash Q \triangleright \Delta$. By the induction hypothesis, $\Gamma, \Theta \vdash Q' \triangleright \Delta'$ for some $\Delta'$ such that $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$ and $\Gamma, \Delta'$ are coherent. By Lemma 2, then $\Gamma, \Theta \vdash P' \triangleright \Delta'$. $\square$

Since we restrict our attention to linear environments, type judgements ensure linearity of session channels. With subject reduction, this holds for all derivatives of well-typed processes.

**Lemma 5 (Linearity).** Let $\Gamma \vdash P \triangleright \Delta$, $\Gamma, \Delta$ be coherent, and there are no name clashes on session channels. Then all session channels of $P$ are linear, i.e., for all $P \longmapsto P'$ and all $s, r, r_1, r_2$ there is at most one unguarded actor $s[r]$ and at most one queue $s_{r_1 \to r_2}$ in $P'$.

*Proof.* By Theorem 4, there is some $\Delta'$ such that $\Gamma \vdash P' \triangleright \Delta'$ and $\Gamma, \Delta'$ are coherent. By the Definition 3 of coherence and projection, $\Delta'$ contains at most one actor $s[r]$ and at most one queue $s_{r_1 \to r_2}$ for each $a:G \in \Gamma$ and $r \in R(G)$. By the Figures 3 and 4, only the Rules (Req), (Acc), and (Res2) can introduce new actors or queues. The linearity of global environments ensures, that all new actors and queues introduced by the rules are on fresh channel names and are pairwise distinct. The Rules (Req) and (Acc) introduce exactly one actor each on a fresh session channel $s$ that is bound by a prefix for session initialisation. Rule (Res2) introduces assignments for actors and queues for pairwise different roles on a fresh session channel $s$ that is bound by restriction. Since there are no name clashes, the session channels in binders are
pairwise different and distinct from free session channels. By the typing rules and because $\Gamma, \Theta \vdash P' \succ \Delta'$, all actors and queues in $P'$ have to satisfy their specification as described by an assignment of this actor or queue towards a local type. By the linearity of session environments and since new assignments for actors result from bound session channels, all unguarded actors and queues in $P'$ are pairwise different. □

For strongly reliable systems coherence ensures that for each actor there is a matching communication partner. In the case of asynchronous communication, this means that for each sender (or message on a queue) there is a receiver and for each receiver there is a sender or a message on a queue, where the receiver as well as the sender or the message queue appear under the same binder of the session channel or both are free. In the case of unreliable communication, messages get lost, senders can crash, and receivers can crash themselves or suspect the sender. In the case of weakly reliable branching for each sender (or message on a queue) there are all specified receivers that are not crashed and vice versa.

We summarise these properties of strongly reliable and weakly reliable interactions in error-freedom that we inherit verbatim from [2]: for each strongly reliable sender or message there is a matching receiver and vice versa, for each weakly reliable sender or message there is a possibly crashed receiver and vice versa. We obtain similar requirements for session delegation.

**Lemma 6 (Error-Freedom).** If $\Gamma \vdash P \succ \Delta$ and $\Gamma, \Delta$ is coherent then:

* for each unguarded $s[r_1, r_2]!_r \langle y \rangle$. $Q_1$ and each message $\langle y \rangle^r$ on a message queue $s_{r_1 \to r_2}$ in $P$ there is some $s[r_2, r_1]!_r(x)$. $Q_2$ in $P$,

* for each unguarded $s[r_2, r_1]!_r(x)$. $Q_2$ in $P$ there is some $s[r_1, r_2]!_r \langle y \rangle$. $Q_1$ or a message $\langle y \rangle^r$ on a message queue $s_{r_1 \to r_2}$ in $P$,

* for each unguarded $s[r_1, r_2]!_r l.Q$ and each message $l^r$ on a message queue $s_{r_1 \to r_2}$ in $P$ there is some $j \in I$ and $s[r_2, r_1]!_r \{l_i.Q_i\}_{i \in I}$ in $P$ with $l_j \doteq l$,

* for each unguarded $s[r_2, r_1]!_r \{l_i.Q_i\}_{i \in I}$ in $P$ there is $j \in I$ and $s[r_1, r_2]!_r l.Q$ or a message $l^r$ on a message queue $s_{r_1 \to r_2}$ in $P$ with $l_j \doteq l$,

* for each unguarded $s[r, R]!_w l.Q$ and each message $l^w$ on a message queue $s_{r \to r'}$ in $P$ and each $r' \in R$ there is some $s[r', r]?_w \{l_i.P_i\}_{i \in I, l_d}$ and $j \in I$ in $P$ with $l_j \doteq l$ or $P$ does not contain an actor $s[r']$,

* for each unguarded $s[r', r]!?_w \{l_i.P_i\}_{i \in I, l_d}$ in $P$ there is $j \in I$ and $s[r, R]!_w l.Q$ or a message $l^w$ on a message queue $s_{r \to r'}$ in $P$ with $l_j \doteq l$ and $r' \in R$ or $P$ does not contain an actor $s[r]$,

* for each unguarded $s[r_1, r_2]!\langle\langle s'[r] \rangle\rangle$. $Q_1$ and each message $s'[r]$ on a message queue $s_{r_1 \to r_2}$ in $P$ there is some $s[r_2, r_1]?(\langle\langle s''[r'] \rangle\rangle)$. $Q_2$ in $P$, and

* for each unguarded $s[r_2, r_1]?(\langle\langle s''[r'] \rangle\rangle)$. $Q_2$ in $P$ there is some $s[r_1, r_2]!\langle\langle s'[r] \rangle\rangle$. $Q_1$ or a message $s'[r]$ on a message queue $s_{r_1 \to r_2}$ in $P$.

**Proof.** By coherence and projection for each strongly reliable and each weakly reliable sender there is initially a matching receiver for each free session channel in the session environment. By the typing rules and Rule (Res2) in particular, this holds also for restricted session channels. Session environments may evolve using $\overset{s}{\mapsto}$ but all such steps preserve the above defined requirements, i.e., strongly reliable or weakly reliable send prefixes can be mapped onto the type of the respective message in a queue but no such message can be dropped. The typing rules ensure that the processes follow their specification in the local types of session environments. Then, the first four and the last two cases follow from the typing rules and coherence, and the fact that only unreliable processes can crash. The remaining two cases follow from the typing rules and coherence. □

*Session fidelity* claims that the interactions of a well-typed process follow exactly the specification described by its global types, i.e., if a system is well-typed w.r.t. coherent type environments then the system follows its specification in the global type. One direction of this property already follows from the above variant of subject reduction. The steps of well-typed systems are reflected by corresponding steps of the session environment and, thus, respect their specification in global types. What remains to show is that the specified interactions can indeed be performed. The above formulation of error-freedom alone is not strong enough to show this, because it ensures only the existence of matching communication partners and not that they can be unguarded.

To obtain session fidelity we prove *progress*. *Progress* states that no part of a well-typed and coherent system can block other parts, that eventually all matching communication partners as described by
error-freedom are unguarded, that interactions specified by the global type can happen, and that there are no communication mismatches. Subject reduction and progress together then imply session fidelity, i.e., that processes behave as specified in their global types.

In the literature there are different formulations of progress. We are interested in a rather strict definition of progress that ensures that well-typed systems cannot block. Therefore, we need an additional assumption on session requests and acceptances. Coherence ensures the existence of communication partners within sessions only. If we want to avoid blocking, we need to be sure, that no participant of a session is missing during its initialisation. Note that without action prefixes all participants either terminated or crashed.

**Theorem 7 (Progress/Session Fidelity).** Let $\Gamma, \Delta$ be coherent, $\Gamma, \Theta \vdash P \triangleright \Delta$, and let $P$ be free of cyclic dependencies between sessions. Assume that in the derivation of $\Gamma, \Theta \vdash P \triangleright \Delta$, whenever $\bar{a}[n](s).Q$ or $a[r](s).Q$ in $P$, then $a:G \in \Gamma$, $|R(G)| = n$, and there are $\bar{a}[n](s).Q_n$ as well as $a[r_i](s).Q_i$ in $P$ for all $1 \le r_i < n$.

1. Then either $P$ does not contain any action prefixes or $P \mapsto P'$.

2. If $P$ does not contain recursion or loops, then there exists $P'$ such that $P \mapsto^* P'$ and $P'$ does not contain any action prefixes.

*Proof of Theorem 7.* 1.) If $P$ contains an unguarded conditional, then it can perform a step $P \mapsto P'$ such that $\Gamma, \Theta \vdash P' \triangleright \Delta$ using one of the Rules (If-T) or (If-F) as described in the corresponding cases of the proof of Theorem 4. Similarly, if $P$ contains an unguarded recursion, then it can perform a step $P \mapsto P'$ such that $\Gamma, \Theta \vdash P' \triangleright \Delta'$ with $\Delta \stackrel{s}{\mapsto} \Delta'$ using Rule (Rec) as described in the corresponding case of the proof of Theorem 4. Assume that $P$ is not structural congruent to $\mathbf{0}$ and does not contain unguarded conditionals or recursions.

Since $P$ is not structural congruent to $\mathbf{0}$ it contains session channels. All session channels of $P$ that are not contained in $\Delta$ are bound in $P$, i.e., the names of $\Delta$ are exactly the free session channels of $P$. Since there are no cyclic dependencies between sessions, we can pick a minimal session in $P$, i.e., a session such that its next action is not blocked by any action of another session or session delegation. Let $s$ denote this session channel. By the typing rules in the Figures 3 and 4, there are some $G, b$ such that $b:G \in \Gamma$ and $G$ specifies the session $s$. Since the next action of this session is not blocked, $P$ contains at least one unguarded prefix or at least one unguarded not empty queue on $s$. Among all such unguarded prefixes and messages that are head of a queue we pick a minimal, i.e., one that is typed by the projection of a part of $G$ such that no part of $G$ that is guarding it is used to type another unguarded prefix or message in $P$:

$\bar{a}[n](s).Q$ Then $s^\sharp\Delta$ and $a:G \in \Gamma$. By the assumption on session initialisation, then for all $1 \le r_i < n$ we have $a[r_i](s)$. in $P$. Since $s$ is minimal, all these session acceptances are unguarded. By Rule (Init), then $P \mapsto P'$.

$a[r](s).Q$ Then $s^\sharp\Delta$ and $a:G \in \Gamma$. By the assumption on session initialisation, then $\bar{a}[n](s).Q$ and for all $1 \le r_i < n$ with $r_i \ne r$ we have $a[r_i](s)$. in $P$. Since $s$ is minimal, all this session request and these session acceptances are unguarded. By Rule (Init), then $P \mapsto P'$.

$s[r_1, r_2]!_r \langle v \rangle.Q$ If $s^\sharp\Delta$ then the typing rules in the Figures 3 and 4 and (Req), (Acc), and (Res2) in particular ensure that $s_{r_1 \to r_2}:\text{MT}$ in $P$. If $s$ is free in $\Delta$, then $s_{r_1 \to r_2}:\text{MT}$ in $P$ because of coherence. Since $s$ and the action are minimal, $s_{r_1 \to r_2}:\text{MT}$ is unguarded. By Rule (RSend), then $P \mapsto P'$.

$s_{r_1 \to r_2}:\langle v \rangle^\text{r}\#\text{M}$ By Lemma 6, then $s[r_2, r_1]!?_r(x).Q$ in $P$. Because exit messages cannot be dropped unless the corresponding loop is terminated (Condition 1.8), $s[r_2, r_1]!?_r(x).Q$ is not guarded by a loop. Since $s$ and the action are minimal, $s[r_2, r_1]!?_r(x).Q$ is unguarded. By Rule (RGet), then $P \mapsto P'$.

$s[r_2, r_1]!?_r(x).Q$ By Lemma 6, then $s_{r_1 \to r_2}:\langle v \rangle^\text{r}\#\text{M}$ in $P$. Since $s$ and the action are minimal, $s_{r_1 \to r_2}:\langle v \rangle^\text{r}\#\text{M}$ is unguarded. By Rule (RGet), then $P \mapsto P'$.

$s[r_1, r_2]!_u \langle v \rangle.Q$ If $s^\sharp\Delta$ then the typing rules in the Figures 3 and 4 and (Req), (Acc), and (Res2) in particular ensure that $s_{r_1 \to r_2}:\text{MT}$ in $P$. If $s$ is free in $\Delta$, then $s_{r_1 \to r_2}:\text{MT}$ in $P$, because of coherence. Since $s$ and the action are minimal, $s_{r_1 \to r_2}:\text{MT}$ is unguarded. By Rule (USend), then $P \mapsto P'$.
$s_{r_1 \to r_2}: l\langle v \rangle^u \# M$ Then the typing rules and coherence ensure that either there is no actor $s[r_2]$, the actor $s[r_2]$ had skipped, $s[r_2, r_1]_u l\langle dv \rangle(x)$. $Q$ in $P$, or $s[r_2, r_1]_u l\langle dv \rangle(x)$. $Q$ in $P$ was originally inside a loop program of an already terminated loop. If there is no actor $s[r_2]$, then it has crashed. Then the pattern $FP_{crash}(Q, \dots)$ was satisfied with $s[r_2] \in A(Q)$. By Condition 1.5, then eventually $FP_{m1}(s, r_1, r_2, l, \dots)$. By Rule (ML), then $P \mapsto P'$. If the actor $s[r_2]$ skipped this reception, then $FP_{uskip}(s, r_2, r_1, l, \dots)$. By Condition 1.3, then $FP_{m1}(s, r_1, r_2, l, \dots)$. By Rule (ML), then $P \mapsto P'$. Because exit messages cannot be dropped unless the corresponding loop is terminated (Condition 1.8), $s[r_2, r_1]_u l\langle dv \rangle(x)$. $Q$ is not guarded by a loop. If $s[r_2, r_1]_u l\langle dv \rangle(x)$. $Q$ in $P$, since $s$ and the action are minimal, then this term is unguarded. By Condition 1.2 and Rule (UGet), then $P \mapsto P'$. If $s[r_2, r_1]_u l\langle dv \rangle(x)$. $Q$ in $P$ was originally inside a loop program of an already terminated loop, then the actor of the terminated loop was $s[r_2]$. By Condition 1.7, then eventually $FP_{m1}(s, r_1, r_2, l, \dots)$. By Rule (ML), then $P \mapsto P'$.

$s[r_2, r_1]_u l\langle dv \rangle(x)$. $Q$ Then the typing rules and coherence ensure that there is the queue $s_{r_1 \to r_2}$ and either $l\langle v \rangle^u$ is on top of it, or this message was dropped, or the sender did not yet send this message, or the sender crashed before transmitting this message. If $l\langle v \rangle^u$ is on top of the queue, then $P \mapsto P'$ by Rule (UGet) and Condition 1.2. If the message was dropped, then $FP_{m1}(s, r_1, r_2, l, \dots)$. By Condition 1.3, then $FP_{uskip}(s, r_2, r_1, l, \dots)$. By Rule (USkip), then $P \mapsto P'$. If the sender did not yet send the message, we proceed as in the Case $s[r_1, r_2]_u l\langle y \rangle$. $Q$ above. If the sender crashed, then $FP_{crash}(Q, \dots)$ with $s[r_1] \in A(Q)$. By Condition 1.4, then eventually $FP_{uskip}(s, r_2, r_1, l, \dots)$. By Rule (USkip), then $P \mapsto P'$.

$s[r_1, r_2]_l, l. Q$ If $s^\Delta \Delta$ then the typing rules in the Figures 3 and 4 and (Req), (Acc), and (Res2) in particular ensure that $s_{r_1 \to r_2}: \text{MT}$ in $P$. If $s$ is free in $\Delta$, then $s_{r_1 \to r_2}: \text{MT}$ in $P$, because of coherence. Since $s$ and the action are minimal, $s_{r_1 \to r_2}: \text{MT}$ is unguarded. By Rule (RSel), then $P \mapsto P'$.

$s_{r_1 \to r_2}: l^r \# M$ By Lemma 6, then $s[r_2, r_1]_r \{l_i \cdot Q_i\}_{i \in I}$ in $P$. Because exit messages cannot be dropped unless the corresponding loop is terminated (Condition 1.8), $s[r_2, r_1]_r \{l_i \cdot Q_i\}_{i \in I}$ is not guarded by a loop. Since $s$ and the action are minimal, the action $s[r_2, r_1]_r \{l_i \cdot Q_i\}_{i \in I}$ is unguarded. By (RBran), then $P \mapsto P'$.

$s[r_2, r_1]_r \{l_i \cdot Q_i\}_{i \in I}$ By Lemma 6, then $s_{r_1 \to r_2}: l^r \# M$ in $P$ with $j \in I$ and $l \doteq l_j$. Since $s$ and the action are minimal, $s_{r_1 \to r_2}: l^r \# M$ is unguarded. By (RBran), then $P \mapsto P'$.

$s[r, R]_w l. Q$ If $s^\Delta \Delta$ then the typing rules and (Req), (Acc), and (Res2) in particular ensure that $s_{r \to r_i}: \text{MT}_i$ in $P$ for all $r_i \in R$. If $s$ is free in $\Delta$, then $s_{r \to r_i}: \text{MT}_i$ in $P$ for all $r_i \in R$, because of coherence. Since $s$ and the action are minimal, all $s_{r \to r_i}: \text{MT}_i$ are unguarded. By Rule (WSel), then $P \mapsto P'$.

$s_{r_1 \to r_2}: l^w \# M$ Then the typing rules, coherence, and Condition 1.6 ensure that either there is no actor $s[r_2]$ or $s[r_2, r_1]_w \{l_i \cdot Q_i\}_{i \in I, l_d}$ in $P$. In the former case the actor $s[r_2]$ has crashed. Then, since the message queue will not be needed any more, proceed with the next session and action that are minimal if you ignore the queue $s_{r_1 \to r_2}$.

$s[r_2, r_1]_w \{l_i \cdot Q_i\}_{i \in I, l_d}$ Then the typing rules and coherence ensure that there is the queue $s_{r_1 \to r_2}$ and either $l^w$ is on top of it, or the sender did not yet send this message, or the sender crashed before transmitting this message. If $l^w$ is on top of the queue, then $P \mapsto P'$ by Rule (WBran). If the sender did not yet send the message, we proceed as in the Case $s[r, R]_w l. Q$ above. If the sender crashed, then $FP_{crash}(Q', \dots)$ with $s[r_1] \in Q'$. By Condition 1.4, then eventually $FP_{wskip}(s, r_2, r_1, l, \dots)$ for $s[r_2]$. By Rule (WSkip), then $P \mapsto P'$.

$s[r_1, r_2]_w \langle s'[r] \rangle$. $Q$ If $s^\Delta \Delta$ then the typing rules in the Figures 3 and 4 and (Req), (Acc), and (Res2) in particular ensure that $s_{r_1 \to r_2}: \text{MT}$ in $P$. If $s$ is free in $\Delta$, then $s_{r_1 \to r_2}: \text{MT}$ in $P$ because of coherence. Since $s$ and the action are minimal, $s_{r_1 \to r_2}: \text{MT}$ is unguarded. By Rule (Deleg), then $P \mapsto P'$.

$s_{r_1 \to r_2}: s'[r] \# M$ By Lemma 6, then $s[r_2, r_1]_w \{(s''[r])\}$. $Q$ in $P$. Since $s$ and the action are minimal, the action $s[r_2, r_1]_w \{(s''[r])\}$. $Q$ is unguarded. By Rule (SRecv), then $P \mapsto P'$.
$s[r_2, r_1]?(s''[r'])$. By Lemma 6, then $s_{r_1 \to r_2}:s'[r]#M$ in $P$. Since $s$ and the action are minimal, the action $s_{r_1 \to r_2}:s'[r]#M$ is unguarded. By Rule (SConv), then $P \mapsto P'$.

**call**($e_l, e_v$) By the typing rules in the Figures 3 and 4 and (Req), (Acc), and (Res2) in particular or by coherence, **call**($e_l, e_v$) is in the loop body of an unguarded loop eval($e_l$) in $P$. By Rule (LCall), then $P \mapsto P'$.

**exit**($e_l, e_v$) By the typing rules in the Figures 3 and 4 and (Req), (Acc), and (Res2) in particular or by coherence, **exit**($e_l, e_v$) is in the loop body of an unguarded loop eval($e_l$) in $P$. Let $s[r]$ be the channel of this loop and $R$ its remaining roles. If $s \nvdash \Delta$ then the typing rules in the Figures 3 and 4 and (Req), (Acc), and (Res2) in particular ensure that $s_{r \to r_i}:\text{MT in } P$ for all $r_i \in R$. If $s$ is free in $\Delta$, then $s_{r \to r_i}:\text{MT in } P$ for all $r_i \in R$, because of coherence. Since $s$ and the action are minimal, these $s_{r \to r_i}:\text{MT}$ are unguarded for all $r_i \in R$. By Rule (LExitS), then $P \mapsto P'$.

$s_{r_1 \to r_2}:\text{exit}(id, v)#M$ Then the typing rules and coherence ensure that either there is no actor $s[r_2]$, the actor $s[r_2]$ already terminated the loop *id*, or the actor $s[r_2]$ still has the loop *id* in *P*. If there is no actor $s[r_2]$, then it has crashed. Then the pattern $\text{FP}_{\text{crash}}(Q, \dots)$ was satisfied with $s[r_2] \in A(Q)$. By Condition 1.5, then eventually $\text{FP}_{\text{drop}}(r_2, id)$. By Rule (EDrop), then $P \mapsto P'$. If the actor $s[r_2]$ already terminated the loop, then eventually $\text{FP}_{\text{drop}}(r_2, id)$, by Condition 1.7. By Rule (EDrop), then $P \mapsto P'$. If the loop is still in *P*, since *s* and the action are minimal, then this loop is unguarded. By Rule (LExitG), then $P \mapsto P'$.

2.) By Theorem 4, $P'$ is well-typed w.r.t. coherent $\Gamma, \Delta'$ with $\Delta \stackrel{s}{\rightleftharpoons} \Delta'$. If $P$ does not contain recursion or loops, then the session environment strictly reduces with every reduction of the process that does not reduce a conditional, though it may grow in cases of session initialisation. Since $P$ is finite and loop-free there are only finitely many possible session initialisations. We can repeat the above proof for 1.) to show that $P$ cannot get stuck as long as it contains action prefixes. $\square$

## References

[1] Lukas Bartl, Julian Linne & Kirstin Peters (2025): *Fault-Tolerant Multiparty Session Types with Global Escape Loops*. In: *Proceedings of Express/SOS*, EPTCS.

[2] Kirstin Peters, Uwe Nestmann & Christoph Wagner (2023): *FTMPST: Fault-Tolerant Multiparty Session Types*. *Logical Methods in Computer Science* 19(4), doi:10.46298/LMCS-19(4:14)2023.