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

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
Safe asynchronous mixed-choice for timed
interactions*

Jonah Pears¹[0000-0003-4492-4072], Laura Bocchi¹[0000-0002-7177-9395], and Andy King¹[0000-0001-5806-4822]

University of Kent, Canterbury, UK
{jjp38, l.bocchi, a.m.king}@kent.ac.uk

**Abstract.** Mixed-choice has long been barred from models of asyn-
chronous communication since it compromises key properties of com-
municating finite-state machines. Session types inherit this restriction,
which precludes them from fully modelling timeouts – a key program-
ming feature to handle failures. To address this deficiency, we present (bi-
nary) TimeOut Asynchronous Session Types (TOAST) as an extension
to (binary) asynchronous timed session types to permit mixed-choice.
TOAST deploy timing constraints to regulate the use of mixed-choice so
as to preserve communication safety. We provide a new behavioural se-
mantics for TOAST which guarantees progress in the presence of mixed-
choice. Building upon TOAST, we provide a calculus featuring process
timers which is capable of modelling timeouts using a receive-after
pattern, much like Erlang, and informally illustrate the correspondence
with TOAST specifications.

**Keywords:** Session types · Mixed-choice · Timeouts · π-calculus

# 1 Introduction

Mixed-choice is an inherent feature of models of communications such as com-
municating finite-state machines (CFSM) [11] where actions are classified as
either send or receive. In this setting, a state of a machine is said to be mixed
if there exist both a sending action and a receiving action from that state.
When considering an asynchronous model of communication, absence of dead-
locks is undecidable in general [17] but can be guaranteed in presence of three
sufficient and decidable conditions: determinism, compatibility, and absence of
mixed-states [17,15]. Intuitively, determinism means that it is not possible, from
a state, to reach two different states with the same kind of action, and compat-
ibility requires that for each send action of one machine, the rest of the system
can eventually perform a complementary receive action.

* This work has been partially supported by EPSRC project EP/T014512/1 (STAR-DUST) and the BehAPI project funded by the EU H2020 RISE under the Marie Sklodowska-Curie action (No: 778233). We thank Simon Thompson and Maurizio Murgia for their insightful comments on an early version of this work.
<figure><img src="image_2.png" /><figcaption>**Fig. 1.** An Erlang snippet and its mixed-state machine representation</figcaption></figure>

In the desire to ensure deadlock freedom, mixed-choice has been given up, even though this curtails the descriptive capabilities of CFSM and its derivatives. Despite the rapid evolution of session types, even to the point of deployment in Java [19], Python [28,26], Rust [22], F# [27] and Go [13], thus far mixed-choice has only been introduced into the synchronous binary setting [29]. In fact, the exclusion of mixed-choice pervades work on asynchronous communication which guarantee deadlock-freedom, both for communicating timed automata [8,21] and session types [6,12,18,30]. Determinism and the absence of mixed-states is baked into the very syntax of session types (the correspondence between session types and so-called safe CFSM is explained in [15]).

Timed session types [4,9,10], which extend session types with time constraints, inherit the same syntactic restrictions of session types, and hence rule out mixed-states. This is unfortunate since in the timed setting, mixed-states are a useful abstraction for timeouts. Illustrated in Figure 1, the mixed-state CFSM (right) can be realised using a receive-after statement in Erlang (left). In the Erlang snippet, the process waits to receive either a ‘data’ or ‘done’ message. If neither are received within 3 seconds, then a timeout message is issued.

Timeouts are important for handling failure and unexpected delays, for instance, the SMTP protocol stipulates: “An SMTP client must provide a timeout mechanism” [20, Section 4.5.3.2]. Mixed-states would allow, for example, states where a server is waiting to receive a message from the client and, if nothing is received after a certain amount of time, send a notification that ends the session. Current variants of timed session types allow deadlines to be expressed but cannot, because of the absence of mixed-states, characterise (and verify) the behaviour that should follow a missed deadline, e.g., a restart or retry strategy. In this paper, we argue that time makes mixed-states more powerful (allowing timeouts to be expressed), while just adding sufficient synchronisation to ensure that mixed-states are safe in an asynchronous semantics (cannot produce deadlocks).

*Contributions* This work makes three orthogonal contributions to the theory of binary session types, with a focus on improving their descriptive capabilities:

- We introduce TimeOut Asynchronous (binary) Session Types (TOAST) to support timeouts. Inspired by asynchronous timed binary session types [9], TOAST shows how timing constraints provide an elegant solution for guaranteeing the safety of mixed-choice. Technically, we provide a semantics for
TOAST and a well-formedness condition. We show that well-formedness is sufficient to guarantee progress for TOAST (which may, instead, get stuck in general).

- We provide a new process calculus whose functionality extends to support programming motifs such as the widely used receive-after pattern of Erlang for expressing timeouts.

- We introduce timers in our process calculus to structure the counterpart of a timeout (i.e., a process that interacts with one other process displaying a timeout), as well as time-sensitive conditional statements, where the selection of a branch may be determined by timers. Time-sensitive conditional statements provide processes with knowledge that can be used to decide which branch should be followed e.g., helping understanding whether the counterpart may have timed out or not.

- We provide an informal discussion on the correspondence between TOAST and the aforementioned primitives of our new process calculus.

## 2 Timeout Asynchronous Session Types (TOAST)

This section presents the syntax, semantics and formation rules for TimeOut Asynchronous Session Types (TOAST), which extend asynchronous binary timed session types [9] with a well-disciplined (hence safe) form of mixed-choice.

*Clocks & Constraints* We start with a few preliminary definitions borrowed from timed automata [1]. Let $\mathcal{X}$ be a finite set of clocks denoted $x, y$ and $z$. A (clock) valuation $\nu$ is a map $\nu: \mathcal{X} \to \mathbb{R}_{\ge 0}$. The initial valuation is $\nu_0$ where $\nu_0 = \{x \mapsto 0 \mid x \in \mathcal{X}\}$. Given a time offset $t \in \mathbb{R}_{\ge 0}$ and a valuation $\nu, \nu+t = \{x \mapsto \nu(x)+t \mid x \in \mathcal{X}\}$. Given $\lambda \subseteq \mathcal{X}$ and $\nu, \lambda \mapsto 0$] = {$\nu(x) \mid x \in \mathcal{X}$}. Observe $\nu[\emptyset \mapsto 0] = \nu$. $\mathbb{G}(\mathcal{X})$ denotes the set of clock constraints, where a clock constraint $\delta$ takes the form:

$$ \delta ::= \mathbf{true} \mid x > t \mid x = t \mid x - y > t \mid x - y = t \mid \neg \delta \mid \delta_1 \wedge \delta_2 \quad (1) $$

