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

HAL
open science

# Towards Multiparty Session Types for Fault-Tolerant Web Applications

Richard Casetta, Nils Gesbert, Pierre Genevès

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

## To cite this version:

Richard Casetta, Nils Gesbert, Pierre Genevès. Towards Multiparty Session Types for Fault-Tolerant Web Applications. 2026. hal-05502022

HAL Id: hal-05502022

https://inria.hal.science/hal-05502022v1

Preprint submitted on 10 Feb 2026

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published 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_3.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Towards Multiparty Session Types for Fault-Tolerant Web Applications

Richard CASETTA

BNP Paribas

Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG

Nils GESBERT

Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG

Pierre GENEVES

Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG

Modern web applications combine persistent state updates, concurrent interactions, and unreliable communication with external services. Failures such as timeouts can occur after partial state changes, producing temporary inconsistencies whose resolution depends on liveness properties that are often not verified in practice. Although formal methods offer rigorous guarantees for reasoning about complex software, they remain rarely adopted in enterprise settings due to their perceived complexity and lack of practical automation. Multiparty Session Types (MPST) offer strong guarantees for communication safety, yet they do not account for the interplay between state evolution, dynamic workflow structure, and failure behaviour that are essential for reasoning about the correctness of real web applications. This paper introduces a global-type framework that equips MPST with explicit failure semantics and dynamic participation. We define the syntax and operational semantics of these enriched global types and establish core properties, including well-formedness preservation. This foundation enables formal reasoning about communications in web applications where failures may occur, and lays the groundwork for future stateful extensions and automated verification of liveness properties.

# 1 Introduction

Modern web applications orchestrate workflows that interleave user-interface actions, backend logic, persistent state updates, and calls to unreliable external services. Failures such as timeouts or connection errors frequently arise after partial state changes, leading to temporary inconsistencies that standard Multiparty Session Types (MPST) cannot express.

## 1.1 Motivating example

Consider a user purchasing a ticket for her favourite show through a typical web application. Such applications integrate several layers: a client handling user interactions, a backend server orchestrating multiple concurrent requests, and external services (e.g., payment, inventory, fraud-prevention APIs) operated by independent teams.

A simplified ticket-ordering workflow is as follows: the user submits an order through the web client, the client forwards the request to the backend, then continues handling further user interactions, the backend records the order and forwards payment and inventory requests to

© Richard CASETTA et al.
This work is licensed under the
Creative Commons Attribution License.
external services and once these services respond, the backend returns a final confirmation to the client, updating the displayed state.

Although the happy path appears straightforward, failures introduce subtle inconsistencies. In practice, external APIs frequently suffer from high load or unpredictable latency. When the payment or inventory service responds too slowly, the backend may commit state locally (e.g., create the order, reserve seats) yet fail to reply to the client before its timeout window elapses. The user then sees the familiar error message: "Something went wrong. Please try again later". At this point, two distinct states coexist: the backend state, where the order may already be created and the seats reserved and the client state, where the order is believed to have failed.

A simple page refresh often reconciles this discrepancy: the client issues a fresh request and re-synchronizes with the authoritative backend state, revealing whether the order was successfully recorded or rejected (e.g., due to invalid payment or insufficient inventory). Crucially, this behaviour expresses a liveness property: the user must eventually obtain a coherent view of the order's outcome, even when failures and state updates interleave. However, this property is not guaranteed by the standard communication protocol alone. The resolution relies on the existence of a reconciliation path (here, the manual refresh) which bridges the inconsistent states. In analogous server-to-server workflows, no such manual recovery step exists, and the system may remain indefinitely inconsistent if the protocol does not explicitly model and enforce a liveness-preserving recovery path. This simple yet ubiquitous example illustrates a core challenge of modern web applications: state updates and failures routinely coexist, and correctness depends on eventually reconciling their effects.

## 1.2 Contributions

We introduce a global-type framework extending MPST with explicit timeout and connection-error actions, dynamic thread spawning, and crashes of active participants. We define the syntax and labelled-transition semantics of these global types, together with well-formedness conditions ensuring determinism of choices, timeout completeness, and robustness to faults. We furthermore prove two fundamental properties: preservation of well-formedness and absence of orphan participants, ensuring that reductions maintain correctness and that all actions involve valid, active endpoints. This framework provides a foundation for reasoning about communication behaviours in web applications and prepares the way for future work defining state updates extension, local types, projection, and automated liveness verification.

In the following, Section 2 develops the syntax and semantics; Section 3 presents key properties of the global type; Section 4 situates our work; Section 5 concludes and mentions future work.

# 2 Syntax and Semantics

We consider that participants are threads, represented by indexed roles ($A_0, B_1, ...$). As such, we define $role(A_r) = A$. As we use names $p, q$ for participants, if we have $p = A_r$ we write $role(p)[s]$ to mean $A_s$.

## 2.1 Global type syntax

The syntax of global types is inspired from [7] where we change the actions available, the request creation is extended from [6] with annotated thread directly in the syntax and local thread
spawning, and we extend the crashed participants from [3] to also model two-step timeouts on a channel. Let $\mathcal{N}$ be a set of channel names.

$$ \mathcal{G} ::= \gamma \cdot \mathcal{G} \qquad \text{Action} \\ \qquad \sum_i \mathcal{G}_i \qquad \text{Choice} \\ \qquad \mathcal{G}_1 \parallel \mathcal{G}_2 \qquad \text{Parallel composition} \\ \qquad \mu X \cdot \mathcal{G} \mid X \mid \text{end} \mid \textbf{stop} \qquad \text{Recursion, type variable, termination, cancellation} $$

$$ \gamma ::= \mathbf{p} \to \mathbf{q} : s\langle m \rangle \quad \text{type}(\cdot) = \text{comm} \quad \text{Communication, request or local thread spawning} \\ \qquad \mathbf{p}^\dagger \leftarrow \mathbf{q}^\dagger : s\langle \epsilon \rangle \quad \text{type}(\cdot) = \text{err} \quad \text{Timeout or connection errors} $$

$$ s \in \mathcal{N} \cup \{\perp\} \qquad m = l(T) \mid \nu s \qquad \dagger = \cdot \mid \lhd \qquad \epsilon = \text{timeout} \mid \text{connErr} $$

