# On the Almost-Sure Termination of Binary Sessions

Ugo Dal Lago, Luca Padovani

► To cite this version:

Ugo Dal Lago, Luca Padovani. On the Almost-Sure Termination of Binary Sessions. PPDP 2024 - 26th International Symposium on Principles and Practice of Declarative Programming, Sep 2024, Milano, Italy. pp.1 - 12, 10.1145/3678232.3678239. hal-04836087

HAL Id: hal-04836087

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

Submitted on 13 Dec 2024

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# On the Almost-Sure Termination of Binary Sessions

Ugo Dal Lago

Università di Bologna

Italy

INRIA Sophia Antipolis

France

Luca Padovani

Università di Camerino

Italy

## ABSTRACT

We investigate the termination problem in a calculus of sessions with probabilistic choices. In this setting, a whole range of termination properties can be defined, from the weaker almost-sure termination to strong almost-sure termination, passing through positive almost-sure termination. We present two similar session type systems closely related to classical linear logic with exponents that guarantee the two extremal properties in such range. In both type systems, the definitional overhead that deals with the ensured termination property is kept to a minimum.

## CCS CONCEPTS

* Theory of computation → Process calculi; Linear logic; Type theory; Type structures; Program analysis; Probabilistic computation; Distributed computing models.

## KEYWORDS

binary sessions, probabilities, almost-sure termination, linear logic

**ACM Reference Format:**

Ugo Dal Lago and Luca Padovani. 2024. On the Almost-Sure Termination of Binary Sessions. In *26th International Symposium on Principles and Practice of Declarative Programming (PPDP 2024), September 09–11, 2024, Milano, Italy*. ACM, New York, NY, USA, 12 pages. https://doi.org/10.1145/3678232.3678239

## 1 INTRODUCTION

Sessions [2, 19–21] are well-studied abstractions of communication channels equipped with protocol descriptions in the form of *session types*. A session type system can be used to enforce a number of useful safety properties, including *communication safety* (no messages of the wrong type are exchanged), *protocol fidelity* (messages are exchanged in the expected order) and *deadlock freedom* (if the interaction halts, no pending communications remain). However, the enforcement of *livelock freedom*, namely that every communication action can be eventually completed, usually requires additional effort and possibly a richer type structure, as witnessed by the variety of static analysis techniques developed specifically for this purpose in previous years [11, 24, 33, 35].

An alternative *hybrid* approach to the enforcement of livelock freedom stems from an observation made by Kobayashi and San-giorgi [26], namely that livelock freedom is implied by deadlock

freedom in conjunction with termination. This approach paves the way to the development of type systems that ensure livelock freedom indirectly, as the consequence of arguably more basic properties. Many session type systems based on linear logic [6, 7, 29, 37], where well-typed processes are guaranteed to be both deadlock free and terminating, ensure livelock freedom in this way.

The same hybrid approach is also applicable if termination is only guaranteed “in the limit” or when certain assumptions are made. For example, *fair termination* [17, 18] is a weaker form of termination that only requires the so-called *fair executions* (as opposed to *all executions*) of a system to be finite. The fairness of an execution is some suitable formalization of the fact that the execution is considered to be “realistic”. Session type systems ensuring both deadlock freedom and fair termination (and therefore livelock freedom) have been recently proposed by Ciccone and Padovani [10], Ciccone et al. [8, 9] and Padovani [34]. In these works, the adopted fairness assumption is an instance of *full fairness* which van Glabbeek and Höfner [36] prove to be the *strongest conceivable fairness assumption*. While this assumption guarantees that such works target the largest possible family of fairly terminating processes, there may be contexts in which full fairness cannot be considered sufficiently “realistic” or where stronger termination guarantees are sought.

In this paper we consider one such context where processes perform *probabilistic* – as opposed to *non-deterministic* – choices. A typical example of process performing probabilistic choices is the *random walk* over the natural numbers, that is a process whose states $\underline{n}$ are in one-to-one correspondence with the elements of $\mathbb{N}$ and such that $n+1$ reduces to $\underline{n}$ with probability $p \in (0, 1)$ and to $n+2$ with probability $1-p$. The process $\underline{0}$ does not reduce, hence is terminated. In general, every process $\underline{n}$ is fairly terminating under a full fairness assumption, for no matter how large $n$ is, there always exists a reduction sequence from $\underline{n}$ to $\underline{0}$. At the same time, it is a known fact that $\underline{n}$ is not guaranteed to terminate with probability 1 unless $p \ge \frac{1}{2}$. In summary, $\underline{n}$ is an example of process which would be classified as “eventually terminating” under a non-deterministic semantics (and a full fairness assumption) but not necessarily under a probabilistic semantics.

As it turns out, the notion of terminating probabilistic process can be expressed in essentially different ways. The weakest termination property is the one requiring the probability of termination to be maximal, i.e. equal to 1. In this case we simply speak of *almost-sure termination* (AST in the following). The fact that in an AST process the probability of termination is maximal does *not* mean that all possible probabilistic evolutions of the process lead to termination. On the contrary, the possibility of divergence remains, even if it has zero probability. As a consequence, it also makes sense to consider a stronger notion of probabilistic termination whereby

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

This work is licensed under a Creative Commons Attribution International 4.0 License.
the expected computation time, i.e. the number of computation steps weighed by their probability, is finite. This property, called *positive almost-sure termination* (PAST in the following), is strictly stronger than AST. In fact, it is relatively easy to find processes that are AST but not PAST [3]. In the presence of non-deterministic behaviors it is also possible to go one step further and require the existence of a finite upper-bound to the expected computation time *independently* of the underlying scheduler. This property is even stronger than PAST [3] and is called *strongly positive* (*or strong*) *almost-sure termination* (SAST in the following).

Type systems and verification techniques guaranteeing these properties for probabilistic programs and systems have been studied extensively in the past [30, 31]. The same cannot be said about the world of concurrency and session types, where the literature on probabilistic termination is sparse. Inverso et al. [22] have studied a probabilistic session type system for reasoning about the success probability of a process, where the notion of “success” is user-definable. Their type system is unable to ensure that well-typed processes are AST and in fact their main soundness theorem is given under the assumption that the process under analysis is AST. More recently, Das et al. [16] have defined a probabilistic version of RAST [13–15] called NomosPro that can be used to estimate the expected amount of work of processes communicating through sessions and performing probabilistic choices, again for a user-definable notion of “work”. Das et al. [16] show how their type system can be used to ensure that well-typed processes are AST, provided that they are suitably instrumented to account for the number of spawns they create.

*Contributions.* In this paper we introduce ProSe, a calculus of probabilistic sessions equipped with two session type systems ensuring that well-typed processes are both deadlock free and almost-surely terminating, hence almost-surely livelock free. ProSe differs from NomosPro [16] in various ways. First of all, we study two type systems addressing different probabilistic termination properties (SAST and AST), the former being strictly stronger than the latter. The two type systems are structurally identical and based on infinitary versions of classical linear logic, differing only in the way probabilistic choices are weighed. Second, ProSe is a plain process calculus equipped with probabilistic choices. Unlike NomosPro, ProSe does not distinguish between non-deterministic and probabilistic choices resulting in lighter syntax, semantics and type systems. Also, the operational semantics of ProSe is standard and directly related to probabilistic term rewriting [3] instead of being tailored to the calculus and its type systems as in the case of NomosPro. Finally, additive connectives in ProSe’s types are not annotated with probabilities. As a consequence, the type systems and the typing rules are more streamlined than those of NomosPro, not needing complex operators for the probabilistic combination of session types.

*Structure of the paper.* The rest of the paper is organized as follows. Sections 2 and 3 respectively present syntax and semantics of ProSe. Section 4 formalizes AST, PAST and SAST, the three increasingly strong almost-sure termination properties for ProSe. Section 5 presents a type system for ProSe that ensures the strongest almost-sure termination property, whereas Section 6 shows a minimal variation of the same type system that ensures the weakest one.

<table><caption>Table 1: Syntax of processes.</caption><thead><tr><th>Process</th><th>P, Q</th><th>::=</th><th>x</th><th>↔</th><th>y</th><th>link</th></tr></thead><tbody><tr><td></td><td></td><td></td><td>A⟨x⟩</td><td></td><td></td><td>invocation</td></tr><tr><td></td><td></td><td></td><td>x().P</td><td></td><td></td><td>wait</td></tr><tr><td></td><td></td><td></td><td>x[]</td><td></td><td></td><td>close</td></tr><tr><td></td><td></td><td></td><td>x(y).P</td><td></td><td></td><td>receive</td></tr><tr><td></td><td></td><td></td><td>x[y](P, Q)</td><td></td><td></td><td>send</td></tr><tr><td></td><td></td><td></td><td>x▷{a<sub>i</sub> : P<sub>i</sub>}<sub>i∈I</sub></td><td></td><td></td><td>branch</td></tr><tr><td></td><td></td><td></td><td>x▷<sub>a</sub>.P</td><td></td><td></td><td>select</td></tr><tr><td></td><td></td><td></td><td>!x(y).P</td><td></td><td></td><td>server</td></tr><tr><td></td><td></td><td></td><td>?x[y].P</td><td></td><td></td><td>client</td></tr><tr><td></td><td></td><td></td><td>(x)(P | Q)</td><td></td><td></td><td>composition</td></tr><tr><td></td><td></td><td></td><td>P<sub>p</sub>⊕Q</td><td></td><td></td><td>choice</td></tr></tbody></table><p><i>p</i> ∈ (0, 1)</p>

We discuss closely related work more in detail in Section 7 and Section 8 concludes.

## 2 SYNTAX

The syntax of ProSe makes use of an infinite set of channel names ranged over by $x, y, z, \dots$, of a set of process names ranged over by $A, B, \dots$, and of a set of labels ranged over by $a, b, \dots$. We write $\bar{x}$ for possibly empty sequences of channel names $x_1, \dots, x_n$. Hereafter, we use the same notation to denote sequences of other entities as well.

The syntax of processes is defined by the grammar in Table 1 and is closely structured after that of session calculi based on classical linear logic such as CP [37]. A link $x \leftrightarrow y$ denotes the process that forwards every message received from $x$ to $y$ and vice versa, effectively unifying the channels $x$ and $y$. A process invocation $A\langle\bar{x}\rangle$ denotes an occurrence of the process named $A$, which is given by a global process definition of the form $A(\bar{x}) = P$. We assume that there is a unique global process definition for each process name.

