# Deadlock Freedom for
Asynchronous and Cyclic Process Networks††thanks: Research partially supported
by the Dutch Research Council (NWO) under project No. 016.Vidi.189.046
(Unifying Correctness for Communicating Software).

Bas van den Heuvel and Jorge A. Pérez University of Groningen, The Netherlands

###### Abstract

This paper considers the challenging problem of establishing deadlock freedom
for message-passing processes using behavioral type systems. In particular, we
consider the case of processes that implement session types by communicating
asynchronously in cyclic process networks. We present APCP, a typed process
framework for deadlock freedom which supports asynchronous communication,
delegation, recursion, and a general form of process composition that enables
specifying cyclic process networks. We discuss the main decisions involved in
the design of APCP and illustrate its expressiveness and flexibility using
several examples.

##  1 Introduction

Modern software systems often comprise independent components that interact by
passing messages. The $\pi$-calculus is a consolidated formalism for
specifying and reasoning about message-passing processes [20, 21]. Type
systems for the $\pi$-calculus can statically enforce communication
correctness. In this context, _session types_ are a well-known approach,
describing two-party communication protocols for channel endpoints and
enforcing properties such as _protocol fidelity_ and _deadlock freedom_.

Session type research has gained a considerable impulse after the discovery by
Caires and Pfenning [8] and Wadler [29] of Curry-Howard correspondences
between session types and linear logic [13]. Processes typable in type systems
derived from these correspondences are inherently deadlock free. This is
because the Cut-rule of linear logic imposes that processes in parallel must
connect on exactly one pair of dual endpoints. However, whole classes of
deadlock free processes are not expressible with the restricted parallel
composition and endpoint connection resulting from Cut [10]. Such classes
comprise _cyclic process networks_ in which parallel components are connected
on multiple endpoints at once. Defining a type system for deadlock free,
cyclic processes is challenging, because such processes may contain _cyclic
dependencies_ , where components are stuck waiting for each other.

Advanced type systems that enforce deadlock freedom of cyclic process networks
are due to Kobayashi [18], who exploits _priority annotations_ on types to
avoid circular dependencies. Dardha and Gay bring these insights to the realm
of session type systems based on linear logic by defining Priority-based CP
(PCP) [9]. Indeed, PCP incorporates the type annotations of Padovani’s
simplification of Kobayashi’s type system [22] into Wadler’s Classical
Processes (CP) derived from classical linear logic [29].

In this paper, we study the effects of _asynchronous communication_ on type
systems for deadlock free cyclic process networks. To this end, we define
_Asynchronous PCP_ (APCP), which combines Dardha and Gay’s type annotations
with DeYoung et al.’s semantics for asynchronous communication [11], and adds
support for tail recursion. APCP uncovers fundamental properties of type
systems for asynchronous communication, and simplifies PCP’s type annotations
while preserving deadlock freedom results.

In Section 2, we motivate APCP by discussing Milner’s cyclic scheduler [20].
Section 3 defines APCP’s language and type system, and proves Type
Preservation (Theorem 2) and Deadlock Freedom (Theorem 6). In Section 4, we
showcase APCP by returning to Milner’s cyclic scheduler and using examples
inspired by Padovani [22] to illustrate asynchronous communication and
deadlock detection. Section 5 discusses related work and draws conclusions.

##  2 Motivating Example: Milner’s Cyclic Scheduler

We motivate by example the development of APCP, our type system for deadlock
freedom in asynchronous, cyclic message-passing processes. We consider
Milner’s cyclic scheduler [20], which crucially relies on asynchrony and
recursion. This example is inspired by Dardha and Gay [9], who use PCP to type
a synchronous, non-recursive version of the scheduler.

$A_{\\_}1$$A_{\\_}2$$A_{\\_}3$$A_{\\_}4$$A_{\\_}5$$A_{\\_}6$$P_{\\_}1$$P_{\\_}2$$P_{\\_}3$$P_{\\_}4$$P_{\\_}5$$P_{\\_}6$$A_{\\_}1$$A_{\\_}2$$A_{\\_}3$$A_{\\_}4$$A_{\\_}5$$A_{\\_}6$$P_{\\_}1$$P_{\\_}2$$P_{\\_}3$$P_{\\_}4$$P_{\\_}5$$P_{\\_}6$
Figure 1: Milner’s cyclic scheduler with 6 workers. Lines denote channels
connecting processes.

The system consists of $n\geq 1$ worker processes $P_{\\_}i$ (the workers, for
short), each attached to a partial scheduler $A_{\\_}i$. The partial
schedulers connect to each other in a ring structure, together forming the
cyclic scheduler. The scheduler then lets the workers perform their tasks in
rounds, each new round triggered by the leading partial scheduler $A_{\\_}1$
(the _leader_) once each worker finishes their previous task. We refer to the
non-leading partial schedulers $A_{\\_}{i+1}$ for $1\leq i<n$ as the
_followers_.

Each partial scheduler $A_{\\_}i$ has a channel endpoint $a_{\\_}i$ to connect
with the worker $P_{\\_}i$’s channel endpoint $b_{\\_}i$. The leader
$A_{\\_}1$ has an endpoint $c_{\\_}n$ to connect with $A_{\\_}n$ and an
endpoint $d_{\\_}1$ to connect with $A_{\\_}2$ (or with $A_{\\_}1$ if $n=1$;
we further elude this case for brevity). Each follower $A_{\\_}{i+1}$ has an
endpoint $c_{\\_}i$ to connect with $A_{\\_}i$ and an endpoint $d_{\\_}{i+1}$
to connect with $A_{\\_}{i+2}$ (or with $A_{\\_}1$ if $i+1=n$; we also elude
this case).

In each round of the scheduler, each follower $A_{\\_}{i+1}$ awaits a start
signal from $A_{\\_}i$, and then asynchronously signals $P_{\\_}{i+1}$ and
$A_{\\_}{i+2}$ to start. After awaiting acknowledgment from $P_{\\_}{i+1}$ and
a next round signal from $A_{\\_}i$, the follower then signals next round to
$A_{\\_}{i+2}$. The leader $A_{\\_}1$, responsible for starting each round of
tasks, signals $A_{\\_}2$ and $P_{\\_}1$ to start, and, after awaiting
acknowledgment from $P_{\\_}1$, signals next round to $A_{\\_}2$. Then, the
leader awaits $A_{\\_}n$’s start and next round signals.

It is crucial that $A_{\\_}1$ does not await $A_{\\_}n$’s start signal before
starting $P_{\\_}1$, as the leader would otherwise not be able to initiate
rounds of tasks. Asynchrony thus plays a central role here: because
$A_{\\_}n$’s start signal is non-blocking, it can start $P_{\\_}n$ before
$A_{\\_}1$ has received the start signal. Of course, $A_{\\_}1$ does not need
to await $A_{\\_}n$’s start and next round signals to make sure that every
partial scheduler is ready to start the next round.

Let us specify the partial schedulers formally:

$\displaystyle A_{\\_}1$ $\displaystyle:=\mu
X(a_{\\_}1,c_{\\_}n,d_{\\_}1);d_{\\_}1\mathbin{\triangleleft}\mathsf{start}\cdot
a_{\\_}1\mathbin{\triangleleft}\mathsf{start}\cdot
a_{\\_}1\mathbin{\triangleright}\mathsf{ack};d_{\\_}1\mathbin{\triangleleft}\mathsf{next}\cdot
c_{\\_}n\mathbin{\triangleright}\mathsf{start};c_{\\_}n\mathbin{\triangleright}\mathsf{next};X\langle
a_{\\_}1,c_{\\_}n,d_{\\_}1\rangle$ $\displaystyle A_{\\_}{i+1}$
$\displaystyle:=\mu
X(a_{\\_}{i+1},c_{\\_}i,d_{\\_}{i+1});\begin{array}[t]{l}c_{\\_}i\mathbin{\triangleright}\mathsf{start};a_{\\_}{i+1}\mathbin{\triangleleft}\mathsf{start}\cdot
d_{\\_}{i+1}\mathbin{\triangleleft}\mathsf{start}\cdot
a_{\\_}{i+1}\mathbin{\triangleright}\mathsf{ack};\\\
c_{\\_}i\mathbin{\triangleright}\mathsf{next};d_{\\_}{i+1}\mathbin{\triangleleft}\mathsf{next}\cdot
X\langle a_{\\_}{i+1},c_{\\_}i,d_{\\_}{i+1}\rangle\end{array}\qquad\forall
1\leq i<n$

The syntax ‘$\mu X(\tilde{x});P$’ denotes a recursive loop where $P$ has
access to the endpoints in $\tilde{x}$ and $P$ may contain recursive calls
‘$X\langle\tilde{y}\rangle$’ where the endpoints in $\tilde{y}$ are assigned
to $\tilde{x}$ in the next round of the loop. The syntax
‘$x\mathbin{\triangleleft}\ell$’ denotes the output of label $\ell$ on $x$,
and ‘$x\mathbin{\triangleright}\ell$’ denotes the input of label $\ell$ on
$x$. Outputs are non-blocking, denoted ‘$\cdot$’, whereas inputs are blocking,
denoted ‘;’. For example, process $x\mathbin{\triangleleft}\ell\cdot
y\mathbin{\triangleright}\ell^{\prime};P$ may receive $\ell^{\prime}$ on $y$
and continue as $x\mathbin{\triangleleft}\ell\cdot P$.

Leaving the workers unspecified, we formally specify the complete scheduler as
a ring of partial schedulers connected to workers:

$Sched_{\\_}n:=(\mkern-1.0mu\bm{\nu}c_{\\_}id_{\\_}i)_{\\_}{1\leq i\leq
n}(\mathchoice{\textstyle}{}{}{}{\prod}_{\\_}{1\leq i\leq
n}(\mkern-1.0mu\bm{\nu}a_{\\_}ib_{\\_}i)(A_{\\_}i\mathbin{|}P_{\\_}i))$

The syntax ‘$(\mkern-1.0mu\bm{\nu}xy)P$’ denotes the connection of endpoints
$x$ and $y$ in $P$, and ‘$\mathchoice{\textstyle}{}{}{}{\prod}_{\\_}{i\in
I}P_{\\_}i$’ and ‘$P\mathbin{|}Q$’ denote parallel composition. Figure 1
illustrates $Sched_{\\_}6$, the scheduler for six workers.

We return to this example in Section 4, where we type check the scheduler
using APCP to show that it is deadlock free.

##  3 APCP: Asynchronous Priority-based Classical Processes

In this section, we define APCP, a linear type system for $\pi$-calculus
processes that communicate asynchronously (i.e., the output of messages is
non-blocking) on connected channel endpoints. In APCP, processes may be
recursive and cyclically connected. Our type system assigns to endpoints types
that specify two-party protocols, in the style of binary session types [15].

APCP combines the salient features of Dardha and Gay’s Priority-based
Classical Processes (PCP) [9] with DeYoung et al.’s semantics for asynchronous
communication [11], both works inspired by Curry-Howard correspondences
between linear logic and session types [8, 29]. Recursion—not present in the
works by Dardha and Gay and DeYoung et al.—is an orthogonal feature, whose
syntax is inspired by the work of Toninho et al. [26].

As in PCP, types in APCP rely on _priority_ annotations, which enable cyclic
connections by ruling out circular dependencies between sessions. A key
insight of our work is that asynchrony induces significant improvements in
priority management: the non-blocking outputs of APCP do not need priority
checks, whereas PCP’s outputs are blocking and thus require priority checks.

Properties of well-typed APCP processes are _type preservation_ (Theorem 2)
and _deadlock freedom_ (Theorem 6). This includes cyclically connected
processes, which priority-annotated types guarantee free from circular
dependencies that may cause deadlock.

###  3.1 The Process Language

