Prioritise the Best Variation

Wen Kokke, Ornela Dardha

► To cite this version:

Wen Kokke, Ornela Dardha. Prioritise the Best Variation. 41th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2021, Valletta, Malta. pp.100-119, 10.1007/978-3-030-78089-0_6. http-03740257

HAL Id: hal-03740257

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

Submitted on 29 Jul 2022

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 CC BY 4.0 - Attribution - International License
<figure><img src="image_2.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.
Prioritise the Best Variation*

Wen Kokke¹ and Ornela Dardha²

University of Edinburgh, Edinburgh wen.kokke@ed.ac.uk
University of Glasgow, Glasgow ornela.dardha@glasgow.ac.uk

**Abstract.** Binary session types guarantee communication safety and session fidelity, but *alone* they cannot rule out deadlocks arising from the interleaving of different sessions. In Classical Processes (CP) [53]—a process calculus based on classical linear logic—deadlock freedom is guaranteed by combining channel creation and parallel composition under the same logical cut rule. Similarly, in Good Variation (GV) [54,39]—a linear concurrent λ-calculus—deadlock freedom is guaranteed by combining channel creation and thread spawning under the same operation, called fork. In both CP and GV, deadlock freedom is achieved at the expense of expressivity, as the only processes allowed are tree-structured. Dardha and Gay [19] define Priority CP (PCP), which allows cyclic-structured processes and restores deadlock freedom by using *priorities*, in line with Kobayashi and Padovani [34,44]. Following PCP, we present Priority GV (PGV), a variant of GV which decouples channel creation from thread spawning. Consequently, we type cyclic-structured processes and restore deadlock freedom by using priorities. We show that our type system is sound by proving subject reduction and progress. We define an encoding from PCP to PGV and prove that the encoding preserves typing and is sound and complete with respect to the operational semantics.

**Keywords:** session types · π-calculus · functional programming · deadlock freedom · GV · CP

# 1 Introduction

Session types [29,47,30] are types for protocols. Regular types ensure functions are used according to their specification. Session types ensure *communication channels* are used according to their protocols. Session types have been studied in many settings. For instance, in the π-calculus [29,47,30], a foundational calculus for communication and concurrency, and in concurrent λ-calculi [26], including the focus of our paper: Good Variation [54,39, GV].

GV is a concurrent λ-calculus with *binary* session types, where each channel is shared between exactly two processes. Binary session types guarantee two crucial properties *communication safety*—e.g., if the protocol says to transmit an integer, you transmit an integer—and *session fidelity*—e.g., if the protocol says send, you send. A third crucial property is *deadlock freedom*, which ensures

<footnote>* Supported by the EU HORIZON 2020 MSCA RISE project 778233 "Behavioural Application Program Interfaces" (BehAPI).</footnote>
that processes do not have cyclic dependencies—e.g., when two processes wait for each other to send a value. Binary session types *alone* are insufficient to rule out deadlocks arising from interleaved sessions, but several additional techniques have been developed to guarantee deadlock freedom in session-typed π-calculus and concurrent λ-calculus.

In the π-calculus literature, there have been several attempts at developing Curry-Howard correspondences between session-typed π-calculus and linear logic [27]: Caires and Pfenning's πDILL [9] corresponds to dual intuitionistic linear logic [4], and Wadler's Classical Processes [53, CP] corresponds to classical linear logic [27, CLL]. Both calculi guarantee deadlock freedom, which they achieve by restricting structure of processes and shared channels to *trees*, by combing name restriction and parallel composition into a single construct, corresponding to the logical cut. This ensures that two processes can only communicate via exactly one series of channels, which rules out interleavings of sessions, and guarantees deadlock freedom. There are many downsides to combining name restriction and parallel composition, such as lack of modularity, difficulty typing structural congruence and formulating label-transition semantics, which have led to various approaches to decoupling these constructs. Hypersequent CP [41, 37, 38] and Linear Compositional Choreographies [14] decouple them, but maintain the correspondence to CLL and allow only tree-structured processes. Priority CP [20, PCP] weakens the correspondence to CLL in exchange for a more expressive language which allows cyclic-structured processes. PCP decouples CP's cut rule into two separate constructs: one for parallel composition via a mix rule, and one for name restriction via a cycle rule. To restore deadlock freedom, PCP uses *priorities* [34, 44]. Priorities encode the *order of actions* and rule out bad cyclic interleavings. Dardha and Gay [20] prove cycle-elimination for PCP, adapting the cut-elimination proof for classical linear logic, and deadlock freedom follows as a corollary.

CP and GV are related via a pair of translations which satisfy simulation [40], and which can be tweaked to satisfy reflection. The two calculi share the same strong guarantees. GV achieves deadlock freedom via a similar syntactic restriction: it combines channel creation and thread spawning into a single operation, called “fork”, which is related to the cut construct in CP. Unfortunately, as with CP, this syntactic restriction has its downsides.

Our aim is to develop a more expressive version of GV while maintaining deadlock freedom. While process calculi have their advantages, e.g., their succinctness, we chose to work with GV for several reasons. In general, concurrent λ-calculi support higher-order functions, and have a capability for abstraction not usually present in process calculi. Within a concurrent λ-calculus, one can derive extensions of the communication capabilities of the language via well-understood extensions of the functional fragment, e.g., we can derive internal/external choice from sum types. Concurrent λ-calculi maintain a clear separation between the program which the user writes and the configurations which represent the state of the system as it evaluates the program. However, our main motivation is that results obtained for λ-calculi transfer more easily to real-world functional pro-
gramming languages. Case in point: we easily adapted the type system of PGV to Linear Haskell [6], which gives us a library for deadlock-free session-typed programming [36]. The benefit of working specifically with GV, as opposed to other concurrent λ-calculi, is its relation to CP [53], and its formal properties, including deadlock freedom. We thus pose our research question for GV:

**RQ:** Can we design a more expressive GV which guarantees deadlock freedom for cyclic-structured processes?

We follow the line of work from CP to Priority CP, and present Priority GV (PGV), a variant of GV which decouples channel creation from thread spawning, thus allowing cyclic-structured processes, but which nonetheless guarantees deadlock freedom via priorities. This closes the circle of the connection between CP and GV [53], and their priority-based versions, PCP [20] and PGV. We make the following main contributions:

(§2) **Priority GV.** We present Priority GV (§2, PGV), a session-typed functional language with priorities, and prove subject reduction (theorem 1) and progress (theorem 2). We addresses several problems in the original GV language, most notably: (a) PGV does not require the pseudo-type $S^\sharp$; and (b) its structural congruence is type preserving. PGV answers our research question positively as it allows cyclic-structured binary session-typed processes that are deadlock free.

(§3) **Translation from PCP to PGV.** We present a sound and complete encoding of Priority CP [20] in PGV (§3). We prove the encoding preserves typing (theorem 4) and satisfies operational correspondence (theorems 5 and 6). To obtain a tight correspondence, we update PCP, moving away from commuting conversions and reduction as cut elimination towards reduction based on structural congruence, as it is standard in process calculi.

## 2 Priority GV