Next are the forms describing session communications, which come in pairs of interacting processes. The process $x[]$ sends a termination signal on $x$, whereas the process $x().P$ waits for a termination signal from $x$ and continues as $P$. The process $x[y](P, Q)$ sends a new channel $y$ on $x$, it spawns the process $P$ which uses $y$ and continues as $Q$, whereas the process $x(y).P$ waits for a channel $y$ from $x$ and continues as $P$. The process $x▷<sub>a</sub>.P$ sends the label $a$ on $x$ and continues as $P$, whereas the process $x▷{a_i : P_i}_{i \in I}$ waits for a label $a_i$ from $x$ and continues as $P_i$.

A server $!x(y).P$ describes a process that accepts an unbounded number of connections from channel $x$ whereas a client $?x[y].P$ describes a process that requests a single connection on channel $x$. When client and server connect, the fresh session $y$ is created and a copy of the server is spawned.

A cut $(x)(P | Q)$ denotes the parallel composition of $P$ and $Q$ connected by the channel $x$, which is restricted to the composition. Finally, a probabilistic choice $P_p \oplus Q$ denotes a process that behaves as $P$ with probability $p$ and as $Q$ with probability $1-p$. Hereafter, $p$ and $q$ range over the real numbers in the open interval $(0, 1)$. We assume that the sequential composition operator ‘.’ used in prefixes has higher priority than the probabilistic choice operator $p \oplus$, so that e.g. $x(y).P_p \oplus Q$ means $(x(y).P)_p \oplus Q$ and not $x(y).(P_p \oplus Q)$. When necessary, we will use parentheses to disambiguate the notation.
The notions of free and bound (channel) names are defined in the expected way, bearing in mind that ?x[y].P binds y in P and that x[y](P, Q) binds y in P but not in Q. We write fn(P) for the set of channel names occurring free in P and, for each global definition A(\bar{x}) = P, we assume that fn(P) = {\bar{x}}.

We say that $x \leftrightarrow y, x().P, x[], x(y).P, x[y](P, Q), x \llcorner a.P, x \triangleright \{a_i : P_i\}_{i \in I}, !x(y).P$ and $?x[y].P$ are x-threads (or simply threads).

We impose a guardedness condition on global definitions so that, whenever $A(\bar{x}) = P$, we have $G(P)$ where $G(\cdot)$ is the least predicate defined by the following inference system:

$\underline{G(P)}$ P is a thread or a choice

$$ \frac{\mathcal{G}(P) \qquad \mathcal{G}(Q)}{\mathcal{G}((x)(P \mid Q))} \qquad \frac{\mathcal{G}(P)}{\mathcal{G}(A(\bar{x}))} \qquad A(\bar{x}) = P $$

Intuitively, in a guarded definition $A(\bar{x}) = P$ a finite number of unfoldings of process invocations always suffices to expose a thread or a probabilistic choice along every branch of P. For example, $A(x) = A\langle x \rangle p \boxplus x[]$ is guarded whereas neither $A(\bar{x}) = A\langle \bar{x} \rangle$ nor $A(x) = (y)(y().x[] | A\langle y \rangle)$ is.

**Example 2.1** (buyer-seller). We can model an e-commerce scenario using the following global process definitions:

$$ \text{Buyer}(x, y) = x \llcorner \text{add}.\text{Buyer}\langle x, y \rangle \quad p \boxplus x \llcorner \text{pay}.x().y[] $$

$$ \text{Seller}(x) = x \triangleright \{\text{add} : \text{Seller}(x), \text{pay} : x[]\} $$

$$ \text{Main}(y) = (x)(\text{Buyer}(x, y) | \text{Seller}(x)) $$

Buyer and seller are connected by a session x and they interact repeatedly. At each interaction, the buyer adds one more item into the shopping cart with probability p or pays the seller with probability 1 - p. Once the interaction is over, the buyer sends a termination signal on y.

**Example 2.2** (slot machine). In this example we model the interaction between a player client and a slot machine server using the following global process definitions:

$$ \text{Slot}(x) = !x(y).(y \llcorner \text{win}.y[] \quad p \boxplus y \llcorner \text{lose}.y[]) $$

$$ \text{Play}(x, z) = ?x[y].y \triangleright \{\text{win} : y \leftrightarrow z, \text{lose} : y().\text{Play}(x, z)\} $$

At each connection, the slot machine server performs a probabilistic choice and notifies the player of the outcome which can be win with probability p and lose with probability 1 - p. The player client modeled by the process $\text{Play}(x, z)$ repeatedly connects with the slot machine server until victory is achieved, at which point the player quits.

**Example 2.3** (infinitary random walk). There are various ways in which we can model a random walk in our process calculus. The simplest one makes use of a distinct global process definition $IWalk_n$ for each state $n \in \mathbb{N}$ of the walk where $IWalk_n$ is defined inductively on n as follows:

$$ \text{IWalk}_0(x) = x[] $$

$$ \text{IWalk}_{n+1}(x) = \text{IWalk}_n(x) \quad p \boxplus \text{IWalk}_{n+2}(x) $$

Intuitively, $IWalk_n(x)$ represents a state of the walk in which the process may send a termination signal on x after n reductions. When n = 0 the termination signal is sent immediately. When n > 0,

$IWalk_n$ reduces to $IWalk_{n-1}$ with probability p and to $IWalk_{n+1}$ with probability 1 - p.

**Example 2.4** (finitary random walk). The random walk modeled in Example 2.3 requires an infinite number of global process definitions. Here we present a different modeling in which each state of the walk admits a finite description, although the overall number of states is still necessarily infinite. Consider the process definitions

$$ \text{Step}_0(x) = \text{FWalk}_0\langle x \rangle \quad p \boxplus \text{FWalk}_2\langle x \rangle $$

$$ \text{Step}_{n+1}(x) = (y)(\text{Step}_n\langle y \rangle | y().\text{Step}_0\langle x \rangle) $$

$$ \text{FWalk}_0(x) = x[] $$

$$ \text{FWalk}_{n+1}(x) = (y)(\text{FWalk}_n\langle y \rangle | y().\text{Step}_0\langle x \rangle) $$

and note that the process $FWalk_1$ is finitely described by the global definitions for $Step_0$, $FWalk_0$, $FWalk_2$ and the one for $FWalk_1$ itself. The basic idea is that $FWalk_n(x)$ encodes the natural number n as n nested sessions which must all be closed in order to emit a signal on x. We will have a more precise understanding of this process' behavior in Example 3.3, after we have detailed the reduction semantics of ProSe.

# 3 PROBABILISTIC SEMANTICS

In order to describe the (probabilistic) semantics of ProSe we borrow some auxiliary notions from Avanzini et al. [3]. A *multidistribution* is a multiset $\lceil p_i : P_i \rceil_{i \in I}$ such that $p_i \in \mathbb{R}_{\ge 0}$ for every $i \in I$ and $\sum_{i \in I} p_i \le 1$. A multidistribution is akin to a probability distribution associating a process with a probability, with two important differences. First of all, the *same* process may occur *multiple times* in a given multidistribution. As we will see in Example 3.4, this is necessary to correctly deal with non-determinism. Second, the sum of the probabilities of a multidistribution need not be 1, but is in general smaller than 1. This is due to the fact that the semantics of multidistributions will be expressed in such a way that irreducible processes are eventually *removed* from a multidistribution. Hence, the overall sum of probabilities of a multidistribution only accounts for the processes that can actually perform reductions.

We introduce some more notation: we let M and N range over multidistributions; we write $\cup$ for the empty multidistribution; we write $\lceil p_1 : P_1, \dots, P_n : P_n \rceil$ for the multidistribution $\lceil p_i : P_i \rceil_{i=1}^n$; when $p \in \mathbb{R}_{\ge 0}$ and $M = \lceil q_i : P_i \rceil_{i \in I}$ we let $p \cdot M \stackrel{\text{def}}{=} \lceil pq_i : P_i \rceil_{i \in I}$ and $|M| \stackrel{\text{def}}{=} \sum_{i \in I} q_i$; we write $M \uplus N$ for the multiset union of M and N. Note that $|\cup| = 0$, $|p \cdot M| = p|M|$ and $|M \uplus N| = |M| + |N|$.