Process syntax: $\displaystyle P,Q::=$ $\displaystyle~{}x[y,z]$ output
$\displaystyle~{}~{}~{}\;\mbox{\large{$\mid$}}\;~{}~{}x(y,z);P$ input $\mid$
$\displaystyle~{}x[z]\triangleleft i$ selection
$\displaystyle~{}~{}~{}\;\mbox{\large{$\mid$}}\;~{}~{}x(z)\triangleright\\{i:P_{\\_}i\\}_{\\_}{i\in
I}$ branching
$\displaystyle~{}~{}~{}\;\mbox{\large{$\mid$}}\;~{}~{}(\mkern-1.0mu\bm{\nu}xy)P$
restriction $\mid$ $\displaystyle~{}(P\mathbin{|}Q)$ parallel
$\displaystyle~{}~{}~{}\;\mbox{\large{$\mid$}}\;~{}~{}\bm{0}$ inaction
$\displaystyle~{}~{}~{}\;\mbox{\large{$\mid$}}\;~{}~{}x\mathbin{\leftrightarrow}y$
forwarder $\mid$ $\displaystyle~{}\mu X(\tilde{x});P$ recursive loop
$\displaystyle~{}~{}~{}\;\mbox{\large{$\mid$}}\;~{}~{}X\langle\tilde{x}\rangle$
recursive call .  Structural congruence: $\displaystyle P\equiv_{\\_}\alpha
P^{\prime}\implies{}$ $\displaystyle P$ $\displaystyle\equiv P^{\prime}$
$\displaystyle x\mathbin{\leftrightarrow}y$ $\displaystyle\equiv
y\mathbin{\leftrightarrow}x$ $\displaystyle P\mathbin{|}Q$
$\displaystyle\equiv Q\mathbin{|}P$
$\displaystyle(\mkern-1.0mu\bm{\nu}xy)x\mathbin{\leftrightarrow}y$
$\displaystyle\equiv\bm{0}$ $\displaystyle P\mathbin{|}\bm{0}$
$\displaystyle\equiv P$ $\displaystyle P\mathbin{|}(Q\mathbin{|}R)$
$\displaystyle\equiv(P\mathbin{|}Q)\mathbin{|}R$ $\displaystyle
x,y\notin\mathrm{fn}(P)\implies{}$ $\displaystyle
P\mathbin{|}(\mkern-1.0mu\bm{\nu}xy)Q$
$\displaystyle\equiv(\mkern-1.0mu\bm{\nu}xy)(P\mathbin{|}Q)$
$\displaystyle(\mkern-1.0mu\bm{\nu}xy)\bm{0}$ $\displaystyle\equiv\bm{0}$
$\displaystyle|\tilde{x}|=|\tilde{y}|\implies{}$ $\displaystyle\mu
X(\tilde{x});P$ $\displaystyle\equiv P\\{\mu
X(\tilde{y});P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{\tilde{y}/\tilde{x}\\}}}/X\langle\tilde{y}\rangle\\}$
$\displaystyle(\mkern-1.0mu\bm{\nu}xy)P$
$\displaystyle\equiv(\mkern-1.0mu\bm{\nu}yx)P$
$\displaystyle(\mkern-1.0mu\bm{\nu}xy)(\mkern-1.0mu\bm{\nu}zw)P$
$\displaystyle\equiv(\mkern-1.0mu\bm{\nu}zw)(\mkern-1.0mu\bm{\nu}xy)P$ .
Reduction: $\displaystyle\beta_{\text{Id}}$ $\displaystyle z,y\neq
x\implies{}$
$\displaystyle(\mkern-1.0mu\bm{\nu}yz)(x\mathbin{\leftrightarrow}y\mathbin{|}P)$
$\displaystyle\mathbin{\longrightarrow}P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{x/z\\}}}$
$\displaystyle\beta_{\mathbin{\otimes}\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}}$
$\displaystyle(\mkern-1.0mu\bm{\nu}xy)(x[a,b]\mathbin{|}y(v,z);P)$
$\displaystyle\mathbin{\longrightarrow}P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{a/v,b/z\\}}}$
$\displaystyle\beta_{\oplus\&}$ $\displaystyle j\in I\implies{}$
$\displaystyle(\mkern-1.0mu\bm{\nu}xy)(x[b]\triangleleft
j\mathbin{|}y(z)\triangleright\\{i:P_{\\_}i\\}_{\\_}{i\in I})$
$\displaystyle\mathbin{\longrightarrow}P_{\\_}j{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{b/z\\}}}$
$\displaystyle\kappa_{\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}}$
$\displaystyle x\notin\tilde{v},\tilde{w}\implies{}$
$\displaystyle(\mkern-1.0mu\bm{\nu}\tilde{v}\tilde{w})(x(y,z);P\mathbin{|}Q)$
$\displaystyle\mathbin{\longrightarrow}x(y,z);(\mkern-1.0mu\bm{\nu}\tilde{v}\tilde{w})(P\mathbin{|}Q)$
$\displaystyle\kappa_{\&}$ $\displaystyle
x\notin\tilde{v},\tilde{w}\implies{}$
$\displaystyle(\mkern-1.0mu\bm{\nu}\tilde{v}\tilde{w})(x(z)\triangleright\\{i:P_{\\_}i\\}_{\\_}{i\in
I}\mathbin{|}Q)$
$\displaystyle\mathbin{\longrightarrow}x(z)\triangleright\\{i:(\mkern-1.0mu\bm{\nu}\tilde{v}\tilde{w})(P_{\\_}i\mathbin{|}Q)\\}_{\\_}{i\in
I}$ $(P\equiv
P^{\prime})\wedge(P^{\prime}\mathbin{\longrightarrow}Q^{\prime})\wedge(Q^{\prime}\equiv
Q)$ $\shortrightarrow_{\equiv}$ $P\mathbin{\longrightarrow}Q$
$\raisebox{9.0pt}{}P\mathbin{\longrightarrow}Q$ $\shortrightarrow_{\nu}$
$(\mkern-1.0mu\bm{\nu}xy)P\mathbin{\longrightarrow}(\mkern-1.0mu\bm{\nu}xy)Q$
$\raisebox{9.0pt}{}P\mathbin{\longrightarrow}Q$
$\shortrightarrow_{\mathbin{|}}$
$P\mathbin{|}R\mathbin{\longrightarrow}Q\mathbin{|}R$ Figure 2: Definition of
APCP’s process language.

We consider an asynchronous $\pi$-calculus [16, 5]. We write $x,y,z,\ldots$ to
denote (channel) _endpoints_ (also known as _names_), and write
$\tilde{x},\tilde{y},\tilde{z},\ldots$ to denote sequences of endpoints. Also,
we write $i,j,k,\ldots$ to denote _labels_ for choices and $I,J,K,\ldots$ to
denote sets of labels. We write $X,Y,\ldots$ to denote _recursion variables_ ,
and $P,Q,\ldots$ to denote processes.

Figure 2 (top) gives the syntax of processes. The output action ‘$x[y,z]$’
sends a message $y$ (an endpoint) and a continuation endpoint $z$ along $x$.
The input prefix ‘$x(y,z);P$’ blocks until a message and a continuation
endpoint are received on $x$ (referred to in $P$ as the placeholders $y$ and
$z$, respectively), binding $y$ and $z$ in $P$. The selection action
‘$x[z]\mathbin{\triangleleft}i$’ sends a label $i$ and a continuation endpoint
$z$ along $x$. The branching prefix
‘$x(z)\mathbin{\triangleright}\\{i:P_{\\_}i\\}_{\\_}{i\in I}$’ blocks until it
receives a label $i\in I$ and a continuation endpoint (reffered to in
$P_{\\_}i$ as the placeholder $z$) on $x$, binding $z$ in each $P_{\\_}i$.
Restriction ‘$(\mkern-1.0mu\bm{\nu}xy)P$’ binds $x$ and $y$ in $P$, thus
declaring them as the two endpoints of the same channel and enabling
communication, as in Vasconcelos [28]. The process ‘$(P\mathbin{|}Q)$’ denotes
the parallel composition of $P$ and $Q$. The process ‘$\bm{0}$’ denotes
inaction. The forwarder process ‘$x\mathbin{\leftrightarrow}y$’ is a primitive
copycat process that links together $x$ and $y$. The prefix ‘$\mu
X(\tilde{x});P$’ defines a recursive loop, binding occurrences of $X$ in $P$;
the endpoints $\tilde{x}$ form a context for $P$. The recursive call
‘$X\langle\tilde{x}\rangle$’ loops to its corresponding $\mu X$, providing the
endpoints $\tilde{x}$ as context. We only consider contractive recursion,
disallowing processes with subexpressions of the form ‘$\mu
X_{\\_}1(\tilde{x});\ldots;\mu
X_{\\_}n(\tilde{x});X_{\\_}1\langle\tilde{x}\rangle$’.

Endpoints and recursion variables are free unless otherwise stated (i.e.,
unless they are bound somehow). We write ‘$\mathrm{fn}(P)$’ and
‘$\mathrm{frv}(P)$’ for the sets of free names and free recursion variables of
$P$, respectively. Also, we write
‘$P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{x/y\\}}}$’ to denote the
capture-avoiding substitution of the free occurrences of $y$ in $P$ for $x$.
The notation ‘$P\\{\mu X(\tilde{y});P^{\prime}/X\langle\tilde{y}\rangle\\}$’
denotes the substitution of occurrences of recursive calls
‘$X\langle\tilde{y}\rangle$’ in $P$ with the recursive loop ‘$\mu
X(\tilde{y});P^{\prime}$’, which we call _unfolding_ recursion. We write
sequences of substitutions
‘$P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{x_{\\_}1/y_{\\_}1\\}}}\ldots{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{x_{\\_}n/y_{\\_}n\\}}}$’
as
‘$P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{x_{\\_}1/y_{\\_}1,\ldots,x_{\\_}n/y_{\\_}n\\}}}$’.

Except for asynchrony and recursion, there are minor differences with respect
to the languages of Dardha and Gay [9] and DeYoung et al. [11]. Unlike Dardha
and Gay’s, our syntax does not include empty input and output prefixes that
explicitly close channels; this simplifies the type system. We also do not
include the operator for replicated servers, denoted ‘${!}x(y);P$’, which is
present in the works by both Dardha and Gay and DeYoung et al.Although
replication can be handled without difficulties, we omit it here; we prefer
focusing on recursion, because it fits well with the examples we consider. We
discuss further these omitted constructs in Section 3.4.

#### Simplifying Notation

In an output ‘$x[y,z]$’, both $y$ and $z$ are free; they can be bound to a
continuation process using parallel composition and restriction, as in
$(\mkern-1.0mu\bm{\nu}ya)(\mkern-1.0mu\bm{\nu}zb)(x[y,z]\mathbin{|}P_{\\_}{a,b})$.
The same applies to selection ‘$x[z]\mathbin{\triangleleft}i$’. We introduce
useful notations that elide the restrictions and continuation endpoints:

######  Notation 1 (Derivable Actions and Prefixes).

We use the following syntactic sugar:

$\displaystyle\overline{x}[y]\cdot P$
$\displaystyle:=(\mkern-1.0mu\bm{\nu}ya)(\mkern-1.0mu\bm{\nu}zb)(x[a,b]\mathbin{|}P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{z/x\\}}})$
$\displaystyle\overline{x}\mathbin{\triangleleft}\ell\cdot P$
$\displaystyle:=(\mkern-1.0mu\bm{\nu}zb)(x[b]\mathbin{\triangleleft}\ell\mathbin{|}P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{z/x\\}}})$
$\displaystyle x(y);P$
$\displaystyle:=x(y,z);P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{z/x\\}}}$
$\displaystyle x\mathbin{\triangleright}\\{i:P_{\\_}i\\}_{\\_}{i\in I}$
$\displaystyle:=x(z)\mathbin{\triangleright}\\{i:P_{\\_}i{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{z/x\\}}}\\}_{\\_}{i\in
I}$

Note the use of ‘$\,\cdot\,$’ instead of ‘$\,;\,$’ in output and selection to
stress that they are non-blocking.

#### Operational Semantics

We define a reduction relation for processes ($P\mathbin{\longrightarrow}Q$)
that formalizes how complementary actions on connected endpoints may
synchronize. As usual for $\pi$-calculi, reduction relies on _structural
congruence_ ($P\equiv Q$), which equates the behavior of processes with minor
syntactic differences; it is the smallest congruence relation satisfying the
axioms in Figure 2 (middle).

Structural congruence defines the following properties of our process
language. Processes are equivalent up to $\alpha$-equivalence. Parallel
composition is associative and commutative, with unit ‘$\bm{0}$’. The
forwarder process is symmetric, and equivalent to inaction if both endpoints
are bound together through restriction. A parallel process may be moved into
or out of a restriction as long as the bound channels do not appear free in
the moved process: this is _scope inclusion_ and _scope extrusion_ ,
respectively. Restrictions on inactive processes may be dropped, and the order
of endpoints in restrictions and of consecutive restrictions does not matter.
Finally, a recursive loop is equivalent to its unfolding, replacing any
recursive calls with copies of the recursive loop, where the call’s endpoints
are pairwise substituted for the contextual endpoints of the loop (this is
_equi-recursion_ ; see, e.g., Pierce [23]).

We can now define our reduction relation. Besides synchronizations, reduction
includes _commuting conversions_ , which allow pulling prefixes on free
channels out of restrictions; they are not necessary for deadlock freedom, but
they are usually presented in Curry-Howard interpretations of linear logic [8,
29, 9, 11]. We define the reduction relation
‘$P\mathbin{\longrightarrow}Q\mkern 2.0mu$’ by the axioms and closure rules in
Figure 2 (bottom). Axioms labeled ‘$\beta$’ are _synchronizations_ and those
labeled ‘$\kappa$’ are commuting conversions. We write
‘$\mathbin{\longrightarrow}_{\\_}{\beta}$’ for reductions derived from
$\beta$-axioms, and ‘$\mathbin{\longrightarrow}^{\ast}$’ for the reflexive,
transitive closure of ‘$\mathbin{\longrightarrow}$’.

Rule $\beta_{\\_}{\text{Id}}$ implements the forwarder as a substitution. Rule
$\beta_{\\_}{\mathbin{\otimes}\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}}$
synchronizes an output and an input on connected endpoints and substitutes the
message and continuation endpoint. Rule $\beta_{\\_}{\oplus\&}$ synchronizes a
selection and a branch: the received label determines the continuation
process, substituting the continuation endpoint appropriately. Rule
$\kappa_{\\_}{\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}}$
(resp. $\kappa_{\\_}{\&}$) pulls an input (resp. a branching) prefix on free
channels out of enclosing restrictions. Rules $\rightarrow_{\\_}\equiv$,
$\rightarrow_{\\_}\nu$, and $\rightarrow_{\\_}{\mathbin{|}}$ close reduction
under structural congruence, restriction, and parallel composition,
respectively.

Notice how output and selection actions send free names. This is different
from the works by Dardha and Gay [9] and DeYoung et al. [11], where, following
an internal mobility discipline [4], communication involves bound names only.
As we show in the next subsection, this kind of _bound output_ is derivable
(cf. Theorem 1).

###  3.2 The Type System

APCP types processes by assigning binary session types to channel endpoints.
Following Curry-Howard interpretations, we present session types as linear
logic propositions (cf., e.g., Wadler [29], Caires and Pfenning [7], and
Dardha and Gay [9]). We extend these propositions with recursion and
_priority_ annotations on connectives. Intuitively, actions typed with lower
priority should be performed before those with higher priority. We write
$\mathsf{o},\kappa,\pi,\rho,\ldots$ to denote priorities, and ‘$\omega$’ to
denote the ultimate priority that is greater than all other priorities and
cannot be increased further. That is, $\forall t\in\mathbb{N}.~{}\omega>t$ and
$\forall t\in\mathbb{N}.~{}\omega+t=\omega$.