We present Priority GV (PGV), a session-typed functional language based on GV [54,39] which uses priorities à la Kobayashi and Padovani [34,45] to enforce deadlock freedom. Priority GV offers a more fine-grained analysis of communication structures, and by separating channel creation from thread spawning it allows cyclic structures. We illustrate this with two programs in PGV, examples 1 and 2. Each program contains two processes—the main process, and the child process created by spawn—which communicate using two channels. The child process receives a unit over the channel $x/x'$, and then sends a unit over the channel $y/y'$. The main process does one of two things: (a) in example 1, it sends a unit over the channel $x/x'$, and then waits to receive a unit over the channel $y/y'$; (b) in example 2, it does these in the opposite order, which results in a deadlock. PGV is more expressive than GV: example 1 is typeable and guaranteed deadlock-free in PGV, but is not typeable in GV [53] and not guaranteed deadlock-free in GV's predecessor [26]. We believe PGV is a non-conservative extension of GV, as CP can be embedded in a Kobayashi-style system [22].
Example 1 (Cyclic Structure).

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

Example 2 (Deadlock).

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

**Session types.** Session types ($S$) are defined by the following grammar:

$$S ::= !^o T.S \mid ?^o T.S \mid \mathbf{end}_i^o \mid \mathbf{end}_i^o$$

Session types $!^o T.S$ and $?^o T.S$ describe the endpoints of a channel over which we send or receive a value of type $T$, and then proceed as $S$. Types $\mathbf{end}_i^o$ and $\mathbf{end}_i^o$ describe endpoints of a channel whose communication has finished, and over which we must synchronise before closing the channel. Each connective in a session type is annotated with a *priority* $o \in \mathbb{N}$.

**Types.** Types $(T, U)$ are defined by the following grammar:

$$T, U ::= T \times U \mid \mathbf{1} \mid T + U \mid \mathbf{0} \mid T \xrightarrow{\sim^{p,q}} U \mid S$$

Types $T \times U$, $\mathbf{1}$, $T + U$, and $\mathbf{0}$ are the standard linear $\lambda$-calculus product type, unit type, sum type, and empty type. Type $T \xrightarrow{\sim^{p,q}} U$ is the standard linear function type, annotated with *priority bounds* $p, q \in \mathbb{N} \cup \{\bot, \top\}$. Every session type is also a type. Given a function with type $T \xrightarrow{\sim^{p,q}} U$, $p$ is a *lower bound* on the priorities of the endpoints captured by the body of the function, and $q$ is an *upper bound* on the priority of the communications that take place as a result of applying the function. The type of *pure functions* $T \xrightarrow{\sim} U$, i.e., those which perform no communications, is syntactic sugar for $T \xrightarrow{\sim, \top} U$.

**Environments.** Typing environments $\Gamma, \Delta$ associate types to names. Environments are linear, so two environments can only be combined as $\Gamma, \Delta$ if their names are distinct, i.e., $\text{fv}(\Gamma) \cap \text{fv}(\Delta) = \emptyset$.

$$\Gamma, \Delta ::= \emptyset \mid \Gamma, x : T$$

**Duality.** Duality plays a crucial role in session types. The two endpoints of a channel are assigned dual types, ensuring that, for instance, whenever one program sends a value on a channel, the program on the other end is waiting to receive. Each session type $S$ has a dual, written $\overline{S}$. Duality is an involutive function which preserves priorities:

$$!^o T.S = ?^o T.S \quad ?^o T.S = !^o T.S \quad \overline{\mathbf{end}}_i^o = \mathbf{end}_i^o \quad \overline{\mathbf{end}}_i^o = \mathbf{end}_i^o$$
**Priorities.** Function `pr(·)` returns the smallest priority of a session type. The type system guarantees that the top-most connective always holds the smallest priority, so we simply return the priority of the top-most connective:

$$pr(!^o T.S) = o \quad pr(?^o T.S) = o \quad pr(\mathbf{end}_i^o) = o \quad pr(\mathbf{end}_?^o) = o$$

We extend the function `pr(·)` to types and typing contexts by returning the smallest priority in the type or context, or `⊤` if there is no priority. We use `∩` and `∪` to denote the minimum and maximum:

$$\begin{align*}
\min_{\text{pr}}(T \times U) &= \min_{\text{pr}}(T) \sqcap \min_{\text{pr}}(U) & \min_{\text{pr}}(\mathbf{1}) &= \top \\
\min_{\text{pr}}(T + U) &= \min_{\text{pr}}(T) \sqcap \min_{\text{pr}}(U) & \min_{\text{pr}}(\mathbf{0}) &= \top \\
\min_{\text{pr}}(T - \mathcal{O}^{p,q} U) &= p & \min_{\text{pr}}(S) &= \text{pr}(S) \\
\min_{\text{pr}}(\Gamma, x : A) &= \min_{\text{pr}}(\Gamma) \sqcap \min_{\text{pr}}(A) & \min_{\text{pr}}(\emptyset) &= \top
\end{align*}$$

**Terms.** Terms $(L, M, N)$ are defined by the following grammar:

$$\begin{array}{l@{\hspace{2em}}l}
L, M, N & ::= x \mid K \mid \lambda x.M \mid M N \\
        & \mid () \mid M; N \mid (M, N) \mid \mathbf{let} (x, y) = M \ \mathbf{in} \ N \\
        & \mid \mathbf{inl} M \mid \mathbf{inr} M \mid \mathbf{case} L \{\mathbf{inl} x \mapsto M; \mathbf{inr} y \mapsto N\} \mid \mathbf{absurd} M \\
K & ::= \mathbf{link} \mid \mathbf{new} \mid \mathbf{spawn} \mid \mathbf{send} \mid \mathbf{recv} \mid \mathbf{close} \mid \mathbf{wait}
\end{array}$$

Let $x, y, z$, and $w$ range over variable names. Occasionally, we use $a, b, c$, and $d$. The term language is the standard linear $\lambda$-calculus with products, sums, and their units, extended with constants $K$ for the communication primitives.

Constants are best understood in conjunction with their typing and reduction rules in figs. 1 and 2. Briefly, **link** links two endpoints together, forwarding messages from one to the other, **new** creates a new channel and returns a pair of its endpoints, and **spawn** spawns off its argument as a new thread. The **send** and **recv** functions send and receive values on a channel. However, since the typing rules for PGV ensure the linear usage of endpoints, they also return a new copy of the endpoint to continue the session. The **close** and **wait** functions close a channel. We use syntactic sugar to make terms more readable: we write **let** $x = M$ in $N$ in place of $(\lambda x.N) M$, $\lambda().M$ in place of $\lambda z.z; M$, and $\lambda(x,y).M$ in place of $\lambda z.\mathbf{let} (x, y) = z$ in $M$. We recover **fork** as $\lambda x.\mathbf{let} (y, z) = \mathbf{new} ()$ in **spawn** $(\lambda().x y); z$.

**Internal and External Choice.** Typically, session-typed languages feature constructs for internal and external choice. In GV, these can be defined in terms of the core language, by sending or receiving a value of a sum type [39]. We use the following syntactic sugar for internal $(S \oplus^o S')$ and external $(S \&^o S')$ choice and their units:

$$\begin{align*}
S \oplus^o S' &\triangleq !^o (\overline{S} + \overline{S}').\mathbf{end}_i^{o+1} & \oplus^o \{\} &\triangleq !^o \mathbf{0}.\mathbf{end}_?^{o+1} \\
S \&^o S' &\triangleq ?^o (S + S').\mathbf{end}_?^{o+1} & \&^o \{\} &\triangleq ?^o \mathbf{0}.\mathbf{end}_?^{o+1}
\end{align*}$$