We write $\nu \models \delta$ for a constraint $\delta$ that is satisfied by the valuations of clocks within $\nu$. We write $\downarrow \delta$ (the past of $\delta$) for a constraint $\delta'$ such that $\nu \models \delta'$ if and only if $\exists t: \nu + t \models \delta$. For example $\downarrow (3 < x < 5) = x < 5$ and $\downarrow (x > 2) = \mathbf{true}$.

### 2.1 Syntax of TOAST

The syntax of TOAST (or just *types*) is given in eq. (2). A type $S$ is a choice $\{c_i.S_i\}_{i \in I}$, recursive definition $\mu\alpha.S$, call $\alpha$, or termination type end.

$$ S ::= \{c_i.S_i\}_{i \in I} \mid \mu\alpha.S \mid \alpha \mid \textbf{end} \qquad c ::= \Box l \langle T \rangle (\delta, \lambda) \quad (2) $$

$$ T ::= (\delta, S) \mid \text{Nat} \mid \text{Bool} \mid \text{String} \mid \text{None} \mid \dots \qquad \Box ::= ! \mid ? $$

Type $\{c_i.S_i\}_{i \in I}$ models a choice among options $i$ ranging over a non-empty set $I$. Each option $i$ is a selection/send action if $\Box = !$, or alternatively a branching/receive action if $\Box = ?$. An option sends (resp. receives) a label $l$ and a message of a
specified data type *T* is delineated by *<>*. The send or receive action of an option is guarded by a time constraint *δ*. After the action, the clocks within *λ* are reset to 0. Data types, ranged over by *T*, *T*<sub>i</sub>, ... can be sorts (e.g., natural, boolean), or higher order types (*δ*, *S*) to model session delegation. Only the message label is exchanged when the data type is None. Labels of the options in a choice are pairwise distinct. Recursion and terminated types are standard.

*Remarks on the notation* One convention is to model the exchange of payloads as a separated action with respect to the communication of branching labels. In this paper we follow [8,31], and model them as unique actions. When irrelevant, we omit the payload, yielding a notation closer to that of timed automata.

## 2.2 Semantics of TOAST

We present the semantics of TOAST, building on those given in [9]; any changes are highlighted. Following [9], we define the semantics using three layers: (1) *configurations*, (2) *configurations with queues* that model asynchronous interactions, and (3) *systems* that model the parallel composition of configurations with queues. The semantics are defined over the labels *ℓ* given below:

$$ \ell ::= \Box m \mid t \mid \tau \qquad m ::= l \langle T \rangle \qquad \Box ::= ! \mid ? \qquad (3) $$

where *ℓ* is either a communication, time, or silent action, and *m* is a message.

**Configurations** A configuration *s* is a pair (*ν*, *S*). The semantics for configurations are defined by a Labelled Transition System (LTS) over configurations, the labels in eq. (3), and the rules given in Figure 2.

$$ \begin{array}{c} \nu \models \delta_j \quad j \in I \\ \frac{\begin{array}{c} (\nu, \{ \Box_i l_i \langle T_i \rangle (\delta_i, \lambda_i) . S_i \}_{i \in I}) \xrightarrow{\Box_j l_j \langle T_j \rangle} (\nu [\lambda_j \mapsto 0], S_j) \end{array}} {\text{[act]}} \\ \frac{\begin{array}{c} (\nu, S [\mu t . S / t]) \xrightarrow{\ell} (\nu', S') \\ (\nu, \mu t . S) \xrightarrow{\ell} (\nu', S') \end{array}} {\text{[unfold]}} \qquad (\nu, S) \xrightarrow{t} (\nu + t, S) \qquad \text{[tick]} \end{array} $$

<caption>**Fig. 2.** Semantics of Configurations.</caption>

Rule [act] deviates from [9] and handles choice types. By this rule, a configuration performs one action with index *j* ∈ *I* provided that the constraint *δ*<sub>*j*</sub> is satisfied in the current valuation *ν* (*ν* |*δ*<sub>*j*</sub>). All clocks in *λ*<sub>*j*</sub> are reset to 0 in the resulting configuration’s valuation of clocks. Rule [unfold] unfolds recursive types. Rule [tick] describes time passing. A transition *s* t□m s' indicates *s* t s'' t□m s', where *s''* is some intermediate configuration. We write *s* t□m if there exists *s'* such that *s* t□m s'.
<figure><img src="image_3.png" /><figcaption>**Fig. 3.** Semantics of Configurations with queues.</figcaption></figure>

**Configurations with queues** A configuration with queues $\mathbf{S}$ is a triple $(\nu, S, \mathbf{M})$ where $\mathbf{M}$ is a FIFO queue of messages which have been received but not yet processed. A queue takes the form $\mathbf{M} ::= \emptyset | m; \mathbf{M}$ thus is either empty, or has a message at its head. The transition $\mathbf{S} \xrightarrow{t \sqcap m} \mathbf{S}'$ is defined analogously to $\mathbf{s} \xrightarrow{t \sqcap m} \mathbf{s}'$. The semantics of configurations with queues is defined by an LTS over the labels in eq. (3) and the rules in Figure 3.

Rule [snd] is for sending a message. Message reception is handled by two rules: [que] inserts a message at the back of M, and [rcv] removes a message from the front of the queue. Rule [time] is for time passing which is formulated in terms of a future-enabled configuration, given in Definition 1. The second condition in the premise for rule [time] ensures the latest-enabled action is never missed by advancing the clocks. The third condition models an urgent semantics, ensuring messages are processed as they arrive. Urgency is critical for reasoning about progress.

**Definition 1 (Future-enabled Configurations (FE))**. For some $m$, a configuration $\mathbf{s}$ (resp. a configuration with queues $\mathbf{S}$) is future-enabled (FE) if $\exists t \in \mathbb{R}_{\ge 0} : \mathbf{s} \xrightarrow{t \sqcap m} (\text{resp. } \mathbf{S} \xrightarrow{t \sqcap m})$.

**Systems** Systems are the parallel composition of two configurations with queues, written as $(\nu_1, S_1, \mathbf{M}_1) | (\nu_2, S_2, \mathbf{M}_2)$ or $\mathbf{S}_1 | \mathbf{S}_2$. The semantics of systems is defined by an LTS over the labels in eq. (3) and the transition rules in Figure 4.

Rule [com-1] handles asynchronous communication where $\mathbf{S}_1$ sends a message $m$ via rule [snd], which arrives at the queue of $\mathbf{S}_2$ via rule [que]. Rule [com-r] is symmetric, allowing for $\mathbf{S}_2$ to be the sending party, and is omitted. Rule [par-1] allows $\mathbf{S}_1$ to process the message at the head of $\mathbf{M}_1$ via [rcv]. Rule [par-r] is symmetric, allowing $\mathbf{S}_2$ to receive messages, and is omitted. By rule [wait] time passes consistently across systems.