The operational semantics of ProSe is defined by the three relations in Table 2: a *structural precongruence* $\sqsubseteq$ for processes, a *reduction* $\rightarrow$ of processes and another reduction $\rightarrow$ of multidistributions. Structural precongruence is meant to relate processes that describe equivalent behaviors. In particular, the rules $[\text{s-call}]$, $[\text{s-cut}]$ and $[\text{s-link}]$ state the equivalence between a process invocation and its definition and the expected commutativity of parallel compositions and of links. The $\equiv$ symbol used in these rules denotes the symmetric closure of $\sqsubseteq$. The rule $[\text{s-weak}]$ is needed to erase an unused server. The remaining structural precongruence rules push a cut behind a prefix when the channel used by the prefix differs from the one restricted by the cut. In this way, observable actions are lifted at the top level where they can enable further reductions in the appropriate context. Note that $[\text{s-fork-l}]$ and $[\text{s-fork-r}]$ are
<table><caption>Table 2: Operational semantics of ProSe.</caption><thead><tr><th colspan="3">Structural precongruence</th></tr></thead><tbody><tr><td>[S-CALL]</td><td>A(x&#773;) &equiv; P</td><td>A(x&#773;) = P</td></tr><tr><td>[S-CUT]</td><td>(x)(P | Q) &equiv; (x)(Q | P)</td><td></td></tr><tr><td>[S-LINK]</td><td>x &leftrightarrow; y &equiv; y &leftrightarrow; x</td><td></td></tr><tr><td>[S-WAIT]</td><td>(x)(y().P | Q) &sqsubseteq; y().(x)(P | Q)</td><td>x &ne; y</td></tr><tr><td>[S-SELECT]</td><td>(x)(y &larr; a.P | Q) &sqsubseteq; y &larr; a.(x)(P | Q)</td><td>x &ne; y</td></tr><tr><td>[S-CASE]</td><td>(x)(y &rarr; {a<sub>i</sub>: P<sub>i</sub>}<sub>i&isin;I</sub> | Q) &sqsubseteq; y &rarr; {a<sub>i</sub>: (x)(P<sub>i</sub> | Q)}<sub>i&isin;I</sub></td><td>x &ne; y</td></tr><tr><td>[S-FORK-L]</td><td>(x)(y[z](P, Q) | R) &sqsubseteq; y[z]((x)(P | R), Q)</td><td>x &isin; fn(P) \ {y, z}</td></tr><tr><td>[S-FORK-R]</td><td>(x)(y[z](P, Q) | R) &sqsubseteq; y[z](P, (x)(Q | R))</td><td>x &isin; fn(Q) \ {y, z}</td></tr><tr><td>[S-JOIN]</td><td>(x)(y(z).P | Q) &sqsubseteq; y(z).(x)(P | Q)</td><td>x &ne; y, z</td></tr><tr><td>[S-CLIENT]</td><td>(x)(?y[z].P | Q) &sqsubseteq; ?y[z].(x)(P | Q)</td><td>x &ne; y, z</td></tr><tr><td>[S-SERVER]</td><td>(x)(!y(z).P | !x(u).Q) &sqsubseteq; !y(z).(x)(P | !x(u).Q)</td><td>x &ne; y, z</td></tr><tr><td>[S-WEAK]</td><td>(x)(P | !x(u).Q) &sqsubseteq; P</td><td>x &notin; fn(P)</td></tr></tbody></table><table><thead><tr><th colspan="3">Reduction of processes</th></tr></thead><tbody><tr><td>[R-CHOICE]</td><td>P p&oplus;Q &rarr; {p: P, 1 - p: Q}</td><td></td></tr><tr><td>[R-LINK]</td><td>(x)(x &leftrightarrow; y | P) &rarr; P{y/x}</td><td></td></tr><tr><td>[R-CLOSE]</td><td>(x)(x[] | x().P) &rarr; P</td><td></td></tr><tr><td>[R-FORK]</td><td>(x)(x[y](P, Q) | x(y).R) &rarr; (y)(P | (x)(Q | R))</td><td></td></tr><tr><td>[R-SELECT]</td><td>(x)(x &larr; a<sub>k</sub>.P | x &rarr; {a<sub>i</sub>: Q<sub>i</sub>}<sub>i&isin;I</sub>) &rarr; (x)(P | Q<sub>k</sub>)</td><td>k &isin; I</td></tr><tr><td>[R-CONNECT]</td><td>(x)(!x(y).P | ?x[y].Q) &rarr; (y)(P | (x)(!x(y).P | Q))</td><td></td></tr><tr><td>[R-CUT]</td><td>(x)(P | Q) &rarr; {p<sub>i</sub>: (x)(P<sub>i</sub> | Q)}<sub>i&isin;I</sub></td><td>P &rarr; {p<sub>i</sub>: P<sub>i</sub> &isin; I}</td></tr><tr><td>[R-CONG]</td><td>P &rarr; M</td><td>P &sqsubseteq; Q &rarr; M</td></tr></tbody></table><table><thead><tr><th colspan="3">Reduction of multidistributions</th></tr></thead><tbody><tr><td>[R-DROP]</td><td>{1: P} &rarr; {&emptyset;}</td><td>P &rarr;</td></tr><tr><td>[R-STEP]</td><td>{1: P} &rarr; M</td><td>P &rarr; M</td></tr><tr><td>[R-COMB]</td><td>&cup;<sub>i&isin;I</sub> p<sub>i</sub> &middot; M<sub>i</sub> &rarr; &cup;<sub>i&isin;I</sub> p<sub>i</sub> &middot; N<sub>i</sub></td><td>&forall;i &isin; I: M<sub>i</sub> &rarr; N<sub>i</sub></td></tr></tbody></table>

essentially two different versions of the same structural precongruence rule where the prefix being lifted is a channel output. In this case, the cut must be pushed along the appropriate continuation so as to preserve the binding structure of the original process, as ensured by the side condition. Also note that [s-server] differs from any other rule by the fact that it is only applicable when the right process in the cut is a server on the channel being restricted by the cut. This is necessary to make sure that the resulting process is still well typed, given the particular constraints imposed by the typing rule for servers which we will discuss in Section 5.

There are two reduction relations that share the same symbol $\to$, one that concerns processes and the other that concerns multidistributions. The reduction relation for processes is fairly standard. The rule [r-choice] reduces a probabilistic choice to the corresponding (multi)distribution. The rules [r-link], [r-close], [r-fork], [r-select] and [r-connect] describe the fundamental communication interactions in ProSe and correspond to principal cut reductions of classical linear logic. In these rules, we write $P \to Q$ instead of $P \to \{1: Q\}$ to reduce clutter. The rules [r-cut] and [r-cong] respectively close reductions under cuts and by structural precongruence.

The reduction relation for multidistributions generalizes the one for processes. The rules [r-drop] and [r-step] concern singleton

multidistributions: an irreducible process is erased from a multidistribution by [r-drop] whereas a reducible process is replaced by the multidistribution it produces by [r-step]. In the general case, to reduce a multidistribution we reduce and combine all the singleton multidistributions it is made of using [r-comb].

Hereafter we write $P \to P \to M$ for some $M$ and $P \to \emptyset$ if not $P \to \emptyset$. Also, we write $\Rightarrow$ for the reflexive, transitive closure of $\to$ on multidistributions.

**Example 3.1** (buyer-seller). Let us detail the evolution of the buyer-seller system described in Example 2.1. To do so, it is convenient to introduce two more process definitions

$$ \text{Add}(y) = (x)(x \larr \text{add.Buyer}(x, y) | \text{Seller}(x)) $$

$$ \text{Pay}(y) = (x)(x \larr \text{pay.Buyer}(x, y) | \text{Seller}(x)) $$

representing the states in which the buyer has committed to add an item into the shopping cart and to pay the seller, but the interaction
with the seller has not occurred yet. We derive

$$
\begin{align*}
\text{Main}\langle y \rangle & \to \lceil p : \text{Add}\langle y \rangle, 1 - p : \text{Pay}\langle y \rangle \rceil \\
& \to \lceil p : \text{Main}\langle y \rangle, 1 - p : (x)(x(.).y[] | x[]) \rceil \\
& \to \lceil p^2 : \text{Add}\langle y \rangle, p(1 - p) : \text{Pay}\langle y \rangle, 1 - p : y[] \rceil \\
& \to \lceil p^2 : \text{Main}\langle y \rangle, p(1 - p) : (x)(x(.).y[] | x[]) \rceil \\
& \to \lceil p^3 : \text{Add}\langle y \rangle, p^2(1 - p) : \text{Pay}\langle y \rangle, p(1 - p) : y[] \rceil
\end{align*}
$$

Note that every occurrence of $y[]$ eventually disappears from the sequence of multidistributions since $y[]$ is irreducible. ▼

**Example 3.2** (infinitary random walk). If we reduce $|\text{Walk}_1\langle x \rangle|$ using the definitions in Example 2.3 we obtain

$$
\begin{align*}
|\text{Walk}_1\langle x \rangle| & \to \lceil p : |\text{Walk}_0\langle x \rangle, 1 - p : |\text{Walk}_2\langle x \rangle \rceil \\
& \to \lceil p(1 - p) : |\text{Walk}_1\langle x \rangle, (1 - p)^2 : |\text{Walk}_3\langle x \rangle \rceil \\
& \to \lceil p^2(1 - p) : |\text{Walk}_0\langle x \rangle, p(1 - p)^2 : |\text{Walk}_2\langle x \rangle, \\
& \qquad p(1 - p)^2 : |\text{Walk}_2\langle x \rangle, (1 - p)^3 : |\text{Walk}_4\langle x \rangle \rceil
\end{align*}
$$

In the last multidistribution, there are multiple occurrences of the same $|\text{Walk}_2\langle x \rangle|$ process reflecting the existence of different reduction sequences leading to it from the initial process. In a multidistribution, these occurrences are *not* conflated into one. ▼

**Example 3.3** (finitary random walk). Looking at the definitions for $\text{FWalk}_n$ and $\text{Step}_n$ in Example 2.4 it is easy to establish that

$$
\begin{align*}
\text{FWalk}_{n+1}(\langle x \rangle) &\to \lceil 1 : \text{Step}_n(\langle x \rangle) \rceil \\
&\to \lceil p : \text{FWalk}_n(\langle x \rangle), 1 - p : \text{FWalk}_{n+2}(\langle x \rangle) \rceil
\end{align*}
$$

and therefore we obtain the sequence of reductions

$$
\begin{align*}
\text{FWalk}_1\langle x \rangle &\to^2 \lceil p : \text{FWalk}_0\langle x \rangle, 1-p : \text{FWalk}_2\langle x \rangle \rceil \\
&\to^2 \lceil p(1-p) : \text{FWalk}_1\langle x \rangle, (1-p)^2 : \text{FWalk}_3\langle x \rangle \rceil \\
&\to^2 \lceil p^2(1-p) : \text{FWalk}_0\langle x \rangle, p(1-p)^2 : \text{FWalk}_2\langle x \rangle, \\
&\qquad p(1-p)^2 : \text{FWalk}_2\langle x \rangle, (1-p)^3 : \text{FWalk}_4\langle x \rangle \rceil
\end{align*}
$$

which visits the same states we have already encountered when reducing $|\text{Walk}_1\langle x \rangle$ in Example 3.2, except that here we need two reductions instead of just one to move from one state to another. ▼

**Example 3.4.** To illustrate the relevance of multidistributions in capturing the probabilistic semantics of ProSe, consider the following global process definitions:

$$
\begin{align*}
A(u) &= (x) \left( x \triangleleft a_1 \cdot x[\phantom{\bigoplus}] \right) \otimes \left( x \triangleleft a_2 \cdot x[\phantom{\bigoplus}] \right) \middle| x \triangleright \left\{ \begin{array}{@{}l@{}} a_1 : C\langle x, u \rangle \\ a_2 : C\langle x, u \rangle \end{array} \right\} \\
C(x, u) &= (y)(x(.).y[] | (z)(z[] | z(.).y(.).u[]))
\end{align*}
$$

For the sake of readability, it is useful to also consider a few additional definitions corresponding to some intermediate states in the evolution of $A\langle u \rangle$, namely:

$$
B_i(u) = (x)(x \triangleleft a_i \cdot x[\phantom{\bigoplus}] | x \triangleright \{a_1 : C\langle x, u \rangle, a_2 : C\langle x, u \rangle\})
$$

$$
D_1(u) = (y)(y[] | (z)(z[] | z().y().u[]))
$$

$$
D_2(u) = (x)(x[] | (y)(x().y[] | y().u[]))
$$

We observe that $A\langle u \rangle$ may probabilistically reduce to either $B_1\langle u \rangle$ or $B_2\langle u \rangle$, whereas $(x)(x[] | C\langle x, u \rangle)$ may non-deterministically reduce to either $D_1\langle u \rangle$ or $D_2\langle u \rangle$. More precisely, the first two reductions of $A\langle u \rangle$ are

$$
\begin{align*}
A\langle u \rangle &\to \lceil \frac{1}{2} : B_1\langle u \rangle, \frac{1}{2} : B_2\langle u \rangle \rceil \\
&\to \lceil \frac{1}{2} : (x)(x[] | C\langle x, u \rangle), \frac{1}{2} : (x)(x[] | C\langle x, u \rangle) \rceil
\end{align*}
$$

so that the three-step reducts of $A\langle u \rangle$ according to our semantics are $M_1 \stackrel{\text{def}}{=} \lceil \frac{1}{2} : D_1\langle u \rangle, \frac{1}{2} : D_1\langle u \rangle \rceil$, $M_2 \stackrel{\text{def}}{=} \lceil \frac{1}{2} : D_2\langle u \rangle, \frac{1}{2} : D_2\langle u \rangle \rceil$ and $M_3 \stackrel{\text{def}}{=} \lceil \frac{1}{2} : D_1\langle u \rangle, \frac{1}{2} : D_2\langle u \rangle \rceil$.

If we worked using distributions instead of multidistributions then $A\langle u \rangle$ would reduce in two steps to $\lceil 1 : (x)(x[] | C\langle x, u \rangle) \rceil$, from which we would be able to reach the states $\lceil 1 : D_1\langle u \rangle \rceil$ and $\lceil 1 : D_2\langle u \rangle \rceil$ respectively corresponding to $M_1$ and $M_2$, but not a state corresponding to $M_3$. Roughly speaking, if we use distributions we may end up conflating substates of a system that must be distinguished to track the different paths that may lead to them. ▼

# 4 ALMOST-SURE TERMINATION PROPERTIES

In this section we define a range of termination properties in our probabilistic setting. We start by giving a precise definition of “reduction sequence” of a given process $P$.

**Definition 4.1** (reduction sequence). A reduction sequence of $P$ is an infinite sequence $M_0 M_1 \dots$ of multidistributions such that $M_0 = \lceil 1 : P \rceil$ and $M_i \to M_{i+1}$ for every $i \in \mathbb{N}$.

The fact that we only consider infinite reduction sequences is not a limitation. Indeed, irreducible processes are removed from a multidistribution by $[R-DROP]$ and the empty multidistribution trivially reduces to itself by $[R-COMB]$ (see Table 2).

Recall that the probability of a multidistribution $M$, denoted by $|M|$, overestimates the probability with which the processes therein reduce. So, a process $P$ is said to be almost-surely terminating if the probabilities of the multidistributions along every reduction sequence of $P$ approach zero. More formally:

**Definition 4.2** (almost-sure termination). We say that $P$ is almost-surely terminating (AST) if, for every reduction sequence $M_0 M_1 \dots$ of $P$, we have $\lim_{n \to \infty} |M_n| = 0$.

For example, it is easy to see that the buyer-seller system described in Examples 2.1 and 3.1 is almost-surely terminating regardless of the probability $p$ of the buyer to add an item into the shopping cart. A similar observation can be made for the slot machine described in Example 2.2. It is less obvious to prove that the random walks modeled in Examples 2.3 and 2.4 are almost-surely terminating if and only if $p \ge \frac{1}{2}$ as known from the literature [30].

**Example 4.1.** Consider the process definition

$$
A(x) = x[\phantom{\bigoplus}] \oplus (y)(A\langle y \rangle | y().(z)(A\langle z \rangle | z().A\langle x \rangle))
$$

in which $A\langle x \rangle$ terminates immediately with probability $\frac{1}{2}$ or it recursively invokes itself three times in a row. Olmedo et al. [32] have shown that $A\langle x \rangle$ terminates with probability at most $\frac{\sqrt{5}-1}{2}$, hence $A\langle x \rangle$ is not AST. ▼
Interestingly, although the symmetric random walk (with $p = \frac{1}{2}$) is AST, there is no finite bound to the expected number of reductions needed to terminate it. A stronger notion of almost-sure termination requires such expected number to be finite.

**Definition 4.3** (positive almost-sure termination). Given a reduction sequence $\overline{M} = M_0 M_1 \dots$, the *expected derivation length* of $\overline{M}$ is the quantity $\mathrm{edl}(\overline{M}) \in \mathbb{R}_{\ge 0} \cup \{\infty\}$ such that $\mathrm{edl}(\overline{M}) = \sum_{n \in \mathbb{N}} |M_n|$. We say that $P$ is *positively almost-surely terminating* (PAST) if, for every reduction sequence $\overline{M}$ of $P$, we have $\mathrm{edl}(\overline{M}) \in \mathbb{R}_{\ge 0}$.

If we call $\overline{M}$ the reduction sequence (partially) shown in Example 3.1 we see that

$$ \mathrm{edl}(\overline{M}) = 2 + \sum_{n \in \mathbb{N}} 2p^n = 2 + 2 \sum_{n \in \mathbb{N}} p^n = 2 + \frac{2}{1-p} \quad (1) $$

and any other reduction sequence of the buyer-seller system is the same as $\overline{M}$ up to structural precongruence, which does not alter the probabilities of multidistributions (we formalize this property in Lemma 5.1). We conclude that the buyer-seller system is PAST. From (1) we also see a confirmation of the fact that the higher the probability of adding an item into the shopping cart, the longer the expected interaction between buyer and seller.

There exist (non-deterministic) processes for which every reduction sequence has a finite expected derivation length, but such lengths can be arbitrarily large [3]. Therefore, it makes sense to consider an even stronger notion of almost-sure termination such that there exists a finite bound for any reduction sequence. This is the strongest notion of almost-sure termination we define and that is targeted by the type system in Section 5.

**Definition 4.4** (strong almost-sure termination). Given a process $P$, the *expected derivation height* of $P$ is the quantity $\mathrm{edh}(P) \in \mathbb{R}_{\ge 0} \cup \{\infty\}$ such that

$$ \mathrm{edh}(P) = \sup\{\mathrm{edl}(\overline{M}) \mid \overline{M} \text{ is a reduction sequence of } P\} $$

In words, $\mathrm{edh}(P)$ is the least upper bound to the expected derivation height of any reduction sequence of $P$. We say that $P$ is *strongly almost-surely terminating* (SAST) if $\mathrm{edh}(P) \in \mathbb{R}_{\ge 0}$.

Since every reduction sequence $\overline{M}$ of the buyer-seller system has the same expected derivation length $\mathrm{edl}(\overline{M})$ shown in (1), that system is SAST and its expected derivation height coincides with $\mathrm{edl}(\overline{M})$.

**Remark 4.1.** Example 3.4 shows that the semantics based on multidistributions is a refinement of the semantics based on distributions. More specifically, every reduction sequence in the distribution semantics of a process can be obtained from a reduction sequence in the multidistribution of the same process by conflating together the same states. As a consequence, if a process is (P/S)AST according to the multidistribution semantics, then it is (P/S)AST also according to the distribution semantics. In this sense, adopting the multidistribution semantics can be seen as a conservative design choice that allows the termination properties defined in this section and the soundness results we are about to present to be applicable also to the distribution semantics.

**Remark 4.2.** If ProSe enjoyed the diamond property, then the PAST and SAST properties would coincide. As it turns out, ProSe does

<table><caption>**Table 3: Syntax of types (coinductive).**</caption><thead><tr><th>Type</th><th>A, B</th><th>::= &perp;</th><th>bottom</th></tr></thead><tbody><tr><td></td><td>| 1</td><td></td><td>one</td></tr><tr><td></td><td>| A &otimes; B</td><td></td><td>par</td></tr><tr><td></td><td>| A &otimes; B</td><td></td><td>tensor</td></tr><tr><td></td><td>| &amp;{a<sup>l<sub>i</sub></sup> : A<sub>i</sub>}<sub>i &isin; I</sub></td><td>l<sub>i</sub> &isin; R<sub>&ge;0</sub></td><td>with</td></tr><tr><td></td><td>| &oplus;{a<sup>l<sub>i</sub></sup> : A<sub>i</sub>}<sub>i &isin; I</sub></td><td>l<sub>i</sub> &isin; R<sub>&ge;0</sub></td><td>plus</td></tr><tr><td></td><td>| !<sup>l</sup>A</td><td>l &isin; R<sub>&ge;0</sub></td><td>of course</td></tr><tr><td></td><td>| ?<sup>l</sup>A</td><td>l &isin; R<sub>&ge;0</sub></td><td>why not</td></tr></tbody></table>

not enjoy the diamond property. For example, if we take $A(x) = (y)(y[] | y().x[])$, then we have the reductions

$$ (x)(A\langle x \rangle | (y)(u \triangleright \{ } | v \triangleright \{)}) \rightarrow (x)(x[] | u \triangleright \{ }) $$

$$ (x)(A\langle x \rangle | (y)(u \triangleright \{ } | v \triangleright \{)}) \rightarrow (x)(x[] | v \triangleright \{ }) $$

where the two resulting processes are irreducible and different from each other. Nonetheless, the form of non-determinism of ProSe is quite limited, to the point that the known examples that separate PAST from SAST [3] cannot be modeled in ProSe as it stands. △

# 5 A TYPE SYSTEM FOR SAST

In this section we define a session type system ensuring that well-typed ProSe processes are SAST. Session types are modeled after the propositions of classical linear logic and their structure is given by the productions in Table 3. The interpretation of these propositions as comunication protocols is the usual one [6, 7, 37]: the constants $\perp$ and $1$ describe channels used for the input/output of a session termination signal; the multiplicative connectives $A \otimes B$ and $A \otimes B$ describe channels used for the input/output of another channel of type $A$ and then according to $B$; the additive connectives $\&$ and $\oplus$ describe channels used for the input/output of a label $a_i$ that identifies the subsequent protocol $A_i$; the exponentials $?^l A$ and $!^l A$ describe channels used for requesting/accepting connections between clients and servers.

Compared to the standard propositions of classical linear logic, our types differ in the following ways:

* We use *n*-ary (instead of binary) and labeled versions of the additive connectives “plus” $\oplus$ and “with” $\&$ and $\oplus$ to allow a friendlier description of communication protocols. In each occurrence of these connectives, *I* is finite and labels are pairwise different. Also, the additive units *0* and *$\top$* can be respectively encoded as degenerate forms $\oplus\{\}$ and $\&\{\}$ of these connectives with no branches.

* We annotate each tag $a_i$ in $\oplus\{a^{l_i} : A_i\}_{i \in I}$ and $\&\{a^{l_i} : A_i\}_{i \in I}$ and the exponentials $?^l$ and $!^l$ with quantities $l, l_i \in \mathbb{R}_{\ge 0}$ whose role is to enable the amortized analysis of the expected derivation height of a well-typed process. We will provide more details about the meaning and use of these annotations when we will describe the typing rules. When we omit these annotations we assume they are 0.

* Types are the possibly infinite trees generated by the productions in Table 3 so as to describe possibly infinite protocols. We introduce infinite session types as solutions of equations of the form $A = B$ where the metavariable $A$ may occur
<figure><img src="image_3.png" /><figcaption>**Table 4: Typing rules for processes (coinductive).**</figcaption></figure>

(protected) within B. It is a known fact that finite systems of
such equations admit a unique solution [12].

As usual we write $A^{\perp}$ for the dual of $A$, in which every constant/connective/exponential is changed to its dual. Note that duality is corecursively defined and that the dual of an additive connective or exponential does not alter its annotations.

The typing rules are shown in Table 4 and derive judgments of the form $P \vdash^\ell \Gamma$ where $\ell \in \mathbb{R}_{\ge 0}$ is the expected derivation height of the process being judged and $\Gamma$ is a *typing context*, that is a partial map from channels to session types. We let $\Gamma$ and $\Delta$ range over typing contexts; we write $x : A$ for the singleton typing context mapping $x$ to $A$; we write $\text{dom}(\Gamma)$ for the domain of $\Gamma$, namely for the set of channels for which there is an association in $\Gamma$; we write $\Gamma, \Delta$ for the union of $\Gamma$ and $\Delta$ when $\text{dom}(\Gamma) \cap \text{dom}(\Delta) = \emptyset$. In addition, we define a partial operation $+$ on typing contexts such that

$$
\Gamma + \Delta = \begin{cases} \Gamma, \Delta & \text{if } \text{dom}(\Gamma) \cap \text{dom}(\Delta) = \emptyset \\ (\Gamma' + \Delta'), x : ?^{\ell} A & \text{if } \Gamma = \Gamma', x : ?^{\ell} A \text{ and } \Delta = \Delta', x : ?^{\ell} A \end{cases}
$$

noting that + is commutative and associative. We write ?Γ for an
unlimited typing context, that is a typing context with the property
?Γ + ?Γ = ?Γ.

If we disregard height annotations, the typing rules are fairly
standard: those labeled after constants, connectives, [LINK] and [CUT]
have the same structure as the corresponding proof rules of classical
linear logic (CLL). In addition: [CALL] states that a process invocation
is well typed if so is its definition; [⊕] states that a choice $P_p \oplus Q$ in

Γ is well typed if so are P and Q in the same context; finally, [CLIENT]
and [SERVER] are akin to the dereliction and promotion rules in CLL.

Let us now focus on the differences between the typing rules of ProSe and the proof rules of CLL. First of all, the typing rules are meant to be interpreted coinductively: a process *P* is well typed in Γ if there is a *finite or infinite* typing derivation whose conclusion is the judgment *P* ⊢<sup>*l*</sup> Γ for some *l*. This feature is necessary in order to deal with recursive processes. Indeed, according to [CALL] a process invocation is well typed if so is its definition. It is thus clear that, in order to build typing derivations for recursive processes, it is necessary to build an infinite typing derivation.

Another difference between the typing rules of ProSe and CLL
is the lack of weakening and contraction rules for the “why not”
exponential. Instead, we have embedded the effects of weakening
and contraction in the other typing rules: the rules [CUT], [⊗] and
[CLIENT] make use of the (partial) operation + on typing contexts
to contract multiple usages of the same channel with a “why not”
exponential; also, the axioms [LINK] and [1] allow the typing context
to contain an unused part ?Γ that can only consist of channels
typed using the “why not” exponential. In this way, the type system
remains syntax directed and the operational semantics of ProSe
feels more natural compared to its purely logical version [37].

Let us now shift our attention to the annotations in types and
typing judgments and to their role in ensuring that well-typed pro-
cesses are SAST. Recall that the annotation ℓ in a typing judgment
P ⊢ Γ is meant to represent the expected derivation height of P.
Also recall from Definition 4.4 that the expected derivation height
is the least upper bound of the expected derivation length of every
reduction sequence of P. With these notions in mind, let us see
more in detail how the quantity ℓ is determined.

The basic idea is that the (expected derivation) height of a pro-
cess measures the number of reduction steps required to terminate
that process. Each process reduction stems from either a cut (see
[r-link], [r-close], [r-fork], [r-select] and [r-connect]) or a choice
(see [r-choice]). So, the ℓ annotation essentially counts the num-
ber of links, of positive prefixes/connectives and of probabilistic
choices contained within each process form. We disregard negative
prefixes/connectives since these are meant to interact with the cor-
responding positive one, therefore their contribution to the height
of a process is already taken into account.

The axioms [LINK] and [1] state that the height of $x \leftrightarrow y$ and $x[]$ is 1 since these processes disappear after a single reduction. The rule [CUT] states that the height of a cut ($x(P|Q)$) is the combined height of $P$ and $Q$. Indeed, in order to terminate the cut, it is necessary to terminate both $P$ and $Q$. The rule [CALL] states that the height of a process invocation coincides with that of its definition. Since a process invocation is expanded to its definition by [S-CALL] and not by a reduction, the invocation does not contribute to the height of the process in any way. The rules [⊥] and [⊗] state that the height of $x()$.P and of $x(y)$.P coincides with that of the continuation $P$. Since ⊥ is a negative constant and ⊗ is a negative connective, they do not actively contribute to the height of the process. The rule [⊗] states that the height of $x[y](P, Q)$ is 1 plus the combined height of $P$ and $Q$. This follows from the fact that ⊗ is a positive connective and that terminating this process requires terminating both $P$ and $Q$ as in the case of [CUT].
The rules $[\oplus]$ and $[\&]$, concerning the additive connectives $\oplus$ and $\&$, are a little more involved. It makes sense to start our description from a particular instance of these rules where we assume that the annotations in the types are all zero:

$$ \frac{P \vdash^l \Gamma, x : A_k}{x \lhd a_k.P \vdash^{l+\ell} \Gamma, x : \oplus\{a_i : A_i\}_{i \in I}} \qquad k \in I $$

$$ \frac{\forall i \in I : P_i \vdash^l \Gamma, x : A_i}{x \triangleright \{a_i : P_i\}_{i \in I} \vdash^l \Gamma, x : \&\{a_i : A_i\}_{i \in I}} $$

Formulated in this way, we see that the rules adhere to the template already outlined for the multiplicative connectives: $[\oplus]$ augments the height of its continuation by 1 because $\oplus$ is a positive connective, whereas $[\&]$ does not. We also observe that, in order for $x \triangleright \{a_i : P_i\}_{i \in I}$ to be well typed, every continuation $P_i$ is required to have the same height $\ell$. This requirement turns out to be very strict. A more flexible approach could be to overapproximate the height of each continuation by taking the maximum of the heights of the continuations $P_i$. However, doing so would still prevent us from computing a finite height for many almost-surely terminating processes like those containing a loop going through an output action (cf. Play in Example 2.2).

To enable a more precise annotation for a process $x \triangleright \{a_i : P_i\}_{i \in I}$, in the general formulation of the rule $[\&]$ of Table 4 we allow the height of the process to depend on the label $a_i$ it receives. To this aim, we discharge (part of) the height $\ell + \ell_i$ of the $a_i$-labeled branch to the annotation of the $a_i$ label in the type of $x$ and we only assign height $\ell$ to the process as a whole. Of course this means that we are now underapproximating the height of the process. The missing quantity, however, is charged on the opposite side of the session by the rule $[\oplus]$. There we see that the height $1 + \ell + \ell_k$ of a process of the form $x \lhd a_k.P$ not only accounts for the height $\ell$ of $P$, but also for the amount $\ell_k$ associated to $a_k$ in the type of $x$ which, by duality, coincides with the amount that has been discharged from the receiver side. The advantage of transferring (part of) the height from the receiver to the sender side is that the sender knows which label is being sent, thereby allowing for a more precise computation of the height. We will see in Example 5.2 how this mechanism is key for typing some recursive processes.

The rules $[CLIENT]$ and $[SERVER]$ deal with heights of clients and servers in a similar way, except that the height of a server must be completely discharged on the annotation of the $!$ exponential, only to be charged on the height of each client together with that of its continuation. Intuitively, since a server $!x(y).P$ must be available in an unbounded number of copies, the only way for such copies to have a finite overall height is for the server to have a null weight. Each single client is accounted for the height of the server it connects to.

We conclude with $[\&]$, noting that the height of a probabilistic choice $P \rho \& Q$ is 1 plus the weighted combination of the heights of $P$ and $Q$. The 1 contribution to the height of a probabilistic choice accounts for the fact that the choice reduces to a multidistribution in one step by $[R-CHOICE]$.

Before we describe the properties of well-typed processes we have to provide a typing rule also for multidistributions, since these

are an essential part of the operational semantics of ProSe:

$$ \frac{\text{[DISTRIBUTION]} \qquad \forall i \in I : P_i \vdash^{\ell_i} \Gamma}{\lambda p_i : P_i \int_{j \in I} \vdash^{\sum_{i \in I} p_i (1+\ell_i)} \Gamma} $$

At first sight, $[DISTRIBUTION]$ looks like a mere generalization of $[\&]$ in that the height of a multidistribution is given by the weighted combination of the heights of the processes therein. However, $[DISTRIBUTION]$ differs from $[\&]$ because the 1 contribution in the conclusion of the rule is not added to the overall height, but rather to the height of each process in the multidistribution. The reason for this difference is that a multidistribution represents a choice that has already been performed in the past (hence the lack of the 1 contribution to the overall height), but even terminated processes cause a multidistribution to reduce by $[R-DROP]$ (hence the 1 contribution to the height of each process).

Concerning the properties of well-typed processes, we start from the fact that structural precongruence preserves typing and height:

**Lemma 5.1.** If $P \vdash^l \Gamma$ and $P \sqsupseteq Q$, then $Q \vdash^l \Gamma$.

The fact that the height is preserved may be surprising considering that a particular instance of rule $[S-CASE]$ may erase arbitrarily large processes, e.g. $(x)(y \triangleright \{\} | P) \sqsupseteq y \triangleright \{\}$. However, $[\&]$ is formulated in such a way that $y \triangleright \{\}$ can be given any height.

The same preservation property also holds for the reduction of processes. In this case, however, we start from a well-typed process and end up in a well-typed multidistribution.

**Lemma 5.2.** If $P \vdash^l \Gamma$ and $P \to M$, then $M \vdash^l \Gamma$ and $|M| = 1$.

Also in this case the preservation of the height is suspicious, since we have seen that heights roughly count the number of reductions that are needed to terminate a process and in the statement of Lemma 5.2 one reduction does take place. However, this reduction performed at the level of processes is counterbalanced by the 1 term added in the conclusion of $[DISTRIBUTION]$, which accounts for the fact that multidistributions consisting of a single irreducible process reduce to the empty multidistribution by $[R-DROP]$.

The next result states the ultimate subject reduction property of ProSe and provides the key relationship between the expected derivation height of a multidistribution and that of its reducts.

**Theorem 5.1 (subject reduction).** If $M \vdash^l \Gamma$ and $M \to M'$, then $M' \vdash^{l'} \Gamma$ for some $l'$ such that $\ell \ge |M| + \ell'$.

The reason why in general $\ell$ is only greater than (instead of equal to) $|M| + \ell'$ is that $M$ may contain irreducible processes with an arbitrary height. For example, if $M = \{1 : x \triangleright \{\} \} \cup \{\}$ then $\ell$ may be arbitrarily large, whereas $M' = \{\} \cup \{\}$ and $\ell'$ is necessarily 0. However, when $\Gamma$ has the form $x : 1$, it is possible to strengthen Theorem 5.1 so that $\ell = |M| + \ell'$ for the only irreducible processes in $M$ are of the form $x[]$ whose height is exactly 1.

Soundness of the type system for SAST follows as a straightforward consequence of Theorem 5.1 and of Definition 4.4.

**Theorem 5.2 (soundness for SAST).** If $P \vdash^l \Gamma$, then $P$ is SAST.

*PROOF.* Let $\bar{M} = M_0 M_1 \dots$ be a reduction sequence of $P$. From Theorem 5.1 we deduce $M_n \vdash^{\ell_n} \Gamma$ and $\ell_n \ge |M_n| + \ell_{n+1}$ for every $n \in \mathbb{N}$, where $\ell_0 = \ell$. Hence $\ell \ge \sum_{n \in \mathbb{N}} |M_n| = \text{edl}(\bar{M})$. Since $\bar{M}$ is arbitrary, we conclude $\ell \ge \text{edh}(P)$. □
In order to prove that well-typed processes are also deadlock free, we need a productivity result stating that well-typed, irreducible processes always expose some observable behavior in the sense that they are (structurally precongruent to) a thread.

**Lemma 5.3.** *lemma If P ⌜ℓ Γ and P →, then P ⊒ Q for some thread Q.*

A relevant instance of Lemma 5.3 is obtained when $\Gamma = x: 1$. In this case, $Q$ must be $x[]$ meaning that $P$ is successfully terminated. So, we can formulate the following deadlock freedom result.

**Theorem 5.3 (deadlock freedom).** *If $M \vdash^\ell x: 1$ and $M \Rightarrow \iota p: P \uplus N$ and $P \to$, then $P \sqsubseteq x$.*

That is, every irreducible process found in any reduct of a multidistribution that is well typed in the context $x: 1$ is structurally precongruent to $x$]. In particular, such process does not contain pending communication actions aside from the termination signal sent on $x$ (note that every well-typed ProSe process has at least one free name). When we combine Theorem 5.2 with Theorem 5.3 we conclude that every well-typed process $P$ is almost-surely livelock free, that is every pending communication action that arises in some reduct of $P$ is completed with probability 1.

**Example 5.1.** In order to find a typing derivation for the buyerseller system in Example 2.1 consider the type $A$ defined by the equation $A = \oplus\{\text{add}: A, \text{pay}: \perp\}$ and describing the behavior of the buyer. If we assume that the expected derivation height of $\text{Buyer}(x, y)$ is $\ell$, then we derive

$$ \frac{\begin{array}{c} \vdots \\ \text{Buyer}(x, y) \vdash^\ell x: A, y: 1 \\ x \triangleleft \text{add} \dots \vdash^{1+\ell} x: A, y: 1 \end{array}}{\begin{array}{c} \overline{y[] \vdash^1 y: 1}^{[1]} \\ \text{[}\oplus\text{]} \\ x() \cdot y[] \vdash^1 x: \perp, y: 1 \\ x \triangleleft \text{pay} \dots \vdash^2 x: A, y: 1 \end{array}}^{[\perp]} \\ \frac{\begin{array}{c} x \triangleleft \text{add} \dots \quad p \boxplus x \triangleleft \text{pay} \dots \vdash^{1+p(1+\ell)+2(1-p)} x: A, y: 1 \\ \text{[}\boxplus\text{]} \\ \text{[CALL]} \end{array}}{\text{Buyer}(x, y) \vdash^{3+p\ell-p} x: A, y: 1} $$

from which we obtain $\ell = 3 + p\ell - p$ that is $\ell = 1 + \frac{2}{1-p}$.
Turning the attention to the seller, we derive

$$ \frac{\begin{array}{c} \vdots \\ \text{Seller}(x) \vdash^1 x: A^{\perp} \\ x \triangleright \{\text{add}: \text{Seller}(x), \text{pay}: x\} \vdash^1 x: A^{\perp} \\ \text{[CALL]} \end{array}}{\text{Seller}(x) \vdash^1 x: A^{\perp}}^{[\&]} $$

from which we conclude that the expected derivation height of the buyer-seller system is $2 + \frac{2}{1-p}$. Note that this is exactly the same quantity we obtained in (1) by analyzing the reduction sequence(s) in Example 3.1. ▼

**Example 5.2.** In this example we prove that the system described in Example 2.2 is well typed and therefore SAST. Compared to the buyer-seller system, for which we have provided a typing derivation in Example 5.1, here we face an additional difficulty due to Play being a recursive process that loops through an output action (the connection with the slot machine server). Since every connection is explicitly accounted for in the annotation of typing judgments (cf. the rule [CLIENT] in Table 4), we would be unable to find a finite expected derivation height for Play if we followed the simple

typing strategy used in Example 5.1. Here we have to resort to the amortized analysis of the expected derivation height of a process, by letting this quantity depend on the actual branching structure of the process. To this aim, consider the session type $A$ such that

$$ A = \&\{\text{win}^{\ell_1}: 1, \text{lose}^{\ell_2}: 1\} $$

where, for the time being, we leave $\ell_1$ and $\ell_2$ undefined. Using $A^{\perp}$ we can build the following typing derivation for $\text{Slot}(x)$

$$ \frac{\begin{array}{c} \overline{y[] \vdash^1 y: 1}^{[1]} \\ y \triangleleft \text{win.} y[] \vdash^{2+\ell_1} y: A^{\perp} \end{array}}{\begin{array}{c} \overline{y[] \vdash^1 y: 1}^{[\oplus]} \\ y \triangleleft \text{lose.} y[] \vdash^{2+\ell_2} y: A^{\perp} \end{array}}^{[\oplus]} \\ \frac{\begin{array}{c} y \triangleleft \text{win.} y[] \quad p \boxplus y \triangleleft \text{lose.} y[] \vdash^{3+p\ell_1+(1-p)\ell_2} x: A^{\perp} \\ \text{[SERVER]} \end{array}}{\begin{array}{c} \frac{!x(y) \cdot (y \triangleleft \text{win.} y[] \quad p \boxplus y \triangleleft \text{lose.} y[])) \vdash^0 x: !^\ell A^{\perp}}{\text{Slot}(x) \vdash^0 x: !^\ell A^{\perp}} \end{array}}^{[\text{CALL}]} $$