As the syntax for units suggests, these are the binary and nullary forms of the more common n-ary choice constructs $\oplus^o \{l_i : S_i\}_{i \in I}$ and $\&^o \{l_i : S_i\}_{i \in I}$, which
one may obtain generalising the sum types to variant types. For simplicity, we present only the binary and nullary forms.

Similarly, we use syntactic sugar for the term forms of choice, which combine sending and receiving with the introduction and elimination forms for the sum and empty types. There are two constructs for binary internal choice, expressed using the meta-variable $\ell$ which ranges over $\{\text{inl}, \text{inr}\}$. As there is no introduction for the empty type, there is no construct for nullary internal choice:

select $\ell$ $\triangleq$ $\lambda x.\text{let} (y, z) = \text{new in close} (\text{send} (\ell y, x)); z$

offer $L \{\text{inl} x \mapsto M; \text{inr} y \mapsto N\} \triangleq$

let $(z, w) = \text{recv } L \text{ in wait } w; \text{case } z \{\text{inl } x \mapsto M; \text{inr } y \mapsto N\}$

offer $L \{\}$ $\triangleq$ let $(z, w) = \text{recv } L \text{ in wait } w; \text{absurd } z$

**Operational Semantics.** Priority GV terms are evaluated as part of a configuration of processes. Configurations are defined by the following grammar:

$\phi ::= \bullet | \circ$

$C, D, E ::= \phi M | C \parallel D | (\nu xx')C$

Configurations $(C, D, E)$ consist of threads $\phi M$, parallel compositions $C \parallel D$, and name restrictions $(\nu xx')C$. To preserve the functional nature of PGV, where programs return a single value, we use flags $(\phi)$ to differentiate between the main thread, marked $\bullet$, and child threads created by spawn, marked $\circ$. Only the main thread returns a value. We determine the flag of a configuration by combining the flags of all threads in that configuration:

$\bullet + \circ = \bullet$

$\circ + \bullet = \bullet$

$\circ + \circ = \circ$

($\bullet + \circ$ is undefined)

The use of $\circ$ for child threads [39] overlaps with the use of the meta-variable $o$ for priorities [20]. Both are used to annotate sequents: flags appear on the sequent in configuration typing, and priorities in term typing. To distinguish the two symbols, they are typeset in a different font and a different colour.

Values $(V, W)$, evaluation contexts $(E)$, thread evaluation contexts $(\mathcal{F})$, and configuration contexts $(\mathcal{G})$ are defined by the following grammars:

$V, W ::= x | K | \lambda x.M | () | (V, W) | \text{inl } V | \text{inr } V$

$E ::= \Box | E M | V E$

$| E; N | (E, M) | (V, E) | \text{let } (x, y) = E \text{ in } M$

$| \text{inl } E | \text{inr } E | \text{case } E \{\text{inl } x \mapsto M; \text{inr } y \mapsto N\} | \text{absurd } E$

$\mathcal{F} ::= \phi E$

$\mathcal{G} ::= \Box | \mathcal{G} \parallel \mathcal{C} | (\nu xy)\mathcal{G}$

We factor the reduction relation of PGV into a deterministic reduction on terms $(\rightarrow_M)$ and a non-deterministic reduction on configurations $(\rightarrow_C)$, see fig. 1. We write $\rightarrow_M^+$ and $\rightarrow_C^+$ for the transitive closures, and $\rightarrow_M^*$ and $\rightarrow_C^*$ for the reflexive-transitive closures.

Term reduction is the standard call-by-value, left-to-right evaluation for GV, and only deviates from reduction for the linear $\lambda$-calculus in that it reduces terms to values or ready terms waiting to perform a communication action.
Term reduction.

E-LAM (λx.M) V →$_{M}$ M {V/x}

E-UNIT let () = () in M →$_{M}$ M

E-PAIR let (x, y) = (V, W) in M →$_{M}$ M {V/x} {W/y}

E-INL case inl V {inl x ↦→ M; inr y ↦→ N} →$_{M}$ M {V/x}

E-INR case inr V {inl x ↦→ M; inr y ↦→ N} →$_{M}$ N {V/y}

$$
\begin{array}{c}
\text{E-LIFT} \\
\frac{M \to_M M'}{E[M] \to_M E[M']}
\end{array}
$$

Structural congruence.

SC-LINKSWAP $\mathcal{F}$[link $(x, y)$] ≡ $\mathcal{F}$[link $(y, x)$]

SC-RESLINK $(\nu xy)(\phi \text{ link } (x, y)) \equiv \phi$ ()

SC-RESSWAP $(\nu xy)\mathcal{C}$ ≡ $(\nu xy)\mathcal{C}$

SC-RESCOMM $(\nu xy)(\nu zw)\mathcal{C}$ ≡ $(\nu zw)(\nu xy)\mathcal{C}$, if $\{x, y\} \cap \{z, w\} = \emptyset$

SC-RESEXT $(\nu xy)(\mathcal{C} \parallel \mathcal{D})$ ≡ $\mathcal{C} \parallel (\nu xy)\mathcal{D}$, if $x, y \notin \text{fv}(\mathcal{C})$

SC-PARNIL $\mathcal{C} \parallel \circ(\cdot)$ ≡ $\mathcal{C}$

SC-PARCOMM $\mathcal{C} \parallel \mathcal{D}$ ≡ $\mathcal{D} \parallel \mathcal{C}$

SC-PARASSOC $\mathcal{C} \parallel (\mathcal{D} \parallel \mathcal{E})$ ≡ $(\mathcal{C} \parallel \mathcal{D}) \parallel \mathcal{E}$

Configuration reduction.

E-LINK $(\nu xy)(\mathcal{F}[\text{link } (w, x)] \parallel \mathcal{C}) \to_C \mathcal{F}[(\cdot)] \parallel \mathcal{C}\{w/y\}$

E-NEW $\mathcal{F}[\text{new } ()] \to_C (\nu xy)(\mathcal{F}[(x, y)])$, if $x, y \notin \text{fv}(\mathcal{F})$

E-SPAWN $\mathcal{F}[\text{spawn } V]$ →$_{C}$ $\mathcal{F}[(\cdot)] \parallel \circ V$ ()

E-SEND $(\nu xy)(\mathcal{F}[\text{send } (V, x)] \parallel \mathcal{F}'[\text{recv } y]) \to_C (\nu xy)(\mathcal{F}[x] \parallel \mathcal{F}'[(V, y)])$

E-CLOSE $(\nu xy)(\mathcal{F}[\text{wait } x] \parallel \mathcal{F}'[\text{close } y]) \to_C \mathcal{F}[(\cdot)] \parallel \mathcal{F}'[(\cdot)]$

E-LIFTC
$\frac{\mathcal{C} \to_C \mathcal{C}'}{\mathcal{G}[\mathcal{C}] \to_C \mathcal{G}[\mathcal{C}']}$

E-LIFTM
$\frac{M \to_M M'}{\mathcal{F}[M] \to_M \mathcal{F}[M']}$

E-LIFTSC
\frac{\mathcal{C} \equiv \mathcal{C}' \qquad \mathcal{C}' \to_C \mathcal{D}' \qquad \mathcal{D}' \equiv \mathcal{D}}{\mathcal{C} \to_C \mathcal{D}}