**Example 1 (Weak Persistency)**. In language-based approaches to timed semantics [21], time actions are always possible, even if they bring the model into a
$$ \frac{\mathbf{S}_1 \xrightarrow{1^m} \mathbf{S}'_1 \quad \mathbf{S}_2 \xrightarrow{?^m} \mathbf{S}'_2}{\mathbf{S}_1 | \mathbf{S}_2 \xrightarrow{\tau} \mathbf{S}'_1 | \mathbf{S}'_2} [\text{com-1}] \qquad \frac{\mathbf{S}_1 \xrightarrow{\tau} \mathbf{S}'_1}{\mathbf{S}_1 | \mathbf{S}_2 \xrightarrow{\tau} \mathbf{S}'_1 | \mathbf{S}_2} [\text{par-1}] \\ \frac{\mathbf{S}_1 \xrightarrow{t} \mathbf{S}'_1 \quad \mathbf{S}_2 \xrightarrow{t} \mathbf{S}'_2}{\mathbf{S}_1 | \mathbf{S}_2 \xrightarrow{t} \mathbf{S}'_1 | \mathbf{S}'_2} [\text{wait}] $$

<caption>Fig. 4. Semantics of Systems.</caption>

stuck state by preventing available actions. Execution traces are then filtered a posteriori, removing all ‘bad’ traces (defined on the basis of final states). In contrast, and to facilitate the reasoning on process behaviour, we adopt a process-based approach, e.g., [2,9], that only allows for actions that characterise *intended* executions of the model. Precisely, we build on the semantics in [2] for asynchronous timed automata with mixed-choice, where time actions are possible only if they do not disable: (1) the latest-enabled sending action, and (2) the latest-enabled receiving action if the queue is not empty. This ensures that time actions preserve the viability of at least one action (*weak-persistency*). In our scenario, constraint (1) is too strict. Consider type *S* and its dual below:

$$ S = \left\{ \begin{array}{l} ! \ data<\text{String}> (x < 3) . S' \\ ? \ timeout (x > 4) . \text{end} \end{array} \right\} \qquad \bar{S} = \left\{ \begin{array}{l} ? \ data<\text{String}> (y < 3) . \bar{S}' \\ ! \ timeout (y > 4) . \text{end} \end{array} \right\} $$

According to (1), it would never be possible for *S* to take the timeout branch since a time action of *t* ≥ 3 would disable the latest-enabled send. This is reasonable in [2] because, in their general setting, there is no guarantee that a timeout will indeed be received. Unlike [2], we can rely on duality of $\bar{S}$ (introduced later in this section), which guarantees that $\bar{S}$ will send a timeout message when *y* > 4. Our new rule [*time*] – condition (persistency) – implements a more general constraint than (1), requiring that one latest-enabled (send or receive) action is preserved. Constraint (2) remains to implement urgency and, e.g., prevents $\bar{S}$ from sending a timeout if a message is waiting in the queue when *y* < 3.

## 2.3 Duality, Well-formedness, and Progress

In the untimed scenario, the composition of a binary type with its dual characterises a *protocol*, which specifies the “correct” set of interactions between a party and its co-party. The dual of a type, formally defined below, is obtained by swapping the directions (! or ?) of each interaction:

**Definition 2 (Dual Types).** The dual type $\bar{S}$ of type *S* is defined as follows:

$$ \begin{gathered} \bar{\mu\alpha.S} = \mu\alpha.S \qquad \bar{\alpha} = \alpha \qquad \bar{end} = end \qquad \bar{!} = ? \\ \{ \Box_i l_i \langle T_i \rangle (\delta_i, \lambda_i) . S_i \}_{i \in I} = \{ \bar{\Box}_i l_i \langle T_i \rangle (\delta_i, \lambda_i) . \bar{S}_i \}_{i \in I} \qquad \bar{?} = ! \end{gathered} $$
Unfortunately, when annotating session types with time constraints, one may obtain protocols that are infeasible, as shown in Example 2. This is a known problem, which has been addressed by providing additional conditions or constraints on timed session types, for example compliance [3], feasibility [10], interaction enabling [8], and well-formedness [9].

Building upon [9], well-formedness is given as a set of formation rules for types. The rules check that in every reachable state (which includes every possible clock valuation) it is possible to perform the next action immediately or at some point in the future, unless the state is final. (This is formalized as the progress property in Definition 4.) By these rules, the type in Example 2 would not be well-formed. The use of mixed-choice in asynchronous communications may result in infeasible protocols or, more concretely, systems (or types) that get stuck, even if they are well-formed in the sense of [9] (discussed in Example 3).

**Example 2 (Junk Types).** Consider the junk type defined below:

$$S = !a (x > 3, \emptyset). \{!b (y = 2, \emptyset). \text{end}, ?c (2 < x < 5, \emptyset). \text{end}\}$$

Assume all clocks are 0 before $a$ is sent. After $a$ is sent, all clocks hold values greater than 3. The constraint on sending $b$ is never met, and the one on receiving $c$ may not be met. Types with unsatisfiable constraints are called junk types [9]. $S$ can be amended to obtain, for example, $S'$ or $S''$ below.

$$S' = !a (x > 3, \{y\}). \{!b (y = 2, \emptyset). \text{end}, ?c (2 < x < 5, \emptyset). \text{end}\}$$

$$S'' = !a (3 < x < 5, \emptyset). \{!b (y = 2, \emptyset). \text{end}, ?c (2 < x < 5, \emptyset). \text{end}\}$$

$S'$ makes both options of the choice satisfiable by resetting clock $y$, while $S''$ makes at least one option (?c) always satisfiable by changing the first constraint.

**Example 3 (Unsafe Mixed-choice).** A mixed-choice is considered unsafe if actions of different directions compete to be performed (i.e., they are both viable at the same point in time). Consider system $S_1 | S_2$, where $S_1 = (\nu_0, S_1, \emptyset)$, $S_2 = (\nu_0, S_2, \emptyset)$, and types $S_1$ and $S_2$ are dual as defined below:

$$S_1 = \begin{cases} ?a (x < 5) . \text{end} \\ !b (x = 0) . S'_1 \end{cases}$$

$$S_2 = \begin{cases} !a (y < 5) . \text{end} \\ ?b (y = 0) . S'_2 \end{cases}$$