_Duality_ , the cornerstone of session types and linear logic, ensures that
the two endpoints of a channel have matching actions. Furthermore, dual types
must have matching priority annotations. The following inductive definition of
duality suffices for our tail-recursive types (cf. Gay et al. [12]).

######  Definition 1 (Session Types and Duality).

The following grammar defines the syntax of _session types_ $A,B$, followed by
the dual $\overline{A},\overline{B}$ of each type. Let
$\mathsf{o}\in\mathbb{N}\cup\\{\omega\\}$.

$\displaystyle A,B$
$\displaystyle::=A\mathbin{\otimes}^{\mathsf{o}}B\;\mbox{\large{$\mid$}}\;A\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\mathsf{o}}B\;\mbox{\large{$\mid$}}\;{\oplus}^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in
I}\;\mbox{\large{$\mid$}}\;\&^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in
I}\;\mbox{\large{$\mid$}}\;\bullet\;\mbox{\large{$\mid$}}\;\mu
X.A\;\mbox{\large{$\mid$}}\;X$ $\displaystyle\overline{A},\overline{B}$
$\displaystyle::=\overline{A}\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\mathsf{o}}\overline{B}\;\mbox{\large{$\mid$}}\;\overline{A}\mathbin{\otimes}^{\mathsf{o}}\overline{B}\;\mbox{\large{$\mid$}}\;\&^{\mathsf{o}}\\{i:\overline{A_{\\_}i}\\}_{\\_}{i\in
I}\;\mbox{\large{$\mid$}}\;{\oplus}^{\mathsf{o}}\\{i:\overline{A_{\\_}i}\\}_{\\_}{i\in
I}\;\mbox{\large{$\mid$}}\;\bullet\;\mbox{\large{$\mid$}}\;\mu
X.\overline{A}\;\mbox{\large{$\mid$}}\;X$

An endpoint of type ‘$A\mathbin{\otimes}^{\mathsf{o}}B$’ (resp.
‘$A\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\mathsf{o}}B$’)
first outputs (resp. inputs) an endpoint of type $A$ and then behaves as $B$.
An endpoint of type ‘$\&^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in I}$’ offers a
choice: after receiving a label $i\in I$, the endpoint behaves as $A_{\\_}i$.
An endpoint of type ‘$\oplus^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in I}$’
selects a label $i\in I$ and then behaves as $A_{\\_}i$. An endpoint of type
‘$\bullet$’ is closed; it does not require a priority, as closed endpoints do
not exhibit behavior and thus are non-blocking. We define ‘$\bullet$’ as a
single, self-dual type for closed endpoints, following Caires [6]: the units
‘$\bot$’ and ‘$\bm{1}$’ of linear logic (used by, e.g., Caires and Pfenning
[8] and Dardha and Gay [9] for session closing) are interchangeable in the
absence of explicit closing.

Type ‘$\mu X.A$’ denotes a recursive type, in which $A$ may contain
occurrences of the recursion variable ‘$X$’. As customary, ‘$\mu$’ is a
binder: it induces the standard notions of $\alpha$-equivalence, substitution
(denoted ‘$A{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{B/X\\}}}$’), and
free recursion variables (denoted ‘$\mathrm{frv}(A)$’). We work with tail-
recursive, contractive types, disallowing types of the form ‘$\mu
X_{\\_}1.\ldots.\mu X_{\\_}n.X_{\\_}1$’. We adopt an equi-recursive view: a
recursive type is equal to its unfolding. We postpone formalizing the
unfolding of recursive types, as it requires additional definitions to ensure
consistency of priorities upon unfolding.

The priority of a type is determined by the priority of the type’s outermost
connective:

######  Definition 2 (Priorities).

For session type $A$, ‘$\mathrm{pr}(A)$’ denotes its _priority_ :

$\displaystyle\mathrm{pr}(A\mathbin{\otimes}^{\mathsf{o}}B):=\mathrm{pr}(A\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\mathsf{o}}B)$
$\displaystyle:=\mathsf{o}$ $\displaystyle\mathrm{pr}(\mu X.A)$
$\displaystyle:=\mathrm{pr}(A)$
$\displaystyle\mathrm{pr}(\oplus^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in
I}):=\mathrm{pr}(\&^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in I})$
$\displaystyle:=\mathsf{o}$
$\displaystyle\mathrm{pr}(\bullet):=\mathrm{pr}(X)$ $\displaystyle:=\omega$

The priority of ‘$\bullet$’ and ‘$X$’ is $\omega$: they denote “final”, non-
blocking actions of protocols. Although ‘$\mathbin{\otimes}$’ and ‘$\oplus$’
also denote non-blocking actions, their priority is not constant: duality
ensures that the priority for ‘$\mathbin{\otimes}$’ (resp. ‘$\oplus$’) matches
the priority of a corresponding
‘$\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}$’
(resp. ‘$\&$’), which denotes a blocking action.

Having defined the priority of types, we now turn to formalizing the unfolding
of recursive types. Recall the intuition that actions typed with lower
priority should be performed before those with higher priority. Based on this
rationale, we observe that unfolding should increase the priorities of the
unfolded type. This is because the actions related to the unfolded recursion
should be performed _after_ the prefix. The following definition _lifts_
priorities in types:

######  Definition 3 (Lift).

For proposition $A$ and $t\in\mathbb{N}$, we define ‘${\uparrow\mkern
1.0mu}^{t}A\mkern-2.0mu$’ as the _lift_ operation:

$\displaystyle{\uparrow\mkern 1.0mu}^{t}(A\mathbin{\otimes}^{\mathsf{o}}B)$
$\displaystyle:=({\uparrow\mkern
1.0mu}^{t}A)\mathbin{\otimes}^{\mathsf{o}+t}({\uparrow\mkern 1.0mu}^{t}B)$
$\displaystyle{\uparrow\mkern
1.0mu}^{t}(\oplus^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in I})$
$\displaystyle:=\oplus^{\mathsf{o}+t}\\{i:{\uparrow\mkern
1.0mu}^{t}A_{\\_}i\\}_{\\_}{i\in I}$ $\displaystyle{\uparrow\mkern
1.0mu}^{t}\bullet$ $\displaystyle:=\bullet$ $\displaystyle{\uparrow\mkern
1.0mu}^{t}(A\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\mathsf{o}}B)$
$\displaystyle:=({\uparrow\mkern
1.0mu}^{t}A)\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\mathsf{o}+t}({\uparrow\mkern
1.0mu}^{t}B)$ $\displaystyle{\uparrow\mkern
1.0mu}^{t}(\&^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in I})$
$\displaystyle:=\&^{\mathsf{o}+t}\\{i:{\uparrow\mkern
1.0mu}^{t}A_{\\_}i\\}_{\\_}{i\in I}$ $\displaystyle{\uparrow\mkern
1.0mu}^{t}(\mu X.A)$ $\displaystyle:=\mu X.{\uparrow\mkern 1.0mu}^{t}(A)$
$\displaystyle{\uparrow\mkern 1.0mu}^{t}X$ $\displaystyle:=X$

Henceforth, the recursive type ‘$\mu X.A$’ and its unfolding
‘$A{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{{\uparrow\mkern
1.0mu}^{t}\mu X.A/X\\}}}$’ denote the same type, where the lift
$t\in\mathbb{N}$ of the unfolded recursive calls depends on the context in
which the type appears.

#### Typing Rules

The typing rules of APCP ensure that actions with lower priority are performed
before those with higher priority (cf. Dardha and Gay [9]). To this end, they
enforce the following laws:

  1. 1.

an action with priority $\mathsf{o}$ must be prefixed only by inputs and
branches with priority strictly smaller than $\mathsf{o}$—this law does not
hold for output and selection, as they are not prefixes;

  2. 2.

dual actions leading to synchronizations must have equal priorities (cf. Def.
1).

Judgments are of the form ‘$P\vdash\Omega;\Gamma$’, where $P$ is a process,
$\Gamma$ is a context that assigns types to channels (‘$x{:}A$’), and $\Omega$
is a context that assigns natural numbers to recursion variables (‘$X{:}n$’).
The intuition behind the latter context is that it ensures the amount of
context endpoints to concur between recursive definitions and calls. Both
contexts $\Gamma$ and $\Omega$ obey _exchange_ : assignments may be silently
reordered. $\Gamma$ is _linear_ , disallowing _weakening_ (i.e., all
assignments must be used) and _contraction_ (i.e., assignments may not be
duplicated). $\Omega$ allows weakening and contraction, because a recursive
definition does not necessarily require a recursive call although it may be
called more than once. The empty context is written ‘$\emptyset$’. We write
‘$\mathrm{pr}(\Gamma)$’ to denote the least priority of all types in $\Gamma$.
Notation ‘${(x_{\\_}i{:}A_{\\_}i)}_{\\_}{i\in I}$’ denotes indexing of
assignments by $I$. We write ‘${\uparrow\mkern 1.0mu}^{t}\Gamma$’ to denote
the component-wise extension of lift to typing contexts.

Empty $\bm{0}\vdash\Omega;\emptyset$ $P\vdash\Omega;\Gamma$ $\bullet$
$P\vdash\Omega;\Gamma,x{:}\bullet$ Id
$x\mathbin{\leftrightarrow}y\vdash\Omega;x{:}\overline{A},y{:}A$
$P\vdash\Omega;\Gamma$ $Q\vdash\Omega;\Delta$ Mix
$P\mathbin{|}Q\vdash\Omega;\Gamma,\Delta$
$P\vdash\Omega;\Gamma,x{:}A,y{:}\overline{A}$ Cycle
$(\mkern-1.0mu\bm{\nu}xy)P\vdash\Omega;\Gamma$ $\mathbin{\otimes}$
$x[y,z]\vdash\Omega;x{:}A\mathbin{\otimes}^{\mathsf{o}}B,y{:}\overline{A},z{:}\overline{B}$
$P\vdash\Omega;\Gamma,y{:}A,z{:}B$ $\mathsf{o}<\mathrm{pr}(\Gamma)$
$\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}$
$x(y,z);P\vdash\Omega;\Gamma,x{:}A\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\mathsf{o}}B$
$j\in I$ $\oplus$ $x[z]\triangleleft
j\vdash\Omega;x{:}{\oplus}^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in
I},z{:}\overline{A_{\\_}j}$ $\forall i\in
I.~{}P_{\\_}i\vdash\Omega;\Gamma,z{:}A_{\\_}i$
$\mathsf{o}<\mathrm{pr}(\Gamma)$ $\&$
$x(z)\triangleright\\{i:P_{\\_}i\\}_{\\_}{i\in
I}\vdash\Omega;\Gamma,x{:}\&^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in I}$
$P\vdash\Omega,X{:}|I|;{(x_{\\_}i{:}A_{\\_}i)}_{\\_}{i\in I}$ $\forall i\in
I.~{}A_{\\_}i\neq X$ Rec $\mu X({(x_{\\_}i)}_{\\_}{i\in
I});P\vdash\Omega;{(x_{\\_}i{:}\mu X.A_{\\_}i)}_{\\_}{i\in I}$ Var
$X\langle{(x_{\\_}i)}_{\\_}{i\in
I}\rangle\vdash\Omega,X{:}|I|;{(x_{\\_}i{:}X)}_{\\_}{i\in I}$ .
$P\vdash\Omega;\Gamma,y{:}A,x{:}B$ $\mathbin{\otimes}^{\star}$
$\overline{x}[y]\cdot
P\vdash\Omega;\Gamma,x{:}A\mathbin{\otimes}^{\mathsf{o}}B$
$P\vdash\Omega;\Gamma,x{:}A_{\\_}j$ $j\in I$ $\oplus^{\star}$
$\overline{x}\triangleleft j\cdot
P\vdash\Omega;\Gamma,x{:}{\oplus}^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in I}$
$P\vdash\Omega;\Gamma$ $t\in\mathbb{N}$ Lift $P\vdash\Omega;{\uparrow\mkern
1.0mu}^{t}\Gamma$ Figure 3: The typing rules of APCP (top) and admissible
rules (bottom).

Figure 3 (top) gives the typing rules. Typing is closed under structural
congruence; we sometimes use this explicitly in typing derivations in the form
of a rule ‘$\equiv$’. Axiom ‘Empty’ types an inactive process with no
endpoints. Rule ‘$\bullet$’ silently adds a closed endpoint to the typing
context. Axiom ‘Id’ types forwarding between endpoints of dual type. Rule
‘Mix’ types the parallel composition of two processes that do not share
assignments on the same endpoints. Rule ‘Cycle’ removes two endpoints of dual
type from the context by adding a restriction on them. Note that a single
application of ‘Mix’ followed by ‘Cycle’ coincides with the usual rule ‘Cut’
in type systems based on linear logic [8, 29]. Axiom ‘$\mathbin{\otimes}$’
types an output action; this rule does not have premises to provide a
continuation process, leaving the free endpoints to be bound to a continuation
process using ‘Mix’ and ‘Cycle’. Similarly, axiom ‘$\oplus$’ types an
unbounded selection action. Priority checks are confined to rules
‘$\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}$’
and ‘$\&$’, which type an input and a branching prefix, respectively. In both
cases, the used endpoint’s priority must be lower than the priorities of the
other types in the continuation’s typing context.

Rule ‘Rec’ types a recursive definition by eliminating a recursion variable
from the recursion context whose value concurs with the size of the typing
context, where contractiveness is guaranteed by requiring that the eliminated
recursion variable may not appear unguarded in each of the context’s types.
Axiom ‘Var’ types a recursive call by adding a recursion variable to the
context with the amount of introduced endpoints. As mentioned before, the
value of the introduced and consequently eliminated recursion variable is
crucial in ensuring that a recursion is called with the same amount of
channels as required by its definition.