where we take $\ell = 3 + p\ell_1 + (1-p)\ell_2$. Using $A$ we obtain the derivation

$$ \frac{\vdots}{y \leftrightarrow z \vdash^1 y: \perp, z: 1}^{[\text{LINK}]} \frac{\text{Play}(x, z) \vdash^{1+\ell} x: ?^\ell A, z: 1}{y() \dots \vdash^{1+\ell} x: ?^\ell A, y: \perp, z: 1}^{[\perp]} \\ \frac{y \triangleright \{\text{win} \dots, \text{lose} \dots\} \vdash^0 x: ?^\ell A, y: A, z: 1}{?x[y].y \triangleright \{\text{win} \dots, \text{lose} \dots\} \vdash^{1+\ell} x: ?^\ell A, z: 1}^{[\text{CLIENT}]} \\ \frac{\text{Play}(x, z) \vdash^{1+\ell} x: ?^\ell A, z: 1}{\text{[CALL]}} $$

under the constraints $\ell_1 = 1$ and $\ell_2 = 1+\ell$. These constraints reflect our desire to annotate the conclusion of the [&&] with a null expected derivation height. This way, the expected derivation height of this sub-process fully depends on the actual label (either win or lose) that the player receives from the slot machine. We can now solve the equation for $\ell$ to obtain $\ell = \frac{3}{p}$, confirming that the composition of the player client and the slot machine server is SAST. Note that the expected derivation height of $\text{Play}(x, z)$ increases as the probability of a victory becomes smaller. ▼