In the system $S_1 | S_2$ it is possible for both $S_1 \stackrel{!b}{\to} S'_1$ and $S_2 \stackrel{!a}{\to} S'_2$ to occur at the same time. In the resulting system $(\nu_0, S'_1, a) | (\nu_0, \text{end}, b)$ neither message can be received, and $S'_1$ may be stuck waiting for interactions from $S'_2$ indefinitely.

**Well-formedness** In this work we extend well-formedness of [9] so that progress is guaranteed in the presence of mixed-choice. The formation rules for types are given in Figure 5; rules differing from [9] are highlighted. Types are evaluated against judgements of the form: $A; \delta \vdash S$ where $A$ is an environment containing recursive variables, and $\delta$ is a constraint over all clocks characterising the times in which state $S$ can be reached.
$$
\begin{array}{l}
\forall i \in I : A; \gamma_i \vdash S_i \wedge \delta_i[\lambda_i \mapsto 0] \models \gamma_i \quad (\text{feasibility}) \\
\forall i, j \in I : i \neq j \implies \delta_i \wedge \delta_j \models \mathbf{false} \lor \square_i = \square_j \quad (\text{mixed-choice}) \\
\forall i \in I : T_i = (\delta', S') \implies \emptyset; \gamma' \vdash S' \wedge \delta' \models \gamma' \quad (\text{delegation}) \\
\frac{}{A; \downarrow \bigvee_{i \in I} \delta_i \vdash \{\square_i l_i \langle T_i \rangle (\delta_i, \lambda_i) . S_i\}_{i \in I}} \qquad \text{[choice]} \\
\hline
\overline{A; \text{true} \vdash \text{end}} \quad \text{[end]} \qquad \frac{A, \alpha : \delta; \delta \vdash S}{A; \delta \vdash \mu\alpha.S} \quad \text{[rec]} \qquad \overline{A, \alpha : \delta; \delta \vdash \alpha} \quad \text{[var]}
\end{array}
$$

$$
\overline{A; \text{true} \vdash \text{end}} \quad [\text{end}] \quad \frac{A, \alpha : \delta; \delta \vdash S}{A; \delta \vdash \mu\alpha.S} \quad [\text{rec}] \quad \overline{A, \alpha : \delta; \delta \vdash \alpha} \quad [\text{var}]
$$

<caption>Fig. 5. Well-formedness rules for types.</caption>

Rule [choice] checks well-formedness of choices with three conditions: the first and third conditions are from the branching and delegation rules in [9], respectively; the second condition is new and critical to ensure progress of mixed-choice. By using the weakest past of all constraints ($\downarrow \bigvee_{i \in I} \delta_i$) only one of the options within the choice is required to be always viable, for the choice to be well-formed. The first condition (feasibility) ensures that, for each option in a choice, there exists an environment $\gamma$ such that the continuation $S_i$ is well-formed, given the current constraints on clocks $\delta_i$ (updated with resets in $\lambda_i$). This ensures that in every choice, there is always at least one viable action; it would, for example, rule out the type in Example 2. The second condition (mixed-choice) requires all actions that can happen at the same time to have the same (send/receive) direction. This condition allows for types modelling timeouts, as in Example 1, and rules out scenarios as the one in Example 3. The third condition (delegation) checks for well-formedness of each delegated session with respect to their corresponding initialization constraint $\delta'$. Rule [end] ensures termination types are always well-formed. Rule [rec] associates, in the environment, a variable $\alpha$ with an invariant $\delta$. Rule [var] ensures recursive calls are defined.

**Definition 3 (Well-formedness).** A type *S* is well-formed with respect to $\nu$
if there exists $\delta$ such that $\nu \models \delta$ and $\emptyset; \delta \vdash S$. A type *S* is well-formed if it is
well-formed with respect to $\nu_0$.

Well-formedness, together with the urgent receive features of the semantics (rule
[time] in Figure 3) ensures that the composition of a well-formed type *S* with its
dual *S* enjoys progress. A system enjoys progress if its configurations with queues
can continue communicating until reaching the end of the protocol, formally:

**Definition 4 (Type Progress).** A configuration with queues **S** is final if
**S** = (ν, end, Ø). A system **S**₁ | **S**₂ satisfies progress for all **S**'₁ | **S**'₂ reachable
from **S**₁ | **S**₂, either:

- **S'**₁ and **S'**₂ are final, or

- there exists a $t \in \mathbb{R}_{\ge 0}$ such that $\mathbf{S}'_1 | \mathbf{S}'_2 \xrightarrow{t\tau} \emptyset$.

**Theorem 1 (Progress of Systems).** If *S* is well-formed *against* *ν*₀ then (*ν*₀, *S*, ∅) | (*ν*₀, *S*, ∅) satisfies progress.
The main result of this section is that, for a system composed of *well-formed* and dual types, any state reached is either *final*, or allows for further progress. By ensuring a system will make progress, it follows that such a system is free from communication mismatches and will not reach deadlock.

The main differences with [9] is not in the formulation of the theory (e.g., Definitions 4 and 5, and the statement of Theorem 1 are basically unchanged) but in the proofs that, now, have to check that the conditions of rule [choice] are sufficient to ensure progress of asynchronous mixed-choice. Additionally, the proof of progress in [9] relies on receive urgency. Because of mixed-choice, it is necessary to reformulate (and relax) urgency in the semantic rule [time] in Figure 3. Despite generalising the notion of urgency the desired progress property can still be attained (see Example 1 for a discussion).

The proof of Theorem 1 proceeds by showing that system *compatibility* [9] is preserved by transitions. The formal definition of compatibility is given in Definition 5.

**Definition 5 (Compatible Systems).** Let $S_1 = (\nu_1, S_1, M_1)$ and $S_2 = (\nu_2, S_2, M_2)$. System $S_1 \mid S_2$ is compatible (written $S_1 \perp S_2$) if:

$$1. M_1 = \emptyset \lor M_2 = \emptyset$$

$$2. M_1 = M_2 = \emptyset \implies \nu_1 = \nu_2 \land S_1 = \overline{S_2}$$

$$3. M_1 = m; M'_1 \implies \exists \nu'_1, S'_1 : (\nu_1, S_1) \xrightarrow{?m} (\nu'_1, S'_1) \land (\nu'_1, S'_1, M'_1) \perp S_2$$

$$4. M_2 = m; M'_2 \implies \exists \nu'_2, S'_2 : (\nu_2, S_2) \xrightarrow{?m} (\nu'_2, S'_2) \land S_1 \perp (\nu'_2, S'_2, M'_2)$$

Informally, $S_1 \perp S_2$ if: (1) at most one of their queues is non-empty (equivalent to a half-duplex automaton), (2) if both queues are empty, then $S_1$ and $S_2$ have dual types and same clock valuations, and (3) and (4) a configuration is always able to receive any message that arrives in its queue.

## 3 A Calculus for Processes with Timeouts