<caption>Fig. 1. Operational Semantics for PGV.</caption>

Configuration reduction resembles evaluation for a process calculus: E-LINK, E-SEND, and E-CLOSE perform communications, E-LIFTC allows reduction under configuration contexts, and E-LIFTSC embeds a structural congruence $\equiv$. The remaining rules mediate between the process calculus and the functional language: E-NEW and E-SPAWN evaluate the **new** and **spawn** constructs, creating the equivalent configuration constructs, and E-LIFTM embeds term reduction.

Structural congruence satisfies the following axioms: SC-LINKSWAP allows swapping channels in the link process. SC-RESLINK allows restriction to applied to link which is structurally equivalent to the terminated process, thus allowing elimination of unnecessary restrictions. SC-RESSWAP allows swapping channels and SC-RESCOMM states that restriction is commutative. SC-RESEXT is the standard scope extrusion rule. Rules SC-PARNIL, SC-PARCOMM and SC-PARASSOC
state that parallel composition uses the terminated process as the neutral element; it is commutative and associative.

While our configuration reduction is based on the standard evaluation for GV, the increased expressiveness of PGV allows us to simplify the relation on two counts. (a) *We decompose the fork construct*. In GV, **fork** creates a new channel, spawns a child thread, and, when the child thread finishes, it closes the channel to its parent. In PGV, these are three separate operations: **new**, **spawn**, and **close**. We no longer require that every child thread finishes by returning a terminated channel. Consequently, we also simplify the evaluation of the **link** construct. Intuitively, evaluating **link** causes a substitution: if we have a channel bound as $(vxy)$, then **link**$(w, x)$ replaces all occurrences of $y$ by $w$. However, in GV, **link** is required to return a terminated channel, which means that the semantics for **link** must create a fresh channel of type **end**$_1$/**end**$_?$. The endpoint of type **end**$_1$ is returned by the **link** construct, and a **wait** on the other endpoint guards the *actual* substitution. In PGV, evaluating **link** simply causes a substitution. (b) *Our structural congruence is type preserving*. Consequently, we can embed it directly into the reduction relation. In GV, this is not the case, and subject reduction relies on proving that if $≡ \rightarrow_c$ ends up in an ill-typed configuration, we can rewrite it to a well-typed configuration using $≡$.

**Typing.** Figure 2 gives the typing rules for PGV. Typing rules for terms are at the top of fig. 2. Terms are typed by a judgement $\Gamma \vdash^p M : T$ stating that “a term $M$ has type $T$ and an upper bound on its priority $p$ under the typing environment $\Gamma$”. Typing for the linear $\lambda$-calculus is standard. Linearity is ensured by splitting environments on branching rules, requiring that the environment in the variable rule consists of just the variable, and the environment in the constant and unit rules are empty. Constants $K$ are typed using type schemas, and embedded using $T-CONST$ (mid of fig. 2). The typing rules treat all variables as linear resources, even those of non-linear types such as **1**. However, the rules can easily be extended to allow values with unrestricted usage [53].

The only non-standard feature of the typing rules is the priority annotations. Priorities are based on *obligations/capabilities* used by Kobayashi [34], and simplified to single priorities following Padovani [44]. The integration of priorities into GV is adapted from Padovani and Novara [45]. Paraphrasing Dardha and Gay [20], priorities obey the following two laws: (i) an action with lower priority happens before an action with higher priority; and (ii) communication requires *equal* priorities for dual actions.

In PGV, we keep track of a lower and upper bound on the priorities of a term, i.e., while evaluating the term, when does it start communicating, and when does it finish. The upper bound is written on the sequent, whereas the lower bound is approximated from the typing environment. Typing rules for sequential constructs enforce sequentially, e.g., the typing for $M; N$ has a side condition which requires that the upper bound of $M$ is smaller than the lower bound of $N$, i.e., $M$ finishes before $N$ starts. The typing rule for **new** ensures that both endpoints of a channel share the same priorities. Together, these two constraints guarantee deadlock freedom.
## Static Typing Rules.

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

## Type Schemas for Constants.

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

## Runtime Typing Rules.

<figure><img src="image_7.png" /><figcaption>**Fig. 2.** Typing Rules for PGV.</figcaption></figure>
**Lemma 1.** If $\Gamma \vdash^p V : T$, then $p = \bot$, and $\min_{\text{pr}}(\Gamma) = \min_{\text{pr}}(T)$.

**Lemma 2 (Substitution).**

If $\Gamma, x : U' \vdash^p M : T$ and $\Theta \vdash^q V : U'$, then $\Gamma, \Theta \vdash^p M\{V/x\} : T$.

**Lemma 3 (Subject Reduction, $\rightarrow_M$).**

If $\Gamma \vdash^p M : T$ and $M \rightarrow_M M'$, then $\Gamma \vdash^p M' : T$.

**Lemma 4 (Subject Congruence, $\equiv$).**

If $\Gamma \vdash^\phi C$ and $C \equiv C'$, then $\Gamma \vdash^\phi C'$.

**Theorem 1 (Subject Reduction, $\rightarrow_C$).**

If $\Gamma \vdash^\phi C$ and $C \rightarrow_C C'$, then $\Gamma \vdash^\phi C'$.

**Progress and deadlock freedom.** PGV satisfies progress, as PGV configurations either reduce or are in normal form. However, the normal forms may seem surprising at first, as evaluating a well-typed PGV term does not necessarily produce just a value. If a term returns an endpoint, then its normal form contains a thread which is ready to communicate on the dual of that endpoint. This behaviour is not new to PGV. Let us consider an example, adapted from Lindley and Morris [39], in which a term returns an endpoint linked to an echo server. The echo server receives a value and sends it back unchanged. Consider the program which creates a new channel, with endpoints $x$ and $x'$, spawns off an echo server listening on $x$, and then returns $x'$:

$$ \bullet \begin{array}{l} \text{let } (x, x') = \text{new in} \\ \text{spawn } (\lambda().\text{echo}_x); x' \end{array} \qquad \begin{array}{l} \text{echo}_x \triangleq \begin{array}{l} \text{let } (y, x) = \text{recv } x \text{ in} \\ \text{let } x = \text{send } (y, x) \text{ in close } x \end{array} \end{array} $$

If we reduce the above program, we get $(\nu xx')(\circ \text{echo}_x \parallel \bullet x')$. Clearly, no more evaluation is possible, even though the configuration contains the thread $\circ \text{echo}_x$, which is blocked on $x$. In corollary 1 we will show that if a term does not return an endpoint, it must produce only a value.

Actions are terms which perform communication actions and which synchronise between two threads. Ready terms are terms which perform communication actions, either by themselves, e.g., creating a new channel or thread, or with another thread, e.g., sending or receiving. Progress for the term language is standard for GV, and deviates from progress for linear $\lambda$-calculus only in that terms may reduce to values or ready terms:

**Definition 1 (Actions).** A term acts on an endpoint $x$ if it is send $(V, x)$, recv $x$, close $x$, or wait $x$. A term is an action if it acts on some endpoint $x$.

**Definition 2 (Ready Terms).** A term $L$ is ready if it is of the form $E[M]$, where $M$ is of the form new, spawn $N$, link $(x, y)$, or $M$ acts on $x$. In the latter case, we say that $L$ is ready to act on $x$.

**Lemma 5 (Progress, $\rightarrow_M$).** If $\Gamma \vdash^p M : T$ and $\Gamma$ contains only session types, then: (a) $M$ is a value; (b) $M \rightarrow_M N$ for some $N$; or (c) $M$ is ready.

Canonical forms deviate from those for GV, in that we opt to move all $\nu$-binders to the top. The standard GV canonical form, alternating $\nu$-binders and their corresponding parallel compositions, does not work for PGV, since multiple channels may be split across a single parallel composition.
A configuration either reduces, or it is equivalent to configuration in normal form. Crucial to the normal form is that each term $M_i$ is blocked on the corresponding channel $x_i$, and hence no two terms act on dual endpoints. Furthermore, no term $M_i$ can perform a communication action by itself, since those are excluded by the definition of actions. Finally, as a corollary, we get that well-typed terms which do not return endpoints return just a value:

**Definition 3 (Canonical Forms).** A configuration $C$ is in canonical form if it is of the form $(\nu x_1 x'_1) \dots (\nu x_n x'_n)(\circ M_1 \| \dots \| \circ M_m \| \bullet N)$ where no term $M_i$ is a value.

**Lemma 6 (Canonical Forms).** If $\Gamma \vdash \bullet C$, there exists some $D$ such that $C \equiv D$ and $D$ is in canonical form.

**Definition 4 (Normal Forms).** A configuration $C$ is in normal form if it is of the form $(\nu x_1 x'_1) \dots (\nu x_n x'_n)(\circ M_1 \| \dots \| \circ M_m \| \bullet V)$ where each $M_i$ is ready to act on $x_i$.

**Theorem 2 (Progress, $\rightarrow_C$).** If $\emptyset \vdash \bullet C$ and $C$ is in canonical form, then either $C \rightarrow_C D$ for some $D$; or $C \equiv D$ for some $D$ in normal form.

*Proof (Sketch).* Our proof follows that of Kobayashi [34, theorem 2]. We apply lemma 5 to each thread. Either we obtain a reduction, or each child thread is ready and the main thread ready or a value. We pick the ready term $L$ with the smallest priority bound. If $L$ contains new, spawn, or a link, we apply E-NEW, E-SPAWN, or E-LINK. Otherwise, $L$ must be ready on some $x_i$. Linearity guarantees there is some thread $L'$ which acts on $x'_i$. If $L'$ is ready, priority typing guarantees it is ready on $x'_i$, and we apply E-SEND or E-CLOSE. If $L'$ is not ready, it must be the main thread returning a value. We move $L$ into the $i^{th}$ position and repeat until we either find a reduction or reach normal form.

**Corollary 1.** If $\emptyset \vdash \phi C$, $C \dashv_C C$, and $C$ contains no endpoints, then $C \equiv \phi V$ for some value $V$.

It follows immediately from theorem 2 and corollary 1 that a term which does not return an endpoint will complete all its communication actions, thus satisfying deadlock freedom.

# 3 Relation to Priority CP

We present a correspondence between Priority GV and an updated version of Priority CP [20, PCP], which is Wadler's CP [53] with priorities. This correspondence connects PGV to (a relaxed variant of) classical linear logic.

## 3.1 Revisiting Priority CP

Types $(A, B)$ in PCP correspond to linear logic connectives annotated with priorities $o \in \mathbb{N}$. Typing environments, duality, and the priority function $\text{pr}(\cdot)$ are defined as expected.

$$A, B ::= A \otimes^o B \mid A \nparallel^o B \mid 1^o \mid \bot^o \mid A \oplus^o B \mid A \&^o B \mid 0^o \mid \top^o$$
**Processes** (*P*, *Q*) in PCP are defined by the following grammar.

$$
\begin{array}{l}
P, Q ::= x \leftrightarrow y \mid (\nu x)y P \mid (P \parallel Q) \mid \mathbf{0} \\
\phantom{P, Q ::=} | x[y].P \mid x[\cdot].P \mid x(y).P \mid x().P \\
\phantom{P, Q ::=} | x \triangleleft \text{inl}.P \mid x \triangleleft \text{inr}.P \mid x \triangleright \{\text{inl} : P; \text{inr} : Q\} \mid x \triangleright \}
\end{array}
$$

Processes are typed by sequents $P \vdash \Gamma$, which correspond to the one-sided sequents in classical linear logic. Differently from PGV, in PCP we do not need to store the greatest priority on the sequent, as, due to the absence of higher-order functions, we cannot compose processes sequentially.

PCP decomposes cut into T-RES and T-PAR rules—corresponding to cycle and mix rules, respectively—and guarantees deadlock freedom by using priority constraints, e.g., as in T-SEND.

$$
\frac{
  \begin{array}{c}
    \text{T-RES} \\
    P \vdash \Gamma, x : A, y : A^{\perp} \\
    (\nu xy) P \vdash \Gamma
  \end{array}
}{
  \begin{array}{c}
    \text{T-PAR} \\
    P \vdash \Gamma \\
    P \parallel Q \vdash \Gamma, \Delta
  \end{array}
}
\qquad
\frac{
  \begin{array}{c}
    \text{T-SEND} \\
    P \vdash \Gamma, y : A, x : B \\
    x[y].P \vdash \Gamma, x : A \otimes^o B
  \end{array}
}{
  o < \min_{\text{pr}}(\Gamma, A, B)
}
$$

The main change we make to PCP is *removing commuting conversions* and
defining an operational semantics based on structural congruence. Commuting
conversions are necessary if we want our reduction strategy to correspond *exactly*
to cut elimination. However, from the perspective of process calculi, commuting
conversions behave strangely: they allow an input/output action to be moved
to the top of a process, thus potentially blocking actions which were previously
possible. This makes CP, and Dardha and Gay’s PCP [20], non-confluent. As
Lindley and Morris [39] show, all communications that can be performed *with*
the use of commuting conversions, can also be performed *without* them, using
structural congruence.

In particular for PCP, commuting conversions break our intuition that an
action with lower priority *occurs before* an action with higher priority. To cite
Dardha and Gay [20] “if a prefix on a channel endpoint *x* with priority *o* is
pulled out at top level, then to preserve priority constraints in the typing rules
[..], it is necessary to increase priorities of all actions after the prefix on *x*” by
*o* + 1. One benefit of removing commuting conversions is that we no longer need
to dynamically change the priorities during reduction, which means that the
intuition for priorities holds true in our updated version of PCP. Furthermore,
we can safely define reduction on untyped processes, which means that type and
priority information is erasable!

We prove closed progress for our updated PCP.

**Theorem 3 (Progress, =).**

If $P \vdash \emptyset$, then either $P = \mathbf{0}$ or there exists a $Q$ such that $P \models Q$.

**3.2 Correspondence between PGV and PCP**

We illustrate the relation between PCP and PGV by defining a translation from
PCP to PGV. The translation on types is defined as follows:

$$
\begin{align*}
(\mathbf{A} \otimes^o \mathbf{B}) &= !^o(\overline{\mathbf{A}}).(\mathbf{B}) & (\mathbf{1}^o) &= \mathbf{end}_!^o & (\mathbf{A} \not\otimes^o \mathbf{B}) &= ?^o(\mathbf{A}).(\mathbf{B}) & (\bot^o) &= \mathbf{end}_?^o \\
(\mathbf{A} \oplus^o \mathbf{B}) &= (\mathbf{A}) \oplus^o (\mathbf{B}) & (\mathbf{0}^o) &= \oplus^o \{\} & (\mathbf{A} \&^o \mathbf{B}) &= (\mathbf{A}) \&^o (\mathbf{B}) & (\top^o) &= \&^o \{\}
\end{align*}
$$
There are two separate translations on processes. The main translation, $((\cdot)|)_M$, translates processes to terms:

<table><tr><td>((x<sub>1</sub> &harr; y)<sub>M</sub></td><td>= link (x, y)</td></tr><tr><td>((νxy)P)<sub>M</sub></td><td>= let (x, y) = new in (P)<sub>M</sub></td></tr><tr><td>((P || Q)<sub>M</sub></td><td>= spawn (λ().(P)<sub>M</sub>); (Q)<sub>M</sub></td></tr><tr><td>((0)<sub>M</sub></td><td>= ()</td></tr><tr><td>((x[<sub>i</sub>].P)<sub>M</sub></td><td>= close x; (P)<sub>M</sub></td></tr><tr><td>((x().P)<sub>M</sub></td><td>= wait x; (P)<sub>M</sub></td></tr><tr><td>((x[y].P)<sub>M</sub></td><td>= let (y, z) = new in let x = send (z, x) in (P)<sub>M</sub></td></tr><tr><td>((x(y).P)<sub>M</sub></td><td>= let (y, x) = recv x in (P)<sub>M</sub></td></tr><tr><td>((x &lt; inl.P)<sub>M</sub></td><td>= let x = select inl x in (P)<sub>M</sub></td></tr><tr><td>((x &lt; inr.P)<sub>M</sub></td><td>= let x = select inr x in (P)<sub>M</sub></td></tr><tr><td>((x ▷ {inl : P; inr : Q})<sub>M</sub></td><td>= offer x {inl x <mapsto; (P)<sub>M</sub>; inr x <mapsto; (Q)<sub>M</sub>}</td></tr><tr><td>((x ▷ {})<sub>M</sub></td><td>= offer x {}</td></tr></table>

Unfortunately, the operational correspondence along $((\cdot)|)_M$ is unsound, as it translates $\nu$-binders and parallel compositions to **new** and **spawn**, which can reduce to their equivalent configuration constructs using E-NEW and E-SPAWN. The same goes for $\nu$-binders which are inserted when translating bound send to unbound send. For instance, the process $x[y].P$ is blocked, but its translation uses **new** and can reduce. To address this issue, we use a second translation, $((\cdot)|)_C$, which is equivalent to $((\cdot)|)_M$ followed by reductions using E-NEW and E-SPAWN:

<table><tr><td>((νxy)P)<sub>C</sub></td><td>= (νxy)(P)<sub>C</sub></td></tr><tr><td>((P || Q)<sub>C</sub></td><td>= (P)<sub>C</sub> || (Q)<sub>C</sub></td></tr><tr><td>((x[y].P)<sub>C</sub></td><td>= (νyz)(<sup>◦</sup> let x = send (z, x) in (P)<sub>M</sub>)</td></tr><tr><td>((x &lt; inl.P)<sub>C</sub></td><td>= (νyz)(<sup>◦</sup> let x = close (send (inl y, x))); z in (P)<sub>M</sub>)</td></tr><tr><td>((x &lt; inr.P)<sub>C</sub></td><td>= (νyz)(<sup>◦</sup> let x = close (send (inr y, x))); z in (P)<sub>M</sub>)</td></tr><tr><td>((P)<sub>C</sub></td><td>= <sup>◦</sup>(P)<sub>M</sub>, if none of the above apply</td></tr></table>

Typing environments are translated pointwise, and sequents $P \vdash \Gamma$ are translated as $((\Gamma)|^{\circ} (P)|_C)$, where $\circ$ indicates a child thread. Translated processes do not have a main thread. The translations $((\cdot)|)_M$ and $((\cdot)|)_C$ preserve typing, and the latter induces a sound and complete operational correspondence.

**Lemma 7 (Preservation, $((\cdot)|)_M$).** If $P \vdash \Gamma$, then $((\Gamma)|^P (P)|_M : 1)$.

**Theorem 4 (Preservation, $((\cdot)|)_C$).** If $P \vdash \Gamma$, then $((\Gamma)|^{\circ} (P)|_C)$.

**Lemma 8.** For any $P$, either:

$$- \circ ((P)|_M = (P)|_C; \text{ or}$$

$$- \circ ((P)|_M \xrightarrow{+} (P)|_C, \text{ and for any } C, \text{ if } \circ ((P)|_M \xrightarrow{C} C, \text{ then } C \xrightarrow{C} (P)|_C.$$

**Theorem 5 (Operational Correspondence, Soundness, $((\cdot)|)_C$).**

If $P \vdash \Gamma$ and $((P)|_C) \xrightarrow{C} C$, there exists a $Q$ such that $P \implies^+ Q$ and $C \xrightarrow{C} (Q)|_C$
**Theorem 6 (Operational Correspondence, Completeness, $\langle \cdot, \| \cdot \|_c \rangle$).**
If $P \vdash \Gamma$ and $P \Rightarrow \langle Q, \text{then } \langle \|P\|_c \rightarrow_c^+ \langle Q \| \rangle_c \rangle$.

# 4 Related Work and Discussion

**Deadlock freedom and progress.** Deadlock freedom and progress are well studied properties in the π-calculus. For the ‘standard’ typed π-calculus, an important line of work starts from Kobayashi’s approach to deadlock freedom [33], where priorities are values from an abstract poset. Kobayashi [34] simplifies the abstract poset to pairs of naturals, called *obligations* and *capabilities*. Padovani simplifies these further to a single natural, called a *priority* [44], and adapts obligations/capabilities to session types [43].

For the session-typed π-calculus, Dezani et al. [25] guarantee progress by allowing only one active session at a time. Dezani [24] introduces a partial order on channels, similar to Kobayashi [33]. Carbone and Debois [11] define progress for session typed π-calculus in terms of a *catalyser* which provides the missing counterpart to a process. Carbone et al. [10] use catalysers to show that progress is a compositional form of lock-freedom and can be lifted to session types via the encoding of session types to linear types [35,21,18]. Vieira and Vasconcelos [51] use single priorities and an abstract partial order to guarantee deadlock freedom in a binary session-typed π-calculus and building on conservation types.

While our work focuses on *binary* session types, it is worth to discuss related work on Multiparty Session Types (MPST). The line of work on MPST starts with Honda et al. [31], which guarantees deadlock freedom *within a single session*, but not for session interleaving. Bettini et al. [7] follow a technique similar to Kobayashi’s for MPST. The main difference with our work is that we associate priorities with communication actions, where Bettini et al. [7] associate them with channels. Carbone and Montesi [13] combine MPST with choreographies and obtain a formalism that satisfies deadlock freedom. Deniélou and Yoshida [23] introduce *multiparty compatibility* which generalises duality in binary session types. They synthesise safe and deadlock-free global types from local types leveraging LTSs and communicating automata. Castellani et al. [16] guarantee lock freedom, a stronger property than deadlock freedom, for MPST with *internal delegation*, where participants in the same session are allowed to delegate tasks to each other, and internal delegation is captured by the global type. Scalas and Yoshida [46] provide a revision of the foundations for MPST, and offer a less complicated and more general theory, by removing duality/consistency. The type systems is parametric and type checking is decidable, but allows for a novel integration of model checking techniques. More protocols and processes can be typed and are guaranteed to be free of deadlocks.

Neubauer and Thiemann [42] and Vasconcelos et al. [49,50] introduce the first functional language with session types. Such works did not guarantee deadlock freedom until GV [39,53]. Toninho et al. [48] present a translation of simply-typed λ-calculus into session-typed π-calculus, but their focus is not on deadlock freedom.
**Ties with logic.** The correspondence between logic and types lays the foundation for functional programming [54]. Since its inception by Girard [27], linear logic has been a candidate for a foundational correspondence for concurrent programs. A correspondence with linear π-calculus was established early on by Abramsky [1] and Bellin and Scott [5]. Many years later, several correspondences between linear logic and the π-calculus with binary session types were proposed. Caires and Pfenning [9] propose a correspondence with dual intuitionistic linear logic, while Wadler [53] proposes a correspondence with classical linear logic. Both guarantee deadlock freedom as a consequence of cut elimination. Dardha and Gay [20] integrate Kobayashi and Padovani's work on priorities [34,44] with CP, loosening its ties to linear logic in exchange for expressivity. Dardha and Pérez [22] compare priorities à la Kobayashi with tree restrictions à la CP, and show that the latter is a subsystem of the former. Balzer et al. [2] introduce sharing at the cost of deadlock freedom, which they restore using an approach similar to priorities [3]. Carbone et al. [15,12] give a logical view of MPST with a generalised duality. Caires and Pérez [8] give a presentation of MPST in terms of binary session types and the use of a *medium process* which guarantee protocol fidelity and deadlock freedom. Their binary session types are rooted in linear logic. Ciobanu and Horne [17] give the first Curry-Howard correspondence between MPST and BV [28], a conservative extension of linear logic with a non-commutative operator for sequencing. Horne [32] give a system for subtyping and multiparty compatibility where compatible processes are race free and deadlock free using a Curry-Howard correspondence, similar to the approach in [17].

**Conclusion.** We answered our research question by presenting Priority GV, a session-typed functional language which allows cyclic communication structures and uses priorities to ensure deadlock freedom. We showed its relation to Priority CP [20] via an operational correspondence.

**Future work.** Our formalism so far only captures the core of GV. In future work, we plan to explore recursion, following Lindley and Morris [40] and Padovani and Novara [45], and sharing, following Balzer and Pfenning [2] or Voinea et al. [52].

**Acknowledgements.** The authors would like to thank Simon Fowler, April Gonçalves, and Philip Wadler for their comments on the manuscript.
## References

1. Abramsky, S.: Proofs as processes. Theor. Comput. Sci. **135**(1), 5-9 (1994).
https://doi.org/10.1016/0304-3975(94)00103-0

2. Balzer, S., Pfenning, F.: Manifest sharing with session types. Proc. ACM Program. Lang. **1**(ICFP), 37:1-37:29 (2017). https://doi.org/10.1145/3110281

3. Balzer, S., Toninho, B., Pfenning, F.: Manifest deadlock-freedom for shared session types. In: Proc. of ESOP. Lect. Notes Comput. Sci., vol. 11423, pp. 611-639. Springer (2019). https://doi.org/10.1007/978-3-030-17184-122

4. Barber, A.: Dual intuitionistic linear logic (1996), https://www.lfcs.inf.ed.ac.uk/reports/96/ECS-LFCS-96-347/ECS-LFCS-96-347.pdf

5. Bellin, G., Scott, P.J.: On the π-calculus and linear logic. Theor. Comput. Sci. **135**(1), 11-65 (1994). https://doi.org/10.1016/0304-3975(94)00104-9

6. Bernardy, J.P., Boespflug, M., Newton, R.R., Jones, S.P., Spiwack, A.: Linear haskell: practical linearity in a higher-order polymorphic language. Proc. of POPL **2**, 1-29 (2018). https://doi.org/10.1145/3158093

7. Bettini, L., Coppo, M., D'Antoni, L., Luca, M.D., Dezani-Ciancaglini, M., Yoshida, N.: Global progress in dynamically interleaved multiparty sessions. In: Proc. of CONCUR. Lect. Notes Comput. Sci., vol. 5201, pp. 418-433. Springer (2008).
https://doi.org/10.1007/978-3-540-85361-933

8. Caires, L., Pérez, J.A.: Multiparty session types within a canonical binary theory, and beyond. In: Proc. of FORTE. Lect. Notes Comput. Sci., vol. 9688, pp. 74-95. Springer (2016). https://doi.org/10.1007/978-3-319-39570-826

9. Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Proc. of CONCUR. Lect. Notes Comput. Sci., vol. 6269, pp. 222-236. Springer (2010).
https://doi.org/10.1007/978-3-642-15375-426

10. Carbone, M., Dardha, O., Montesi, F.: Progress as compositional lock-freedom. In: Proc. of COORDINATION. Lect. Notes Comput. Sci., vol. 8459, pp. 49-64. Springer (2014). https://doi.org/10.1007/978-3-662-43376-834

11. Carbone, M., Debois, S.: A graphical approach to progress for structured communication in web services. In: Proc. of ICE. Electron. Proc. in Theor. Comput. Sci., vol. 38, pp. 13-27 (2010). https://doi.org/10.4204/EPTCS.38.4

12. Carbone, M., Lindley, S., Montesi, F., Schürmann, C., Wadler, P.: Coherence generalises duality: A logical explanation of multiparty session types. In: Proc. of CONCUR. LIPIcs, vol. 59, pp. 33:1-33:15. Leibniz-Zentrum für Informatik (2016).
https://doi.org/10.4230/LIPIcs.CONCUR.2016.33

13. Carbone, M., Montesi, F.: Deadlock-freedom-by-design: Multiparty asynchronous global programming. In: Proc. of POPL. pp. 263-274 (2013).
https://doi.org/10.1145/2480359.2429101

14. Carbone, M., Montesi, F., Schürmann, C.: Choreographies, logically. Distrib. Comput. **31**(1), 51-67 (2018). https://doi.org/10.1007/978-3-662-44584-625

15. Carbone, M., Montesi, F., Schürmann, C., Yoshida, N.: Multiparty session types as coherence proofs. In: Proc. of CONCUR. LIPIcs, vol. 42, pp. 412-426. Leibniz-Zentrum für Informatik (2015). https://doi.org/10.1007/s00236-016-0285-y

16. Castellani, I., Dezani-Ciancaglini, M., Giannini, P., Horne, R.: Global types with internal delegation. Theor. Comput. Sci. **807**, 128-153 (2020).
https://doi.org/10.1016/j.tcs.2019.09.027

17. Ciobanu, G., Horne, R.: Behavioural analysis of sessions using the calculus of structures. In: Proc. of PSI. Lect. Notes Comput. Sci., vol. 9609, pp. 91-106. Springer (2015). https://doi.org/10.1007/978-3-319-41579-628
18. Dardha, O.: Recursive session types revisited. In: Proc. of BEAT. Electron. Proc. in Theor. Comput. Sci., vol. 162, pp. 27–34 (2014). https://doi.org/10.4204/EPTCS.162.4

19. Dardha, O., Gay, S.J.: A new linear logic for deadlock-free session-typed processes. In: Proc. of FoSSaCS. Lect. Notes Comput. Sci., vol. 10803, pp. 91–109. Springer (2018). https://doi.org/10.1007/978-3-319-89366-2'5

20. Dardha, O., Gay, S.J.: A new linear logic for deadlock-free session typed processes. In: Proc. of FoSSaCS (2018), http://www.dcs.gla.ac.uk/~ornela/publications/DG18-Extended.pdf

21. Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. In: Proc. of PPDP. pp. 139–150. ACM (2012). https://doi.org/10.1145/2370776.2370794

22. Dardha, O., Pérez, J.A.: Comparing type systems for deadlock-freedom (2018), https://arxiv.org/abs/1810.00635

23. Deniélou, P., Yoshida, N.: Multiparty compatibility in communicating au- tomata: Characterisation and synthesis of global session types. In: Proc. of ICALP. Lect. Notes Comput. Sci., vol. 7966, pp. 174–186. Springer (2013). https://doi.org/10.1007/978-3-642-39212-2'18

24. Dezani-Ciancaglini, M., de'Liguoro, U., Yoshida, N.: On progress for structured communications. In: Proc. of TGC. Lect. Notes Comput. Sci., vol. 4912, pp. 257–275. Springer (2007). https://doi.org/10.1007/978-3-540-78663-4'18

25. Dezani-Ciancaglini, M., Mostrous, D., Yoshida, N., Drossopoulou, S.: Session types for object-oriented languages. In: Proc. of ECOOP. Lect. Notes Comput. Sci., vol. 4067, pp. 328–352. Springer (2006). https://doi.org/10.1007/1178547720

26. Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19–50 (2010). https://doi.org/10.1017/S0956796809990268

27. Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987). https://doi.org/10.1016/0304-3975(87)90045-4

28. Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Log. 8(1), 1 (2007). https://doi.org/10.1145/1182613.1182614

29. Honda, K.: Types for dyadic interaction. In: Proc. of CONCUR. Lect. Notes Com- put. Sci., vol. 715, pp. 509–523. Springer (1993). https://doi.org/10.1007/3-540- 57208-2'35

30. Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Proc. of ESOP. Lect. Notes Comput. Sci., vol. 1381, pp. 122–138. Springer (1998). https://doi.org/10.1007/BFb0053567

31. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous ses- sion types. In: Proc. of POPL. vol. 43(1), pp. 273–284. ACM (2008). https://doi.org/10.1145/2827695

32. Horne, R.: Session subtyping and multiparty compatibility using circular sequents. In: Proc. of CONCUR. LIPIcs, vol. 171, pp. 12:1–12:22. Leibniz-Zentrum für In- formatik (2020). https://doi.org/10.4230/LIPIcs.CONCUR.2020.12

33. Kobayashi, N.: A partially deadlock-free typed process calculus. ACM Trans. Pro- gram. Lang. Syst. 20(2), 436–482 (1998). https://doi.org/10.1145/276393.278524

34. Kobayashi, N.: A new type system for deadlock-free processes. In: Proc. of CONCUR. Lect. Notes Comput. Sci., vol. 4137, pp. 233–247. Springer (2006). https://doi.org/10.1007/1181794916

35. Kobayashi, N.: Type systems for concurrent programs (2007)

36. Kokke, W., Dardha, O.: Deadlock-free session types in Linear Haskell (2021), https://arxiv.org/abs/2103.14481
37. Kokke, W., Montesi, F., Peressotti, M.: Better late than never: A fully-abstract semantics for classical processes. Proc. ACM Program. Lang. 3(POPL) (2019). https://doi.org/10.1145/3290337

38. Kokke, W., Montesi, F., Peressotti, M.: Taking linear logic apart. In: Proc. of Linearity & TLLA. Electron. Proc. in Theor. Comput. Sci., vol. 292, pp. 90–103. Open Publishing Association (2019). https://doi.org/10.4204/EPTCS.292.5

39. Lindley, S., Morris, J.G.: A semantics for propositions as sessions. In: Proc. of ESOP. pp. 560–584 (2015). https://doi.org/10.1007/978-3-662-46669-8'23

40. Lindley, S., Morris, J.G.: Talking bananas: Structural recursion for session types. In: Proc. of ICFP. ACM (2016). https://doi.org/10.1145/2951913.2951921

41. Montesi, F., Peressotti, M.: Classical transitions (2018), https://arxiv.org/abs/1803.01049

42. Neubauer, M., Thiemann, P.: An implementation of session types. In: Jayaraman, B. (ed.) Proc. of PADL. Lect. Notes Comput. Sci., vol. 3057, pp. 56–70. Springer (2004). https://doi.org/10.1007/978-3-540-24836-1'5

43. Padovani, L.: From lock freedom to progress using session types. In: Proc. of PLACES. vol. 137, pp. 3–19. Electron. Proc. in Theor. Comput. Sci. (2013). https://doi.org/10.4204/EPTCS.137.2

44. Padovani, L.: Deadlock and lock freedom in the linear π-calculus. In: Proc. of CSL-LICS. pp. 72:1–72:10. ACM (2014). https://doi.org/10.1145/2603088.2603116

45. Padovani, L., Novara, L.: Types for deadlock-free higher-order programs. In: Proc. of FORTE. Lect. Notes Comput. Sci., vol. 9039, pp. 3–18. Springer (2015). https://doi.org/10.1007/978-3-319-19195-9'1

46. Scalas, A., Yoshida, N.: Less is more: Multiparty session types revisited. Proc. ACM Program. Lang. 3(POPL) (2019). https://doi.org/10.1145/3290343

47. Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: Proc. of PARLE. Lect. Notes Comput. Sci., vol. 817, pp. 398–413. Springer (1994). https://doi.org/10.1007/3-540-58184-7'118

48. Toninho, B., Caires, L., Pfenning, F.: Functions as session-typed processes. In: Proc. of FoSSaCS. Lect. Notes Comput. Sci., vol. 7213, pp. 346–360. Springer (2012). https://doi.org/10.1007/978-3-642-28729-9'23

49. Vasconcelos, V., Ravara, A., Gay, S.J.: Session types for functional multithreading. In: Proc. of CONCUR. Lect. Notes Comput. Sci., vol. 3170, pp. 497–511. Springer (2004). https://doi.org/10.1007/978-3-540-28644-8'32

50. Vasconcelos, V.T., Gay, S.J., Ravara, A.: Type checking a multithreaded functional language with session types. Theor. Comput. Sci. 368(1-2), 64–87 (2006). https://doi.org/10.1016/j.tcs.2006.06.028

51. Vieira, H.T., Vasconcelos, V.T.: Typing progress in communication-centred systems. In: Proc. of COORDINATION. Lect. Notes Comput. Sci., vol. 7890, pp. 236–250. Springer (2013). https://doi.org/10.1007/978-3-662-43376-8'10

52. Voinea, A.L., Dardha, O., Gay, S.J.: Resource sharing via capability-based multi-party session types. In: Proc. of IFM. Lect. Notes Comput. Sci., vol. 11918, pp. 437–455. Springer (2019). https://doi.org/10.1007/978-3-030-34968-4'24

53. Wadler, P.: Propositions as sessions. J. Funct. Program. 24(2-3), 384–418 (2014). https://doi.org/10.1017/S095679681400001X

54. Wadler, P.: Propositions as types. Commun. ACM 58(12), 75–84 (2015). https://doi.org/10.1145/2699407