**Example 5.3.** Consider the family of $IWalk_n$ processes defined in Example 2.3. We can prove that $IWalk_n(\langle x \rangle \vdash^{1+\frac{n}{2p-1}} x: 1)$ is derivable by induction on $n$ by considering the base case

$$ \frac{\overline{x[] \vdash^1 x: 1}^{[1]} \quad \text{[CALL]}}{IWalk_0(x) \vdash^1 x: 1} $$

and the inductive case

$$ \frac{\begin{array}{c} \vdots \\ \text{IWalk}_n(\langle x \rangle \vdash^{1+\frac{n}{2p-1}} x: 1) \\ \text{IWalk}_{n+2}(\langle x \rangle \vdash^{1+\frac{n+2}{2p-1}} x: 1) \end{array}}{\text{IWalk}_n(\langle x \rangle \quad p \boxplus \text{IWalk}_{n+2}(\langle x \rangle \vdash^{1+p(1+\frac{n}{2p-1})+(1-p)(1+\frac{n+2}{2p-1})} x: 1)}^{[\boxplus]} \quad \text{[CALL]} $$

where

$$ 1 + p \left( 1 + \frac{n}{2p-1} \right) + (1-p) \left( 1 + \frac{n+2}{2p-1} \right) = 1 + \frac{n+1}{2p-1} $$

follows by standard calculations. Note that $1 + \frac{1}{2p-1} \in \mathbb{R}_{\ge 0}$ if $p > \frac{1}{2}$ hence $IWalk_1$ is SAST if $p > \frac{1}{2}$ as known from the literature [3]. ▼
**Example 5.4.** Consider the processes defined in Example 2.4. Assuming that the expected derivation height of $Step_0\langle x \rangle$ is $\ell$, it is easy to see that $Step_n\langle x \rangle \upharpoonright^{\ell(n+1)} x : 1$ and also $FWalk_n\langle x \rangle \upharpoonright^{1+\ell n} x : 1$. Indeed, we can derive

$$ \frac{\overline{x[] \upharpoonright^1 x : 1}^{[1]}}{FWalk_0\langle x \rangle \upharpoonright^1 x : 1} \quad [\text{CALL}] $$

as well as

$$ \frac{\vdots \quad \overline{Step_0\langle x \rangle \upharpoonright^{\ell} x : 1}}{FWalk_n\langle y \rangle \upharpoonright^{1+\ell n} y : 1} \quad \overline{y().Step_0\langle x \rangle \upharpoonright^{\ell} x : 1, y : \perp}^{[\perp]} \\ \frac{(y)(FWalk_n\langle x \rangle | y().Step_0\langle x \rangle) \upharpoonright^{1+\ell(n+1)} x : 1}{FWalk_{n+1}\langle x \rangle \upharpoonright^{1+\ell(n+1)} x : 1} \quad [\text{CALL}] $$

therefore

$$ \frac{\overline{FWalk_0\langle x \rangle \upharpoonright^1 x : 1}^{[1]} \quad \overline{FWalk_2\langle x \rangle \upharpoonright^{1+2\ell} x : 1}}{FWalk_0\langle x \rangle p \boxplus FWalk_2\langle x \rangle \upharpoonright^{2+2\ell-2p\ell} x : 1} \quad [\boxplus] \\ \overline{Step_0\langle x \rangle \upharpoonright^{2+2\ell-2p\ell} x : 1} \quad [\text{CALL}] $$

from which we obtain $\ell = 2+2\ell-2p\ell$, that is $\ell = \frac{2}{2p-1}$. As expected, if $p > \frac{1}{2}$ we have that $\ell \in \mathbb{R}_{\ge 0}$ and therefore $FWalk_1\langle x \rangle$ is SAST by Theorem 5.2. Note that the expected derivation height of $FWalk_1\langle x \rangle$ is $1 + \frac{2}{2p-1}$, where the term that depends on $p$ is twice as much as the corresponding term in the expected derivation height of $IWalk_1\langle x \rangle$ in Example 5.3. This is consistent with the observation made in Example 3.3 that the finitary random walk takes twice as many steps to move from one state to another compared to the infinitary one. ▼

# 6 FROM SAST TO AST

At this point it is natural to wonder whether the session type system introduced in Section 5 can be relaxed to enforce a property weaker than SAST. As a calculus of sessions, ProSe does not support the kind of nondeterminism that makes it possible to separate SAST from PAST [3]. In this section we show how we can obtain a type system for AST without altering the type language at all by only tweaking the typing rule for probabilistic choices.

Before showing how this is possible, recall that the annotation $\ell$ in typing judgments $P \upharpoonright^{\ell} \Gamma$ is meant to be an upper bound to the *expected derivation length* of $P$ in the spirit of Lyapunov *ranking functions* [30]. Is it reasonable to think of a similar approach, which however is able to guarantee a weaker property such as AST? In this sense, the recent work of McIver et al. [31] comes to our aid. There, the AST property is guaranteed through the use of a measure that is not necessarily strictly decreasing. We can inject this idea into our type system by changing the probabilistic choice rule thus

$$ \frac{[\boxplus\text{-AST}]}{P \upharpoonright^{\ell} \Gamma \quad Q \upharpoonright^{\ell'} \Gamma} \quad \min\{\ell, \ell'\} \le 1 + p\ell + (1-p)\ell' \\ \frac{P p \boxplus Q \upharpoonright^{p\ell+(1-p)\ell'} \Gamma}{\Gamma} \quad 0 < \varepsilon \le p $$