Let us compare our typing system to that of Dardha and Gay [9] and DeYoung et
al. [11]. Besides our support for recursion, the main difference is that our
rules for output and selection are axioms. This makes priority checking much
simpler for APCP than for Dardha and Gay’s PCP: our outputs and selections
have no typing context to check priorities against, and types for closed
endpoints have no priority at all. Although DeYoung et al.’s output and
selection actions are atomic too, their corresponding rules are similar to the
rules of Dardha and Gay: the rules require continuation processes as premises,
immediately binding the sent endpoints.

As anticipated, the binding of output and selection actions to continuation
processes (1) is derivable in APCP. The corresponding typing rules in Figure 3
(bottom) are admissible using ‘Mix’ and ‘Cycle’. Note that it is not necessary
to include rules for the sugared input and branching in 1, because they rely
on name substitution only and typing is closed under structural congruence and
thus name substitution. Figure 3 (bottom) also includes an admissible rule
‘Lift’ that lifts a process’ priorities.

######  Theorem 1.

The rules ‘$\mathbin{\otimes}^{\star}$’, ‘$\oplus^{\star}$’, and ‘Lift’ in
Figure 3 (bottom) are admissible.

$P\vdash\Gamma,y{:}A,x{:}B$ $\mathbin{\otimes}^{\star}$ $\overline{x}[y]\cdot
P\vdash\Gamma,x{:}A\mathbin{\otimes}^{\mathsf{o}}B$ $\Rightarrow$
$\mathbin{\otimes}$ $x[a,b]\vdash
x{:}A\mathbin{\otimes}^{\mathsf{o}}B,a{:}\overline{A},b{:}\overline{B}$
$P\vdash\Gamma,y{:}A,x{:}B$ $\equiv$
$P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{z/x\\}}}\vdash\Gamma,y{:}A,z{:}B$
Mix
$x[a,b]\mathbin{|}P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{z/x\\}}}\vdash\Gamma,x{:}A\mathbin{\otimes}^{\mathsf{o}}B,y{:}A,a{:}\overline{A},z{:}B,b{:}\overline{B}$
Cycle2
$\underbrace{(\mkern-1.0mu\bm{\nu}ya)(\mkern-1.0mu\bm{\nu}zb)(x[a,b]\mathbin{|}P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{z/x\\}}})}_{\\_}{\overline{x}[y]\cdot
P~{}\text{(cf.\
\lx@cref{creftypecap~refnum}{n:sugar})}}\vdash\Gamma,x{:}A\mathbin{\otimes}^{\mathsf{o}}B$
$P\vdash\Gamma,x{:}A_{\\_}j$ $j\in I$ $\oplus^{\star}$
$\overline{x}\triangleleft j\cdot
P\vdash\Gamma,x{:}{\oplus}^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in I}$
$\Rightarrow$ $j\in I$ $\oplus$ $x[b]\triangleleft j\vdash
x{:}{\oplus}^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in
I},b{:}\overline{A_{\\_}j}$ $P\vdash\Gamma,x{:}A_{\\_}j$ $\equiv$
$P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{z/x\\}}}\vdash\Gamma,z{:}A_{\\_}j$
Mix $x[b]\triangleleft
j\mathbin{|}P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{z/x\\}}}\vdash\Gamma,x{:}{\oplus}^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in
I},z{:}A_{\\_}j,b{:}\overline{A_{\\_}j}$ Cycle
$\underbrace{(\mkern-1.0mu\bm{\nu}zb)(x[b]\triangleleft
j\mathbin{|}P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{z/x\\}}})}_{\\_}{\overline{x}\triangleleft
j\cdot P~{}\text{(cf.\
\lx@cref{creftypecap~refnum}{n:sugar})}}\vdash\Gamma,x{:}{\oplus}^{\mathsf{o}}\\{i:A_{\\_}i\\}_{\\_}{i\in
I}$ Figure 4: Proof that rules ‘$\mathbin{\otimes}^{\star}$’ and
‘$\oplus^{\star}$’ are admissible (cf. Theorem 1).

###### Proof.

We show the admissibility of rules $\mathbin{\otimes}^{\star}$ and
$\oplus^{\star}$ by giving their derivations in Figure 4 (omitting the
recursion context). The rule ‘Lift’ is admissible, because
$P\vdash\Omega;\Gamma$ implies $P\vdash\Omega;{\uparrow\mkern
1.0mu}^{t}\Gamma$ (cf. Dardha and Gay [9]), by simply increasing all
priorities in the derivation of $P$ by $t$. ∎

Theorem 1 highlights how APCP’s asynchrony uncovers a more primitive, lower-
level view of message-passing. In the next subsection we discuss deadlock
freedom, which follows from a correspondence between reduction and the removal
of ‘Cycle’ rules from typing derivations. In the case of APCP, this requires
care: binding output and selection actions to continuation processes leads to
applications of ‘Cycle’ not immediately corresponding to reductions.

###  3.3 Type Preservation and Deadlock Freedom

Well-typed processes satisfy protocol fidelity, communication safety, and
deadlock freedom. All these properties follow from _type preservation_ (also
known as _subject reduction_), which ensures that reduction preserves typing.
In contrast to Caires and Pfenning [8] and Wadler [29], where type
preservation corresponds to the elimination of (top-level) applications of
rule Cut, in APCP it corresponds to the elimination of (top-level)
applications of rule Cycle.

######  Theorem 2 (Type Preservation).

If $P\vdash\Omega;\Gamma$ and $P\mathbin{\longrightarrow}Q$, then
$Q\vdash\Omega;{\uparrow\mkern 1.0mu}^{t}\Gamma$ for $t\in\mathbb{N}$.

$\mathbin{\otimes}$ $x[a,b]\vdash
x{:}A\mathbin{\otimes}^{\mathsf{o}}B,a{:}\overline{A},b{:}\overline{B}$
$P\vdash\Gamma,v{:}\overline{A},z{:}\overline{B}$
$\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}$
$y(v,z).P\vdash\Gamma,y{:}\overline{A}\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\mathsf{o}}\overline{B}$
$\mkern-10.0mu\begin{array}[]{c}\\\ \text{Mix}\,+\\\ \text{Cycle}\end{array}$
$(\mkern-1.0mu\bm{\nu}xy)(x[a,b]\mathbin{|}y(v,z).P)\vdash\Gamma,a{:}\overline{A},b{:}\overline{B}$
$\mathbin{\longrightarrow}$ $P\vdash\Gamma,v{:}\overline{A},z{:}\overline{B}$
$\equiv$
$P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{a/v,b/z\\}}}\vdash\Gamma,a{:}\overline{A},b{:}\overline{B}$
.  Below, the contexts $\Gamma^{\prime}$ and $\Delta^{\prime}$ together
contain $\tilde{v}$ and $\tilde{w}$, i.e.
$\Gamma^{\prime},\Delta^{\prime}={(v_{\\_}i{:}C_{\\_}i)}_{\\_}{v_{\\_}i\in\tilde{v}},{(w_{\\_}i{:}\overline{C_{\\_}i})}_{\\_}{w_{\\_}i\in\tilde{w}}$.
$P\vdash\Gamma,\Gamma^{\prime},y{:}A,z{:}B$ $\mathsf{o}<\mathrm{pr}(\Gamma)$
$\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}$
$x(y,z).P\vdash\Gamma,\Gamma^{\prime},x{:}A\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\mathsf{o}}B$
$Q\vdash\Delta,\Delta^{\prime}$ $\text{Mix}+\text{Cycle}^{\ast}$
$(\mkern-1.0mu\bm{\nu}\tilde{v}\tilde{w})(x(y,z).P\mathbin{|}Q)\vdash\Gamma,\Delta,x{:}A\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\mathsf{o}}B$
$\mathbin{\longrightarrow}$ $P\vdash\Gamma,\Gamma^{\prime},y{:}A,z{:}B$
$Q\vdash\Delta,\Delta^{\prime}$ $\text{Mix}+\text{Cycle}^{\ast}$
$(\mkern-1.0mu\bm{\nu}\tilde{v}\tilde{w})(P\mathbin{|}Q)\vdash\Gamma,\Delta,y{:}A,z{:}B$
Lift
$(\mkern-1.0mu\bm{\nu}\tilde{v}\tilde{w})(P\mathbin{|}Q)\vdash{\uparrow\mkern
1.0mu}^{\mathsf{o}+1}\Gamma,{\uparrow\mkern
1.0mu}^{\mathsf{o}+1}\Delta,y{:}{\uparrow\mkern
1.0mu}^{\mathsf{o}+1}A,z{:}{\uparrow\mkern 1.0mu}^{\mathsf{o}+1}B$
$\mathsf{o}<\mathrm{pr}({\uparrow\mkern
1.0mu}^{\mathsf{o}+1}\Gamma,{\uparrow\mkern 1.0mu}^{\mathsf{o}+1}\Delta)$
$\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}$
$x(y,z).(\mkern-1.0mu\bm{\nu}\tilde{v}\tilde{w})(P\mathbin{|}Q)\vdash{\uparrow\mkern
1.0mu}^{\mathsf{o}+1}\Gamma,{\uparrow\mkern
1.0mu}^{\mathsf{o}+1}\Delta,x{:}({\uparrow\mkern
1.0mu}^{\mathsf{o}+1}A)\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\mathsf{o}}({\uparrow\mkern
1.0mu}^{\mathsf{o}+1}B)$ Figure 5: Type Preservation (cf. Theorem 2) in rules
$\beta_{\mathbin{\otimes}\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}}$
(top) and
$\kappa_{\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}}$
(bottom).

###### Proof.

By induction on the reduction $\mathbin{\longrightarrow}$, analyzing the last
applied rule (Fig. 2 (bottom)). The cases of the closure rules
$\shortrightarrow_{\equiv}$, $\shortrightarrow_{\nu}$, and
$\shortrightarrow_{\mathbin{|}}$ easily follow from the IH. The key cases are
the $\beta$\- and $\kappa$-rules. Figure 5 shows two representative instances
(eluding the recursion context $\Omega$): rule
$\beta_{\mathbin{\otimes}\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}}$
(top), a synchronization, and rule
$\kappa_{\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}}$
(bottom), a commuting conversion. Note how, in the case of rule
$\kappa_{\\_}{\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}}$,
the lift ${\uparrow\mkern 1.0mu}^{t}$ ensures consistent priority checks. ∎

Protocol fidelity ensures that processes respect their intended (session)
protocols. Communication safety ensures the absence of communication errors
and mismatches in processes. Correct typability gives a static guarantee that
a process conforms to its ascribed session protocols; type preservation gives
a dynamic guarantee. Because session types describe the intended protocols and
error-free exchanges, type preservation entails both protocol fidelity and
communication safety. We refer the curious reader to the early work by Honda
et al. [17] for a detailed account, which shows by contradiction that well-
typed processes do not reduce to so-called error processes. This is a well-
known and well-understood result.

In what follows, we consider a process to be deadlocked if it is not the
inactive process and cannot reduce. Our deadlock freedom result for APCP
adapts that for PCP [9], which involves three steps:

  1. 1.

First, Cycle-elimination states that we can remove all applications of Cycle
in a typing derivation without affecting the derivation’s assumptions and
conclusion.

  2. 2.

Only the removal of _top-level_ Cycles captures the intended process
semantics, as the removal of other Cycles corresponds to reductions behind
prefixes which is not allowed [29, 9]. Therefore, the second step is _top-
level deadlock freedom_ , which states that a process with a top-level Cycle
reduces until there are no top-level Cycles left.

  3. 3.

Third, deadlock freedom follows for processes typable under empty contexts.

Here, we address cycle-elimination and top-level deadlock-freedom in one
proof.

As mentioned before, binding APCP’s asynchronous outputs and selections to
continuations involves additional, low-level uses of Cycle, which we cannot
eliminate through process reduction. Therefore, we establish top-level
deadlock freedom for _live processes_ (Theorem 4). A process is live if it is
equivalent to a restriction on _active names_ that perform unguarded actions.
This way, e.g., in ‘$x[y,z]$’ the name $x$ is active, but $y$ and $z$ are not.

######  Definition 4 (Active Names).

The _set of active names_ of $P$, denoted ‘$\mathrm{an}(P)\mkern-2.0mu$’,
contains the (free) names that are used for unguarded actions (output, input,
selection, branching):

$\displaystyle\mathrm{an}(x[y,z])$ $\displaystyle:=\\{x\\}$
$\displaystyle\mathrm{an}(x(y,z).P)$ $\displaystyle:=\\{x\\}$
$\displaystyle\mathrm{an}(\bm{0})$ $\displaystyle:=\emptyset$
$\displaystyle\mathrm{an}(x[z]\triangleleft j)$ $\displaystyle:=\\{x\\}$
$\displaystyle\mathrm{an}(x(z)\triangleright\\{i:P_{\\_}i\\}_{\\_}{i\in I})$
$\displaystyle:=\\{x\\}$
$\displaystyle\mathrm{an}(x\mathbin{\leftrightarrow}y)$
$\displaystyle:=\\{x,y\\}$ $\displaystyle\mathrm{an}(P\mathbin{|}Q)$
$\displaystyle:=\mathrm{an}(P)\cup\mathrm{an}(Q)$
$\displaystyle\mathrm{an}(\mu X(\tilde{x});P)$ $\displaystyle:=\mathrm{an}(P)$
$\displaystyle\mathrm{an}((\mkern-1.0mu\bm{\nu}xy)P)$
$\displaystyle:=\mathrm{an}(P)\setminus\\{x,y\\}$
$\displaystyle\mathrm{an}(X\langle\tilde{x}\rangle)$
$\displaystyle:=\emptyset$