In this model, actions $\gamma$ describe the observable operational steps that occur between participants during a session. A term of the form $\mathbf{p} \to \mathbf{q} : s\langle m \rangle$ represents either a message communication, a connection request, or a local thread-spawning event. Concretely, when $m = l(T)$, the action denotes sending a labelled payload from $\mathbf{p}$ to $\mathbf{q}$ over the private channel $s \in \mathcal{N}$. When $m = \nu s$, the action initiates a request that creates a fresh private channel and spawn a new thread at the receiver; the special case where the sender and receiver coincide ($\mathbf{p} = \mathbf{q}$) on no channel ($s = \perp$) with a new channel ($m = \nu t$) corresponds to local thread spawning. Errors are captured by actions of the form $\mathbf{p}^\dagger \leftarrow \mathbf{q}^\dagger : s\langle \epsilon \rangle$. $\dagger$ annotates whether endpoints are still alive ($\cdot$) or not ($\lhd$), and $\epsilon \in \{\text{timeout}, \text{connErr}\}$ distinguishes between timeouts and connection failures. These error actions express that a communication could not proceed, ensuring that failures are explicitly represented in the global specification. The initiator of an action is the first participant ($init(\mathbf{p} \to \mathbf{q} : s\langle m \rangle) = init(\mathbf{p} \leftarrow \mathbf{q} : s\langle \epsilon \rangle) = \mathbf{p}$). For choices, we define $init$ only when at least one branch has an initiator (stop branch may exist) and all such branches agree on the same initiator. We also note $pub(\mathcal{G})$ the fixed set of participants that expose a public channel. These participants cannot appear elsewhere than in the receiver of a request. Finally, recursion is guarded and highlighted parts of the syntax defines runtime types. Global type stop marks a branch that cannot continue and will be removed. We define a congruence relation ($\equiv$) on global types by:

$$ \mathcal{G}_1 \parallel \mathcal{G}_2 \equiv \mathcal{G}_2 \parallel \mathcal{G}_1 \qquad \mathcal{G} + \text{stop} \equiv \mathcal{G} \qquad \mathcal{G} \parallel \text{end} \equiv \mathcal{G} $$

**Example 2.1.** We illustrate the benefit of our framework using a simple purchase workflow. A classical MPST specification for this interaction is:

$$ \begin{align*} G_{\text{purchase}}^{\text{classic}} &= \text{server} \to \text{api} : s\langle\text{Purchase}(\text{Order})\rangle. \\ \text{api} \to \text{server} : s\langle\text{OrderPurchased}(\text{Id})\rangle. \\ \text{server} \to \text{client} : t\langle\text{OrderComplete}(\text{Infos})\rangle. \end{align*} $$

This well-formed global type describes the happy path only: it provides no way to express that the API may time out or become temporarily unavailable. Our framework introduces explicit timeout actions that make such behaviours part of the protocol:
$$
G_{purchase} = \text{server} \to \text{api} : s\langle\text{Purchase}(\text{Order})\rangle. \\
+ \begin{cases}
\text{api} \to \text{server} : s\langle\text{OrderPurchased}(\text{Id})\rangle. \text{server} \to \text{client} : t\langle\text{OrderComplete}(\text{Infos})\rangle. \text{end} \\
\text{api} \not\to \text{server} : s\langle\text{timeout}\rangle. \text{server} \to \text{client} : t\langle\text{UnexpectedError}\rangle. \text{end}^*
\end{cases}
$$

The second branch models an asynchronous timeout: it may occur even if the API has not crashed, capturing the desynchronisation often observed in web applications. This goes beyond crash-stop behaviour and allows us to express failures that arise from latency, user impatience, or premature cancellation.

Finally, our framework can combine timeouts, crashes, and dynamic participants, enabling a protocol to restart after a failure. For instance, by replacing the trailing end* in the timeout branch with a recursion variable X, we obtain:

$$
G_{restart} = \mu X . \text{client} \to \text{server} : k_{\text{server}} \langle \nu t \rangle . G_{\text{purchase}} \{ \text{end}^* / X \}
$$

A new server thread is spawned on each iteration on the public endpoint k<sub>server</sub>; if it times out or crashes, the client may simply re-enter the loop. This models the familiar *refresh* behaviour of web clients.

**Definition 1. (Participants)** The *participants* of a global type *G* are the indexed roles that appear as live endpoints of its actions, representing exactly the threads that take part (or will take part) in the protocol.

$$
pt(\mathbf{X}) = pt(\mathbf{end}) = pt(\mathbf{stop}) = \{ \} \quad pt(\mu \mathbf{X} . \mathcal{G}) = pt(\mathcal{G}) \quad pt(\mathcal{G}_1 || \mathcal{G}_2) = pt(\mathcal{G}_1) \cup pt(\mathcal{G}_2)
$$

$$
pt(\sum_{i \in I} \mathcal{G}_i) = \bigcup_{i \in I} pt(\mathcal{G}_i) \qquad pt(\gamma . \mathcal{G}) = pt_p(\gamma) \cup pt(\mathcal{G}) \qquad pt_p(p \to q : s(l(T))) = \{p, q\}
$$

$$
pt_p(p \to q : s(\nu t)) = \{ p, q, \mathrm{role}(q)[t] \} \quad pt_p(p^\dagger \not\to q : s(\epsilon)) = \{ q \} \quad pt_p(p \not\to q^\dagger : s(\epsilon)) = \{ p \}
$$

$$
pt_p(p^\dagger \not\to q^\dagger : s(\epsilon)) = \{ \}
$$

**Definition 2. (Active Participants)** The set of *active participants* of a global type *G*, written *A*(*G*), identifies the participants that may currently take part in its interactions. Its definition follows that of *pt*(*G*), except for the case of thread creation:

$$
A(\mathcal{G}) = \begin{cases}
\{\mathbf{p}, \mathbf{q}\} \cup (A(\mathcal{G}') \setminus \{\mathrm{role}(\mathbf{q})[t]\}) & \text{if } \mathcal{G} = \mathbf{p} \to \mathbf{q} : s\langle\nu t\rangle \cdot \mathcal{G}', \\
pt(\mathcal{G}) & \text{otherwise.}
\end{cases}
$$

Intuitively, a thread waiting to be spawned should not yet be considered crashable; hence we remove the newly created role instance from the active set. This allows us to characterise precisely which participants may fail at a given point in the protocol.

**Definition 3. (Crash)** We define the function $\mathcal{G} \nvdash r$ that crashes $r$ over the global type $\mathcal{G}$:

$$
\text{end} \nvdash r = \text{end} \qquad X \nvdash r = X \qquad (\mu X . \mathcal{G}) \nvdash r = \mu X . (\mathcal{G} \nvdash r) \qquad \text{stop} \nvdash r = \text{stop} \qquad \left( \sum_{i \in I} \mathcal{G}_i \right) \nvdash r = \sum_{i \in I} (\mathcal{G}_i \nvdash r)
$$

$$
(\mathcal{G}_1 || \mathcal{G}_2) \nvdash r = (\mathcal{G}_1 \nvdash r) || (\mathcal{G}_2 \nvdash r) \qquad (\gamma . \mathcal{G}) \nvdash r = \begin{cases} \gamma . \mathcal{G} \nvdash r & \text{if } r \notin pt(\gamma) \\ \text{stop} & \text{if } r \in pt(\gamma) \land type(\gamma) = \text{comm} \\ \gamma \{ r^\dagger / r \} . \mathcal{G} \nvdash r & \text{if } r \in pt(\gamma) \land type(\gamma) = \text{err} \end{cases}
$$
**Example 2.2.** To illustrate the semantics of crash propagation in global types, we define the global type derived from $\mathcal{G}_{purchase}$ after the server send:

$$ \mathcal{G}_{purchase}^{\text{response}} = + \begin{cases} \text{api} \to \text{server} : s\langle\text{OrderPurchased}(\mathit{Id})\rangle. \text{server} \to \text{client} : t\langle\text{OrderComplete}(\mathit{Infos})\rangle. \text{end} \\ \text{api} \not\to \text{server} : s\langle\text{timeout}\rangle. \text{server} \to \text{client} : t\langle\text{UnexpectedError}\rangle. \text{end} \end{cases} $$

In this case, we have:

$$ \mathcal{G}_{purchase}^{\text{response}} \stackrel{\text{api}}{=} \text{stop} + (\text{api} \stackrel{\text{api}}{\not\to} \text{server} : s\langle\text{timeout}\rangle. \text{server} \to \text{client} : t\langle\text{UnexpectedError}\rangle. \text{end}) $$

The crash of the api transforms the communication branch into stop and marks it as done in the timeout branch. The congruence relation will then remove the stop branch, enforcing the timeout of the server on s and its communication to the client.

## 2.2 Global type semantics

We give a Labelled Transition System (LTS) semantics to global types with the following rules, where actions are defined by:

$$ \alpha ::= \begin{array}{l} \mathbf{p} \to \mathbf{q} : s\langle m \rangle \\ \text{subj}(\cdot) = \{\mathbf{p}, \mathbf{q}\} \end{array} \quad \begin{array}{l} \mathbf{pq!m} \\ \text{subj}(\cdot) = \{\mathbf{p}\} \end{array} \quad \begin{array}{l} \mathbf{qp?timeout} \\ \text{subj}(\cdot) = \{\mathbf{q}\} \end{array} \quad \begin{array}{l} \mathbf{p} \stackrel{\mathbf{p}}{=} \\ \text{subj}(\cdot) = \{\mathbf{p}\} \end{array} $$

We write $\hat{\alpha}$ for an action that is not a crash $p^z$.

**Definition 4. (LTS semantics)** The LTS semantics of global types is defined by:

$$ [\text{COM}] \mathbf{p} \to \mathbf{q} : s\langle m \rangle. \mathcal{G} \xrightarrow{\mathbf{p} \to \mathbf{q} : s\langle m \rangle} \mathcal{G} \quad [\mathbf{p} \uparrow] \mathbf{p} \not\to \mathbf{q} : s\langle m \rangle. \mathcal{G} \xrightarrow{\mathbf{pq!m}} \mathbf{p}^z \not\to \mathbf{q} : s\langle m \rangle. \mathcal{G} $$

$$ [\mathbf{q} \uparrow] \mathbf{p}^\dagger \not\to \mathbf{q} : s\langle \mathbf{timeout} \rangle. \mathcal{G} \xrightarrow{\mathbf{qp?timeout}} \mathbf{p}^\dagger \not\to \mathbf{q}^z : s\langle \mathbf{timeout} \rangle. \mathcal{G} $$

$$ [\mathbf{q} \uparrow?2] \mathbf{p} \to \mathbf{q} : s\langle l(T) \rangle. \mathcal{G} \xrightarrow{\mathbf{qp?timeout}} \text{stop} \quad [\mathbf{q} \uparrow] \frac{\mathbf{p} \in A(\mathcal{G})}{\mathcal{G} \xrightarrow{\mathbf{p}^z} \mathcal{G}^z \mathbf{p}} \quad [\text{CONCUR}] \frac{\mathcal{G} \xrightarrow{\hat{\alpha}} \mathcal{G}' \quad \text{subj}(\hat{\alpha}) \cap \text{pt}(\gamma) = \emptyset}{\gamma.\mathcal{G} \xrightarrow{\hat{\alpha}} \gamma.\mathcal{G}'} $$

$$ [\text{PAR}] \frac{\mathcal{G}_1 \xrightarrow{\hat{\alpha}} \mathcal{G}'_1}{\mathcal{G}_1 \parallel \mathcal{G}_2 \xrightarrow{\hat{\alpha}} \mathcal{G}'_1 \parallel \mathcal{G}_2} \quad [\text{REC}] \frac{\mathcal{G} \{\mu \times \mathcal{G} / \mathcal{X}\} \xrightarrow{\hat{\alpha}} \mathcal{G}'}{\mu \times \mathcal{G} \xrightarrow{\hat{\alpha}} \mathcal{G}'} \quad [\text{CHOICE}] \frac{\mathcal{G}_j \xrightarrow{\hat{\alpha}} \mathcal{G}'_j \quad \text{init} \left( \sum_{i \in I} \mathcal{G}_i \right) \in \text{subj}(\hat{\alpha})}{\sum_{i \in I} \mathcal{G}_i \xrightarrow{\hat{\alpha}} \mathcal{G}'_j} $$

$$ [\text{CHOICE-BR}] \frac{\forall i. \mathcal{G}_i \xrightarrow{\hat{\alpha}} \mathcal{G}'_i}{\sum_{i \in I} \mathcal{G}_i \xrightarrow{\hat{\alpha}} \sum_{i \in I} \mathcal{G}'_i} $$

The usage of $\hat{\alpha}$ in these definitions ensures that a crash can only happen at the top level and do not miss an occurrence of the crashed participant. Rule [SYNC] and [NEW] respectively models synchronous communication and spawning (either a request or locally). Rule [\_!] allows the sender to handle a timeout or a connection error. Rules [\_?] and [\_?2] allows the receiver of a message to stop waiting and timeout before communication takes place. Rule [\_] represents the crash of an active participant. Rule [CHOICE] models the resolution of the choice by its
initiator. Rule [PAR] allows the first global type to reduce, which models concurrent nature of the parallel composition as the second global type can also reduce due to congruence. Rule [REC] represents the unfolding. Rule [CONCUR] ensures that unrelated actions can be performed in any order. Rule [CHOICE-BR] allows an action to be made before a choice is resolved if it is available in all branches of a choice.

While the core semantics is synchronous, non-blocking sends are obtained by spawning local threads handling the communication, much like goroutines in Go, allowing the parent thread to continue and synchronize later. Finally, we define [REC] up to α-equivalence, in order to create new bound channel names when unfolding to avoid name clash.

**Example 2.3.** Now that the semantics rules are defined, we can show how the asynchronous timeout works. Starting from $G_{purchase}^{response}$, we have, at this point, several possible actions: (i) the api may resolve the choice by selecting one of the branches; (ii) the server or the client may time out before the choice is committed; (iii) one of the active participants may crash.

To see why a timeout from server is allowed, we appeal to rule [CHOICE-BR], which permits an action to occur before the choice is resolved whenever it is available in all branches. Indeed:

$$ \text{By } [\ll?2], \text{api} \to \text{server} : s\langle\text{OrderPurchased}(Id)\rangle \xrightarrow{\text{server api?timeout}} \text{stop} $$

$$ \text{By } [\ll?], \text{api} \not\to \text{server} : s\langle\text{timeout}\rangle \xrightarrow{\text{server api?timeout}} \text{api} \not\to \text{server}^t : s\langle\text{timeout}\rangle $$

Since the timeout action is admissible in both branches, [CHOICE-BR] yields:

$$ G_{purchase}^{response} \xrightarrow{\text{server api?timeout}} \text{stop} + (\text{api} \not\to \text{server}^t : s\langle\text{timeout}\rangle . \text{server} \to \text{client} : t\langle\text{UnexpectedError}\rangle . \text{end}) $$

Together, these rules provide an asynchronous timeout for active participants. Note also that crashing a participant is operationally equivalent to performing a single action that triggers an error on every channel in which that participant is involved (private or public).

Let $\Delta;\Gamma$ be environments where $\Delta = \emptyset | \Delta, X : \Gamma$ is used for recursive variable tracking existing channels, and $\Gamma = \emptyset | \Gamma, s : p | \Gamma, s : \{p, q\}$ is used for public and private channels.

**Definition 5. (Well-formedness)** We mutually define the following two judgments: $\gamma, \mathcal{G}$ is well-prefixed if $\Delta;\Gamma \vdash_p \gamma, \mathcal{G}$ and $\mathcal{G}$ is well-formed if $\Delta;\Gamma \vdash \mathcal{G}$.

It is important to distinguish between well-prefixed and well-formed global types. For instance, a send prefix cannot be well-formed, since a participant crash would reduce it to stop, which we aim to exclude. Conversely, the prefixes appearing in choice constructs must satisfy specific conditions to be considered well-formed, and these checks rely precisely on the notion of being well-prefixed.

$$ [\text{REQ}] \frac{s = \perp \iff p = q \quad s \neq \perp \iff \Gamma(s) = q \quad t \notin \Gamma \quad \Delta;\Gamma, t : \{p, \text{role}(q)[t]\} \vdash \mathcal{G}}{\Delta;\Gamma \vdash_p p \to q : s\langle\nu t\rangle.\mathcal{G}} $$

$$ [\text{SEND}] \frac{p, q \in \Gamma(s) \quad \Delta;\Gamma \vdash \mathcal{G}}{\Delta;\Gamma \vdash_p p \to q : s\langle l(T) \rangle.\mathcal{G}} \qquad [\text{TIMEOUT}] \frac{\Delta;\Gamma \vdash \mathcal{G}}{\Delta;\Gamma, s : \{p^{\dagger p}, q^{\dagger q}\} \vdash_p p^{\dagger p} \not\to q^{\dagger q} : s\langle \text{timeout} \rangle.\mathcal{G}} $$

$$ [\text{CONNERR}] \frac{p \neq q \quad \Gamma(s) = q \quad \Delta;\Gamma \vdash \mathcal{G}}{\Delta;\Gamma \vdash_p p^{\dagger p} \not\to q^{\dagger q} : s\langle \text{connErr} \rangle.\mathcal{G}} \qquad [\text{SUM}] \frac{\Delta;\Gamma \vdash_p \mathcal{G}_i \quad \text{cons} \left( \sum_{i \in I} \mathcal{G}_i \right)}{\Delta;\Gamma \vdash \sum_{i \in I} \mathcal{G}_i} $$
$$ \begin{array}{c} \text{[PAR]} \\ \text{[VAR-REC]} \\ \text{[REC]} \\ \text{[END]} \end{array} \frac{\frac{\Delta_1; \Gamma_1 \vdash \mathcal{G}_1 \quad \Delta_2; \Gamma_2 \vdash \mathcal{G}_2 \quad \Delta_1 \cap \Delta_2 = \emptyset \quad \Gamma_1 \cap \Gamma_2 = \text{pub}(\mathcal{G}_1) \cup \text{pub}(\mathcal{G}_2)}{\Delta_1, \Delta_2; \Gamma_1, \Gamma_2 \vdash \mathcal{G}_1 \parallel \mathcal{G}_2} \quad \frac{\Delta, X; \Gamma \vdash \mathcal{G}}{\Delta; \Gamma \vdash \mu X. \mathcal{G}} \\ \frac{\Delta, X; \Gamma \vdash X}{\Delta; \emptyset \vdash \text{end}} \quad \frac{\Delta, X; \Gamma \vdash \mathcal{G}}{\Delta; \emptyset \vdash \text{end}} \end{array} $$

The judgement $\vdash_p$ ensures that prefixes are defined correctly. Rule [REQ] ensures the channel name is fresh and checks that it is either a request where $p$ and $q$ are different and the public channel is in the environment, or a local thread creation with $p = q$ and $s = \perp$. Rule [SEND] allows communication as long as the channel has been previously opened. Rule [TIMEOUT] allows timeout on existing channels, removing it from the environment so that it cannot be reused. Rule [CONNERR] allows to handle request errors to a public channels, not changing the environment. [REC] and [VAR-REC] stores the state of channels before the recursion and ensures that none of them has been deleted and all channels created during the recursion have been closed (timeout in our framework). [PAR] ensures that only public channels are shared between environments of parallel global types, otherwise no channels, participants, recursion variables and private channels stored in recursion variables can be shared. Rule [END] ensures that every channel has been closed. [SUM] allow a choice to be well-formed if all branches are well-prefixed and where the consistency function *cons* checks that (i) there is one initiator (not all branches are *stop*), (ii) if a message can be sent to a private channel, there is a corresponding *timeout* branch for that channel, (iii) if a message can be sent to a public channel, there is a corresponding *connErr* branch for that channel and (iv) no duplication of labels. We now show the properties satisfied by our well-formedness rules.

## 3 Global Type Properties

We now state the key meta-theoretic properties of our framework. We begin by establishing a basic structural property of the typing environment

**Lemma 1. (Weakening)** If $\Delta; \Gamma \vdash G$ and $X \notin \text{dom}(\Delta)$, then $\Delta, X; \Gamma' ; \Gamma \vdash G$

Weakening is essential in order to add variables binding in the environment for a branch which does not use the recursion variable. We then turn to the interaction between well-formedness and crashes.

**Lemma 2. (Preservation under crash)** If $\Delta; \Gamma \vdash G$, then for every $p \in A(G)$, $\Delta'; \Gamma' \vdash G \not\vdash p$ where $\Delta' = \Delta\{p^\perp/p\}$ and $\Gamma' = \Gamma\{p^\perp/p\}$.

This ensures that eliminating an active participant does not compromise the structure of the protocol. Having established stability under crashes, we now consider stability under operational steps.

**Theorem 3. (Preservation of Well-formedness)** If $\Delta; \Gamma \vdash G$, then for every $\alpha, G'$ such that $G \xrightarrow{\alpha} G'$, there exists $\Delta', \Gamma'$ such that $\Delta'; \Gamma' \vdash G'$.

We conclude by ensuring that the semantics never enables actions from invalid participants.

**Theorem 4. (No Orphan Participants)** If $\Delta; \Gamma \vdash G$ and $G \xrightarrow{\alpha} G'$, then $\text{subj}(\alpha) \in A(G)$.

This property ensures that every action in the protocol can always be attributed to a currently active role, preventing actions from a crashed or nonexistent role. Together, these results show that well-formed global types remain stable under crashes and reductions, and that every step of the semantics involves only valid, active participants. This ensures that our framework provides a coherent and robust foundation for reasoning about failure-prone communication behaviours.
# 4 Related Work

MPST were originally introduced as a global discipline for specifying message-passing protocols [12], building on earlier dyadic interaction types [11]. A rich body of work has since extended MPST along several axes.

**Error Handling.** Affine sessions and exception-tolerant communication [17, 9], optional blocks [1], event-driven fault-tolerant MPST [20], and crash-stop semantics [3, 2, 18] extend MPST with failure behaviours. Tool-oriented systems for Rust support cancellation, affinity, and timed failure handling [15, 13]. However, these works lack dynamic participation: once a participant fails, the protocol cannot be safely restarted.

**Dynamic Behaviour.** MPST extensions have explored connection actions and evolving communication structures [6, 14], dynamic interleaving of sessions [4, 5], and nested or modular protocol structure [8]. More recent work supports replication [16] and unbounded participant creation [7]. Yet, dynamic evolution in these systems is not integrated with error handling: they cannot model recovery paths, restartable workflows, or liveness under partial failures.

**Refinements.** Refinement-typed MPST frameworks [21], specification-agnostic refinement systems [19], and design-by-contract choreographies [10] enhance MPST with logical constraints on values and control flow. These techniques are orthogonal to our contribution and represent natural future extensions to integrate with failure-aware dynamic protocols in order to verify liveness properties.

# 5 Conclusion and Future Work

This work introduced a global-type framework that extends Multiparty Session Types with explicit timeout and connection-error actions, dynamic thread spawning, and a precise notion of active participants. These additions enable the specification of communication behaviours that arise routinely in web applications, where concurrency, partial progress, and failures interact in ways not captured by existing MPST formalisms. We defined the syntax, labelled-transition semantics, and well-formedness conditions of the framework, and established core meta-theoretic guarantees, including preservation of well-formedness and the absence of orphan participants. Several directions remain open. A natural next step is the development of projection to local types and corresponding endpoint type systems, enabling static verification of implementations that incorporate failures and dynamic participants. Further work includes integrating stateful reasoning to capture the interplay between communication, persistent updates, and recovery, as well as developing automated analyses for liveness and consistency properties. Ultimately, we aim to support tool-assisted verification and type-safe implementations of realistic, fault-tolerant web protocols.

# References

[1] Manuel Adameit, Kirstin Peters & Uwe Nestmann (2017): *Session Types for Link Failures*. In Ahmed Bouajjani & Alexandra Silva, editors: *Formal Techniques for Distributed Objects, Components, and Systems*, Springer International Publishing, Cham, pp. 1–16, doi:10.1007/978-3-319-60225-7_1. Available at https://doi.org/10.1007/978-3-319-60225-7_1.
[2] Adam D. Barwell, Ping Hou, Nobuko Yoshida & Fangyi Zhou (2025): *Crash-Stop Failures in Asynchronous Multiparty Session Types*. Logical Methods in Computer Science Volume 21, Issue 2, p. 12622, doi:10.46298/lmcs-21(2:5)2025. Available at https://lmcs.episciences.org/12622.

[3] Adam D. Barwell, Alceste Scalas, Nobuko Yoshida & Fangyi Zhou (2022): *Generalised Multiparty Session Types with Crash-Stop Failures*. LIPIcs, Volume 243, CONCUR 2022 243, pp. 35:1–35:25, doi:10.4230/LIPICS.CONCUR.2022.35. Available at https://drops.dagstuhl.de/entities/document/10.4230/LIPICS.CONCUR.2022.35.

[4] Lorenzo Bettini, Mario Coppo, Loris D'Antoni, Marco De Luca, Mariangiola Dezani-Ciancaglini & Nobuko Yoshida (2008): *Global Progress in Dynamically Interleaved Multiparty Sessions*. In David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Madhu Sudan, Demetri Terzopoulos, Doug Tygar, Moshe Y. Vardi, Gerhard Weikum, Franck Van Breugel & Marsha Chechik, editors: CONCUR 2008 - Concurrency Theory, 5201, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 418–433, doi:10.1007/978-3-540-85361-9_33. Available at http://link.springer.com/10.1007/978-3-540-85361-9_33.

[5] Laura Bocchi, Romain Demangeon & Nobuko Yoshida (2013): *A Multiparty Multi-session Logic*. In Catuscia Palamidessi & Mark D. Ryan, editors: Trustworthy Global Computing, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 97–111.

[6] Marco Carbone, Kohei Honda & Nobuko Yoshida (2012): *Structured Communication-Centered Programming for Web Services*. ACM Trans. Program. Lang. Syst. 34(2), doi:10.1145/2220365.2220367. Available at https://doi.org/10.1145/2220365.2220367.

[7] David Castro-Perez & Nobuko Yoshida (2023): *Dynamically Updatable Multiparty Session Protocols: Generating Concurrent Go Code from Unbounded Protocols*. LIPIcs, Volume 263, ECOOP 2023 263, pp. 6:1–6:30, doi:10.4230/LIPICS.ECOOP.2023.6. Available at https://drops.dagstuhl.de/entities/document/10.4230/LIPICS.ECOOP.2023.6.

[8] Romain Demangeon & Kohei Honda (2012): *Nested Protocols in Session Types*. In David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Madhu Sudan, Demetri Terzopoulos, Doug Tygar, Moshe Y. Vardi, Gerhard Weikum, Maciej Koutny & Irek Ulidowski, editors: CONCUR 2012 – Concurrency Theory, 7454, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 272–286, doi:10.1007/978-3-642-32940-1_20. Available at http://link.springer.com/10.1007/978-3-642-32940-1_20.

[9] Simon Fowler, Sam Lindley, J. Garrett Morris & Sára Decova (2019): *Exceptional asynchronous session types: session types without tiers*. Proc. ACM Program. Lang. 3(POPL), doi:10.1145/3290341. Available at https://doi.org/10.1145/3290341.

[10] Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto & Nobuko Yoshida (2022): *Design-By-Contract for Flexible Multiparty Session Protocols*. LIPIcs, Volume 222, ECOOP 2022 222, pp. 8:1–8:28, doi:10.4230/LIPICS.ECOOP.2022.8. Available at https://drops.dagstuhl.de/entities/document/10.4230/LIPICS.ECOOP.2022.8.

[11] Kohei Honda (1993): *Types for dyadic interaction*. In G. Goos, J. Hartmanis & Eike Best, editors: CONCUR'93, 715, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 509–523,
doi:10.1007/3-540-57208-2_35. Available at http://link.springer.com/10.1007/3-540-57208-2_35.

[12] Kohei Honda, Nobuko Yoshida & Marco Carbone (2008): *Multiparty asynchronous session types*. In: *Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages*, ACM, San Francisco California USA, pp. 273–284, doi:10.1145/1328438.1328472. Available at https://dl.acm.org/doi/10.1145/1328438.1328472.

[13] Ping Hou, Nicolas Lagaillardie & Nobuko Yoshida (2024): *Fearless Asynchronous Communications with Timed Multiparty Session Protocols*. LIPIcs, Volume 313, ECOOP 2024 313, pp. 19:1–19:30, doi:10.4230/LIPICS.ECOOP.2024.19. Available at https://drops.dagstuhl.de/entities/document/10.4230/LIPICS.ECOOP.2024.19.

[14] Raymond Hu & Nobuko Yoshida (2017): *Explicit Connection Actions in Multiparty Session Types*. In: Marieke Huisman & Julia Rubin, editors: *Fundamental Approaches to Software Engineering*, 10202, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 116–133, doi:10.1007/978-3-662-54494-5_7. Available at https://link.springer.com/10.1007/978-3-662-54494-5_7.

[15] Nicolas Lagaillardie, Rumyana Neykova & Nobuko Yoshida (2022): *Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types*. In: *36th European Conference on Object-Oriented Programming (ECOOP 2022)*, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, pp. 4:1–4:29, doi:10.4230/LIPICS.ECOOP.2022.4. Available at https://drops.dagstuhl.de/entities/document/10.4230/LIPICS.ECOOP.2022.4.

[16] Matthew Alan Le Brun, Simon Fowler & Ornela Dardha (2025): *Multiparty Session Types with a Bang!* In: *Programming Languages and Systems: 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3–8, 2025, Proceedings, Part II*, Springer-Verlag, Berlin, Heidelberg, p. 125–153, doi:10.1007/978-3-031-91121-7_6. Available at https://doi.org/10.1007/978-3-031-91121-7_6.

[17] Dimitris Mostrous & Vasco T. Vasconcelos (2018): *Affine Sessions*. *Logical Methods in Computer Science* Volume 14, Issue 4, p. 4815, doi:10.23638/LMCS-14(4:14)2018. Available at http://lmcs.episciences.org/4815.

[18] Kirstin Peters, Uwe Nestmann & Christoph Wagner (2023): *FTMPST: Fault-Tolerant Multiparty Session Types*. *Logical Methods in Computer Science* Volume 19, Issue 4:14, doi:10.46298/lmcs-19(4:14)2023. Available at https://lmcs.episciences.org/10424.

[19] Martin Vassor & Nobuko Yoshida (2024): *Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation*. LIPIcs, Volume 313, ECOOP 2024 313, pp. 41:1–41:29, doi:10.4230/LIPICS.ECOOP.2024.41. Available at https://drops.dagstuhl.de/entities/document/10.4230/LIPICS.ECOOP.2024.41.

[20] Malte Viering, Raymond Hu, Patrick Eugster & Lukasz Ziarek (2021): *A multiparty session typing discipline for fault-tolerant event-driven distributed programming*. *Proceedings of the ACM on Programming Languages* 5(OOPSLA), pp. 1–30, doi:10.1145/3485501. Available at https://dl.acm.org/doi/10.1145/3485501.

[21] Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova & Nobuko Yoshida (2020): *Statically verified refinements for multiparty protocols*. *Proceedings of the ACM*
on Programming Languages 4(OOPSLA), pp. 1–30, doi:10.1145/3428216. Available at
https://dl.acm.org/doi/10.1145/3428216.

A Proof of Lemma 1

By induction on the derivation of $\Delta;\Gamma \vdash \mathcal{G}$ with $\alpha$-equivalence for renaming when needed.

B Proof of Lemma 2

By induction on the derivation of $\Delta;\Gamma \vdash \mathcal{G}$.

Case: [END]

We have $A(\mathcal{G}) = \emptyset$ so it trivially holds.

Case: [SUM]

We have $\mathcal{G} = \sum_{i \in I} \mathcal{G}_i$. By the inversion lemma<fnref n="1" />, we have

$$ [\text{SUM}] \frac{\Delta; \Gamma \vdash_p \mathcal{G}_i \quad \text{cons} \left( \sum_{i \in I} \mathcal{G}_i \right)}{\Delta; \Gamma \vdash \sum_{i \in I} \mathcal{G}_i} $$

As $\mathcal{G}_i$ is well-prefixed, the definition of crash gives:

$$ \mathcal{G}_{i \downarrow} r = \text{stop} \text{ or } \gamma_i . (\mathcal{G}_{i \downarrow}^{\text{next} \downarrow} r) \text{ or } \gamma_i \{r \downarrow / r\} . (\mathcal{G}_{i \downarrow}^{\text{next} \downarrow} r) $$

By the induction hypothesis, $\Delta'; \Gamma' \vdash_p \mathcal{G}_i^{\text{next} \downarrow} r$, all with the same environments $\Delta' = \Delta\{r \downarrow / r\}$ and $\Gamma' = \Gamma\{r \downarrow / r\}$. So in every cases, $\mathcal{G}_{i \downarrow} r$ is either well-prefixed or stop. By congruence, we remove the stop branches. Furthermore, the cons condition still holds because (i) every communication that ends with stop has a corresponding error branch, thus there exists an initiator, which is unique due to the removal-only nature of crash, (ii) and (iii) are true because it was true before and crash only removes some branches, and (iv) is true before branches have been removed. We thus have $\Delta'; \Gamma' \vdash \sum_{i \in I} (\mathcal{G}_{i \downarrow} r)$, and by definition of crash for sum, $\mathcal{G}_{i \downarrow} r$ is well-formed with the same environment.

Case: [REC]

By the inversion lemma and the induction hypothesis, the updated environment for X and $\Gamma$ are modified similarly, so the updated environment satisfies the hypothesis for [REC], applying it gives the result.

Case: [VAR-REC]

Same as [REC].

<footnote n="1">¹The inversion lemma holds in our system, as each well-formedness judgment corresponds to a unique syntactic form and no two well-formedness rules overlap. Because the rules are fully syntax-directed and contain no duplications or ambiguities, inversion follows immediately from the structure of the rules.</footnote>
Case: [PAR]

We remark that as participants cannot appear in both global type, only one may be updated. So one global type does not change through crash. The other one only sees its environment being updated without addition. Thus the hypothesis that environments are disjoint are still valid. By the inversion lemma and the induction hypothesis, we have that $\mathcal{G}$ is well-formed.

## C Proof of Theorem 3

*Proof.* By induction on the derivation of $\mathcal{G} \xrightarrow{\alpha} \mathcal{G}'$.

Case: [CHOICE]

The initiator selects a branch $j \in I$ with $\mathcal{G}_j \xrightarrow{\alpha} \mathcal{G}'_j$ and

$$ \sum_{i \in I} \mathcal{G}_i \xrightarrow{\alpha} \mathcal{G}'_j. $$

As the sum is well-formed, we have

$$ \frac{\Delta; \Gamma \vdash_{\mathcal{P}} \mathcal{G}_i \quad \text{cons} \left( \sum_{i \in I} \mathcal{G}_i \right)}{[\text{SUM}] \quad \Delta; \Gamma \vdash \sum_{i \in I} \mathcal{G}_i} $$

As $\mathcal{G}_j$ is well-prefixed, we have $\Delta; \Gamma \vdash_{\mathcal{P}} \gamma_j \cdot \mathcal{G}_j^{\text{next}}$. As $\alpha$ cannot be a crash, it can only be either a communication or an error from the initiator of the choice. In case of a message send on a private channel, $\Delta; \Gamma \vdash \mathcal{G}_j^{\text{next}} = \mathcal{G}'_j$. In case of a request or local thread spawn, $\Delta; \Gamma' \vdash \mathcal{G}_j^{\text{next}} = \mathcal{G}'_j$ where $\Gamma'$ has a new channel. In case of a timeout, we have $\Delta; \Gamma' \vdash \gamma'_j \cdot \mathcal{G}_j^{\text{next}} = \mathcal{G}'_j$ where $\Gamma'$ has a removed channel due to the timeout and $\gamma_j$ is updated by marking the initiator of the choice as not alive anymore on this specific channel. In case of a connection error, we have $\Delta; \Gamma \vdash \gamma'_j \cdot \mathcal{G}_j^{\text{next}} = \mathcal{G}'_j$ where $\gamma'_j$ is updated by marking the initiator of the choice as not alive anymore on this public channel creation. In all cases, $\mathcal{G}'_j$ is well-formed.

Case: [CHOICE-BR]

Here $\forall i \in I, \mathcal{G}_i \xrightarrow{\alpha} \mathcal{G}'_i$, and

$$ \sum_{i \in I} \mathcal{G}_i \xrightarrow{\alpha} \sum_{i \in I} \mathcal{G}'_i. $$

As the sum is well-formed, we have

$$ \frac{\Delta; \Gamma \vdash_{\mathcal{P}} \mathcal{G}_i \quad \text{cons} \left( \sum_{i \in I} \mathcal{G}_i \right)}{[\text{SUM}] \quad \Delta; \Gamma \vdash \sum_{i \in I} \mathcal{G}_i} $$

As all $\mathcal{G}_i$ are well-prefixed, we have $\Delta; \Gamma \vdash_{\mathcal{P}} \gamma_i \cdot \mathcal{G}_i^{\text{next}}$ and $\Delta_i, \Gamma_i \vdash \mathcal{G}_i^{\text{next}}$. There are two ways $\alpha$ may occur: it may reduce inside the continuation using rule CONCUR, or it may update the prefix itself.
* If the reduction occurs inside $\mathcal{G}_i^{\text{next}}$ for some branches, the induction hypothesis gives $\mathcal{G}_i^{\text{next}'}$ well-formed. Since the action cannot have as subjects the participant of the prefixed and cannot be a crash, the actions cannot modify the environment that the prefix rely on. As environments are all updated in the same manner due to the same action, we can find $\Delta'$, $\Gamma'$ such that $\Delta'; \Gamma' \vdash_p \gamma_i \cdot \mathcal{G}_i^{\text{next}'}$ and **cons** still holds because the prefix has not changed.

* If the prefix is updated for some branches and there are more than one branches, the only rule that can be available in all branches is a timeout on the receiver (1/2). Timeout removes the communication branches and marks the timeout branch as taken; in both cases the resulting prefixes remain well-prefixed, we remove the **stop** branches by congruence and **cons** still holds (branches are removed or still well-prefixed, which never violates **cons**). Thus the resulting choice is well-formed. If there is a single error branch, the other available rules are handled by the previous case for [CHOICE].

**Case: [VAR-REC]**

Here $\mu X \cdot \mathcal{G} \xrightarrow{\alpha} \mathcal{G}'$. We have $\Delta; \Gamma \vdash \mu X \cdot \mathcal{G}$ and by inversion, $\Delta, \mathcal{G} : \Gamma; \Gamma \vdash \mathcal{G}$. To use the induction hypothesis, we must show that $\mathcal{G}\{\mu X \cdot \mathcal{G} / X\}$ is well-formed. But this holds true because $X$ and $\mu X \cdot \mathcal{G}$ are well-formed under the same environment $\Gamma$. Thus, by the induction hypothesis on $\mathcal{G}\{\mu X \cdot \mathcal{G} / X\} \xrightarrow{\alpha} \mathcal{G}'$ we have $\mathcal{G}'$ is well-formed.

**Case: [PAR]**

Here $\mathcal{G}_1 || \mathcal{G}_2 \xrightarrow{\alpha} \mathcal{G}'_1 || \mathcal{G}_2$. We suppose that $\mathcal{G}_1$ and $\mathcal{G}_2$ have not shared recursion variable name or channel name due to $\alpha$-equivalence. We have

$$ [\text{PAR}] \frac{\Delta_1; \Gamma_1 \vdash \mathcal{G}_1 \quad \Delta_2; \Gamma_2 \vdash \mathcal{G}_2 \quad \Delta_1 \cap \Delta_2 = \emptyset \quad \Gamma_1 \cap \Gamma_2 = \text{pub}(\mathcal{G}_1) \cup \text{pub}(\mathcal{G}_2)}{\Delta_1, \Delta_2; \Gamma_1, \Gamma_2 \vdash \mathcal{G}_1 || \mathcal{G}_2} $$

As $\mathcal{G}_1$ is well-formed, by the induction hypothesis, we have $\Delta'_1; \Gamma'_1 \vdash \mathcal{G}'_1$. As there are no name clashes, the condition for well-formedness still holds, thus $\mathcal{G}'_1 || \mathcal{G}_2$ is well-formed.

□

# D Proof of Theorem 4

*Proof.* By induction on the derivation of $\Delta; \Gamma \vdash \mathcal{G}$. We show that if $\mathcal{G} \xrightarrow{\alpha} \mathcal{G}'$, then $\text{subj}(\alpha) \in A(\mathcal{G})$.

**Case: [SUM]**

As the sum is well-formed, we have

$$ [\text{SUM}] \frac{\Delta; \Gamma \vdash_p \mathcal{G}_i \quad \text{cons} \left( \sum_{i \in I} \mathcal{G}_i \right)}{\Delta; \Gamma \vdash \sum_{i \in I} \mathcal{G}_i} $$

There are two reduction modes.

**Case: [CHOICE]**

The initiator selects branch $j$ with $\mathcal{G}_j \xrightarrow{\alpha} \mathcal{G}'_j$. By inversion, $\mathcal{G}_j$ is well-prefixed, thus we
have $\Delta; \Gamma \vdash_{\mathbf{p}} \gamma_j . \mathcal{G}_j^{\text{next}}$. As $\alpha$ cannot be a crash, it can only be either a communication or an error from the initiator of the choice. In the following cases, we use the definition of $A(\gamma . \mathcal{G})$. In case of a message send on a private channel, $\mathit{subj}(\alpha) = \{\mathbf{p}, \mathbf{q}\} \in A(\mathcal{G}_j)$. In case of a request or local thread spawn, $\mathit{subj}(\alpha) = \{\mathbf{p}, \mathbf{q}\} \in A(\mathcal{G}_j)$. In case of a timeout, we have $\mathit{subj}(\alpha) = \{\mathbf{p}\} \in A(\mathcal{G}_j)$. In case of a connection error, we have $\mathit{subj}(\alpha) = \{\mathbf{p}\} \in A(\mathcal{G}_j)$.

**Case: [CHOICE-BR]**

Here $\alpha$ must be enabled in every branch, so for every $i$, we have $\mathcal{G}_i \xrightarrow{\alpha} \mathcal{G}_i'$. By inversion, $\mathcal{G}_i$ is well-prefixed, thus we have $\Delta; \Gamma \vdash_{\mathbf{p}} \gamma_i . \mathcal{G}_i^{\text{next}}$ and $\mathcal{G}_i^{\text{next}}$ is well-formed. $\alpha$ is either:

* an action inside $\mathcal{G}_i^{\text{next}}$, in which case the induction hypothesis applied to the premise $\mathcal{G}_i^{\text{next}}$ gives $\mathbf{subj}(\alpha) \in A(\mathcal{G}_i)$. If the prefix is not a request or a thread spawn, we have $A(\mathcal{G}_i) \subseteq A(\mathcal{G})$ by definition. If the prefix is a request or a thread spawn, the hypothesis to apply the rule [CONCUR] ensures that the subject is not in the participants of the prefix. As we remove one of the participants of the prefix, if the subject is not in it and is in $A(\mathcal{G}_i)$, it is also in $A(\mathcal{G})$;

* an update of the prefix $\gamma_i$, which is possible only for receiver-side timeout (?2). In this case, the subject is the receiver of $\gamma_i$, which is in $A(\mathcal{G})$.

**Case: [VAR-REC]**

By inversion, $\Delta, X : \Gamma; \Gamma \vdash \mathcal{G}$. Reduction unfolds the recursion through rule REC: $\mathcal{G}\{\mu X.\mathcal{G}/X\} \xrightarrow{\alpha} \mathcal{G}'$. By the induction hypothesis applied to $\mathcal{G}\{\mu X.\mathcal{G}/X\}$, $\mathbf{subj}(\alpha) \in A(\mathcal{G}\{\mu X.\mathcal{G}/X\})$. Since unfolding does not change the active participants of the body, $A(\mathcal{G}\{\mu X.\mathcal{G}/X\}) = A(\mathcal{G}) = A(\mu X.\mathcal{G})$. Thus $\mathbf{subj}(\alpha) \in A(\mathcal{G})$.

**Case: [PAR]**

By inversion, $\Delta = \Delta_1, \Delta_2$ and $\Gamma = \Gamma_1, \Gamma_2$, with disjoint domains, and $\mathcal{G} = \mathcal{G}_1 \parallel \mathcal{G}_2$ where $\Delta_1; \Gamma_1 \vdash \mathcal{G}_1$ and $\Delta_2; \Gamma_2 \vdash \mathcal{G}_2$. We have $\mathcal{G}_1 \xrightarrow{\alpha} \mathcal{G}_1'$. By the induction hypothesis applied to $\mathcal{G}_1$, $\mathbf{subj}(\alpha) \in A(\mathcal{G}_1)$. By definition of active participants, $A(\mathcal{G}_1) \subseteq A(\mathcal{G}_1 \parallel \mathcal{G}_2) = A(\mathcal{G})$. Thus $\mathbf{subj}(\alpha) \in A(\mathcal{G})$.

□