where $\varepsilon$ is an arbitrary, globally defined, strictly positive constant.

Note the differences between [box-ast] above and [box] in Table 4. The annotation $p\ell + (1-p)\ell'$ in the conclusion of [box-ast] no longer accounts for the reduction of the probabilistic choice and is always strictly smaller than the annotation $1+p\ell + (1-p)\ell'$ in the conclusion of [box]. Having a smaller annotation in the conclusion of [box-ast] broadens the range of typing derivations that can be obtained, as we strive to keep such annotations finite. The side condition $\min\{\ell, \ell'\} \le 1 + p\ell + (1-p)\ell'$ requires the existence of at least one continuation whose measure is not much larger than the measure of the probabilistic choice as a whole. The mere existence of this continuation is enough to ensure that the process terminates with probability 1. The side condition $0 < \varepsilon \le p$ simply ensures the existence of a strictly positive lower bound for the probabilities that occur in the process. This is trivially true if the process is finite or regular. In our setting, where we work with possibly infinite typing derivations and global process definitions, this is not the case in general. However, note that all of the examples discussed in the previous sections satisfy this side condition.

In the rest of this section, all typing judgments $P \upharpoonright^{\ell} \Gamma$ are meant to be derived by the type system where [box] is replaced by [box-ast].

The properties of well-typed processes go through smoothly as in Section 5. In particular, Lemma 5.1 holds in exactly the same form here. The same preservation property also holds for the reduction of processes, but it is necessary to formalize a precise relationship between the annotation of the process being reduced and that of one component in the resulting multidistribution. In the next result, for any multidistribution $M = \{p_i : P_i \}_{i \in I}$, we let $M(Q) \stackrel{\text{def}}{=} \sum_{P_i=Q} p_i$.

**Lemma 6.1.** If $P \upharpoonright^{\ell} \Gamma$ and $P \to M$, then there exist $Q, \ell'$ and $\ell''$ such that $M \upharpoonright^{\ell'} \Gamma, Q \upharpoonright^{\ell''} \Gamma, \ell', \ell'' \le \ell + 1$ and $\varepsilon \le M(Q)$.