######  Definition 5 (Live Process).

A process $P$ is _live_ , denoted ‘$\mkern
1.0mu\mathrm{live}(P)\mkern-2.0mu$’, if there are names $x,y$ and process
$P^{\prime}$ such that $P\equiv(\mkern-1.0mu\bm{\nu}xy)P^{\prime}$ with
$x,y\in\mathrm{an}(P^{\prime})$.

We additionally need to account for recursion: as recursive definitions do not
entail reductions, we must fully unfold them before eliminating Cycles.

######  Lemma 3 (Unfolding).

If $P\vdash\Omega;\Gamma$, then there is process $P^{\star}$ such that
$P^{\star}\equiv P$ and $P^{\star}$ is not of the form ‘$\mu X(\tilde{x});Q$’
and $P^{\star}\vdash\Omega;\Gamma$.

Var $X\langle{(y_{\\_}i)}_{\\_}{i\in
I}\rangle\vdash\Omega^{\prime},X{:}|I|;{(y_{\\_}i{:}X)}_{\\_}{i\in I}$
$\vdots$ $\textstyle{\ddots}$ …
$Q\vdash\Omega,X{:}|I|;{(x_{\\_}i{:}A_{\\_}i)}_{\\_}{i\in I}$ Rec $\mu
X({(x_{\\_}i)}_{\\_}{i\in I});Q\vdash\Omega;{(x_{\\_}i{:}\mu
X.A_{\\_}i)}_{\\_}{i\in I}$ .  Var $X\langle{(y_{\\_}i)}_{\\_}{i\in
I}\rangle\vdash\Omega^{\prime\prime},X{:}|I|;{(y_{\\_}i{:}X)}_{\\_}{i\in I}$
$\vdots$ $\textstyle{\ddots}$ …
$Q\vdash\Omega^{\prime},X{:}|I|;{(x_{\\_}i{:}A_{\\_}i)}_{\\_}{i\in I}$
$\equiv$
$Q{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{{(y_{\\_}i)}_{\\_}{i\in
I}/{(x_{\\_}i)}_{\\_}{i\in
I}\\}}}\vdash\Omega^{\prime},X{:}|I|;{(y_{\\_}i{:}A_{\\_}i)}_{\\_}{i\in I}$
Rec $\mu X({(y_{\\_}i)}_{\\_}{i\in
I});Q{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{{(y_{\\_}i)}_{\\_}{i\in
I}/{(x_{\\_}i)}_{\\_}{i\in I}\\}}}\vdash\Omega^{\prime};{(y_{\\_}i{:}\mu
X.A_{\\_}i)}_{\\_}{i\in I}$
$t\geq\max_{\\_}{\mathsf{pr}}{(A_{\\_}i)}_{\\_}{i\in I}$ Lift $\mu
X({(y_{\\_}i)}_{\\_}{i\in
I});Q{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{{(y_{\\_}i)}_{\\_}{i\in
I}/{(x_{\\_}i)}_{\\_}{i\in
I}\\}}}\vdash\Omega^{\prime};{(y_{\\_}i{:}{\uparrow\mkern 1.0mu}^{t}\mu
X.A_{\\_}i)}_{\\_}{i\in I}$ $\vdots$ $\textstyle{\ddots}$ …
$R\vdash\Omega;{(x_{\\_}i{:}A_{\\_}i{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{{\uparrow\mkern
1.0mu}^{t}\mu X.A_{\\_}i/X\\}}})}_{\\_}{i\in I}$ Figure 6: Typing recursion
before (top) and after (bottom) unfolding (cf. Lemma 3).

###### Proof.

By induction on the amount $n$ of consecutive recursive definitions prefixing
$P$, such that $P$ is of the form ‘$\mkern-1.0mu\mu
X_{\\_}1(\tilde{x});\ldots;\mu X_{\\_}n(\tilde{x});Q$’. If $n=0$, the thesis
follows immediately by letting $P^{\star}:=P$.

Otherwise, $n\geq 1$. Then there are $X,Q$ such that $P=\mu
X({(x_{\\_}i)}_{\\_}{i\in I});Q$. By inversion of typing rule Rec,
$P\vdash\Omega;{(x_{\\_}i{:}\mu X.A_{\\_}i)}_{\\_}{i\in I}$. Generally
speaking, such typing derivations have the shape as in Figure 6 (top), with
zero or more Var-axioms on $X$ appearing at the top. We use structural
congruence (Fig. 2 (middle)) to unfold the recursion in $P$, obtaining the
process $R:=Q\\{\mu X({(y_{\\_}i)}_{\\_}{i\in
I});Q{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{{(y_{\\_}i)}_{\\_}{i\in
I}/{(x_{\\_}i)}_{\\_}{i\in I}\\}}}/X\langle{(y_{\\_}i)}_{\\_}{i\in
I}\rangle\\}\equiv P$.

We can type $R$ by taking the derivation of $P$ (cf. Figure 6 (top)), removing
the final application of the Rec-rule and replacing any uses of the Var-axiom
on $X$ by a copy of the original derivation, applying $\alpha$-conversion
where necessary. Moreover, we lift the priorities of all types by at least the
highest priority occurring in any type in $\Gamma$ using the Lift-rule,
ensuring that priority conditions on typing rules remain valid; we explicitly
use _at least_ the highest priority, as the context of connected endpoints may
lift the priorities in dual types even more. Writing the highest priority in
$\Gamma$ as ‘$\max_{\\_}{\mathsf{pr}}(\Gamma)$’, the resulting proof is of the
shape in Figure 6 (bottom). Since types are equi-recursive,
$A_{\\_}i{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{{\uparrow\mkern
1.0mu}^{t}\mu X.A_{\\_}i/X\\}}}=A_{\\_}i$ for every $i\in I$. Hence,
${(y_{\\_}i{:}A_{\\_}i{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{{\uparrow\mkern
1.0mu}^{t}\mu X.A_{\\_}i/X\\}}})}_{\\_}{i\in I}=\Gamma$. Thus, the above is a
valid derivation of $R\vdash\Omega;\Gamma$.

The rules applied after Lift in the derivation of $R$ in Figure 6 (bottom) are
the same as those applied after Var and before Rec in the derivation of $P$ in
Figure 6 (top) before unfolding. By the assumption that recursion is
contractive, there must be an application of a rule other than Rec in this
part of the derivation. Therefore, the application of Rec in the derivation of
$R$ is not part of a possible sequence of Recs in the last-applied rules of
this derivation. Hence, since we removed the final application of Rec in the
derivation of $P$, the size of this sequence of Recs is $n-1$, i.e. $R$ is
prefixed by $n-1$ recursive definitions. Thus, we apply the IH to find a
process $P^{\star}$ not prefixed by recursive definitions s.t.
$P^{\star}\equiv R\equiv P\vdash\Omega;\Gamma$. ∎

Dardha and Gay’s top-level deadlock freedom result concerns a sequence of
reduction steps that reaches a process that is not live anymore [9]. In our
case, top-level deadlock freedom concerns a single reduction step only,
because recursive processes might stay live across reductions forever.

######  Theorem 4 (Top-Level Deadlock Freedom).

If $P\vdash\emptyset;\Gamma$ and $\mathrm{live}(P)$, then there is process $Q$
such that $P\mathbin{\longrightarrow}Q$.

###### Proof.

By structural congruence (Fig. 2 (middle)), there is
$P_{\\_}c=(\mkern-1.0mu\bm{\nu}x_{\\_}iy_{\\_}i)_{\\_}{i\in
I}(\mkern-1.0mu\bm{\nu}\tilde{n}\tilde{m})P_{\\_}m$ such that $P_{\\_}c\equiv
P$, with $P_{\\_}m=\mathchoice{\textstyle}{}{}{}{\prod}_{\\_}{k\in K}P_{\\_}k$
and
$P_{\\_}m\vdash\emptyset;\Lambda,{(x_{\\_}i{:}A_{\\_}i,y_{\\_}i{:}\overline{A_{\\_}i})}_{\\_}{i\in
I}$ s.t. for every $i\in I$, $x_{\\_}i$ and $y_{\\_}i$ are active names in
$P_{\\_}m$, and $\Lambda$ consists of $\Gamma$ and the channels
$\tilde{n},\tilde{m}$ which are dually typed pairs of endpoints of which at
least one is inactive in $P_{\\_}m$. Because $P$ is live, there is always at
least one pair $x_{\\_}i,y_{\\_}i$.

Next, we take the $j\in I$ s.t. $A_{\\_}j$ has the least priority, i.e.
$\forall i\in
I\setminus\\{j\\}.~{}\mathrm{pr}(A_{\\_}j)\leq\mathrm{pr}(A_{\\_}i)$. If there
are multiple to choose from, any suffices. The rest of the analysis depends on
whether there is an endpoint $z$ of input/branching type in $\Gamma$ with
lower priority than $\mathrm{pr}(A_{\\_}j)$. We thus distinguish the two cases
below. Note that output/selection types in $\Gamma$ are associated with non-
blocking actions and can be safely ignored.

  * •

If there is such $z$, assume w.l.o.g. it is of input type. The input on $z$
cannot be prefixed by an input/branch on another endpoint, because then that
other endpoint would have a type with lower priority than $z$. Hence, there is
$k^{\prime}\in K$ s.t.
$P_{\\_}{k^{\prime}}=z(u,v);P^{\prime}_{\\_}{k^{\prime}}$. We thus apply
communicating conversion
$\kappa_{\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}}$
to find $Q$ such that $P\mathbin{\longrightarrow}Q$:

$P\equiv(\mkern-1.0mu\bm{\nu}x_{\\_}iy_{\\_}i)_{\\_}{i\in
I}(\mkern-1.0mu\bm{\nu}\tilde{n}\tilde{m})(\mathchoice{\textstyle}{}{}{}{\prod}_{\\_}{k\in
K\setminus\\{k^{\prime}\\}}P_{\\_}k\mathbin{|}z(u,v);P^{\prime}_{\\_}{k^{\prime}})\mathbin{\longrightarrow}z(u,v);(\mkern-1.0mu\bm{\nu}x_{\\_}iy_{\\_}i)_{\\_}{i\in
I}(\mkern-1.0mu\bm{\nu}\tilde{n}\tilde{m})(\mathchoice{\textstyle}{}{}{}{\prod}_{\\_}{k\in
K\setminus\\{k^{\prime}\\}}P_{\\_}k\mathbin{|}P^{\prime}_{\\_}{k^{\prime}})=Q$

  * •

If there is no such $z$, we continue with $x_{\\_}j{:}A_{\\_}j$ and
$y_{\\_}j{:}\overline{A_{\\_}j}$. In case there is $k^{\prime}\in K$ s.t.
$P_{\\_}k\equiv u\mathbin{\leftrightarrow}v$ with
$u\in\\{x_{\\_}j,y_{\\_}j\\}$, the reduction is trivial by
$\shortrightarrow_{\text{Id}}$; we w.l.o.g. assume there is no such
$k^{\prime}$.

By duality, $A_{\\_}j$ and $\overline{A_{\\_}j}$ have the same priority, so
priority checks in typing derivations prevent an input/branching prefix on
$x_{\\_}j$ (resp. $y_{\\_}j$) from blocking an output/selection on $y_{\\_}j$
(resp. $x_{\\_}j$). Hence, $x_{\\_}j$ and $y_{\\_}j$ appear in separate
parallel components of $P_{\\_}m$, i.e.
$P_{\\_}m=P_{\\_}{x_{\\_}j}\mathbin{|}P_{\\_}{y_{\\_}j}\mathbin{|}P_{\\_}R$
s.t.

$P_{\\_}{x_{\\_}j}\vdash\emptyset;\Lambda_{\\_}{x_{\\_}j},x_{\\_}j{:}A_{\\_}j~{},\quad
P_{\\_}{y_{\\_}j}\vdash\emptyset;\Lambda_{\\_}{y_{\\_}j},y_{\\_}j{:}\overline{A_{\\_}j}~{}\text{,
and}\quad P_{\\_}R\vdash\emptyset;\Lambda_{\\_}R~{},$

where
$\Lambda_{\\_}{x_{\\_}j},\Lambda_{\\_}{y_{\\_}j},\Lambda_{\\_}R,x_{\\_}j{:}A_{\\_}j,y_{\\_}j{:}\overline{A_{\\_}j}=\Lambda,{(x_{\\_}i{:}A_{\\_}i,y_{\\_}i{:}\overline{A_{\\_}i})}_{\\_}{i\in
I}$.

By Lemma 3 (unfolding), $P_{\\_}{x_{\\_}j}\equiv P_{\\_}{x_{\\_}j}^{\star}$
and $P_{\\_}{y_{\\_}j}\equiv P_{\\_}{y_{\\_}j}^{\star}$ s.t.
$P_{\\_}{x_{\\_}j}^{\star}$ and $P_{\\_}{y_{\\_}j}^{\star}$ are not prefixed
by recursive definitions and
$P_{\\_}{x_{\\_}j}^{\star}\vdash\emptyset;\Lambda_{\\_}{x_{\\_}j},x_{\\_}j{:}A_{\\_}j$
and
$P_{\\_}{y_{\\_}j}^{\star}\vdash\emptyset;\Lambda_{\\_}{y_{\\_}j},y_{\\_}j{:}\overline{A_{\\_}j}$.
We take the unfolded form of $A_{\\_}j$: by the contractiveness of recursive
types, $A_{\\_}j$ has at least one connective. We w.l.o.g. assume that
$A_{\\_}j$ is an input or branching type, i.e. either (a)
$A_{\\_}j=B\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\mathsf{o}}C$
or (b) $A_{\\_}j=\&^{\mathsf{o}}\\{l:B_{\\_}l\\}_{\\_}{l\in L}$.