We present a new calculus for timed processes which extends existing timed session calculi [8,9] with: (1) timeouts, and (2) time-sensitive conditional statements. Timeouts are defined on receive actions and may be immediately followed by sending actions, hence providing an instance of mixed-choice – which is normally not supported. Time-sensitive conditional statements (i.e., if-then-else with conditions on program clocks/timers) provide a natural counterpart to the timeout construct and enhance the expressiveness of the typing system in [9]. By counterpart, we intend a construct to be used by the process communicating with the one that sets the timeout.
Processes are defined by the grammar below. To better align processes with
TOAST, send and select actions have been streamlined by each message con-
sisting of both a label *l* and some message value *v*, which is either data or a
delegated session; the same holds for receive/branch actions where *q* is a vari-
able for data or delegated sessions. We assume a set of timer names *T*, ranged
over by *x*, *y* and *z*.

$$
\begin{array}{l@{\hspace{4em}}l@{\hspace{2em}}l}
P, Q ::= & \mathbf{set}(x).P & X\langle\mathbf{v}; \mathbf{t}; \mathbf{r}\rangle \\
| & p \triangleleft \mathit{lv}.P & \emptyset \\
| & p \triangleright \{l_i(q_i) : P_i\} & \mathbf{after} \ e : Q \\
| & \mathbf{if} \ \delta \ \mathbf{then} : P \ \mathbf{else} : Q & (\nu pq)P \\
| & \mathbf{delay}(\delta).P & P \mid Q \\
| & \mathbf{delay}(t).P & qp : h \\
| & \mathbf{def} \ X(\mathbf{v}; \mathbf{t}; \mathbf{r}) = P \ \mathbf{in} \ Q & h ::= \emptyset \mid h \cdot \mathit{lv}
\end{array}
\qquad (4)
$$

Process set (x) .P creates a timer x, initialises it to 0 and continues as P. If x already exists it is reset to 0. For simplicity, we assume that the timers set by each process P and Q in a parallel composition P | Q are pair-wise disjoint.

Process $p \triangleleft \mathit{lv}.P$ is the select/send process: it selects label $l$ and sends payload $\mathbf{v}$ to endpoint $p$, and continues as $P$. Its dual is the branch/receive process $p \triangleright \{l_i(\mathbf{v}_i) : P_i\}_{i \in I} \mathbf{after} e : Q$. It receives one of the labels $l_i$, instantiates $q_i$ with the received payload, and continues as $P_i$. (Note that a similar construct has been used to model timeouts in the Temporal Process Language [7], outside of session types.) Parameter $e$ is a linear expression over the timers and numeric constants drawn from $\mathbb{N}_{\ge 0} \cup \{\infty\}$. The expression $e$ determines the duration of a timeout, after which $Q$ is executed. Once a process with an **after** branch is reached, its expression $e$ is evaluated against the values of the timers, to derive a timeout value $n$ where $n \in \mathbb{N}_{\ge 0} \cup \{\infty\}$. Setting $e = \infty$ models a blocking receive primitive that waits potentially forever for a message. Setting $e = 0$ models a non-blocking receive action. To retain expressiveness from [9] where non-blocking receive actions would trigger an exception (i.e., modelling deadlines that must not be missed) we allow $Q$ to be **error**. For simplicity: (i) we write $p \triangleright \{l_i(q_i) : P_i\}_{i \in I}$ when $e = \infty$; (ii) we omit the brackets in the case of a single option; (iii) for options with no payloads we omit $q_i$. The advantage of using an expression $e$ to express the value of a timeout, rather than a fixed constant, is illustrated in Example 4.

Process `if δ then : P else : Q` is a conditional statement, except that the condition `δ` is on timers. Syntactically, the condition is expressed as a time constraint `δ` in eq. (1), but instead of clocks, defined on the timers previously set by that process. Process `delay(δ).P` models time passing for an unknown duration described by `δ`, and is at runtime reduced to process `delay(t).P` if `|δ|` = `δ[t/x]`. In `delay(δ).P` we assume `δ` is a constraint on a single clock `x`. The name of the clock here is immaterial, where `x` is a syntactic tool used to determine the duration of a time-consuming (delay) action at run-time. In this sense, assume `x` is bound within `delay(δ).P`. Recursive processes are defined by a process variable
X and parameters v, T and r containing base type values, timers and session channels, respectively. The end process is 0. The error process is error.