The proof of this lemma is very similar to that of Lemma 5.2. All base cases except for [r-choice] can be treated in exactly the same way as before, the only cases that must be slightly modified being those for [r-choice] and [r-cut].

Any probabilistic transition system for which the weight of states evolves along the lines of Lemma 6.1 can be proved to be almost surely terminating using results of Kassing and Giesl [23]:

**Theorem 6.1** (soundness for AST). If $P \upharpoonright^{\ell} \Gamma$, then $P$ is AST.

**Example 6.1.** Consider again the family of $IWalk_n$ processes defined in Example 2.3 where we take $p = \frac{1}{2}$ so as to model a symmetric random walk. As is well known, the obtained stochastic process is AST but not SAST nor PAST. We can prove that $IWalk_n\langle x \rangle \upharpoonright^{n+1} x : 1$ is derivable by induction on $n$ by considering the base case

$$ \frac{\overline{x[] \upharpoonright^1 x : 1}^{[1]}}{IWalk_0\langle x \rangle \upharpoonright^1 x : 1} \quad [\text{CALL}] $$

and the inductive case

$$ \frac{\vdots \quad \overline{IWalk_n\langle x \rangle \upharpoonright^{n+1} x : 1}^{[1]} \quad \overline{IWalk_{n+2}\langle x \rangle \upharpoonright^{n+3} x : 1}^{[\boxplus]} \quad \overline{IWalk_n\langle x \rangle \upharpoonright^{1/2\boxplus} IWalk_{n+2}\langle x \rangle \upharpoonright^{n+2} x : 1}^{[\boxplus]} \quad [\text{CALL}]}{IWalk_{n+1}\langle x \rangle \upharpoonright^{n+2} x : 1} $$

In particular we have $IWalk_1\langle x \rangle \upharpoonright^{2} x : 1$, hence $IWalk_1\langle x \rangle$ is AST by Theorem 6.1. ▼
# 7 RELATED WORK

Among the existing works that have addressed the relationship between sessions and probabilities [1, 5, 16, 22], the ones more closely related to our own are by Inverso et al. [22] and Das et al. [16]. Inverso et al. [22] study a session type system for reasoning about the probability that a session terminates *successfully*, where the notion of successful session termination is user definable. For example, with such type system it is possible to compute the probability of winning at least one game when playing against the slot machine, assuming a bounded number of played games. In fact, the type system of Inverso et al. [22] does not guarantee any form of almost-sure termination and their main soundness result holds *assuming* that the system under analysis is AST.