Since $\mathrm{pr}(A_{\\_}j)=\mathsf{o}$ is the least of the priorities in
$\Gamma$, we know that either (in case a) $P_{\\_}{x_{\\_}j}^{\star}\equiv
x_{\\_}j(v,z).Q_{\\_}{x_{\\_}j}$ or (in case b)
$P_{\\_}{x_{\\_}j}^{\star}\equiv
x_{\\_}j(z)\triangleright\\{l:Q_{\\_}{x_{\\_}j}^{l}\\}_{\\_}{l\in L}$.
Moreover, since either (in case a)
$\overline{A_{\\_}j}=\overline{B}\mathbin{\otimes}^{\mathsf{o}}\overline{C}$
or (in case b)
$\overline{A_{\\_}j}={\oplus}^{\mathsf{o}}\\{l:\overline{B_{\\_}l}\\}_{\\_}{l\in
L}$, we have that either (in case a) $P_{\\_}{y_{\\_}j}^{\star}\equiv
y_{\\_}j[a,b]\mathbin{|}Q_{\\_}{y_{\\_}j}$ or (in case b)
$P_{\\_}{y_{\\_}j}^{\star}\equiv y_{\\_}j[b]\triangleleft
l^{\star}\mathbin{|}Q_{\\_}{y_{\\_}j}$ for $l^{\star}\in L$. In case (a), let
$Q^{\prime}_{\\_}{x_{\\_}j}:=Q_{\\_}{x_{\\_}j}{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{a/v,b/z\\}}}$;
in case (b), let
$Q^{\prime}_{\\_}{x_{\\_}j}:=Q_{\\_}{x_{\\_}j}^{l^{\star}}{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{b/z\\}}}$.
Then, (in case a) by reduction
$\beta_{\mathbin{\otimes}\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}}$
or (in case b) by reduction $\beta_{\oplus\&}$,

$\displaystyle
P\equiv(\mkern-1.0mu\bm{\nu}x_{\\_}iy_{\\_}i)_{\\_}i(\mkern-1.0mu\bm{\nu}\tilde{n}\tilde{m})(P_{\\_}{x_{\\_}j}^{\star}\mathbin{|}P_{\\_}{y_{\\_}j}^{\star}\mathbin{|}P_{\\_}R)$
$\displaystyle\equiv(\mkern-1.0mu\bm{\nu}x_{\\_}iy_{\\_}i)_{\\_}{i\setminus
j}(\mkern-1.0mu\bm{\nu}\tilde{n}\tilde{m})((\mkern-1.0mu\bm{\nu}x_{\\_}jy_{\\_}j)(P_{\\_}{x_{\\_}j}^{\star}\mathbin{|}P_{\\_}{y_{\\_}j}^{\star})\mathbin{|}P_{\\_}R)$
$\displaystyle\mathbin{\longrightarrow}(\mkern-1.0mu\bm{\nu}x_{\\_}iy_{\\_}i)_{\\_}{i\setminus
j}(\mkern-1.0mu\bm{\nu}\tilde{n}\tilde{m})(Q^{\prime}_{\\_}{x_{\\_}j}\mathbin{|}Q_{\\_}{y_{\\_}j}\mathbin{|}P_{\\_}R).$
∎

Our deadlock freedom result concerns processes typable under empty contexts
(as in, e.g., Caires and Pfenning [8] and Dardha and Gay [9]). This way, the
reduction guaranteed by Theorem 4 corresponds to a synchronization
($\beta$-rule), rather than a commuting conversion ($\kappa$-rule). We first
need a lemma which ensures that non-live processes typable under empty
contexts do not contain actions or prefixes.

######  Lemma 5.

If $P\vdash\emptyset;\emptyset$ and $P$ is not live, then $P$ contains no
actions or prefixes whatsoever.

###### Proof.

Suppose, for contradiction, that $P$ does contain actions or prefixes. For
example, $P$ contains some subterm $x(y,z);P^{\prime}$. Because
$P\vdash\emptyset;\emptyset$, there must be a restriction on $x$ in $P$
binding it with, e.g., $x^{\prime}$. Now, $x^{\prime}$ does not appear in
$P^{\prime}$, because the type of $x$ in the derivation of
$P\vdash\emptyset;\emptyset$ must be lower than the types of the endpoints in
$P^{\prime}$, and by duality the types of $x$ and $x^{\prime}$ have equal
priority. Hence, there is some $Q$ s.t.
$P\equiv(\mkern-1.0mu\bm{\nu}\tilde{u}\tilde{v})(\mkern-1.0mu\bm{\nu}xx^{\prime})(x(y,z);P^{\prime}\mathbin{|}Q)$
where $x^{\prime}\in\mathrm{fn}(Q)$. There are two cases for the appearance of
$x^{\prime}$ in $Q$: (1) not prefixed, or (2) prefixed.

  * •

In case (1), $x^{\prime}\in\mathrm{an}(Q)$, so the restriction on
$x,x^{\prime}$ in $P$ is on a pair of active names, contradicting the fact
that $P$ is not live.

  * •

In case (2), $x^{\prime}$ appears in $Q$ behind at least one prefix. For
example, $Q$ contains some subterm $a(b,c);Q^{\prime}$ where
$x^{\prime}\in\mathrm{fn}(Q^{\prime})$. Again, $a$ must be bound in $P$ to,
e.g., $a^{\prime}$. Through similar reasoning as above, we know that
$a^{\prime}$ does not appear in $Q^{\prime}$. Moreover, the type of $a$ must
have lower priority than the type of $x^{\prime}$, so by duality the type of
$a^{\prime}$ must have lower priority than the type of $x$. So, $a^{\prime}$
also does not appear in $P^{\prime}$. Hence, there is $R$ s.t.
$P\equiv(\mkern-1.0mu\bm{\nu}\tilde{u}\tilde{v})(\mkern-1.0mu\bm{\nu}aa^{\prime})(\mkern-1.0mu\bm{\nu}xx^{\prime})(x(y,z);P^{\prime}\mathbin{|}a(b,c);Q^{\prime}\mid
R)$ where $a^{\prime}\in\mathrm{fn}(R)$.

Now, the case split on whether $a^{\prime}$ appears prefixed in $R$ or not
repeats, possibly finding new names that prefix the current name again and
again following case (2). However, process terms are finite in size, so we
know that at some point there cannot be an additional parallel component in
$P$ to bind the new name, contradicting the existence of the newly found
prefix. Hence, eventually case (1) will be reached, uncovering a restriction
on a pair of active names and contradicting the fact that $P$ is not live.

In conclusion, the assumption that there are actions or prefixes in $P$ leads
to a contradiction. Hence, $P$ contains no actions or prefixes whatsoever. ∎

We now state our deadlock freedom result:

######  Theorem 6 (Deadlock Freedom).

If $P\vdash\emptyset;\emptyset$, then either $P\equiv\bm{0}$ or
$P\mathbin{\longrightarrow}_{\\_}\beta Q\mkern 2.0mu$ for some $Q$.

###### Proof.

The analysis depends on whether $P$ is live or not.

  * •

If $P$ is not live, then, by Lemma 5, it does not contain any actions or
prefixes. Any recursive loops in $P$ are thus of the form ‘$\mu
X_{\\_}1();\ldots;\mu X_{\\_}n();\bm{0}$’: contractiveness requires recursive
calls to be prefixed by inputs/branches or bound to parallel
outputs/selections, of which there are none. Hence, we can use structural
congruence to rewrite each recursive loop in $P$ to $\bm{0}$ by unfolding,
yielding $P^{\prime}\equiv P$. The remaining derivation of $P^{\prime}$ only
contains applications of Empty, Mix, $\bullet$, or Cycle on closed endpoints.
It follows easily that $P\equiv P^{\prime}\equiv\bm{0}$.

  * •

If $P$ is live, by Theorem 4 there is $Q$ s.t. $P\mathbin{\longrightarrow}Q$.
Moreover, $P$ does not have free names, for otherwise it would not be typable
under empty context. Because commuting conversions apply only to free names,
this means $P\mathbin{\longrightarrow}_{\\_}\beta Q$. ∎

###  3.4 Explicit Closing and Replicated Servers

$\bm{1}$ $x[]\vdash\Omega;x{:}\bm{1}^{\mathsf{o}}$ $P\vdash\Omega;\Gamma$
$\mathsf{o}<\mathrm{pr}(\Gamma)$ $\bot$
$x();P\vdash\Omega;\Gamma,x{:}\bot^{\mathsf{o}}$ ${?}$
${?}x[y]\vdash\Omega;x{:}{?}^{\mathsf{o}}A,y{:}\overline{A}$
$P\vdash\Omega;{?}\Gamma,y{:}A$ $\mathsf{o}<\mathrm{pr}({?}\Gamma)$ ${!}$
${!}x(y);P\vdash\Omega;{?}\Gamma,x{:}{!}^{\mathsf{o}}A$ $P\vdash\Omega;\Gamma$
W $P\vdash\Omega;\Gamma,x{:}{?}^{\mathsf{o}}A$
$P\vdash\Omega;\Gamma,x{:}{?}^{\mathsf{o}}A,x^{\prime}{:}{?}^{\kappa}A$
$\pi=\min(\mathsf{o},\kappa)$ C
$P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{x/x^{\prime}\\}}}\vdash\Omega;\Gamma,x{:}{?}^{\pi}A$
$P\vdash\Omega;\Gamma,y{:}A$ ${?}^{\star}$ ${?}\overline{x}[y]\cdot
P\vdash\Omega;\Gamma,x{:}{?}^{\mathsf{o}}A$ .
$\displaystyle\beta_{\bm{1}\bot}$
$\displaystyle(\mkern-1.0mu\bm{\nu}xy)(x[]\mathbin{|}y();P)$
$\displaystyle\mathbin{\longrightarrow}P$ $\displaystyle\beta_{{?}{!}}$
$\displaystyle(\mkern-1.0mu\bm{\nu}xy)({?}x[a]\mathbin{|}{!}y(v);P\mathbin{|}Q)$
$\displaystyle\mathbin{\longrightarrow}P{\mathchoice{\scriptstyle}{\scriptstyle}{}{}{\\{a/v\\}}}\mathbin{|}(\mkern-1.0mu\bm{\nu}xy)({!}y(v);P\mathbin{|}Q)$
$\displaystyle\kappa_{\bot}$ $\displaystyle
x\notin\tilde{v},\tilde{w}\implies$
$\displaystyle(\mkern-1.0mu\bm{\nu}\tilde{v}\tilde{w})(x();P\mathbin{|}Q)$
$\displaystyle\mathbin{\longrightarrow}x();(\mkern-1.0mu\bm{\nu}\tilde{v}\tilde{w})(P\mathbin{|}Q)$
$\displaystyle\kappa_{{!}}$ $\displaystyle x\notin\tilde{v},\tilde{w}\implies$
$\displaystyle(\mkern-1.0mu\bm{\nu}\tilde{v}\tilde{w})({!}x(y);P\mathbin{|}Q)$
$\displaystyle\mathbin{\longrightarrow}{!}x(y);(\mkern-1.0mu\bm{\nu}\tilde{v}\tilde{w})(P\mathbin{|}Q)$
Figure 7: Typing rules for explicit closing and replicated servers.

As already mentioned, our presentation of APCP does not include explicit
closing and replicated servers. We briefly discuss what APCP would look like
if we were to include these constructs.

We achieve explicit closing by adding empty outputs ‘$x[]$’ and empty inputs
‘$x();P$’ to the syntax of Figure 2 (top). We also add the synchronization
‘$\beta_{\bm{1}\bot}$’ and the commuting conversion ‘$\kappa_{\bot}$’ in
Figure 7 (bottom). At the level of types, we replace the conflated type
‘$\bullet$’ with ‘$\bm{1}^{\mathsf{o}}$’ and ‘$\bot^{\mathsf{o}}$’, associated
to empty outputs and empty inputs, respectively. Note that we do need priority
annotations on types for closed endpoints now, because the empty input is
blocking and thus requires priority checks. In the type system of Figure 3
(top), we replace rule ‘$\bullet$’ with the rules ‘$\bm{1}$’ and ‘$\bot$’ in
Figure 7 (top).

For replicated servers, we add client requests ‘${?}x[y]$’ and servers
‘${!}x(y);P$’, typed ‘${?}^{\mathsf{o}}A$’ and ‘${!}^{\mathsf{o}}A$’,
respectively. We include syntactic sugar for binding client requests to
continuations as in 1: ‘${?}\overline{x}[y]\cdot
P:=(\mkern-1.0mu\bm{\nu}ya)({?}x[a]\mathbin{|}P)$’. New reduction rules are in
Figure 7 (bottom): synchronization rule ‘$\beta_{{?}{!}}$’, connecting a
client and a server and spawns a copy of the server, and commuting conversion
‘$\kappa_{{!}}$’. Also, we add a structural congruence axiom to clean up
unused servers: $(\mkern-1.0mu\bm{\nu}xz)({!}x(y);P)\equiv\bm{0}$. In the type
system, we add rules ‘${?}$’, ‘${!}$’, ‘W’ and ‘C’ in Figure 7 (top); the
former two are for typing client requests and servers, respectively, and the
latter two are for connecting to a server without requests and for multiple
requests, respectively. In rule ‘${!}$’, notation ‘${?}\Gamma$’ means that
every type in $\Gamma$ is of the form ‘${?}^{\mathsf{o}}A$’. Figure 7 (top)
also includes an admissible rule ‘${?}^{\star}$’ which types the syntactic
sugar for bound client requests.

##  4 Examples

Up to here, we have presented our process language and its type system, and we
have discussed the influence of asynchrony and recursion in their design and
properties ensured by typing. We now present examples to further illustrate
the design and expressiveness of APCP.