As standard [10,18,30], the process calculus allows parallel processes $P | Q$ and scoped processes $(\nu pq)P$ between endpoints $p$ and $q$. Endpoints communicate over pairs of channels $pq$ and $qp$, each with their own unbounded FIFO buffers $h$.<fnref n="1" /> Within a session, $p$ sends messages over $pq$ and receives messages from $qp$ (and vica versa for $q$). We have adopted the simplifying assumption in [9] that sessions are already instantiated. Therefore, rather than relying on reduction rules to produce correct session instantiation, we rely on a syntactic well-formedness assumption. A *well-formed process* consists of sessions of the form $(\nu pq)(P | Q | pq : h | qp : h')$, which can be checked syntactically as in [9].

*Example 4 (Parametric Timeouts).* Consider the process below:

$$ \mathit{delay}(z < 2).p \triangleright \{ \mathit{msg} : P \} \mathit{after} 3 : Q $$

It expresses a timeout of 3 after a delay with a duration between 0 and 2 time units (whatever this delay turns out to be). To express a timeout of 3 despite prior execution of a time-consuming action, we need a way to tune the timeout with the actual delay of the time-consuming action. A *parametric timeout* can model this behaviour:

$$ \mathit{set}(x).\mathit{delay}(z < 2).p \triangleright \{ \mathit{msg} : P \} \mathit{after} 3 - z : Q $$

By setting the timeout as an expression, $3 - x$, with parameter $x$ reflecting the passage of time, we allow the process to compensate for the exact delay occurred.

## 3.1 Process Reduction

A *timer environment* $\theta$ is a map from a set of timer names $\mathbb{T}$ to $\mathbb{R}_{\ge 0}$. We define $\theta + t = \{x \mapsto \theta(x) + t \mid x \in \mathbb{T}\}$ and $\theta[x \mapsto 0]$ to be the map $\theta[x \mapsto 0](y) = \text{if } (x = y) 0 \text{ else } \theta(y)$.

The semantics of processes are given in Figure 6, as a reduction relation on pairs of the form $(\theta, P)$. The reduction relation is defined on two kinds of reduction: instantaneous communication actions $\to$, and time-consuming actions $\rightsquigarrow$. We write $\to$ to denote a reduction that is either by $\to$ or $\rightsquigarrow$.

Rule [Set] creates a new timer $x$ if $x$ is undefined, and otherwise resets $x$ to 0. Rule [IfT] selects a branch $P$ depending on time-sensitive condition $\delta$. The symmetric rule selects branch $Q$ if the condition is not met, and is omitted. Rules [Recv] and [Send] are standard [24]. Rule [Det] determines the actual duration $t$ of the delay $\delta$ (which is a constraint on a single clock). Rule [Delay] outsources time-passing to function $\Phi_t(P)$ (see Definition 6), which returns process $P$ after the elapsing of $t$ units of time, and updates $\theta$ accordingly. Rules [Scope] and [ParL] are as standard and the only instant reductions, which may update $\theta$, if any timers are introduced by [Set]. We omit the symmetric rule for [ParL]. The rule for structural congruence [Str] applies to both instantaneous and

<footnote n="1">¹ Similar to the queues used by configurations in Section 2.2.</footnote>
<figure><img src="image_4.png" /><figcaption>Fig. 6. Reduction Rules for Processes</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Fig. 7. Definition of Wait(P) and NEQueue(P)</figcaption></figure>
time-consuming actions. Structural equivalence of P and Q, denoted $P \equiv Q$ is
as standard with the addition of rule delay(0). $P \equiv P$ following [9,10].

**Definition 6.** The time-passing function $\Phi_t(P)$ is a partial function on process terms, defined only for the cases below, where we use $C_I$ as a short notation for $\{l_i(v_i) : P_i\}_{i \in I}$:

$$
\begin{align*}
\Phi_t (p \triangleright C_I \text{ after } e : Q) &= \begin{cases} p \triangleright C_I \text{ after } e : Q & e = \infty \\ p \triangleright C_I \text{ after } e - t : Q & e \in \mathbb{R}_{\ge 0} \text{ and } e \ge t \\ \Phi_{t-e}(Q) & \text{otherwise} \end{cases} \\
\Phi_t (\text{delay}(t').P) &= \begin{cases} \text{delay}(t' - t).P & \text{if } t' \ge t \\ \Phi_{t-t'}(P) & \text{otherwise} \end{cases} \\
\Phi_t (P_1 | P_2) &= \Phi_t (P_1) | \Phi_t (P_2) & \text{if } \text{Wait}(P_i) \cap \text{NEQueue}(P_j) = \emptyset, i \ne j \in \{1, 2\} \\
\Phi_t (\emptyset) &= \emptyset & \Phi_t (\text{error}) &= \text{error} \\
\Phi_t (pq : h) &= pq : h & \Phi_t ((\nu pq) P) &= (\nu pq) \Phi_t (P) \\
\Phi_t (\text{def } X(\mathbf{v}; \mathbf{t}; \mathbf{R}) = P \text{ in } Q) &= \text{def } X(\mathbf{v}; \mathbf{t}; \mathbf{R}) = P \text{ in } \Phi_t (Q)
\end{align*}
$$

The first case in Definition 6 models the effect of time passing on timeouts. The
second case is for time-consuming processes. The third case distributes time
passing in parallel compositions and ensures that time passes for all parts of the
system equally. The auxiliary functions Wait(P) and NEQueue(P) ensure time
does not pass while a process is waiting to receive a message already in their
queue, similar to rule [time] in Figure 3 for configuration transitions. Informally,
Wait(P) returns the set of channels on which P is waiting to receive a message,
and NEQueue(P) returns the set of endpoints with a non-empty inbound queue.
Full definitions are given in Figure 7. The remaining cases allow time to pass.

*Example 5.* Consider the process below:

$$
P = (\nu pq) (p \triangleright \{l_i(v_i) : P_i\}_{i \in I} \text{ after } e : Q \mid qp : \emptyset \mid Q')
$$

For a time-consuming action of *t* to occur on *P* it is required that $\Phi_t$ is defined for all parallel components in *P*. Note that, if *qp* was not empty, then time could not pass since $\text{NEQueue}(P) = \text{Wait}(P) = \{p\}$. Set *t* = *n* + 1 so that we can observe the expiring of the timeout. The evaluation of $\Phi_t (p \triangleright \{l_i(v_i) : P_i\}_{i \in I} \text{ after } e : Q)$ results in the evaluation of $\Phi_1(Q)$. If $Q = \emptyset$ (or similarly error, a delay, or a timeout with $n > 0$) and $\Phi_t(Q')$ is defined then time passing of *t* is possible and:

$$
\Phi_t (P) = (\nu pq)(\emptyset | qp : \emptyset | \Phi_t (Q'))
$$

If $Q$ is a sending process then $\Phi_t(Q)$ would be undefined, and hence $\Phi_t(P)$.
# 4 Expressiveness

In this section we reflect on the expressiveness of our mixed-choice extension, particularly in regard to [9], using examples to illustrate differences. Furthermore, given the increase in expressiveness, we discuss how type-checking becomes more interesting with the inclusion of receive-after.

## 4.1 Missing deadlines

The process corresponding to ?a (true, Ø).S is merely $p \triangleright \{a : P\}$, which waits to receive a forever. By way of contrast, ?a ($x < 3$, Ø).S, cannot receive when $x \ge 3$, requiring the process to take the form: $p \triangleright \{a : P\}$ after 3 : Q, where Q = error. More generally, if an action is enabled when $x \ge 3$:

$$ \{?a (x < 3, \emptyset).S, ?b (3 < x < 5, \emptyset).S'\} $$

then, amending the previous process, $Q = p \triangleright \{b : P'\}$ after 2 : error.

## 4.2 Ping-pong protocol

The example in this section illustrates the usefulness of time-sensitive conditional statements. The ping-pong protocol consists of two participants exchanging messages between themselves on receipt of a message from the other [23]. One interpretation of the protocol is the following:

$$ \mu\alpha. \left\{ \begin{array}{l} !ping(x \le 3, \{x\}). \left\{ \begin{array}{l} ?ping(x \le 3, \{x\}).\alpha \\ ?pong(x > 3, \{x\}).\alpha \end{array} \right\} \\ \\ !pong(x > 3, \{x\}). \left\{ \begin{array}{l} ?ping(x \le 3, \{x\}).\alpha \\ ?pong(x > 3, \{x\}).\alpha \end{array} \right\} \end{array} \right\} $$

where each participant exchanges the role of sender, either sending ping early, or pong late. Without time-sensitive conditional statements, the setting in [9] only allows implementations where the choice between the 'ping' and the 'pong' branch are hard-coded. In presence of non-deterministic delays (e.g., delay($z < 6$)), the hard-coded choice can only be for the latest branch to 'expire', and the highlighted fragment of the ping-pong protocol above could be naively implemented as follows (omitting Q for simplicity):

$$ \texttt{def } X(v; t; r) = P \text{ in } P \quad P = \text{delay}(z < 6). p \triangleleft pong.Q $$

The choice of sending ping is always discarded as it may be unsatisfied in some executions. The calculus in this paper, thanks to the time-awareness deriving from a program timer y, allows us to potentially honour each branch, as follows:

$$ \begin{array}{l} \texttt{def } X(v; t; r) = P \text{ in } P \quad P = \text{set}(y).\text{delay}(z < 6). \text{if } (y \le 3) \\ \quad \quad \text{then : } p \triangleleft \text{ping}.Q \\ \quad \quad \text{else : } p \triangleleft \text{pong}.Q' \end{array} $$
<figure><img src="image_6.png" /><figcaption>Fig. 8. Message throttling protocol for $m = 2$.</figcaption></figure>

## 4.3 Mixed-choice Ping-pong protocol

An alternative interpretation of the ping-pong protocol can result in an implementation with mixed-choice, as shown below:

$$ \mu\alpha. \left\{ \begin{array}{l} ?ping(x \le 3, \{x\}).\left\{ \begin{array}{l} !pong(x \le 3, \{x\}).\alpha \\ ?timeout(x > 3, \emptyset).\end{array} \right\} \\ \\ !pong(x > 3, \{x\}).\left\{ \begin{array}{l} ?ping(x \le 3, \{x\}).\alpha \\ !timeout(x > 3, \emptyset).\end{array} \right\} \end{array} \right\} $$

where pings are responded by pongs and vica versa. Notice that if a timely ping is not received, a pong is sent instead, which if not responded to by a ping, triggers a timeout. Similarly, once a ping has been received, a pong must be sent on time to avoid a timeout. Such a convoluted protocol can be fully implemented:

$$ \begin{array}{l} \textbf{def } X(v; t; r) = P \text{ in } P \\ P = \text{set}(x).p \triangleright \text{ping} : \text{set}(x).\text{if } (x \le 3) \\ \quad \text{then} : p \triangleleft \text{pong}.X(v'; t'; r') \\ \quad \text{else} : p \triangleright \text{timeout} : \emptyset \\ \text{after } 3-x : p \triangleleft \text{pong}.\text{set}(x).p \triangleright \text{pong} : X(v''; t''; r'') \\ \quad \quad \text{after } 3-x : p \triangleleft \text{timeout}.\emptyset \end{array} $$

## 4.4 Message throttling

A real-world application of the previous example is message throttling. The rationale behind message throttling is to cull unresponsive processes, which do not keep up with the message processing tempo set by the system. This avoids a server from becoming overwhelmed by a flood of incoming messages. In such a protocol, upon receiving a message, a participant is permitted a grace period to respond before receiving another. The grace period is specified as a number of unacknowledged messages, rather than a period of time. Below we present a fully parametric implementation of this behaviour, where $m$ is the maximum number of messages that can go unacknowledged before a timeout is issued.

$$ \begin{align*} S_0 &= \mu\alpha^0. !msg(x \ge 3, \{x\}).S_1 \\ S_i &= \mu\alpha^i. \{ ?ack(x < 3, \{x\}).\alpha^{i-1}, !msg(x \ge 3, \{x\}).S_{i+1} \} \\ S_m &= \{ ?ack(x < 3, \{x\}).\alpha^{m-1}, !tout(x \ge 3, \emptyset).\end{align*} $$
which has the corresponding processes:

$$ \mathbf{def} X_0 (v_0; t_0; r_0) = P_0 \text{ in } p \triangleleft msg.P_1 $$

$$ \mathbf{def} X_i (v_i; t_i; r_i) = P_i \text{ in } p \triangleright ack : X_{i-1} \langle v_{i-1}; t_{i-1}; r_{i-1} \rangle \\ \text{after } 3 : p \triangleleft msg.P_{i+1} $$

$$ P_m = p \triangleright ack : P_{m-1} \\ \text{after } 3 : p \triangleleft tout.\emptyset $$

The system shown in fig. 8 illustrates the system for the $m = 2$ instance. Arguably, instead of sending the message *tout*, it would also be equally valid for the system to simply reach an error state: $P_m = p \triangleright ack : P_{m-1} \text{ after } 3 : \text{error}$.

# 5 Concluding Discussion

We have shown how timing constraints provide an intuitive way of integrating mixed-choice into asynchronous session types. The desire for mixed-choice has already prompted work in (untimed) synchronous session types [29]. Further afield, coordination structures have been proposed that overlap with mixed-choice, for example, fork and join [14], which permit messages within a fork (and its corresponding join) to be sent or received in any order; reminiscent of mixed-choice. Affine sessions [23,25] support exception handling by enabling an end-point to perform a subset of the interactions specified by their type, but there is no consideration of time, hence timeouts. Before session types gained traction, timed processes [5] were proposed for realising timeouts, but lacked any notion of a counterpart for timeouts.

We have integrated the notion of mixed-choice with that of time-constraints. There are many conceivable ways to realise mixed-choice using programming primitives. However, our integration with time, embodied in TOAST, offers new capabilities for modelling timeouts which sit at the heart of protocols and are a widely-used idiom in programming practice. To provide a bridge to programming languages, we provide a timed session calculus enriched with a receive-after pattern and process timers, the latter providing a natural counterpart to the former. Taken altogether, we have lifted a long-standing restriction on asynchronous session types by allowing for safe mixed-choice, through the judicious application of timing constraints.

Future work will provide type checking against TOAST for our new processes, and establish time-safety (a variant of type-safety which ensures punctuality of interactions via subject reduction) for well-typed processes. Time-safety for timed session types [9,10] (without mixed-choice) relies on a progress property called receive-liveness, which is defined on the untimed counterpart of a timed process. Receive-liveness that can be checked with existing techniques for global progress [6,16]. A progress property may seem too strong a precondition for ensuring time-safety. In untimed formulations of session types, type-safety and subject reduction do not depend on progress. Arguably, when considering time and punctuality, the distinction between progress and safety is no longer clear-cut, since deadlocks may cause violation of time constraints.
References

1. Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8

2. Bartoletti, M., Bocchi, L., Murgia, M.: Progress-Preserving Refinements of CTA. In: CONCUR. Leibniz International Proceedings in Informatics, vol. 118, pp. 40:1–40:19. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2018). https://doi.org/10.4230/LIPIcs.CONCUR.2018.40

3. Bartoletti, M., Cimoli, T., Murgia, M.: Timed Session Types. Logical Methods in Computer Science 13(4) (2017). https://doi.org/10.23638/LMCS-13(4:25) 2017

4. Bartoletti, M., Cimoli, T., Pinna, G.M.: A note on two notions of compliance. EPTCS 166, 86–93 (2014). https://doi.org/10.4204/EPTCS.166.9

5. Berger, M., Yoshida, N.: Timed, Distributed, Probabilistic, Typed Processes. In: APLAS. Lecture Notes in Computer Science, vol. 4807, pp. 158–174. Springer-Verlag (2007). https://doi.org/10.1007/978-3-540-76637-7_11

6. Bettini, L., Coppo, M., D'Antoni, L., Luca, M.D., Dezani-Ciancaglini, M., Yoshida, N.: Global Progress in Dynamically Interleaved Multiparty Sessions. In: CONCUR. Lecture Notes in Computer Science, vol. 5201, pp. 418–433. Springer-Verlag (2008). https://doi.org/10.1007/978-3-540-85361-9_33

7. Bocchi, L., Lange, J., Thompson, S., Voinea, A.L.: A Model of Actors and Grey Failures. In: COORDINATION. Lecture Notes in Computer Science, vol. 13271, pp. 140–158. Springer-Verlag (2022). https://doi.org/10.1007/978-3-031-08143-9_9

8. Bocchi, L., Langue, J., Yoshida, N.: Meeting Deadlines Together. In: CONCUR. Leibniz International Proceedings in Informatics, vol. 42, pp. 283–296 (2015). https://doi.org/10.4230/LIPIcs.CONCUR.2015.283

9. Bocchi, L., Murgia, M., Vasconcelos, V.T., Yoshida, N.: Asynchronous timed session types: from duality to time-sensitive processes. In: ESOP. Lecture Notes in Computer Science, vol. 11423, pp. 583–610. Springer-Verlag (2019). https://doi.org/10.1007/978-3-030-17184-1_21, https://kar.kent.ac.uk/72337/

10. Bocchi, L., Yang, W., Yoshida, N.: Timed Multiparty Session Types. In: CONCUR. Lecture Notes in Computer Science, vol. 8704, pp. 419–434. Springer-Verlag (2014). https://doi.org/10.1007/978-3-662-44584-6_29

11. Brand, D., Zafropulo, P.: On Communicating Finite-State Machines. Journal of the ACM 30(2), 323–342 (1983). https://doi.org/10.1145/322374.322380

12. Carbone, M., Honda, K., Yoshida, N.: Structured Interactional Exceptions in Session Types. In: CONCUR. Lecture Notes in Computer Science, vol. 5201, pp. 402–417. Springer Berlin Heidelberg (2008). https://doi.org/10.1007/978-3-540-85361-9_32

13. Castro, D., Hu, R., Jongmans, S.S., Ng, N., Yoshida, N.: Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures. In: POPL. vol. 3, pp. 1–30. ACM (2019). https://doi.org/10.1145/3290342

14. Deniélou, P.M., Yoshida, N.: Multiparty Session Types Meet Communicating Automata. In: ESOP. Lecture Notes in Computer Science, vol. 7966, pp. 194–213. Springer-Verlag (2012). https://doi.org/10.1007/978-3-642-28869-2_10

15. Deniélou, P.M., Yoshida, N.: Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. In: ICALP. Lecture Notes in Computer Science, vol. 7966, pp. 174–186. Springer-Verlag (2013). https://doi.org/10.1007/978-3-642-39212-2_18
16. Dezani-Ciancaglini, M., de'Liguoro, U., Yoshida, N.: On Progress for Structured Communications. In: Trustworthy Global Computing. Lecture Notes in Computer Science, vol. 4912, pp. 257–275. Springer-Verlag (2007). https://doi.org/10.1007/978-3-540-78663-4_18, https://doi.org/10.1007/978-3-540-78663-4_18

17. Gouda, M., Manning, E., Yu, Y.: On the progress of communication between two finite state machines. Information and Control **63**(3), 200–216 (1984). https://doi.org/10.1016/S0019-9958(84)80014-5

18. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL. pp. 273–284. ACM (2008). https://doi.org/10.1145/1328438.1328472

19. Hu, R., Yoshida, N., Honda, K.: Session-Based Distributed Programming in Java. In: ECOOP. Lecture Notes in Computer Science, vol. 5142, pp. 516–541. Springer-Verlag (2008). https://doi.org/10.1007/978-3-540-70592-5_22

20. Klensin, J.: SMTP, Request for Comments: 5321 (2008), https://datatracker.ietf.org/doc/html/rfc5321

21. Krcál, P., Yi, W.: Communicating Timed Automata: The More Synchronous, the More Difficult to Verify. In: CAV. Lecture Notes in Computer Science, vol. 4144, pp. 249–262. Springer-Verlag (2006). https://doi.org/10.1007/11817963_24

22. Lagaillardie, N., Neykova, R., Yoshida, N.: Implementing Multiparty Session Types in Rust. In: COORDINATION. pp. 127–136. Springer-Verlag (2020). https://doi.org/10.1007/978-3-030-50029-0_8

23. Lagaillardie, N., Neykova, R., Yoshida, N.: Stay Safe under Panic: Affine Rust Programming with Multiparty Session Types. In: ECOOP. Leibniz International Proceedings in Informatics, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2022). https://doi.org/10.4230/LIPIcs.ECOOP.2022.4

24. Milner, R.: Communicating and mobile systems - the Pi-calculus. Cambridge University Press (1999)

25. Mostrous, D., Vasconcelos, V.T.: Affine Sessions. Logical Methods in Computer Science **14**(4) (2018). https://doi.org/10.23638/LMCS-14(4:14)2018

26. Neykova, R.: Session Types Go Dynamic or How to Verify Your Python Conversations. EPTCS **137** (2013). https://doi.org/10.4204/EPTCS.137.8

27. Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: compile-time API generation of distributed protocols with refinements in F#. In: CC. pp. 128–138. ACM (2018). https://doi.org/10.1145/3178372.3179495

28. Neykova, R., Yoshida, N., Hu, R.: SPY: Local Verification of Global Protocols. In: RV. Lecture Notes in Computer Science, vol. 8174, pp. 358–363. Springer-Verlag (2013). https://doi.org/10.1007/978-3-642-40787-1_25, https://doi.org/10.1007/978-3-642-40787-1_25

29. Vasconcelos, V.T., Casal, F., Almeida, B., Mordido, A.: Mixed Sessions. In: ESOP. Lecture Notes in Computer Science, vol. 12075, pp. 715–742. Springer International Publishing (2020). https://doi.org/10.1007/978-3-030-44914-8_26

30. Yoshida, N., Vasconcelos, V.T.: Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication. Electronic Notes in Theoretical Computer Science **171**(4), 73–93 (2007). https://doi.org/10.1016/j.entcs.2007.02.056

31. Yoshida, N., Zhou, F., Ferreira, F.: Communicating Finite State Machines and an Extensible Toolchain for Multiparty Session Types. In: Fundamentals of Computation Theory. Lecture Notes in Computer Science, vol. 12867, pp. 18–35. Springer-Verlag (2021). https://doi.org/10.1007/978-3-030-86593-1_2