More recently, Das et al. [16] have introduced NomosPro, a probabilistic version of RAST [13–15] for reasonning about work and resource utilization in session-based systems. Das et al. [16] show how the type system of NomosPro can be used to ensure that well-typed processes are AST, provided that processes are suitably instrumented for tracking the spawning of (recursive) processes. The main difference between NomosPro and ProSe is that in NomosPro (and in earlier probabilistic session types [1, 22] as well) the additive connectives are annotated with probabilities, whereas in ProSe they are not (the height annotations in ProSe's session types are present also in NomosPro and RAST, albeit in a different form and with a different purpose). The presence of probabilities in NomosPro's types make them more informative. For example, it is possible to use NomosPro's type system to check (or even infer) the probability with which a process sends a given label. However, probabilities in types also cause two major complications. First of all, NomosPro needs different forms for probabilistic and non-deterministic choices, both in types and in processes. In ProSe, this duplication of constructs is not necessary. Second, the typing preservation result of NomosPro (analogous to Lemma 5.2) is challenging to prove and needs the support of substantial technical machinery both in the type system and in the operational semantics of the calculus itself. The problem is that performing a probabilistic choice in general requires tuning the probabilities in types, and the effects of this tuning may spread globally in the system. NomosPro tames this problem by introducing a fairly sophisticated operational semantics – called *nested multiverse semantics* – that localizes the effects of probabilistic choices as much as possible. In contrast, the probabilistic semantics of ProSe is a straightforward instantiation of that for probabilistic term rewriting introduced by Avanzini et al. [3] which seamlessly handles both probabilistic and non-deterministic choices (cf. Example 3.4).

Another difference between the type systems of ProSe and NomosPro is that we explicitly address both SAST (Section 5) and AST (Section 6) whereas the technique illustrated by Das et al. [16] ensures AST but only as a consequence of SAST where the expected work concerns the number of (recursive) process invocations. In particular, the symmetric infinitary random walk (Example 2.3) cannot be proved to be AST using the technique of Das et al. [16].

It is easy to see that almost-sure termination (Definition 4.2) implies fair termination under the assumption that if termination is infinitely often possible, then it is inevitable (this assumption is a particular instance of full fairness [36]). In this sense, our type

system provides stronger guarantees compared to the type systems that ensure fair session termination [8–10, 34] using this fairness assumption. For example, the random walk processes described in Examples 2.3 and 2.4 are all fairly terminating if we turn the probabilistic choice therein into a non-deterministic choice. However, the same processes are AST only if the walk is symmetric ($p = \frac{1}{2}$) and they are SAST only if $p > \frac{1}{2}$.

Verifying termination properties of probabilistic functional programs via type systems is known to be possible via type-based approaches [4, 27, 28]. Some of these approaches share the use of a weight system with the system considered in this paper. A feature not present in ProSe which is instead often present in some of the aforementioned systems is that of monadic types, i.e. distributions of types.

# 8 CONCLUDING REMARKS

We have defined two type systems for ProSe, a calculus of binary sessions with probabilistic choices, ensuring that well-typed processes are deadlock free and (S)AST. The combination of these two properties guarantees that well-typed processes are *almost surely livelock free*, namely that every pending communication action is performed with probability 1.

Livelock freedom and AST are interesting properties not just on their own, but also because there are other properties that may depend on, or may be affected by, the knowledge that certain communication actions are (not) guaranteed to occur or the knowledge that the system as a whole eventually terminates. This is the case e.g. of information-flow analysis [25], where the presence or lack of communications may leak information that should not be revealed. Another example is the type system studied by Inverso et al. [22], which can be used to estimate the success probability of a system of interacting processes, provided that such system is known to be AST. Thus, ProSe can serve as a foundation for more sophisticated forms of static analysis that rely on livelock freedom and/or AST.

To the best of our knowledge, NomosPro [16] is the only other session calculus equipped with a type system capable of ensuring AST. NomosPro types are quantitatively more informative compared to those of ProSe and allow reasoning on the probability that specific actions are performed. On the other hand, NomosPro static and dynamic semantics turn out to be much more complex than those of ProSe, which relies on a canonical probabilistic semantics and an arguably simpler type system. Whether the type system of NomosPro can be partly simplified along the lines of ProSe or whether ProSe could benefit from more sophisticated static and dynamic semantics of NomosPro remain to be established.

# REFERENCES

[1] Bogdan Aman and Gabriel Ciobanu. 2019. Probabilities in Session Types. In *Proceedings Third Symposium on Working Formal Methods, FROM 2019, Timişoara, Romania, 3-5 September 2019 (EPTCS, Vol. 303)*, Mircea Marin and Adrian Craciun (Eds.). 92–106. https://doi.org/10.4204/EPTCS.303.7

[2] Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. 2016. Behavioral Types in Programming Languages. *Found. Trends Program. Lang.* 3, 2-3 (2016), 95–230. https://doi.org/10.1561/2500000031

[3] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. 2020. On probabilistic term rewriting. *Sci. Comput. Program.* 185 (2020). https://doi.org/10.1016/J.SCICO.2019.102338
[4] Flavien Breuvart, Ugo Dal Lago, and Agathe Herrou. 2021. On Higher-Order Probabilistic Subrecursion. *Log. Methods Comput. Sci.* 17, 4 (2021). https://doi.org/10.46298/LMCS-17(4:25)2021

[5] Christian Bartolo Burlò, Adrian Francalanza, Alceste Scalas, Catia Trubiani, and Emilio Tuosto. 2022. PSTMonitor: Monitor synthesis from probabilistic session types. *Sci. Comput. Program.* 222 (2022), 102847. https://doi.org/10.1016/j.SCICO.2022.102847

[6] Luis Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In *CONCUR 2010 - Concurrency Theory, 21st International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings (Lecture Notes in Computer Science, Vol. 6269)*, Paul Gastin and François Laroussinie (Eds.). Springer, 222-236. https://doi.org/10.1007/978-3-642-15375-4_16

[7] Luis Caires, Frank Pfenning, and Bernardo Toninho. 2016. Linear logic propositions as session types. *Math. Struct. Comput. Sci.* 26, 3 (2016), 367-423. https://doi.org/10.1017/S0960129514000218

[8] Luca Ciccone, Francesco Dagnino, and Luca Padovani. 2022. Fair Termination of Multiparty Sessions. In *36th European Conference on Object-Oriented Programming, ECOOP 2022, June 6-10, 2022, Berlin, Germany (LIPIcs, Vol. 222)*, Karim Ali and Jan Vitek (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 26:1-26:26. https://doi.org/10.4230/LIPIcs.ECOOP.2022.26

[9] Luca Ciccone, Francesco Dagnino, and Luca Padovani. 2024. Fair termination of multiparty sessions. *Journal of Logical and Algebraic Methods in Programming* 139 (2024), 100964. https://doi.org/10.1016/j.jlamp.2024.100964

[10] Luca Ciccone and Luca Padovani. 2022. Fair termination of binary sessions. *Proc. ACM Program. Lang.* 6, POPL (2022), 1-30. https://doi.org/10.1145/3498666

[11] Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. 2016. Global progress for dynamically interleaved multiparty sessions. *Math. Struct. Comput. Sci.* 26, 2 (2016), 238-302. https://doi.org/10.1017/S0960129514000188

[12] Bruno Courcelle. 1983. Fundamental Properties of Infinite Trees. *Theor. Comput. Sci.* 25 (1983), 95-169. https://doi.org/10.1016/0304-3975(83)90059-2

[13] Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, and Ishani Santurkar. 2021. Resource-Aware Session Types for Digital Contracts. In *34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021, IEEE*, 1-16. https://doi.org/10.1109/CSF51468.2021.00004

[14] Ankush Das, Jan Hoffmann, and Frank Pfenning. 2018. Work Analysis with Resource-Aware Session Types. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, Anuj Dawar and Erich Grädel (Eds.). ACM, 305-314. https://doi.org/10.1145/3209108.3209146

[15] Ankush Das and Frank Pfenning. 2022. Rast: A Language for Resource-Aware Session Types. *Log. Methods Comput. Sci.* 18, 1 (2022). https://doi.org/10.46298/LMCS-18(1:9)2022

[16] Ankush Das, Di Wang, and Jan Hoffmann. 2023. Probabilistic Resource-Aware Session Types. *Proc. ACM Program. Lang.* 7, POPL (2023), 1925-1956. https://doi.org/10.1145/3571259

[17] Nissim Francez. 1986. Fairness. Springer. https://doi.org/10.1007/978-1-4612-4886-6

[18] Orna Grumberg, Nissim Francez, and Shmuel Katz. 1984. Fair Termination of Communicating Processes. In *Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing* (Vancouver, British Columbia, Canada) (PODC '84). Association for Computing Machinery, New York, NY, USA, 254-265. https://doi.org/10.1145/800222.806752

[19] Kohei Honda. 1993. Types for Dyadic Interaction. In *CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings (Lecture Notes in Computer Science, Vol. 715)*, Eike Best (Ed.). Springer, 509-523. https://doi.org/10.1007/3-540-57208-2_35

[20] Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In *Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings (Lecture Notes in Computer Science, Vol. 1381)*, Chris Hankin (Ed.). Springer, 122-138. https://doi.org/10.1007/Bf80053567

[21] Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luis Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. 2016. Foundations of Session Types and Behavioural Contracts. *ACM Comput. Surv.* 49, 1 (2016), 3:1-3:36. https://doi.org/10.1145/2873052

[22] Omar Inverso, Hernán C. Melgratti, Luca Padovani, Catia Trubiani, and Emilio Tuosto. 2020. Probabilistic Analysis of Binary Sessions. In *31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference) (LIPIcs, Vol. 171)*, Igor Konnov and Laura Kovács (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 14:1-14:21. https://doi.org/10.4230/LIPICS.CONCUR.2020.14

[23] Jan-Christoph Kassing and Jürgen Giesl. 2023. Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs. In *Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings (Lecture Notes in Computer Science, Vol. 14132)*, Brigitte Pientka and Cesare Tinelli (Eds.). Springer, 344-364. https://doi.org/10.1007/978-3-031-38499-8_20

[24] Naoki Kobayashi. 2002. A Type System for Lock-Free Processes. *Inf. Comput.* 177, 2 (2002), 122-159. https://doi.org/10.1006/inco.2002.3171

[25] Naoki Kobayashi. 2005. Type-based information flow analysis for the pi-calculus. *Acta Informatica* 42, 4-5 (2005), 291-347. https://doi.org/10.1007/S00236-005-0179-X

[26] Naoki Kobayashi and Davide Sangiorgi. 2008. A Hybrid Type System for Lock-Freedom of Mobile Processes. In *Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings (Lecture Notes in Computer Science, Vol. 5123)*, Aarti Gupta and Sharad Malik (Eds.). Springer, 80-93. https://doi.org/10.1007/978-3-540-70545-1_10

[27] Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca. 2021. Intersection types and (positive) almost-sure termination. *Proc. ACM Program. Lang.* 5, POPL (2021), 1-32. https://doi.org/10.1145/3434313

[28] Ugo Dal Lago and Charles Grellois. 2019. Probabilistic Termination by Monadic Affine Sized Typing. *ACM Trans. Program. Lang. Syst.* 41, 2 (2019), 10:1-10:65. https://doi.org/10.1145/3293605

[29] Sam Lindley and J. Garrett Morris. 2016. Talking bananas: structural recursion for session types. In *Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016*, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 434-447. https://doi.org/10.1145/2951913.2951921

[30] Annabelle McIver and Carroll Morgan. 2005. *Abstraction, Refinement and Proof for Probabilistic Systems*. Springer. https://doi.org/10.1007/B138392

[31] Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. 2018. A new proof rule for almost-sure termination. *Proc. ACM Program. Lang.* 2, POPL (2018), 33:1-33:28. https://doi.org/10.1145/3158121

[32] Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In *Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16*, New York, NY, USA, July 5-8, 2016, Martin Grohe, Eric Koskinen, and Natarajan Shankar (Eds.). ACM, 672-681. https://doi.org/10.1145/2933575.2935317

[33] Luca Padovani. 2014. Deadlock and lock freedom in the linear π-calculus. In *Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, Thomas A. Henzinger and Dale Miller (Eds.). ACM, 72:1-72:10. https://doi.org/10.1145/2603088.2603116

[34] Luca Padovani. 2022. On the Fair Termination of Client-Server Sessions. In *28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France (LIPIcs, Vol. 269)*, Delia Kesner and Pierre-Marie Pédrot (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 5:1-5:21. https://doi.org/10.4230/LIPICS.TYPES.2022.5

[35] Luca Padovani, Vasco Thudichum Vasconcelos, and Hugo Torres Vieira. 2014. Typing Liveness in Multiparty Communicating Systems. In *Coordination Models and Languages - 16th IFIP WG 6.1 International Conference, COORDINATION 2014, Held as Part of the 9th International Federated Conferences on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3-5, 2014, Proceedings (Lecture Notes in Computer Science, Vol. 8459)*, Eva Kühn and Rosario Pugliese (Eds.). Springer, 147-162. https://doi.org/10.1007/978-3-662-43376-8_10

[36] Rob van Glaabek and Peter Hофner. 2019. Progress, Justness, and Fairness. *ACM Comput. Surv.* 52, 4 (2019), 69:1-69:38. https://doi.org/10.1145/3329125

[37] Philip Wadler. 2014. Propositions as sessions. *J. Funct. Program.* 24, 2-3 (2014), 384-418. https://doi.org/10.1017/S095679681400001X