###  4.1 Milner’s Typed Cyclic Scheduler

Var $\vdash X{:}3;a_{\\_}1{:}X,c_{\\_}n{:}X,d_{\\_}1{:}X$ $\&$ $\vdash
X{:}3;a_{\\_}1{:}X,c_{\\_}n{:}\&^{\rho_{\\_}n}\\{\mathsf{next}:X\\},d_{\\_}1{:}X$
$\&$ $\vdash
X{:}3;a_{\\_}1{:}X,c_{\\_}n{:}\&^{\pi_{\\_}n}\\{\mathsf{start}:\&^{\rho_{\\_}n}\\{\mathsf{next}:X\\}\\},d_{\\_}1{:}X$
$\oplus^{\star}$ $\vdash
X{:}3;a_{\\_}1{:}X,c_{\\_}n{:}\&^{\pi_{\\_}n}\\{\mathsf{start}:\&^{\rho_{\\_}n}\\{\mathsf{next}:X\\}\\},d_{\\_}1{:}{\oplus}^{\rho_{\\_}1}\\{\mathsf{next}:X\\}$
$\&$ $\vdash
X{:}3;a_{\\_}1{:}\&^{\kappa_{\\_}1}\\{\mathsf{ack}:X\\},c_{\\_}n{:}\&^{\pi_{\\_}n}\\{\mathsf{start}:\&^{\rho_{\\_}n}\\{\mathsf{next}:X\\}\\},d_{\\_}1{:}{\oplus}^{\rho_{\\_}1}\\{\mathsf{next}:X\\}$
$\oplus^{\star}$ $\vdash
X{:}3;a_{\\_}1{:}{\oplus}^{\mathsf{o}_{\\_}1}\\{\mathsf{start}:\&^{\kappa_{\\_}1}\\{\mathsf{ack}:X\\}\\},c_{\\_}n{:}\&^{\pi_{\\_}n}\\{\mathsf{start}:\&^{\rho_{\\_}n}\\{\mathsf{next}:X\\}\\},d_{\\_}1{:}{\oplus}^{\rho_{\\_}1}\\{\mathsf{next}:X\\}$
$\oplus^{\star}$ $\vdash
X{:}3;~{}a_{\\_}1{:}{\oplus}^{\mathsf{o}_{\\_}1}\\{\mathsf{start}:\&^{\kappa_{\\_}1}\\{\mathsf{ack}:X\\}\\},\begin{array}[t]{l}c_{\\_}n{:}\&^{\pi_{\\_}n}\\{\mathsf{start}:\&^{\rho_{\\_}n}\\{\mathsf{next}:X\\}\\},\\\
d_{\\_}1{:}{\oplus}^{\pi_{\\_}1}\\{\mathsf{start}:{\oplus}^{\rho_{\\_}1}\\{\mathsf{next}:X\\}\\}\end{array}$
Rec $\vdash\emptyset;~{}a_{\\_}1{:}\mu
X.{\oplus}^{\mathsf{o}_{\\_}1}\\{\mathsf{start}:\&^{\kappa_{\\_}1}\\{\mathsf{ack}:X\\}\\},\begin{array}[t]{l}c_{\\_}n{:}\mu
X.\&^{\pi_{\\_}n}\\{\mathsf{start}:\&^{\rho_{\\_}n}\\{\mathsf{next}:X\\}\\},\\\
d_{\\_}1{:}\mu
X.\&^{\pi_{\\_}1}\\{\mathsf{start}:{\oplus}^{\rho_{\\_}1}\\{\mathsf{next}:X\\}\\}\end{array}$
Figure 8: Typing derivation of the leader scheduler $A_{\\_}1$ of Milner’s
cyclic scheduler (processes omitted).

To consider a process that goes beyond the scope of PCP, here we show that our
specification of Milner’s cyclic scheduler from Section 2 is typable in APCP,
and thus deadlock free (cf. Theorem 6). Let us recall the process definitions
of the leader and followers, omitting braces ‘$\\{\ldots\\}$’ for branches
with one option:

$\displaystyle A_{\\_}1$ $\displaystyle:=\mu
X(a_{\\_}1,c_{\\_}n,d_{\\_}1);d_{\\_}1\mathbin{\triangleleft}\mathsf{start}\cdot
a_{\\_}1\mathbin{\triangleleft}\mathsf{start}\cdot
a_{\\_}1\mathbin{\triangleright}\mathsf{ack};d_{\\_}1\mathbin{\triangleleft}\mathsf{next}\cdot
c_{\\_}n\mathbin{\triangleright}\mathsf{start};c_{\\_}n\mathbin{\triangleright}\mathsf{next};X\langle
a_{\\_}1,c_{\\_}n,d_{\\_}1\rangle$ $\displaystyle A_{\\_}{i+1}$
$\displaystyle:=\mu
X(a_{\\_}{i+1},c_{\\_}i,d_{\\_}{i+1});\begin{array}[t]{l}c_{\\_}i\mathbin{\triangleright}\mathsf{start};a_{\\_}{i+1}\mathbin{\triangleleft}\mathsf{start}\cdot
d_{\\_}{i+1}\mathbin{\triangleleft}\mathsf{start}\cdot
a_{\\_}{i+1}\mathbin{\triangleright}\mathsf{ack};\\\
c_{\\_}i\mathbin{\triangleright}\mathsf{next};d_{\\_}{i+1}\mathbin{\triangleleft}\mathsf{next}\cdot
X\langle a_{\\_}{i+1},c_{\\_}i,d_{\\_}{i+1}\rangle\end{array}\qquad\forall
1\leq i<n$

Each process $A_{\\_}{i+1}$ for $0\leq i<n$—thus including the leader—is
typable as follows, assuming $c_{\\_}i$ is $c_{\\_}n$ for $i=0$ (see Fig. 8
for the derivation of $A_{\\_}1$, omitting processes from judgments):

$\displaystyle A_{\\_}{i+1}$
$\displaystyle\vdash\emptyset;~{}a_{\\_}{i+1}{:}\mu
X.{\oplus}^{\mathsf{o}_{\\_}{i+1}}\\{\mathsf{start}:\&^{\kappa_{\\_}{i+1}}\\{\mathsf{ack}:X\\}\\},\begin{array}[t]{l}c_{\\_}i{:}\mu
X.\&^{\pi_{\\_}i}\\{\mathsf{start}:\&^{\rho_{\\_}i}\\{\mathsf{next}:X\\}\\},\\\
d_{\\_}{i+1}{:}\mu
X.{\oplus}^{\pi_{\\_}{i+1}}\\{\mathsf{start}:{\oplus}^{\rho_{\\_}{i+1}}\\{\mathsf{next}:X\\}\\}\end{array}$

Note how, for each $1\leq i\leq n$, the types for $c_{\\_}i$ and $d_{\\_}i$
are duals.

To verify these typing derivations, we need to assign values to the priorities
$\mathsf{o}_{\\_}i,\kappa_{\\_}i,\pi_{\\_}i,\rho_{\\_}i$ for each $1\leq i\leq
n$ that satisfy the necessary requirements. From the derivation of $A_{\\_}1$
we require $\kappa_{\\_}1<\rho_{\\_}1,\pi_{\\_}n$. For each $1\leq i<n$, from
the derivation of $A_{\\_}{i+1}$ we require $\rho_{\\_}i<\rho_{\\_}{i+1}$ and
$\kappa_{\\_}{i+1}<\rho_{\\_}i,\rho_{\\_}{i+1}$ and
$\pi_{\\_}i<\mathsf{o}_{\\_}{i+1},\pi_{\\_}{i+1}$. We can easily satisfy these
requirements by assigning $\mathsf{o}_{\\_}i:=\kappa_{\\_}i:=\pi_{\\_}i:=i$
and $\rho_{\\_}i:=i+2$ for each $1\leq i\leq n$.

Assuming that $P_{\\_}i\vdash\emptyset;a_{\\_}i{:}\mu
X.\&^{\mathsf{o}_{\\_}i}\\{\mathsf{start}:{\oplus}^{\kappa_{\\_}i}\\{\mathsf{ack}:X\\}\\}$
for each $1\leq i\leq n$, we have $Sched_{\\_}n\vdash\emptyset;\emptyset$.
Hence, it follows from Theorem 6 that $Sched_{\\_}n$ is deadlock free for each
$n\geq 1$.

###  4.2 Comparison to Padovani’s Type System for Deadlock Freedom

Padovani’s type system for deadlock freedom [22] simplifies a type system by
Kobayashi [18]; both these works do not consider session types. Just as for
Dardha and Gay’s PCP [9], the priority annotations of APCP are based on
similar annotations in Padovani’s and Kobayashi’s type systems. Here, we
compare APCP to these type systems by discussing some of the examples in
Padovani’s work.

#### Ring of Processes

To illustrate APCP’s flexible support for recursion, we consider Padovani’s
ever-growing ring of processes [22, Ex. 3.8]. For the ring to continuously
loop, Padovani uses self-replicating processes. Although this exact method is
not possible in APCP, we can use recursion instead:

$Ring_{\\_}x^{y}:=\mu
X(x,y);(\mkern-1.0mu\bm{\nu}aa^{\prime})(x(z);(\mkern-1.0mu\bm{\nu}bb^{\prime})(X\langle
z,b\rangle\mathbin{|}X\langle
b^{\prime},a\rangle)\mathbin{|}\overline{y}[c]\cdot
a^{\prime}\mathbin{\leftrightarrow}c)\vdash\emptyset;x{:}\mu
X.X\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\mathsf{o}}\bullet,y{:}\mu
X.X\mathbin{\otimes}^{\kappa}\bullet$

Each iteration, this process receives a fresh endpoint from its left neighbor
and sends another fresh endpoint to its right neighbor. It then spawns two
copies of itself, connected to each other on a fresh channel, and one
connected to the left neighbor and the other to the right neighbor. There are
no priority requirements, so we can let $\mathsf{o}=\kappa$. We can then
connect the initial copy of $Ring$ to itself, forming a deadlock free ring of
processes that doubles in size at every iteration (cf. Theorem 6):

$\begin{array}[]{c}(\mkern-1.0mu\bm{\nu}xy)Ring_{\\_}x^{y}\mathbin{\longrightarrow}^{3}(\mkern-1.0mu\bm{\nu}x_{\\_}1y_{\\_}1)(\mkern-1.0mu\bm{\nu}x_{\\_}2y_{\\_}2)(Ring_{\\_}{x_{\\_}1}^{y_{\\_}2}\mathbin{|}Ring_{\\_}{x_{\\_}2}^{y_{\\_}1})\\\\[4.0pt]
\mathbin{\longrightarrow}^{6}(\mkern-1.0mu\bm{\nu}x_{\\_}1y_{\\_}1)(\mkern-1.0mu\bm{\nu}x_{\\_}2y_{\\_}2)(\mkern-1.0mu\bm{\nu}x_{\\_}3y_{\\_}3)(\mkern-1.0mu\bm{\nu}x_{\\_}4y_{\\_}4)(Ring_{\\_}{x_{\\_}1}^{y_{\\_}2}\mathbin{|}Ring_{\\_}{x_{\\_}2}^{y_{\\_}3}\mathbin{|}Ring_{\\_}{x_{\\_}3}^{y_{\\_}4}\mathbin{|}Ring_{\\_}{x_{\\_}4}^{y_{\\_}1})\mathbin{\longrightarrow}^{12}\ldots\end{array}$

#### Blocking versus Non-blocking

Padovani discusses the significance of blocking inputs versus non-blocking
outputs [22, Exs. 2.2 & 3.6]. Although we can express Padovani’s example in
APCP with minor modifications, we can do so more directly by including
replication as in Section 3.4. Consider the following processes, which are
identical up to the order of input and output:

${Node}_{\\_}A:={!}c_{\\_}A(c);c(x);c(y);\overline{x}[a]\cdot
y(z);\bm{0}\hskip
30.00005pt{Node}_{\\_}B:={!}c_{\\_}B(c);c(x);c(y);y(z);\overline{x}[a]\cdot\bm{0}$

We consider several configurations of nodes, using the syntactic sugar
$\overline{x}\langle y\rangle\cdot
P:=\overline{x}[y^{\prime}]\cdot(y\mathbin{\leftrightarrow}y^{\prime}\mathbin{|}P)$:

$\displaystyle L_{\\_}1(X)$
$\displaystyle:=(\mkern-1.0mu\bm{\nu}c_{\\_}Ac^{\prime}_{\\_}A)(\mkern-1.0mu\bm{\nu}c_{\\_}Bc^{\prime}_{\\_}B)({Node}_{\\_}A\mathbin{|}{Node}_{\\_}B\mathbin{|}{?}\overline{c^{\prime}_{\\_}X}[c]\cdot(\mkern-1.0mu\bm{\nu}ee^{\prime})(\overline{c}\langle
e\rangle\cdot\overline{c}\langle e^{\prime}\rangle\cdot\bm{0}))$
$\displaystyle L_{\\_}2(X,Y)$
$\displaystyle:=(\mkern-1.0mu\bm{\nu}c_{\\_}Ac^{\prime}_{\\_}A)(\mkern-1.0mu\bm{\nu}c_{\\_}Bc^{\prime}_{\\_}B)({Node}_{\\_}A\mathbin{|}{Node}_{\\_}B\mathbin{|}(\mkern-1.0mu\bm{\nu}ee^{\prime})(\mkern-1.0mu\bm{\nu}ff^{\prime})\left(\begin{array}[]{l}{?}\overline{c^{\prime}_{\\_}X}[c]\cdot\overline{c}\langle
e\rangle\cdot\overline{c}\langle f\rangle\cdot\bm{0}\\\
\mathbin{|}\,{?}\overline{c^{\prime}_{\\_}Y}[c^{\prime}]\cdot\overline{c^{\prime}}\langle
f^{\prime}\rangle\cdot\overline{c^{\prime}}\langle
e^{\prime}\rangle\cdot\bm{0}\end{array}\right))$ $\displaystyle
L_{\\_}3(X,Y,Z)$
$\displaystyle:=(\mkern-1.0mu\bm{\nu}c_{\\_}Ac^{\prime}_{\\_}A)(\mkern-1.0mu\bm{\nu}c_{\\_}Bc^{\prime}_{\\_}B)({Node}_{\\_}A\mathbin{|}{Node}_{\\_}B\mathbin{|}(\mkern-1.0mu\bm{\nu}ee^{\prime})(\mkern-1.0mu\bm{\nu}ff^{\prime})(\mkern-1.0mu\bm{\nu}gg^{\prime})\left(\begin{array}[]{l}{?}\overline{c^{\prime}_{\\_}X}[c]\cdot\overline{c}\langle
e\rangle\cdot\overline{c}\langle f\rangle\cdot\bm{0}\\\
\mathbin{|}\,{?}\overline{c^{\prime}_{\\_}Y}[c^{\prime}]\cdot\overline{c^{\prime}}\langle
g\rangle\cdot\overline{c^{\prime}}\langle e^{\prime}\rangle\cdot\bm{0}\\\
\mathbin{|}\,{?}\overline{c^{\prime}_{\\_}Z}[c^{\prime\prime}]\cdot\overline{c^{\prime\prime}}\langle
f^{\prime}\rangle\cdot\overline{c^{\prime\prime}}\langle
g^{\prime}\rangle\cdot\bm{0}\end{array}\right))$

where $X,Y,Z\in\\{A,B\\}$.

To illustrate the significance of APCP’s asynchrony, let us consider how
$L_{\\_}2(A,A)$ reduces:

$L_{\\_}2(A,A)\mathbin{\longrightarrow}^{6}(\mkern-1.0mu\bm{\nu}ee^{\prime})(\mkern-1.0mu\bm{\nu}ff^{\prime})(\overline{e}[a]\cdot
f(z);\bm{0}\mathbin{|}\overline{f^{\prime}}[a^{\prime}]\cdot
e^{\prime}(z^{\prime});\bm{0})\mathbin{\longrightarrow}(\mkern-1.0mu\bm{\nu}ff^{\prime})(f(z);\bm{0}\mathbin{|}\overline{f^{\prime}}[a^{\prime}]\cdot\bm{0})\mathbin{\longrightarrow}\bm{0}.$

The synchronization on $e$ and $e^{\prime}$ is possible because the output on
$f^{\prime}$ is non-blocking. It is also possible for $f$ and $f^{\prime}$ to
synchronize first, because the output on $e$ is also non-blocking. In
contrast, the reduction of $L_{\\_}2(B,B)$ illustrates the blocking behavior
of inputs:

$L_{\\_}2(B,B)\mathbin{\longrightarrow}^{6}(\mkern-1.0mu\bm{\nu}ee^{\prime})(\mkern-1.0mu\bm{\nu}ff^{\prime})(f(z);\overline{e}[a]\cdot\bm{0}\mathbin{|}e^{\prime}(z^{\prime});\overline{f^{\prime}}[a^{\prime}]\cdot\bm{0}){\centernot\longrightarrow}.$

This results in deadlock, for each node awaits a message, blocking their
output to the other node.

Let us show how APCP detects (freedom of) deadlocks in each of these
configurations by considering priority requirements. For $X\in\\{A,B\\}$, we
have
${Node}_{\\_}X\vdash\emptyset;c_{\\_}X{:}{!}^{\mathsf{o}}((\bullet\mathbin{\otimes}^{\kappa_{\\_}X}\bullet)\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\pi_{\\_}X}(\bullet\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\rho_{\\_}X}\bullet)\mathbin{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\textstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle{\&}$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle{\&}$}}}^{\psi_{\\_}X}\bullet)$,
requiring $\rho_{\\_}B<\kappa_{\\_}B$ and
$\pi_{\\_}X,\psi_{\\_}X<\kappa_{\\_}X,\rho_{\\_}X$. In each configuration, the
input endpoint of one node is connected to the output endpoint of another.
Duality thus requires that $\kappa_{\\_}W=\rho_{\\_}{W^{\prime}}$ for
$W,W^{\prime}\in\\{X,Y,Z\\}$. Hence, in any configuration, if the input
endpoint of a $Node_{\\_}B$ is connected the output endpoint of another
$Node_{\\_}B$, we require $\kappa_{\\_}B=\rho_{\\_}B$, violating the
requirement that $\rho_{\\_}B<\kappa_{\\_}B$. From this we can conclude that
the above configurations are deadlock free if and only if at least one of
$X,Y,Z$ is $A$, and at most one of them is $B$. This verifies that
$L_{\\_}2(A,A)$ contains no deadlock, while $L_{\\_}2(B,B)$ does.

Note that in PCP the conditions for deadlock freedom are much stricter, as
PCP’s blocking outputs additionally require that $\kappa_{\\_}A<\rho_{\\_}A$.
Hence, we also cannot connect the input of a $Node_{\\_}A$ to the output of
another $Node_{\\_}A$. This means that $L_{\\_}2(A,B)$ and $L_{\\_}2(B,A)$ are
the only deadlock free configurations in PCP.

##  5 Related Work & Conclusion

We have already discussed several related works throughout the paper [9, 11,
18, 22]. The work of Kobayashi and Laneve [19] is related to APCP in that it
addresses deadlock freedom for _unbounded_ process networks. Another related
approach is Toninho and Yoshida’s [27], which addresses deadlock freedom for
cyclic process networks by generating global types from binary types. The work
by Balzer et al. [2, 3] is also worth mentioning: it guarantees deadlock
freedom for processes with shared, mutable resources by means of manifest
sharing, i.e. explicitly acquiring and releasing access to resources. Finally,
Pruiksma and Pfenning’s session type system derived from adjoint logic [24,
25] treats asynchronous, non-blocking actions via axiomatic typing rules,
similarly as we do (cf. axioms ‘$\mathbin{\otimes}$’ and ‘$\oplus$’ in Figure
3); we leave a precise comparison with their approach for future work.

In this paper, we have presented APCP, a type system for deadlock freedom of
cyclic process networks with asynchronous communication and recursion. We have
shown that, when compared to (the synchronous) PCP [9], asynchrony in APCP
significantly simplifies the management of priorities required to detect
cyclic dependencies (cf. the discussion at the end of Section 4.2). We
illustrated the expressivity of APCP using multiple examples, and concluded
that it is comparable in expressivity to similar type systems not based on
session types or logic, in particular the one by Padovani [22]. More in-depth
comparisons with this and the related type systems cited above would be much
desirable. Finally, in ongoing work we are applying APCP to the analysis of
multiparty protocols implemented as processes [14].

#### Acknowledgements

We are grateful to the anonymous reviewers for their careful reading of our
paper and their useful feedback. We also thank Ornela Dardha for clarifying
the typing rules of PCP to us.

## References

  * [1]
  * [2] Stephanie Balzer & Frank Pfenning (2017): _Manifest Sharing with Session Types_.  Proc. ACM Program. Lang. 1(ICFP), pp. 37:1–37:29, 10.1145/3110281.
  * [3] Stephanie Balzer, Bernardo Toninho & Frank Pfenning (2019): _Manifest Deadlock-Freedom for Shared Session Types_.  In Luís Caires, editor: Programming Languages and Systems, Lecture Notes in Computer Science, Springer International Publishing, Cham, pp. 611–639, 10.1007/978-3-030-17184-122.
  * [4] Michele Boreale (1998): _On the Expressiveness of Internal Mobility in Name-Passing Calculi_.  Theoretical Computer Science 195(2), pp. 205–226, 10.1016/S0304-3975(97)00220-X.
  * [5] Gérard Boudol (1992): _Asynchrony and the Pi-Calculus_.  Research Report RR-1702, INRIA.
  * [6] Luís Caires (2014): _Types and Logic, Concurrency and Non-Determinism_.  Technical Report MSR-TR-2014-104, In Essays for the Luca Cardelli Fest, Microsoft Research.
  * [7] Luís Caires & Jorge A. Pérez (2017): _Linearity, Control Effects, and Behavioral Types_.  In Hongseok Yang, editor: Programming Languages and Systems, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, pp. 229–259, 10.1007/978-3-662-54434-19.
  * [8] Luís Caires & Frank Pfenning (2010): _Session Types as Intuitionistic Linear Propositions_.  In Paul Gastin & François Laroussinie, editors: CONCUR 2010 - Concurrency Theory, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, pp. 222–236, 10.1007/978-3-642-15375-416.
  * [9] Ornela Dardha & Simon J. Gay (2018): _A New Linear Logic for Deadlock-Free Session-Typed Processes_.  In Christel Baier & Ugo Dal Lago, editors: Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, Springer International Publishing, pp. 91–109, 10.1007/978-3-319-89366-25.
  * [10] Ornela Dardha & Jorge A. Pérez (2015): _Comparing Deadlock-Free Session Typed Processes_.  Electronic Proceedings in Theoretical Computer Science 190, pp. 1–15, 10.4204/EPTCS.190.1.
  * [11] Henry DeYoung, Luís Caires, Frank Pfenning & Bernardo Toninho (2012): _Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication_.  In Patrick Cégielski & Arnaud Durand, editors: Computer Science Logic (CSL’12) - 26th International Workshop/21st Annual Conference of the EACSL, Leibniz International Proceedings in Informatics (LIPIcs) 16, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, pp. 228–242, 10.4230/LIPIcs.CSL.2012.228.
  * [12] Simon J. Gay, Peter Thiemann & Vasco T. Vasconcelos (2020): _Duality of Session Types: The Final Cut_.  Electronic Proceedings in Theoretical Computer Science 314, pp. 23–33, 10.4204/EPTCS.314.3.
  * [13] Jean-Yves Girard (1987): _Linear Logic_.  Theoretical Computer Science 50(1), pp. 1–101, 10.1016/0304-3975(87)90045-4.
  * [14] Bas van den Heuvel & Jorge A. Pérez (2021): _A Decentralized Analysis of Multiparty Protocols_.  arXiv:2101.09038 [cs].
  * [15] Kohei Honda (1993): _Types for Dyadic Interaction_.  In Eike Best, editor: CONCUR’93, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, pp. 509–523, 10.1007/3-540-57208-235.
  * [16] Kohei Honda & Mario Tokoro (1991): _An Object Calculus for Asynchronous Communication_.  In Pierre America, editor: ECOOP’91 European Conference on Object-Oriented Programming, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, pp. 133–147, 10.1007/BFb0057019.
  * [17] Kohei Honda, Vasco T. Vasconcelos & Makoto Kubo (1998): _Language Primitives and Type Discipline for Structured Communication-Based Programming_.  In Chris Hankin, editor: Programming Languages and Systems, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, pp. 122–138, 10.1007/BFb0053567.
  * [18] Naoki Kobayashi (2006): _A New Type System for Deadlock-Free Processes_.  In Christel Baier & Holger Hermanns, editors: CONCUR 2006 – Concurrency Theory, Lecture Notes in Computer Science, Springer Berlin Heidelberg, pp. 233–247, 10.1007/1181794916.
  * [19] Naoki Kobayashi & Cosimo Laneve (2017): _Deadlock Analysis of Unbounded Process Networks_.  Information and Computation 252, pp. 48–70, 10.1016/j.ic.2016.03.004.
  * [20] Robin Milner (1989): _Communication and Concurrency_.  Prentice Hall International Series in Computer Science, Prentice Hall, New York, USA.
  * [21] Robin Milner, Joachim Parrow & David Walker (1992): _A Calculus of Mobile Processes, I_.  Information and Computation 100(1), pp. 1–40, 10.1016/0890-5401(92)90008-4.
  * [22] Luca Padovani (2014): _Deadlock and Lock Freedom in the Linear $\pi$-Calculus_.  In: Proceedings of the 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, ACM, New York, NY, USA, pp. 72:1–72:10, 10.1145/2603088.2603116.
  * [23] Benjamin C. Pierce (2002): _Types and Programming Languages_.  MIT Press, Cambridge, Massachusetts.
  * [24] Klaas Pruiksma & Frank Pfenning (2019): _A Message-Passing Interpretation of Adjoint Logic_.  In: Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES), Electronic Proceedings in Theoretical Computer Science 291, Open Publishing Association, pp. 60–79, 10.4204/EPTCS.291.6.
  * [25] Klaas Pruiksma & Frank Pfenning (2021): _A Message-Passing Interpretation of Adjoint Logic_.  Journal of Logical and Algebraic Methods in Programming 120(100637), 10.1016/j.jlamp.2020.100637.
  * [26] Bernardo Toninho, Luis Caires & Frank Pfenning (2014): _Corecursion and Non-Divergence in Session-Typed Processes_.  In Matteo Maffei & Emilio Tuosto, editors: Trustworthy Global Computing, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, pp. 159–175, 10.1007/978-3-662-45917-111.
  * [27] Bernardo Toninho & Nobuko Yoshida (2018): _Interconnectability of Session-Based Logical Processes_.  ACM Transactions on Programming Languages and Systems (TOPLAS) 40(4), p. 17, 10.1145/3242173.
  * [28] Vasco T. Vasconcelos (2012): _Fundamentals of Session Types_.  Information and Computation 217, pp. 52–70, 10.1016/j.ic.2012.05.002.
  * [29] Philip Wadler (2012): _Propositions As Sessions_.  In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP ’12, ACM, New York, NY, USA, pp. 273–286, 10.1145/2364527.2364568.