Client-server sessions are based on a variation of the traditional
interpretation of linear logic propositions as session types in which
non-linear channels (those regulating the interaction between a pool of
clients and a single server) are typed by coexponentials instead of
the usual exponentials.

Coexponentials enable the modeling of racing interactions, whereby clients
compete to interact with a single server whose internal state (and thus the
offered service) may change as the server processes requests sequentially.

In this work we present a fair termination result for , a core
calculus of client-server sessions. We design a type system such that every
well-typed term corresponds to a valid derivation in , the infinitary
proof theory of linear logic with least and greatest fixed points. We then
establish a correspondence between reductions in the calculus and principal
reductions in . Fair termination in follows from cut
elimination in .

§ INTRODUCTION

Session types [13, 14, 15] are
descriptions of communication protocols enabling the static enforcement of a
variety of safety and liveness properties, including the fact that communication
channels are used according to their protocol (fidelity), that processes
do not get stuck (deadlock freedom), that pending communications are
eventually completed (livelock freedom), that sessions eventually end

It is possible to trace a close correspondence between session types and
propositions of linear logic, and between the typing rules of a session type
system and the proof rules of linear
logic [20, 6, 18]. This
correspondence provides session type theories with a solid logical foundation
and enables the application of known results concerning linear logic proofs into
the domain of communicating protocols. One notable example is cut
elimination: the fact that every linear logic proof can be reduced to a form
that does not make use of the cut rule means that the process described by the
proof can be reduced to a form in which no pending communication is present,
provided that there is a good correspondence between cut reductions in proofs
and reductions in processes.

The development of session type systems based on linear logic also poses some
challenges with respect to their ability to cope with “real-world” scenarios.
An example, which is the focus of this work, is the modeling of the interactions
between a pool of clients and a single server. By definition, a
server is a process that can handle an unbounded number of requests made by
clients. In a session type system based on linear logic, it is natural to
associate the channel from which a server accepts client requests with a type of
the form $!\Type$, indicating the unlimited availability of a service with type
$\Type$. In fact, it was observed early on [10] that the
meaning of the “of course” modality $!\Type$ could be informally expressed by
the equation

\[
!\Type \cong \One \branch \Type \branch (!\Type \tfork !\Type)
\]

which could be read “as many copies of $\Type$ as the clients require”.

While appealing from a theoretical point of view, the association between the
concept of server and the “of course” modality is both unrealistic and

First of all, it models the “unlimited” availability of the server by means of
unlimited parallel copies of the server, each copy dealing with a single
request, rather than by a single process that is capable of handling an
unlimited number of requests sequentially.

Second, it fails to capture the fact that each connection between a client and
the server may alter the server's internal state, in such a way that different
connections may potentially affect each other.

These considerations have led Qian et al. [19] to develop
(for “Client-Server Linear Logic”), a session type system based on
linear logic which includes the coexponential modalities $\tclient\Type$
and $\tserver\Type$ whose meaning can be (informally) expressed by the equations

\begin{equation}
\label{eq:coexp}
\tclient\Type \cong \One \choice \Type \choice (\tclient\Type \tfork \tclient\Type)
\text{\qquad and\qquad}
\tserver\Type \cong \Bot \branch \Type \branch (\tserver\Type \tjoin \tserver\Type)
\end{equation}

according to which a server that behaves as $\tserver\Type$ offers $\Type$ as
many times as necessary to satisfy all client requests, but it does so
sequentially and in some (unspecified) order.

Qian et al. [19] show that well-typed processes are
deadlock free, but they leave a proof of termination to future work conjecturing
that it could be quite involved. A proof of this property is valuable since
termination (combined with deadlock freedom) implies livelock freedom.

In this paper we attack the problem of establishing a termination result for
. Instead of providing an ad hoc proof, we attempt to reduce the
termination problem for to the cut elimination property of a known logical
system. To this aim, we propose a variation of called that is in
close relationship with
[3, 8, 2], the infinitary
proof theory of multiplicative-additive linear logic with least and greatest
fixed points. The basic idea is to encode the coexponentials in 's type
system as fixed points in following their expected meaning
(<ref>). At this point, the cut elimination property of should
allow us to deduce that well-typed processes do not admit infinite
reduction sequences.

As it turns out, we are unable to follow this plan of action in full. The
problem is that some reductions in do not correspond to cut reduction
steps in . More specifically, even though clients are queued into client
pools, they should be able to reduce in any order, independently of their
position in the queue. This independent reduction of the clients in the same
pool is not matched by the sequence of cut reduction steps that are performed in
the cut elimination proof of .

Still, the cut elimination property of allows us to prove a useful
result, namely that every well-typed process is fairly
terminating. Fair termination [12, 9] is weaker
than termination since it does not rule out the existence of infinite reduction
sequences. However, it guarantees that every fair and maximal reduction
sequence of a well-typed process is finite, under a suitable fairness
assumption. In particular, fair termination is strong enough (when combined with
deadlock freedom) to guarantee livelock freedom.

The adoption of as logical foundation for has another
advantage. In the original presentation of  [19] the
process calculus is equipped with an unconventional operational semantics
whereby reductions can occur underneath prefixes and prefixes may be moved
around crossing restrictions, parallel compositions and other (unrelated)
prefixes. This semantics is justified to keep the process reduction rules and
the cut reduction rules sufficiently aligned, so that the cut elimination
property in the logic can be reflected to some valuable property in the
calculus, such as deadlock freedom. In contrast, features an entirely
conventional reduction semantics. We can afford to do so because is an
infinitary proof system in which the cut elimination property is proved
bottom-up by reducing outermost cuts first. This reduction strategy
matches the ordinary reduction semantics of any process calculus in which
reductions happen at the outermost levels of processes. In the end, since the
reduction semantics of is stricter than that of , the deadlock
freedom and the fair termination results we prove for are somewhat
stronger than their counterparts in the context of .

Structure of the paper.

<ref> describes syntax and semantics of and defines the
notion of fairly terminating process.

We develop the type system for in <ref>.

In <ref> we recall the key elements of , before addressing
the proof that well-typed processes fairly terminate in

<ref> revisits an example of non-deterministic server given by Qian
et al. [19] in our setting.

We summarize our results and further compare with
[19] and other related work in

Some proofs and definitions have been moved into <ref>.

§ SYNTAX AND SEMANTICS OF

Syntax of .

P, Q
::=          invocation

|         failure

|     .P     wait

|     .P     input

|     PQ     branch

|     PQ     server

|     PQ     parallel composition

|         empty pool

|         close

|     PQ     output

|     _i.P     select     i∈1,2

|     PQ     client pool

In this section we define syntax and semantics of , a
calculus of sessions in which servers handle client requests

The syntax of makes use of an infinite set $\VarSet$ of
channels ranged over by $x$, $y$ and $z$ and a set $\ProcessSet$ of
process names ranged over by $\A$, $\B$, and so on. In channels
are of two kinds (which will be distinguished by their type): session
channels connect two communicating processes; shared channels connect an
unbounded number of clients with a single server. The structure of terms is
given by the grammar in <ref> and their meaning is informally
described below.

The term $\Cut\x{P}{Q}$ represents the parallel composition of $P$ and $Q$
connected by the restricted channel $x$, which can be either a session channel
or a shared channel.

The term $\Fail\x$ represents a process that signals a failure on
channel $x$.

The term $\Close\x$ models the closing of a session, whereas
$\Wait\x.P$ models a process that waits for $x$ to be closed and
then continues as $P$.

The term $\Fork\x\y{P}{Q}$ models a process that creates a new
channel $y$, sends $y$ over $x$, uses $y$ as specified by $P$ and
$x$ as specified by $Q$.

The term $\Join\x\y.P$ models a process that receives a channel $y$
from $x$ and then behaves as $P$.

The term $\Select\x{\InTag_i}.P$ models a process that sends the label
$\InTag_i$ over $x$ and then behaves as $P$. In this work we only consider two
labels $\InTag_1$ and $\InTag_2$, although it is common to allow for an
arbitrary set of atomic labels. Dually, the term $\Case\x{P_1}{P_2}$ models a
process that waits for a label $\InTag_i$ from $x$ and then behaves according to

The term $\Nil\x$ models the empty pool of clients connecting with a server on
the shared channel $x$, whereas the term $\Cons\x\y{P}Q$ models a client pool
consisting of a client that connects with a server on channel $x$ and behaves as
$P$ and another client pool $Q$. Occasionally we write $\Client\x\y.P$ instead
of $\Cons\x\y{P}\Nil\x$.

The term $\Server\x\y{P}{Q}$ models a server that waits for
connections on the shared channel $x$. If a new connection $y$ is
established, the server continues as $P$. If no clients are left
connecting on $x$, the service on $x$ is terminated and the process
continues as $Q$.

Finally, a term $\Call\A{\seqof\x}$ represents the invocation of the process
named $\A$ with arguments $\seqof\x$. We assume that each process name is
associated with a unique global definition of the form $\Let\A{\seqof\x}{P}$.
The notation $\seqof{e}$ is used throughout the paper to represent possibly
empty sequences $e_1,\dots,e_n$ of various entities.

The notions of free and bound names are defined in the expected way. Note that
the output operations $\Fork\x\y{P}{Q}$ and $\Cons\x\y{P}Q$ bind $y$ in $P$ but
not in $Q$. We write $\fn{P}$ and $\bn{P}$ for the sets of free and bound names
in $P$, we identify processes up to renaming of bound channel names and we
require $\fn{P} = \set{\seqof\x}$ for each global definition

Structrual pre-congruence and reduction semantics of .

\[
\begin{array}{@{}rll@{}}
\defrule{s-par-comm} &
\Cut\x{P}{Q} \pcong \Cut\x{Q}{P}
\\
\defrule{s-pool-comm} &
\multicolumn{2}{l@{}}{
\Cons\x\y{P}\Cons\u\v{Q}R \pcong \Cons\u\v{Q}\Cons\x\y{P}R
\\
\defrule{s-par-assoc} &
\Cut\x{P}{\Cut\y{Q}{R}} \pcong \Cut\y{\Cut\x{P}{Q}}{R} &
x\in\fn{Q}\setminus\fn{R}, y\not\in\fn{P}
\\
\defrule{s-pool-par} &
\Cons\x\y{P}\Cut\z{Q}{R} \pcong \Cut\z{\Cons\x\y{P}Q}{R} &
x \in \fn{Q}, z \not\in \fn{\Client\x\y.P}
\\
\defrule{s-par-pool} &
\Cut\z{\Cons\x\y{P}Q}{R} \pcong \Cons\x\y{P}\Cut\z{Q}{R} &
\\
\defrule{s-call} &
\Call\A{\seqof\x} \pcong P &
\Let\A{\seqof\x}{P}
\\
\\
\defrule{r-close} &
\Cut\x{\Close\x}{\Wait\x.P} \red P
\\
\defrule{r-comm} &
\multicolumn{2}{l@{}}{
\Cut\x{\Fork\x\y{P}{Q}}{\Join\x\y.R} \red \Cut\y{P}{\Cut\x{Q}{R}}
\\
\defrule{r-case} &
\Cut\x{\Select\x{\InTag_i}.P}{\Case\x{Q_1}{Q_2}} \red \Cut\x{P}{Q_i}
\\
\defrule{r-done} &
\Cut\x{\EmptyPool\x}{\Server\x\y{P}{Q}} \red Q
\\
\defrule{r-connect} &
\multicolumn{2}{l@{}}{
\Cut\x{\Cons\x\y{P}Q}{\Server\x\y{R_1}{R_2}} \red \Cut\y{P}{\Cut\x{Q}{R_1}}
\\
\defrule{r-par} &
\Cut\x{P}{R} \red \Cut\x{Q}{R} &
P \red Q
\\
\defrule{r-pool} &
\Cons\x\y{R}P \red \Cons\x\y{R}Q &
P \red Q
\\
\defrule{r-struct} &
P \red Q &
P \pcong P' \red Q' \pcong Q
\end{array}
\]

The operational semantics of is given by a structural precongruence
relation $\pcong$ and a reduction relation $\red$, both defined in
<ref> and described below.

Rules s-par-comm and s-pool-comm state the expected
commutativity of parallel and pool compositions. In particular,
s-pool-comm allows clients in the same queue to swap positions,
modeling the fact that the order in which they connect to the server is not

Rule s-par-assoc models the associativity of parallel composition. The
side conditions make sure that no channel is captured ($y\not\in\fn{P}$) or left
dangling ($x\not\in\fn{R}$) and that parallel processes remain connected

The rules s-pool-par and s-par-pool deal with the mixed
associativity between parallel and pool compositions. The side conditions ensure
that no bound name leaves its scope and that parallel processes remain

Finally, s-call unfolds a process invocation to its definition.

Concerning the reduction relation, rule r-close models the closing of
a session, rule r-comm models the exchange of a channel and
r-case that of a label.

Rule r-connect models the connection of a client with a server,
whereas r-done deals with the case in which there are no clients left.

Finally, r-par and r-pool close reductions under parallel
compositions and client pools whereas r-struct allows reductions up to
structural pre-congruence.

Hereafter we write $\wred$ for the reflexive, transitive closure of
$\red$, we write $P \red$ if $P \red Q$ for some $Q$ and $P \nred$
if not $P \red$.

Later on we will also use a restriction of dubbed whose reduction relation, denoted by $\dred$, is obtained by
removing the rules s-pool-comm, s-pool-par,
s-par-pool and r-pool (all those with
“pool” in their name) from $\red$.  In essence, is a more deterministic version of in which clients are
forced to connect and reduce in the order in which they appear in
client pools. Also, clients are no longer allowed to cross
restricted channels.

We illustrate the features of by modeling a pool of clients that
compete to access a shared resource, represented as a simple lock.
When one client manages to acquire the lock, meaning that it has gained
access to the resource, it prevents other clients from accessing the
resource until the resource is released.

We model the lock with this definition:

\[
\Let\Lock{x,z}{\Server\x\y{\Wait\y.\Call\Lock{x,z}}{\Close\z}}
\]

The lock is a server waiting for connections on the shared channel $x$,
whereas each user is a client of the lock connecting on $x$. When a
connection is established, the server waits until the resource is released,
which is signalled by the termination of the session $y$, and then makes
itself available again to handle further requests.

The following process models the concurrent access to the lock by two clients:

\[
\Cut\x{\Cons\x\u{\Close\u}\Cons\x\v{\Close\v}\Nil\x}{\Call\Lock{x,z}}
\]

The order in which requests are handled by $\Lock$ is non-deterministic
because of s-pool-comm. In this oversimplified example the users
are indistinguishable and so non-determinism does not prevent the system to
be confluent. In <ref> we will see a more interesting example
in which confluence is lost.

This kind of interaction is typeable in thanks to coexponentials,
which enable the concurrent access to a shared resource.

We conclude this section by defining various termination properties
of interest.

A run of $P$ is a (finite or infinite) sequence $(P_0,P_1,\dots)$ of
processes such that $P = P_0$ and $P_i \red P_{i+1}$ whenever $P_{i+1}$ is a
term in the sequence. A run is maximal if it is infinite or if it is
finite and its last term (say $Q$) cannot reduce any further (that is, $Q
\nred$).

We say that $P$ is terminating if every maximal run of $P$ is finite. We
say that $P$ is weakly terminating if $P$ has a maximal finite run.

A run of $P$ is fair if it contains finitely many weakly terminating
processes. We say that $P$ is fairly terminating if every fair run of $P$
is finite.

A fundamental property of any fairness notion is the fact that every
finite run of a process should be extendable to a maximal fair
one. This property, called
feasibility [1] or machine
closure [17], holds for our fairness notion and
follows immediately from the next proposition.

Every process has at least one maximal fair run.

For an arbitrary process $P$ there are two possibilities.

If $P$ is weakly terminating, then there exists $Q$ such that $P \wred Q
\nred$. From this sequence of reductions we obtain a maximal run of $P$ that
is fair since it is finite.

If $P$ is not weakly terminating, then $P \red$ and $P \wred Q$ implies that
$Q$ is not weakly terminating. In this case we can build an infinite run of
$P$ which is fair since it does not go through any weakly terminating process.

The given notion of fair termination admits an alternative characterization that
does not refer to fair runs. This characterization provides us with the key
proof principle to show that well-typed processes fairly terminate

$P$ is fairly terminating iff $P \wred Q$ implies that $Q$ is weakly

($\Leftarrow$) Suppose by contradiction that $(P_0,P_1,\dots)$ is an infinite
fair run of $P$ and note that $P \wred P_i$ for every $i$. From the hypothesis
we deduce that every $P_i$ is weakly terminating. Then the run contains
infinitely many weakly terminating processes, which is absurd by definition of
fair run.

Suppose that $P \wred Q$. Then there is a finite run of $P$ that ends in $Q$.
By <ref> there is a maximal fair run of $Q$. By
concatenating these two runs we obtain a maximal fair run of $P$ that contains
$Q$. From the hypothesis we deduce that this run is finite. Since $Q$ occurs
in this run, we conclude that $Q$ is weakly terminating.

§ TYPE SYSTEM

In this section we develop the type system of .  Types are
defined thus:

\[
\textbf{Type}
\qquad
\TypeT, \TypeS ::= \Bot \mid \One \mid \Top \mid \Zero \mid \TypeT \tjoin \TypeS \mid \TypeT \tfork \TypeS \mid \TypeT \branch \TypeS \mid \TypeT \choice \TypeS \mid \tserver\Type \mid \tclient\Type
\]

Types extend the usual constants and connectives of multiplicative-additive
linear logic with the coexponentials $\tserver\Type$ and $\tclient\Type$ and, in
the context of , they describe how channels are used by processes.

Positive types indicate output operations whereas negative types indicate input
operations. In particular: $\One$/$\Bot$ describe a session channel used for
sending/receiving a session termination signal; $\Zero$/$\Top$ describe a
session channel used for sending/receiving an impossible (empty) message;
$\TypeT\tfork\TypeS$/$\TypeT\tjoin\TypeS$ describe a session channel used for
sending/receiving a channel of type $\TypeT$ and then according to $\TypeS$;
$\Type_1\choice\Type_2$/$\Type_1\branch\Type_2$ describe a session channel used
for sending/receiving a label $\InTag_i$ and then according to $\Type_i$;
finally, $\tclient\Type$/$\tserver\Type$ describe a shared channel used for
sending/receiving a connection message establishing a session of type $\Type$.

Each type $\Type$ has a dual $\dual\Type$ obtained in the
expected way.  For example, we have
$\dual{(\One \choice \Type)} = \Bot \branch \dual\Type$ and
$\dual{(\tserver\Type)} = \tclient\dual\Type$.

Typing rules for .

Px :

x :

P, x :

Q, x :

, x :

, x : .P

x :

P, y : , x :

.P, x :

P, y :

Q, x :

PQ, , x :

P, x :

Q, x :

PQ, x :

P, x : _i

_i.P, x : _1 _2

P, x : , y :

PQ, x :

P, y :

Q, x :

PQ, , x :

x :

The typing rules for are shown in
<ref>. Typing judgments have the form
$\wtp{P}\Context$ and relate a process $P$ with a context

Contexts are finite maps from channel names to types written as
$\seqof{x:\Type}$. We let $\ContextC$ and $\ContextD$ range over
contexts, we write $\emptyset$ for the empty context, we write
$\dom\Context$ for the domain of $\Context$, namely for the set of
channel names for which there is an association in $\Context$, and
we write $\ContextC,\ContextD$ for the union of $\ContextC$ and
$\ContextD$ when $\dom\ContextC \cap \dom\ContextD = \emptyset$.

For the most part, the typing rules coincide with those of a
standard session type system based on linear
logic [20, 18]. In particular,
, , ,
, , ,
and relate the standard proof
rules of multiplicative-additive classical linear logic with the
corresponding forms of .

The rule deals with process invocations
$\Call\A{\seqof\x}$ by unfolding the global definition of $\A$,
noted as side condition to the rule.

Rule deals with servers $\Server\x\y{P}{Q}$. The
continuation $P$, which is the actual handler of incoming
connections, must be well typed in a context enriched with the
channel $y$ resulting from the connection. Note that $x$ is still
present in the context and with the same type, meaning that $P$ must
also be able to handle any further connection on the shared
channel $x$. The continuation $Q$, which models the behavior of the
server once no more clients are connecting on $x$, is not supposed
to use $x$ any longer.

Rule deals with non-empty client pools
$\Cons\x\y{P}Q$. The client $P$ is connecting with a server through
a shared channel $x$ and establishes a session $y$. The rest of the
pool $Q$ is using $x$ in the same way.

Rule deals with the empty pool of clients
connecting on $x$.

The typing rules are interpreted coinductively. Therefore, a judgment
$\wtp{P}\Context$ is derivable if there is a possibly infinite typing derivation
for it. The need for infinite typing derivations stems from the fact that we
type process invocations by “unfolding” them to the process they represent, so
this unfolding may go on forever in the case of recursive processes.

Let us consider once again the process definitions in <ref>. We

\[
\begin{prooftree}
\[
\[
\[
\smash\vdots
\justifies
\wtp{\Call\Lock{x,z}}{x : \tserver\Bot, z : \One}
\using\refrule\CallRule
\]
\justifies
\wtp{\Wait\y.\Call\Lock{x,z}}{x : \tserver\Bot, y : \Bot, z : \One}
\using\refrule\WaitRule
\]
\[
\justifies
\wtp{\Close\z}{z : \One}
\using\refrule\CloseRule
\]
\justifies
\wtp{\Server\x\y{\Wait\y.\Call\Lock{x,z}}{\Close\z}}{x : \tserver\Bot, z : \One}
\using\refrule\ServerRule
\]
\justifies
\wtp{\Call\Lock{x,z}}{x : \tserver\Bot, z : \One}
\using\refrule\CallRule
\end{prooftree}
\]

showing that $\Lock$ is well typed. Note that the typing derivation is
infinite since $\Lock$ is a recursive process.

We can now obtain the following typing derivation

\[
\begin{prooftree}
\[
\[
\justifies
\wtp{\Close\u}{u : \One}
\using\refrule\CloseRule
\]
\[
\[
\justifies
\wtp{\Close\v}{v : \One}
\using\refrule\CloseRule
\]
\[
\justifies
\wtp{\Nil\x}{x : \tclient\One}
\using\refrule\NilRule
\]
\justifies
\wtp{
\Cons\x\v{\Close\v}
\Nil\x
x : \tclient\One
\using\refrule\ConsRule
\]
\justifies
\wtp{
\Cons\x\u{\Close\u}
\Cons\x\v{\Close\v}
\Nil\x
x : \tclient\One
\using\refrule\ConsRule
\]
\[
\smash\vdots
\justifies
\wtp{\Call\Lock{x,z}}{x : \tserver\Bot, z : \One}
\]
\justifies
\wtp{
\Cut\x{
\Cons\x\u{\Close\u}
\Cons\x\v{\Close\v}
\Nil\x
\Call\Lock{x,z}
z : \One
\using\refrule\CutRule
\end{prooftree}
\]

showing that the system as a whole is well typed.

Adopting an infinitary type system will make it easy to relate with
(<ref>). However, we must be careful in that some
infinite typing derivations allow us to type processes that are not weakly
terminating, as illustrated in the next example.

[non-terminating process]

Consider the process $\Let\Omega{}{\Cut\x{\Close\x}{\Wait\x.\Omega}}$ which
creates a session $x$, immediately closes it and then repeats the same
behavior. Clearly, this process is not weakly terminating because it can
only reduce thus:

\[
\Call\Omega{} \pcong
\Cut\x{\Close\x}{\Wait\x.\Call\Omega{}} \red
\Call\Omega{} \pcong
\Cut\x{\Close\x}{\Wait\x.\Call\Omega{}} \red
\cdots
\]

Nonetheless, we are able to find the following (infinite) typing
derivation for $\Call\Omega{}$.

\[
\begin{prooftree}
\[
\[
\justifies
\wtp{
\Close\x
x : \One
\using\refrule\CloseRule
\]
\[
\[
\smash\vdots\mathstrut
\justifies
\wtp{
\Call\Omega{}
\emptyset
\using\refrule\CallRule
\]
\justifies
\wtp{
\Wait\x.\Call\Omega{}
x : \Bot
\using\refrule\WaitRule
\]
\justifies
\wtp{
\Cut\x{\Close\x}{\Wait\x.\Call\Omega{}}
\emptyset
\using\refrule\CutRule
\]
\justifies
\wtp{
\Call\Omega{}
\emptyset
\using\refrule\CallRule
\end{prooftree}
\]

Since we aim at ensuring fair termination for well-typed
processes, we must consider this derivation as invalid.

In order to rule out processes like $\Omega$ in <ref>, we identify a
class of valid typing derivations as follows.

A typing derivation is valid if every infinite branch in it goes
through infinitely many applications of the rule concerning the same channel.

This validity condition requires that every infinite branch of a typing
derivation describes the behavior of a server willing to accept an unbounded
number of connection requests.

If we look back at the infinite typing derivation for the $\Lock$ process in
<ref>, we see that it is valid according to
<ref> since the only infinite branch in it goes through
infinitely many applications of the rule concerning the very
same shared channel $x$.

On the contrary, the typing derivation in <ref> is invalid
since the infinite branch in it does not go through any application
of .

The fact that every infinite branch must go through infinitely many
applications of concerning the very same
shared channel is a subtle point. Without the specification that
it is the same shared channel to be found infinitely often,
it would be possible to obtain invalid typing derivations as
illustrated by the next example.

Consider the definition

\[
\Let\OmegaServer\x{
\Server\x\y{
\Wait\y.\Call\OmegaServer\x
\Cut\z{\EmptyPool\z}{\Call\OmegaServer\z}
\]

describing a server that waits for connections on the shared channel $x$.
After each request, the server makes itself available again for handling
more requests by the recursive invocation $\Call\OmegaServer\x$. Once all
requests have been processed, the server creates a new shared channel on
which an analogous server operates.

Using the typing rules in <ref> we are able to find the
following typing derivation:

\[
\begin{prooftree}
\[
\[
\[
\smash\vdots\mathstrut
\justifies
\wtp{\Call\OmegaServer\x}{x : \tserver\Bot}
\using\refrule\CallRule
\]
\justifies
\wtp{
\Wait\y.\Call\OmegaServer\x
x : \tserver\Bot,
y : \Bot
\using\refrule\WaitRule
\]
\[
\[
\justifies
\wtp{\EmptyPool\z}{z : \tclient\One}
\using\refrule\NilRule
\]
\[
\smash\vdots
\justifies
\wtp{\Call\OmegaServer\z}{z : \tserver\Bot}
\using\refrule\CallRule
\]
\justifies
\wtp{
\Cut\z{\EmptyPool\z}{\Call\OmegaServer\z}
\emptyset
\using\refrule\CutRule
\]
\justifies
\wtp{
\Server\x\y{
\Wait\y.\Call\OmegaServer\x
\Cut\z{\EmptyPool\z}{\Call\OmegaServer\z}
x : \tserver\Bot
\using\refrule\ServerRule
\]
\justifies
\wtp{\Call\OmegaServer\x}{x : \tserver\Bot}
\using\refrule\CallRule
\end{prooftree}
\]

Notice that the derivation bifurcates in correspondence of the application
of and also that each sub-tree is infinite, since it
contains an unfolding of the $\OmegaServer$ process.

For this reason, the derivation contains (infinitely) many
infinite branches, which are obtained by either “going left”
or “going right” each time is
encountered. Each of these infinite branches goes through an
application of infinitely many times, as
requested by <ref>.

Also, any such branch that “goes right” finitely many times
eventually ends up going through infinitely many applications of
that concern the same channel. In contrast,
any branch that “goes right” infinitely many times keeps going
through applications of concerning new
shared channels created in correspondence of the application of

In conclusion, this typing derivation is invalid and rightly so,
or else the diverging process
$\Cut\x{\EmptyPool\x}{\Call\OmegaServer\x}$ would be well typed
in the empty context.

We conclude this section by stating two key properties of the type
system, starting from the fact that typing is preserved by
structural pre-congruence and reductions.

Let $P \rrel Q$ where ${\rrel}\in\set{{\pcong},{\red}}$. Then
$\wtp{P}\Context$ implies $\wtp{Q}\Context$.

Also, processes that are well typed in a context of the form
$x : \One$ are deadlock free.

[deadlock freedom]theoremthmdf

If $\wtp{P}{x : \One}$ then either $P \pcong \Close\x$ or $P \dred$.

Note that <ref> uses $\dred$ instead of $\red$ in order to state that
$P$ is able to reduce if it is not (structurally pre-congruent to) $\Close\x$.
Recalling that ${\dred} \subseteq {\red}$, the deadlock freedom property ensured
by <ref> is slightly stronger than one would normally expect. This
formulation will be necessary in <ref> when proving the
soundness of the type system. The proofs of <ref> can
be found in <ref>.

Most session calculi based on linear logic include a form $\Link\x\y$ whose
typing rule $\wtp{\Link\x\y}{x : \Type, y : \dual\Type}$ corresponds to the
axiom $\vdash \Type, \dual\Type$ of linear logic.

The form $\Link\x\y$ is usually interpreted as a forwarder between the
channels $x$ and $y$ and it is useful for example to model the output of a
free channel $\Send\x\y.P$ as the term $\Fork\x\z{\Link\y\z}{P}$.

In this example we show that there is no need to equip with a native form $\Link\x\y$ since its behavior can be encoded
as a well-typed process. To this aim, we define a
family $\ExpandLink\Type$ of process definitions by induction on
$\Type$ as follows

\begin{align*}
\Let{\ExpandLink\Bot}{x,y&}{\Wait\x.\Close\y} \\
\Let{\ExpandLink\Top}{x,y&}{\Fail\x} \\
\Let{\ExpandLink{\TypeT \tjoin \TypeS}}{x,y&}{
\Join\x\u.\Fork\y\v{
\Call{\ExpandLink\TypeT}{u,v}
\Call{\ExpandLink\TypeS}{x,y}
} \\
\Let{\ExpandLink{\TypeT \branch \TypeS}}{x,y&}{
\Case\x{\Left\y.\Call{\ExpandLink\TypeT}{x,y}}{\Right\y.\Call{\ExpandLink\TypeS}{x,y}}
} \\
\Let{\ExpandLink{\tserver\Type}}{x,y&}{
\Server\x\u{
\Cons\y\v{
\Call{\ExpandLink\TypeT}{u,v}
\Call{\ExpandLink{\tserver\Type}}{x,y}
\Nil\y
\end{align*}

with the addition of the definitions
$\Let{\ExpandLink\Type}{x,y}{\Call{\ExpandLink{\dual\Type}}{y,x}}$ for the
positive type constructors.

It is easy to build a typing derivation for the judgment
$\wtp{\Call{\ExpandLink\Type}{x,y}}{x : \Type, y : \dual\Type}$.

Also, every infinite branch in such derivation eventually loops through an
invocation of the form $\Call{\ExpandLink{\tserver\TypeS}}{u,v}$, which goes
through an application of concerning the channel $u$.
So, the derivation of $\wtp{\Call{\ExpandLink\Type}{x,y}}{x : \Type, y :
\dual\Type}$ is valid and the process $\Call{\ExpandLink\Type}{x,y}$ is well

§ A QUICK RECOLLECTION OF

In this section we recall the main elements of
[8, 3, 2], the
infinitary proof system of the multiplicative additive fragment of
linear logic extended with least and greatest fixed points.

The syntax of pre-formulas makes use of an infinite
set of propositional variables ranged over by $X$ and $Y$ and
is given by the grammar below:

\[
\textbf{Pre-formula}
\qquad
\FormulaF, \FormulaG ::= \X \mid \Bot \mid \Top \mid \Zero \mid \One \mid \FormulaF \tjoin \FormulaG \mid \FormulaF \tfork \FormulaG \mid \FormulaF \branch \FormulaG \mid \FormulaF \choice \FormulaG \mid \tnu\X.\FormulaF \mid \tmu\X.\FormulaF
\]

The fixed point operators $\tmu$ and $\tnu$ are the binders of
propositional variables and the notions of free and bound variables
are defined accordingly. A formula is a closed
pre-formula. We write $\subst\Formula\X$ for the capture-avoiding
substitution of all free occurrences of $X$ with $\Formula$ and
$\dual\Formula$ for the dual of $\Formula$, which is the
involution such that

\[
\dual\X = X
\qquad
\dual{(\tmu\X.\Formula)} = \tnu\X.\dual\Formula
\qquad
\dual{(\tnu\X.\Formula)} = \tmu\X.\dual\Formula
\]

among the other expected equations. Postulating that $\dual\X = \X$
is not a problem since we will always dualize formulas, which do not
contain free propositional variables.

We write $\subf$ for the subformula ordering, that is the
least partial order such that $\FormulaF \subf \FormulaG$ if
$\FormulaF$ is a subformula of $\FormulaG$. For example, if
$\FormulaF \eqdef \tmu\X.\tnu\Y.(X \choice Y)$ and
$\FormulaG \eqdef \tnu\Y.(\FormulaF \choice Y)$ we have
$\FormulaF \subf \FormulaG$ and
$\FormulaG \not\subf \FormulaF$.

When $\Formulas$ is a set of formulas, we write $\minf\Formulas$ for
its $\subf$-minimum formula if it is defined.

Occasionally we let $\star$ stand for an arbitrary binary connective
(one of $\choice$, $\tfork$, $\branch$, or $\tjoin$) and $\sigma$
stand for an arbitrary fixed point operator (either $\tmu$ or

In it is important to distinguish among different
occurrences of the same formula in a proof derivation. To
this aim, formulas are annotated with addresses.

We assume an infinite set $\AddressSet$ of atomic addresses,
$\dual\AddressSet$ being the set of their duals such that
$\AddressSet \cap \dual\AddressSet = \emptyset$ and
$\dual{\dual\AddressSet{}} = \AddressSet$. We use $a$ and $b$ to
range over elements of $\AddressSet \cup \dual\AddressSet$.  An
address is a string $aw$ where $w \in \set{i,l,r}^*$. The
dual of an address is defined as $\dual{(aw)} = \dual{a}w$.

We use $\addressA$ and $\addressB$ to range over addresses, we write
$\prefix$ for the prefix relation on addresses and we say that
$\addressA$ and $\addressB$ are disjoint if
$\addressA \not\prefix \addressB$ and
$\addressB \not\prefix \addressA$.

A formula occurrence (or simply occurrence) is a pair
$\Formula_\address$ made of a formula $\Formula$ and an address
$\address$. We use $F$ and $G$ to range over occurrences and we
extend to occurrences several operations defined on formulas. In
particular: we use logical connectives to compose occurrences so
$\FormulaF_{\address l} \mathbin\star \FormulaG_{\address r} \eqdef
(\FormulaF \mathbin\star \FormulaG)_\address$ and
$\sigma\X.\Formula_{\address i} \eqdef
(\sigma\X.\Formula)_\address$; the dual of an occurrence is obtained
by dualizing both its formula and its address, that is
$\dual{(\Formula_\address)} \eqdef \dual\Formula_{\dual\address}$;
occurrence substitution preserves the address in the type within
which the substitution occurs, but forgets the address of the
occurrence being substituted, that is
$\FormulaF_\addressA\subst{\FormulaG_\addressB}\X \eqdef
\FormulaF\subst\FormulaG\X_\addressA$.

We write $\strip{F}$ for the formula obtained by forgetting the
address of $F$.  Finally, we write $\tred$ for the least reflexive
relation on types such that $F_1 \star F_2 \tred F_i$ and
$\sigma\X.F \tred F\subst{\sigma\X.F}\X$.

Proof rules of  [3, 8, 2].

⊢, F

⊢, F

⊢, F, G

⊢, F G

⊢, F

⊢, G

⊢, , F G

⊢, F

⊢, G

⊢, F G

⊢, F_i

⊢, F_1 F_2

⊢, F.F
⊢, .F

⊢, F.F
⊢, .F

The proof rules of are shown in <ref>, where
$\SequentS$ and $\SequentT$ range over sets of occurrences written
as $F_1, \dots, F_n$. The rules allow us to derive sequents
of the form $\vdash \Sequent$ and are standard except for
, which unfolds a greatest fixed point just
like does.

Being an infinitary proof system, rules are meant to be
interpreted coinductively. That is, a sequent $\vdash \Sequent$ is
derivable if there exists an arbitrary (finite or infinite)
proof derivation whose conclusion is $\vdash \Sequent$. Without a
validity condition on derivations, such proof system is
notoriously unsound.

's validity condition requires every infinite branch of a
derivation to be supported by the continuous unfolding of a greatest
fixed point. In order to formalize this condition, we start by
defining threads, which are sequences of occurrences.

A thread of $F$ is a (finite or infinite) sequence of
occurrences $(F_0,F_1,\dots)$ such that $F_0 = F$ and
$F_i \tred F_{i+1}$ whenever $i+1$ is a valid index of the

Hereafter we use $t$ to range over threads. For example, if we
consider $\Formula \eqdef \tmu\X.(X \choice \One)$, we have that
$t \eqdef
(\Formula_a,(\Formula\choice\One)_{ai},\Formula_{ail},\dots)$ is an
infinite thread of $\Formula_a$.

Among all threads, we are interested in finding those in which a
$\tnu$-formula is unfolded infinitely often. These threads, called
$\tnu$-threads, are precisely defined thus:

Let $t = (F_0,F_1,\dots)$ be an infinite thread, let $\strip{t}$ be the
corresponding sequence $(\strip{F_0},\strip{F_1},\dots)$ of formulas and let
$\InfOften{t}$ be the set of elements of $\strip{t}$ that occur infinitely
often in $\strip{t}$. We say that $t$ is a $\tnu$-thread if
$\minf\InfOften{t}$ is defined and is a $\tnu$-formula.

If we consider the infinite thread $t$ above, we have
$\InfOften{t} = \set{\Formula, \Formula \choice \One}$ and
$\minf\InfOften{t} = \Formula$, so $t$ is not a $\tnu$-thread
because $\Formula$ is not a $\tnu$-formula.

Consider instead $\FormulaF \eqdef \tnu\X.\tmu\Y.(X \choice Y)$ and
$\FormulaG \eqdef \tmu\Y.(\FormulaF \choice Y)$ and observe that
$\FormulaG$ is the “unfolding” of $\FormulaF$. Now
$t_1 \eqdef (\FormulaF_a, \FormulaG_{ai}, (\FormulaF \choice
\FormulaG)_{aii}, \FormulaF_{aiil}, \dots)$ is a thread of
$\FormulaF_a$ such that
$\InfOften{t_1} = \set{\FormulaF, \FormulaG, \FormulaF \choice
\FormulaG}$ and we have $\minf\InfOften{t_1} = \FormulaF$ because
$\FormulaF \subf \FormulaG$, so $t_1$ is a $\tnu$-thread.

If, on the other hand, we consider the thread
$t_2 \eqdef (\FormulaF_a, \FormulaG_{ai}, (\FormulaF \choice
\FormulaG)_{aii}, \FormulaG_{aiir}, (\FormulaF \choice
\FormulaG)_{aiiri}, \dots)$ such that
$\InfOften{t_2} = \set{\FormulaG, \FormulaF \choice \FormulaG}$ we
have $\minf\InfOften{t_2} = \FormulaG$ because
$\FormulaG \subf \FormulaF \choice \FormulaG$, so $t_2$ is not a

Intuitively, the $\subf$-minimum formula among those that occur
infinitely often in a thread is the outermost fixed point operator
that is being unfolded infinitely often. It is possible to show that
this minimum formula is always well defined [8]. If
such minimum formula is a greatest fixed point operator, then the
thread is a $\tnu$-thread.

Note that a $\tnu$-thread is necessarily infinite.

Now we proceed by identifying threads along branches of proof
derivations. To this aim, we provide a precise definition of

A branch of a proof derivation is a sequence $(\vdash \Sequent_0,
\vdash \Sequent_1, \dots)$ of sequents such that $\vdash \Sequent_0$ occurs
somewhere in the derivation and $\vdash \Sequent_{i+1}$ is a premise of the
rule application that derives $\vdash \Sequent_i$ whenever $i+1$ is a valid
index of the sequence.

An infinite branch is valid if supported by a $\tnu$-thread that
originates somewhere therein.

Let $\gamma = (\vdash \Sequent_0, \vdash \Sequent_1, \dots)$ be an infinite
branch in a derivation. We say that $\gamma$ is valid if there exists
$I \subseteq \Nat$ such that $(F_i)_{i\in I}$ is a $\tnu$-thread and $F_i
\in \Sequent_i$ for every $i\in I$.

A derivation is valid if so are its infinite branches.

§ FAIR TERMINATION OF

In this section we prove that well-typed processes fairly
terminate.  We do so by appealing to the alternative
characterization of fair termination given by
<ref>. Using that characterization and using
the fact that typing is preserved by reductions
(<ref>), it suffices to show that well-typed
processes weakly terminate.

To do that, we encode a well-typed process $P$ into a
(valid) proof and we use the cut elimination property of
to argue that $P$ has a finite maximal run.

*Encoding of types

The encoding of types into formulas is the map
$\tencode\cdot$ defined by

\begin{equation}
\label{eq:encoding-type}
\tencode{\tclient\Type} = \tmu\X.(\One \choice (\tencode\Type \tfork X))
\qquad
\tencode{\tserver\Type} = \tnu\X.(\Bot \branch (\tencode\Type \tjoin X))
\end{equation}

and extended homomorphically to all the other type constructors,
which are in one-to-one correspondence with the connectives and
constants of . Notice that the image of the encoding is a
relatively small subset of formulas in which different fixed
point operators are never intertwined.

Also notice that the encoding of the coexponentials does not follow
exactly their expansion in <ref>. Basically, we choose to
interpret $\tclient\Type$ as a list of clients rather than as
a tree of clients, following to the intuition that clients
are queued when connecting to a server. The interpretation of
$\tserver$ follows as a consequence, as we want it to be the dual of
the interpretation of $\tclient$.

Note that this interpretation of the coexponential modalities is the
same used by Qian et al. [19].

*Encoding of typing contexts

The next step is the encoding of contexts into sequents.
Recall that a sequent is a set of occurrences and that an occurrence is
a pair $\Formula_\address$ made of a formula $\Formula$ and an address
$\address$. In order to associate addresses with formulas, we parametrize the
encoding of contexts with an injective map $\cmap$ from channels to addresses, since channels in (the domain of a) context
uniquely identify the occurrence of a type (and thus of a formula).

We write $\extend\x\address$ for the singleton map that associates
$x$ with the address $\address$ and $\cmap_1,\cmap_2$ for the union
of $\cmap_1$ and $\cmap_2$ when they have disjoint domains and

Now, the encoding of a context is set of formulas defined by

\[
\cencode{x_1 : \Type_1, \dots, x_n : \Type_n}{\cmap,\extend{x_1}{\address_1},\dots,\extend{x_n}{\address_n}} \eqdef
\tencode{\Type_1}_{\address_1}, \dots, \tencode{\Type_n}_{\address_n}
\]

*Encoding of typing derivations

Just like for the encoding of contexts, also the encoding of typing
derivations is parametrized by a map $\cmap$ from channels to
addresses. In addition, we also have to take into account the possibility that
restricted channels are introduced in a context, which happens
in the rule of <ref>. The formula occurrence
corresponding to the type of this newly introduced channel must have an address
that is disjoint from that of any other occurrence. To guarantee this
disjointness, we parametrize the encoding of derivations by an
infinite stream $\amap$ of pairwise distinct atomic addresses. Formally,
$\amap$ is an injective function $\Nat \to \AddressSet$.  We write $a\amap$,
$\even\amap$ and $\odd\amap$ for the streams defined by

\[
(a\amap)(0) \eqdef 0
\qquad
(a\amap)(n + 1) \eqdef \amap(n)
\qquad
\even\amap(n) \eqdef \amap(2n)
\qquad
\odd\amap(n) \eqdef \amap(2n+1)
\]

respectively. In words, $a\amap$ is the stream of atomic addresses
that starts with $a$ and continues as $\amap$ whereas $\even\amap$
and $\odd\amap$ are the sub-streams of $\amap$ consisting of
addresses with an even (respectively, odd) index.

The encoding of a typing derivation is coinductively defined by a map
$\dencode\cdot\cmap\amap$ which we describe using the following notation. For
every typing rule in <ref>

\[
\inferrule[\rulename{rule}]{\Judgment_1\\\cdots\\\Judgment_n}{\Judgment}
\text{\qquad we write \qquad}
\dencode{\inferrule{\Judgment_1\\\cdots\\\Judgment_n}\Judgment}\cmap\amap =
\pi
\]

meaning that $\pi$ is the derivation resulting from the encoding of the
derivation for the judgment $\Judgment$ in which the last rule is an
application of $\rulename{rule}$. Within $\pi$ there will be instances of the
$\dencode{\Judgment_i}{\cmap_i}{\amap_i}$ for suitable $\cmap_i$ and $\amap_i$
standing for the encodings of the sub-derivations for the judgments
$\Judgment_i$ that we find as premises of $\rulename{rule}$.

There is a close correspondence between many typing rules and proof rules so we only detail a few interesting cases of the encoding,

starting from the typing rules and . A
typing derivation ending with an application of these rules is encoded
as follows:

\[
\begin{array}{@{}r@{~}l@{}}
\dencode{
\inferrule{
\wtp{P}{\ContextC, y : \TypeT}
\\
\wtp{Q}{\ContextD, x : \TypeS}
\wtp{\Fork\x\y{P}{Q}}{\ContextC, \ContextD, x : \TypeT \tfork \TypeS}
}{\cmap,\extend\x\address}\amap & =
\inferrule{
\dencode{\wtp{P}{\ContextC, y : \TypeT}}{\cmap,\extend\y{\address l}}{\even\amap}
\\
\dencode{\wtp{Q}{\ContextD, x : \TypeS}}{\cmap,\extend\x{\address r}}{\odd\amap}
\vdash \cencode{\ContextC, \ContextD}\cmap, \tencode{\TypeT \tfork \TypeS}_\address
\,\refrule\ForkRule
\\
\dencode{
\inferrule{
\wtp{P}{\Context, y : \TypeT, x : \TypeS}
\wtp{\Join\x\y.P}{\Context, x : \TypeT \tjoin \TypeS}
}{\cmap,\extend\x\address}\amap & =
\inferrule{
\dencode{\wtp{P}{\Context, y : \TypeT, x : \TypeS}}{\cmap,\extend\y{\address l},\extend\x{\address r}}\amap
\vdash \cencode\Context\cmap, \tencode{\TypeT \tjoin \TypeS}_\address
\,\refrule\JoinRule
\end{array}
\]

Notice that the types $\TypeT \tfork \TypeS$ and $\TypeT \tjoin \TypeS$
associated with $x$ in the conclusion of the rules are encoded into the
occurrences $\tencode{\TypeT \tfork \TypeS}_\address$ and $\tencode{\TypeT
\tjoin \TypeS}_\address$ where $\address$ is the address associated with $x$ in
$\cmap,\extend\x\address$. This address is suitably updated in the encoding of
the premises of the rules.

In the case of , the original stream $\amap$ of
atomic addresses is split into two disjoint streams in the encoding
of the premises to ensure that no atomic address is used twice.

Every application of is simply erased in the encoding:

\[
\dencode{
\inferrule{
\wtp{P}{\seqof{x : \Type}}
\wtp{\Call\A{\seqof\x}}{\seqof{x : \Type}}
}\cmap\amap = \dencode{\wtp{P}{\seqof{x : \Type}}}\cmap\amap
\]

The validity of the typing derivation guarantees that there cannot be
an infinite chain of process invocations in a well-typed process. A proof of
this fact is given by <ref> in <ref>. For this
reason, the encoding of derivations is well defined despite the fact
that applications of are erased.

Another case worth discussing is that of the rule , which is
handled as follows:

\[
\dencode{
\inferrule{
\wtp{P}{\ContextC, x : \Type}
\\
\wtp{Q}{\ContextD, x : \dual\Type}
\wtp{\Cut\x{P}{Q}}{\ContextC, \ContextD}
}\cmap{a\amap} =
\inferrule{
\dencode{\wtp{P}{\ContextC, x : \Type}}{\cmap,\extend\x{a}}{\even\amap}
\quad
\dencode{\wtp{Q}{\ContextD, x : \dual\Type}}{\cmap,\extend\x{\dual{a}}}{\odd\amap}
\vdash \cencode{\ContextC, \ContextD}\cmap
\,\refrule\CutRule
\]

The first address from the infinite stream $a\amap$, which is guaranteed to be
distinct from any other address used so far and that will be used in the rest of
the encoding, is associated with the newly introduced variable $x$. Similarly to
the case of , the tail of the stream is split in the encoding
of the two premises of so as to preserve this guarantee.

We now consider the applications of ,
and which account for the most
relevant part of the encoding.  These rule applications are encoded
by considering the interpretation of the co-exponentials in terms of
least and greatest fixed points (<ref>) and then
by applying the suitable proof rules (and
in particular).

We have

\[
\dencode{
\inferrule{~}{
\wtp{\Nil\x}{x : \tclient\Type}
}{\cmap,\extend\x\address}\amap =
\inferrule{
\inferrule{
\inferrule{~}{
\vdash \One_{\address il}
\rlap{\refrule\CloseRule}
\vdash \tencode{\One \choice (\Type \tfork \tclient\Type)}_{\address i}
\rlap{\refrule\SelectRule}
\vdash \tencode{\tclient\Type}_\address
\refrule\RecRule
\]

for the applications of and

\begin{multline*}
\dencode{
\inferrule{
\wtp{P}{\ContextC, y : \Type}
\\
\wtp{Q}{\ContextD, x : \tclient\Type}
\wtp{\Cons\x\y{P}Q}{\ContextC, \ContextD, x : \tclient\Type}
}{\cmap,\extend\x\address}\amap = \\
\begin{prooftree}
\[
\[
\dencode{
\wtp{P}{\ContextC, y : \Type}
}{\cmap,\extend\y{\address irl}}{\even\amap}
\qquad
\dencode{
\wtp{Q}{\ContextD, x : \tclient\Type}
}{\cmap,\extend\x{\address irr}}{\odd\amap}
\justifies
\vdash
\cencode{\ContextC, \ContextD}\cmap,
\tencode{\Type \tfork \tclient\Type}_{\address ir}
\using\refrule\ForkRule
\]
\justifies
\vdash
\cencode{\ContextC, \ContextD}\cmap,
\tencode{\One \choice (\Type \tfork \tclient\Type)}_{\address i}
\using\refrule\SelectRule
\]
\justifies
\vdash \cencode{\ContextC, \ContextD}\cmap, \tencode{\tclient\Type}_\address
\using\refrule\RecRule
\end{prooftree}
\end{multline*}

for the applications of . Finally, the applications
of are encoded thus:

\begin{multline*}
\dencode{
\inferrule{
\wtp{P}{\Context, x : \tserver\Type, y : \Type}
\\
\wtp{Q}\Context
\wtp{\Server\x\y{P}{Q}}{\Context, x : \tserver\Type}
}{\cmap,\extend\x\address}\amap = \\
\begin{prooftree}
\[
\[
\dencode{
\wtp{Q}\Context
\justifies
\vdash
\cencode\Context\cmap, \Bot_{\address il}
\using\refrule\WaitRule
\]
\[
\dencode{
\wtp{P}{\Context, x : \tserver\Type, y : \Type}
}{\cmap,\extend\x{\address irr},\extend\y{\address irl}}\amap
\justifies
\vdash
\cencode\Context\cmap,
\tencode{\Type \tjoin \tserver\Type}_{\address ir}
\using\refrule\JoinRule
\]
\justifies
\vdash
\cencode\Context\cmap,
\tencode{\Bot \branch (\Type \tjoin \tserver\Type)}_{\address i}
\using\refrule\CaseRule
\]
\justifies
\vdash \cencode\Context\cmap, \tencode{\tserver\Type}_\address
\using\refrule\CorecRule
\end{prooftree}
\end{multline*}

Note that in this last case it is not necessary to split the stream $\amap$
since the $P$ and $Q$ branches of the server are mutually exclusive (the
reduction rules r-connect and r-done pick one or the other
branch, but not both). A similar thing happens in the encoding of the
applications of , not shown here.

*Validity of encoded typing derivations

Now that we have shown how every typing derivation is encoded into a
derivation, we argue that the encoding preserves validity. More
specifically, a valid typing derivation (<ref>) is
encoded into a valid derivation (<ref>).

To see that this is the case, first observe that there is a one-to-one
correspondence between the infinite branches in the two derivations. From
<ref> we know that every infinite branch in a derivation contains infinitely many applications of concerning the same shared channel $x$ having type $\tserver\Type$ for some
$\Type$. In the encoded derivation, this translates to the existence of a
formula $\tencode{\tserver\Type}$ that occurs infinitely often in the sequents
making up this infinite branch. Now, suppose that the first occurrence of this
formula is associated with some address $\address$. From the encoding of
we can then build the thread

\[
t \eqdef
\tencode{\tserver\Type}_\address,
\tencode{\Bot \branch (\Type \tjoin \tserver\Type)}_{\address i},
\tencode{\Type \tjoin \tserver\Type}_{\address ir},
\tencode{\tserver\Type}_{\address irr},
\dots
\]

which is infinite. Also note that $\InfOften{t} = \set{
\tencode{\tserver\Type}, \tencode{\Bot \branch (\Type \tjoin \tserver\Type)},
\tencode{\Type \tjoin \tserver\Type} }$, that $\minf\InfOften{t} =
\tencode{\tserver\Type}$, and that $\tencode{\tserver\Type}$ is a $\nu$-formula
by <ref>.

In conclusion, $t$ is a $\tnu$-thread (<ref>) as required by the
validity condition for pre-proofs (<ref>).

*Soundness of the type system

Now that we know how to obtain a proof from a well-typed process we observe that each reduction rule of corresponds to one
or more principal reductions in a proof <cit.>.
In particular, the reductions r-close, r-comm and
r-case correspond to exactly one principal reduction in (for $\One/\Bot$, ${\tfork}/{\tjoin}$ and ${\choice}/{\branch}$ respectively),
whereas r-done and t-client correspond to three
subsequent principal reductions in . For example, r-connect
corresponds to the principal reduction $\tmu$/$\tnu$ followed by
${\choice}/{\branch}$ followed by ${\tfork}/{\tjoin}$.

Using this correspondence between and , we can prove
that every process that is well typed in a context of the
form $x : \One$ is weakly terminating.

If $\wtp{P}{x : \One}$ then $P$ is weakly terminating.

Let $a\amap$ be an infinite stream of pairwise distinct atomic addresses.

Every reduction of $P$ can be mimicked by one or more principal reductions
in the proof $\dencode{\wtp{P}{x : \One}}{\extend\x{a}}\amap$.

We know that enjoys cut elimination [8]. In particular,
there cannot be an infinite sequence of principal reductions in a proof <cit.>.

It follows that there is no infinite sequence of reductions starting from
$P$ (using the semantics), that is $P \dreds Q \ndred$ for some

From <ref> we deduce $\wtp{Q}{x : \One}$ and from
<ref> we deduce $Q \pcong \Close\x$.

We conclude $P \wred\pcong \Close\x \nred$. In other words, $P$ is weakly

If $\wtp{P}{x : \One}$ then $P$ is fairly terminating.

Straightforward consequence of

§ EXAMPLE: A COMPARE-AND-SWAP REGISTER

In this section we illustrate a more complex scenario of client-server
interaction that hightlights not only the fact that the server handles
connections sequentially in an unspecified order but also the fact that each
connection may change the server's internal state and affect other connections.

More specifically, we show a modeling of the Compare-and-Swap (CAS) register of
Qian et al. [19] in . A CAS register holds a
boolean value $\True$ or $\False$ and is represented as a server that accepts
connections from clients. Each client sends two boolean values to the server, an
expected value and a desired value. If the expected value matches
the content of the register, then the register is overwritten with the desired
value. Otherwise, the register remains unchanged. We model boolean values as
choices made in some session $y$. For instance, we can model the sending of
$\True$ on $y$ by the selection $\Left\y$ and the sending of $\False$ on $y$ by
the selection $\Right\y$. In fact, in this section we write $\True$ and $\False$
as aliases for the labels $\LeftTag$ and $\RightTag$, respectively.

Below are two definitions for clients that differ for the expected and desired
values they send to the CAS register:

\[
\Let{\CASClient\True\False}{y}{\Select\y\True.\Select\y\False.\Close\y}
\qquad
\Let{\CASClient\False\True}{y}{\Select\y\False.\Select\y\True.\Close\y}
\]

It is easy to see that both definitions are well typed. In particular, we can
derive $\wtp{\Call{\CASClient{b}{c}}{y}}{y : (\One \choice \One) \choice (\One
\choice \One)}$ for every $b,c\in\set{\True,\False}$ with two applications of
and one application of .

We combine two clients in a single pool as by the following definition

\[
\Let\CASClients{x}{
\Cons\x\y{\Call{\CASClient\True\False}\y}
\Cons\x\y{\Call{\CASClient\False\True}\y}
\Nil\x
\]

for which we derive $\wtp{\Call\CASClients\x}{x :
\tclient((\One\choice\One)\choice(\One\choice\One))}$ using and .

For the CAS server we provide two definitions $\CASServer\True$ and
$\CASServer\False$ corresponding to the states in which the register holds the
value $\True$ and $\False$, respectively.

\begin{align*}
\Let{\CASServer\True}{x,z&}{
\begin{array}[t]{@{}l@{}l@{}}
\Server\x\y{&
\begin{array}[t]{@{}l@{}l@{}}
\Case\y{&
\Case\y{
\Wait\y.\Call{\CASServer\True}{x,z}
\Wait\y.\Call{\CASServer\False}{x,z}
\Case\y{
\Wait\y.\Call{\CASServer\True}{x,z}
\Wait\y.\Call{\CASServer\True}{x,z}
\end{array}
\\&
\Select\z\True.\Close\z
\end{array}
\\
\Let{\CASServer\False}{x,z&}{
\begin{array}[t]{@{}l@{}l@{}}
\Server\x\y{&
\begin{array}[t]{@{}l@{}l@{}}
\Case\y{&
\Case\y{
\Wait\y.\Call{\CASServer\False}{x,z}
\Wait\y.\Call{\CASServer\False}{x,z}
\Case\y{
\Wait\y.\Call{\CASServer\True}{x,z}
\Wait\y.\Call{\CASServer\False}{x,z}
\end{array}
\\&
\Select\z\False.\Close\z
\end{array}
\end{align*}

The server in state $b\in\set{\True,\False}$ waits for connections on the shared
channel $x$. If there is no client, the server sends $b$ on $z$ and terminates.
If a client connects, then a session $y$ is established. At this stage the
server performs two input operations to receive the expected and desired values
from the client. If the expected value does \emph{not} match $b$, then the
desired value is ignored and the server recursively invokes itself in the same
state $b$. If the expected value matches $b$, then the server recursively
invokes itself in a state that matches the client's desired value.

It is not difficult to obtain derivations for the judgments
$\wtp{\Call{\CASServer{b}}{x,z}}{x :
\tserver((\Bot\branch\Bot)\branch(\Bot\branch\Bot)), z : \One \choice \One}$ for
every $b\in\set{\True,\False}$. These derivations are valid since every infinite
branch in them goes through an application of \refrule\ServerRule concerning the
channel $x$.
In conclusion, the CAS server is well typed and so is the composition

Note that the process $\Cut\x{\Call\CASClients\x}{\Call{\CASServer\True}{x,z}}$
is not deterministic since it may reduce to either $\Select\z\True.\Close\z$ or
$\Select\z\False.\Close\z$ depending on the order in which clients connect.
Indeed, if $\CASClient\True\False$ connects first, then the state of the
register changes from $\True$ to $\False$ and then the connection with the
second client changes it back from $\False$ to $\True$. If, on the other hand,
$\CASClient\False\True$ connects first (because \refrule{s-pool-comm} is used),
then the initial state of the register does not change and then it is changed
from $\True$ to $\False$ when the client $\CASClient\True\False$ finally

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:

\section{Concluding Remarks}
\label{sec:conclusion}

\CSLL~[19] is a non-deterministic session calculus based
on linear logic in which servers handle multiple client requests sequentially.
In this work we have targeted the problem of proving the termination of
well-typed \CSLL processes. To this aim, we have introduced \CoreCSLL, a variant
of \CSLL closely related to
\muMALL~[3, 8, 2], the infinitary
proof system for multiplicative additive linear logic with fixed points. We have
shown that well-typed \CoreCSLL processes are fairly terminating by encoding
\CoreCSLL typing derivations into \muMALL proofs and using the cut elimination
property of \muMALL. Although fair termination is weaker than termination, it is
strong enough to imply livelock freedom, which was one of the motivations for
proving termination in the original \CSLL work~[19]. In
our work, fair termination is termination under the fairness assumption that
termination is not avoided forever (\cref{thm:fair-termination}). However,
inspection of our proof (\cref{sec:termination}) reveals that the fairness
assumption can be substantially weakened: the fair termination in \CoreCSLL is
reduced to the termination in \DetCSLL, meaning that fair termination in
\CoreCSLL is guaranteed if client requests are handled in order.

\CoreCSLL differs from the original \CSLL in a few ways.
In the interest of simplicity, we have chosen to omit constructs for
modeling (pools of) sequential clients and replicated servers which
are meant to be typed using the traditional exponential
modalities. These features are orthogonal to the ones we are
interested in and we think that they can be accommodated without
substantial challenges following the same technical development
illustrated in the present paper. In fact, the general support to
fixed points in \muMALL allows for this and other extensions, such
as (co)recursive session
types~[18, 7].
Another difference is that \CoreCSLL adopts a reduction semantics that is
completely ordinary for a process calculus. In particular, reductions are
\emph{not} allowed under prefixes, restrictions can\emph{not} be moved beyond
prefixes and (unrelated) prefixes can\emph{not} be swapped. Nonetheless, we are
able to relate the reduction semantics of \CoreCSLL with the cut reduction
strategy of \muMALL since \muMALL proofs, which can be infinite, are reduced
bottom-up. For this reason, we find that \muMALL provides a natural logical
foundation for session calculi based on linear logic.

Just like \CSLL, also \CoreCSLL is related to
\SILLS~[4, 5] and
\HCPND~[16], two session calculi based on linear logic
that allow for races and non-determinism.
In \SILLS, sessions can be \emph{shared} among more than two communicating
processes. Access to a shared session is regulated by means of explicit
acquire/release actions that manifest themselves as special modalities in
session types. The flexibility gained by session sharing may compromise deadlock
freedom, which can be recovered by means of additional type
\HCPND uses bounded exponentials~[11] to implement
client/server interactions in which the amount of channel sharing is known (and
bounded) in advance. Neither \CSLL nor \CoreCSLL require such bounds. For
example, the forwarder process $\Call{\ExpandLink{\tserver\Type}}{x,y}$ in
\cref{ex:forwarder} would be ill typed in \HCPND since the number of clients
that may be willing to connect on $x$ is not known \emph{a priori}.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:

\appendix

\section{Supplement to Section~\ref{sec:types}}
\label{sec:extra-types}

In the proofs of \cref{lem:pcong,lem:sr} below we only focus on the
\emph{derivability} of the typing judgment a structural
pre-congruence or a reduction, without worrying about the
\emph{validity} of the derivation. It is easy to see that validity
is preserved since both structural pre-congruence and reductions
either change a \emph{finite} region of the typing derivation or
\emph{remove} an entire sub-tree of the derivation (as in the case
of \refrule{r-case}). Either way, the fact that every infinite
branch in the residual derivation satisfies the validity conditions
(\cref{def:valid-typing}) follows from the hypothesis that the
initial typing derivation is valid.

\begin{lemma}
\label{lem:pcong}
If $\wtp{P}\Context$ and $P \pcong Q$ then $\wtp{Q}\Context$.
\end{lemma}
\begin{proof}
By induction on the derivation of $P \pcong Q$ and by cases on the last rule
applied. The proof is standard, we only discuss \refrule{s-par-pool} for
illustration purposes.
In this case $P = \Cut\z{\Cons\x\y{P_1}{P_2}}{P_3} \pcong
\Cons\x\y{P_1}{\Cut\z{P_2}{P_3}} = Q$ where $z \not\in
\fn{\Client\x\y.P_1}$.
From \refrule\CutRule we deduce $\wtp{\Cons\x\y{P_1}P_2}{\Context_{12}, z :
\TypeT}$ and $\wtp{P_3}{\Context_{3}, z : \dual\TypeT}$ where $\Context =
\Context_{12}, \Context_3$.
From \refrule\ConsRule and $z\not\in\fn{\Client\x\y.P_1}$ we deduce
$\wtp{P_1}{\Context_1, y : \TypeS}$ and $\wtp{P_2}{\Context_2, x :
\tclient\TypeS, z : \TypeT}$ where $\Context_{12} = \Context_1, \Context_2, x
: \tclient\TypeS$.
We derive $\wtp{\Cut\z{P_2}{P_3}}{\Context_2, \Context_3, x : \tclient\TypeS}$
with one application of \refrule\CutRule.
We conclude $\wtp{Q}\Context$ with one application of \refrule\ConsRule.
\end{proof}

\begin{lemma}
\label{lem:sr}
If $\wtp{P}\Context$ and $P \red Q$ then $\wtp{Q}\Context$.
\end{lemma}
\begin{proof}
By induction on the derivation of $P \red Q$ and by cases on the
last rule applied.

\begin{itemize}
\item \refrule{r-close} Then
$P = \Cut\x{\Close\x}{\Wait\x.Q} \red Q$.  From
\refrule\CutRule, \refrule\CloseRule and \refrule\WaitRule we
deduce $\wtp{\Close\x}{x:\One}$ and
From \refrule\WaitRule we conclude $\wtp{Q}\Context$.

\item \refrule{r-comm} Then
$P = \Cut\x{\Fork\x\y{P_1}{P_2}}{\Join\x\y.P_3} \red
\Cut\y{P_1}{\Cut\x{P_2}{P_3}} = Q$.
From \refrule\CutRule we deduce
$\wtp{\Fork\x\y{P_1}{P_2}}{\Context_{12}, x : \TypeT \tfork
\TypeS}$ and
$\wtp{\Join\x\y.P_3}{\Context_3, x : \dual\TypeT \tjoin
\dual\TypeS}$ where $\Context = \Context_{12}, \Context_3$.
From \refrule\ForkRule we deduce
$\wtp{P_1}{\Context_1, y : \TypeT}$ and
$\wtp{P_2}{\Context_2, x : \TypeS}$ where
$\Context_{12} = \Context_1, \Context_2$.
From \refrule\JoinRule we deduce
$\wtp{P_3}{\Context_3, y : \dual\TypeT, x : \dual\TypeS}$.
We derive
with one application of \refrule\CutRule.
We conclude $\wtp{\Cut\y{P_1}{\Cut\x{P_2}{P_3}}}\Context$ with
one application of \refrule\CutRule.

\item \refrule{r-case} Then
$P = \Cut\x{\Select\x{\InTag_i}.R}{\Case\x{Q_1}{Q_2}} \red
\Cut\x{R}{Q_i} = Q$.
From \refrule\CutRule, \refrule\SelectRule and \refrule\CaseRule
we deduce
\choice\Type_2}$ and
where $\Context = \Context_1,\Context_2$.
From \refrule\SelectRule we deduce
From \refrule\CaseRule we deduce
$\wtp{Q_i}{\Context_2,x:\dual{\Type_i}}$ for $i=1,2$.
We conclude $\wtp{\Cut\x{R}{Q_i}}{\Context}$ with one
application of \refrule\CutRule.

\item \refrule{r-connect} Then $P =
\Cut\x{\Cons\x\y{P_1}P_2}{\Server\x\y{Q_1}{Q_2}} \red
\Cut\y{P_1}{\Cut\x{P_2}{Q_1}} = Q$.
From \refrule\CutRule, \refrule\ConsRule and \refrule\ServerRule we deduce
$\wtp{\Cons\x\y{P_1}P_2}{\Context_{12}, x : \tclient\Type}$ and
$\wtp{\Server\x\y{Q_1}{Q_2}}{\ContextD, x : \tserver\dual\Type}$ where
$\Context = \Context_{12},\ContextD$.
From \refrule\ConsRule we deduce $\wtp{P_1}{\Context_1,y:\Type}$ and
$\wtp{P_2}{\Context_2,x:\tclient\Type}$ where $\Context_{12} =
\Context_1,\Context_2$.
From \refrule\ServerRule we deduce $\wtp{Q_1}{\ContextD, x :
\tserver\dual\Type, y : \dual\Type}$.
We derive $\wtp{\Cut\x{P_2}{Q_1}}{\Context_2, \ContextD, y : \dual\Type}$
with one application of \refrule\CutRule.
We conclude $\wtp{\Cut\y{P_1}{\Cut\x{P_2}{Q_1}}}\Context$ with another
application of \refrule\CutRule.

\item \refrule{r-done} Then $P = \Cut\x{\Nil\x}{\Server\x\y{R}{Q}} \red Q$.
From \refrule\CutRule, \refrule\NilRule and \refrule\ServerRule we deduce
$\wtp{\EmptyPool\x}{x:\tclient\Type}$ and $\wtp{\Server\x\y{R}{Q}}{\Context,
x : \tserver\dual\Type}$.
From \refrule\ServerRule we conclude $\wtp{Q}\Context$.

\item \refrule{r-par} Then
$P = \Cut\x{P_1}{P_2} \red \Cut\x{Q_1}{P_2} = Q$ where
$P_1 \red Q_1$.
From \refrule\CutRule we deduce $\wtp{P_1}{\Context_1,x:\Type}$ and
$\wtp{P_2}{\Context_2,x:\dual\Type}$ where $\Context=\Context_1,\Context_2$.
Using the induction hypothesis we derive $\wtp{Q_1}{\Context_1,x:\Type}$.
We conclude $\wtp{\Cut\x{Q_1}{P_2}}\Context$ with an application of
\refrule\CutRule.

\item \refrule{r-pool} Then $P = \Cons\x\y{P_1}{P_2} \red \Cons\x\y{P_1}{Q_2}
= Q$ where $P_1 \red Q_2$.
From \refrule\ConsRule we deduce $\wtp{P_1}{\Context_1, y : \Type}$ and
$\wtp{P_2}{\Context_2, x : \tclient\Type}$ where $\Context = \Context_1,
\Context_2, x : \tclient\Type$.
Using the induction hypothesis we derive $\wtp{Q_2}{\Context_2, x :
\tclient\Type}$.
We conclude $\wtp{\Cons\x\y{P_1}{Q_2}}\Context$ with an application of
\refrule\ConsRule.

\item \refrule{r-struct} Using the induction hypothesis with two applications
of \cref{lem:pcong}.
\qedhere
\end{itemize}
\end{proof}

In order to prove deadlock freedom it is convenient to introduce \emph{reduction
contexts} to make it easy to refer to unguarded sub-terms of a process. A
reduction context is basically a process with a single hole denoted by $\Hole$.
\[
\textbf{Reduction context}
\qquad
\RC, \RD ~~::=~~ \Hole ~~\mid~~ \Cut\x\RC{P} ~~\mid~~ \Cut\x{P}\RC
\]

Note that holes cannot occur in the tail of client pools, that is
$\Cons\x\y{P}\RC$ is \emph{not} a reduction context even though the tail of a
client pool may reduce by means of \refrule{r-pool}. The point is that, in order
to prove deadlock freedom, it is never necessary to reduce the tail of a client
Hereafter we write $\RC[P]$ for the process obtained by replacing the hole in
$\RC$ with $P$. Note that this notion of replacement may capture some channels
occurring free in $P$.

Before addressing deadlock freedom, we prove the following proximity lemma,
showing that it is always possible to move a restriction close to a process in
which the restricted channel occurs free.

\begin{lemma}
\label{lem:proximity}
If $x\in\fn{P}\setminus(\fn\RC\cup\bn\RC)$ then $\Cut\x{\RC[P]}Q \pcong
\RD[\Cut\x{P}{Q}]$ for some $\RD$.
\end{lemma}
\begin{proof}
By induction on $\RC$ and by cases on its shape. We do not detail symmetric
cases and we assume, without loss of generality, that $\fn{Q} \cap \bn\RC =
\emptyset$.

\begin{itemize}
\item $\RC = \Hole$. We conclude by taking $\RD \eqdef \Hole$ and by
reflexivity of $\pcong$.

\item $\RC = \Cut\y{\RC'}{R}$. Then $x \in \fn{P} \setminus (\fn{\RC'}
\cup \bn{\RC'} \cup \fn{R} \cup \set\y)$. We derive
\[
\begin{array}[b]{r@{~}c@{~}ll}
\Cut\x{\RC[P]}{Q} & = & \Cut\x{\Cut\y{\RC'[P]}R}{Q}
& \text{by definition of $\RC$}
\\
& \pcong & \Cut\x{Q}{\Cut\y{\RC'[P]}{R}}
& \text{by \refrule{s-par-comm}}
\\
& \pcong & \Cut\y{\Cut\x{Q}{\RC'[P]}}{R}
& \text{by \refrule{s-par-assoc} since $x\not\in\fn{R}$, $y\not\in\fn{Q}$}
\\
& \pcong & \Cut\y{\Cut\x{\RC'[P]}Q}{R}
& \text{by \refrule{s-par-comm}}
\\
& \pcong & \Cut\y{\RD'[\Cut\x{P}{Q}]}{R}
& \text{by ind. hyp. for some $\RD'$}
\\
& = & \RD[\Cut\x{P}{Q}]
& \text{by taking $\RD \eqdef \Cut\y{\RD'}R$}
\end{array}
\qedhere
\]
\end{itemize}
\end{proof}

\newcommand{\tdepth}[1]{\mathsf{cd}(#1)}

The next auxiliary result proves that, in a well-typed process, a finite number
of applications of \refrule{s-call} is always sufficient to unfold all of the
process invocations occurring in it. To this aim, we introduce some more
terminology on processes.
We say that $P$ is a \emph{guard} if it is not a parallel composition or a
process invocation. Note that every guard specifies a topmost action on some
channel $x$. In this case, we say that $P$ is an $x$-guard. We say that $P$ is
\emph{unguarded} in $Q$ if $Q = \RC[P]$ for some $\RC$.
We say that $P$ is \emph{unfolded} if $P = \RC[Q]$ implies that $Q$ is not an

\begin{lemma}
\label{lem:unfolded}
If $\wtp{P}\Context$ then there exists an unfolded $Q$ such that $P \pcong
\end{lemma}
\begin{proof}
Let the \emph{call depth} of $P$ be the natural number $\tdepth{P}$
inductively defined as follows:
\[
\tdepth{P} =
\begin{cases}
1 + \tdepth{Q} & \text{if $P = \Call\A{\seqof\x}$ and $\Let\A{\seqof\x}{Q}$} \\
1 + \max\set{\tdepth{P_1},\tdepth{P_2}} & \text{if
$P = \Cut\x{P_1}{P_2}$} \\
0 & \text{otherwise}
\end{cases}
\]

Roughly, $\tdepth{P}$ is the maximum depth in the typing derivation of $P$
where an unguarded guard is encountered.
To see that $\tdepth{P}$ is well defined, recall that in every infinite branch
of a valid typing derivation there are infinitely many applications of
\refrule\ServerRule and that a process of the form $\Server\x\y{Q}{R}$ is a
Therefore, the value of $\tdepth{P}$ is only determined by the portion of
$P$'s derivation tree that stops at each occurrence of a guard. This portion
is finite.
The proof proceeds by induction on $\tdepth{P}$ and by cases on the shape of
$P$. The desired $Q$ is obtained by applying \refrule{s-call} each time an
unguarded invocation is encountered and the induction guarantees that this
rewriting is finite.
\end{proof}

\thmdf*
\begin{proof}
By \cref{lem:unfolded} we may assume, without loss of generality, that $P$
is unfolded. We want to show that there are two $x$-guards in $P$ that can
synchronize. To this aim, let $\threads{P}$ be inductively defined as
\[
\threads{P} =
\begin{cases}
\threads{P_1} + \threads{P_2} & \text{if $P = \Cut\x{P_1}{P_2}$} \\
1 & \text{otherwise}
\end{cases}
\]
and let $\channels{P}$ be inductively defined as
\[
\channels{P} =
\begin{cases}
1 + \channels{P_1} + \channels{P_2} & \text{if $P = \Cut\x{P_1}{P_2}$} \\
0 & \text{otherwise}
\end{cases}
\]

In words, $\threads{P}$ counts the number of unguarded guards in $P$ whereas
$\channels{P}$ counts the number of unguarded restrictions in $P$.
It is easy to prove that $\threads{P} > \channels{P}$. So, there must be at
least one channel name $x$ such that $P$ contains two unguarded $x$-guards.
That is, $P = \RC[\Cut\x{\RC_1[P_1]}{\RC_2[P_2]}]$ and both $P_1$ and $P_2$
are $x$-guards and $x\not\in\fn{\RC_i}\cup\bn{\RC_i}$ for $i=1,2$.
Then we derive
\[
\begin{array}{rcll}
P & = & \RC[\Cut\x{\RC_1[P_1]}{\RC_2[P_2]}]
& \text{by definition of $P$, $P_1$ and $P_2$}
\\
& \pcong & \RC[\RD_1[\Cut\x{P_1}{\RC_2[P_2]}]]
& \text{by \cref{lem:proximity} for some $\RD_1$}
\\
& \pcong & \RC[\RD_1[\Cut\x{\RC_2[P_2]}{P_1}]]
& \text{by \refrule{s-par-comm}}
\\
& \pcong & \RC[\RD_1[\RD_2[\Cut\x{P_2}{P_1}]]]
& \text{by \cref{lem:proximity} for some $\RD_2$}
\end{array}
\]

Now we reason by cases on the shape of $P_1$ and $P_2$, knowing that they
are $x$-guards and that they are well typed in contexts that contain the
associations $x : \Type$ and $x : \dual\Type$ for some $\Type$.
If $P_2 = \Client\x\y.Q$ then $P_1 = \Server\x\y{Q_1}{Q_2}$ and $P$ may
reduce using \refrule{r-connect}. The case in which $P_1 = \Client\x\y.Q$ is
symmetric and can be handled in a similar way with an additional application
of \refrule{s-par-comm}.
The cases in which one of $P_1$ and $P_2$ is $\Nil\x$ can be handled
analogously, deducing that $P$ may reduce using \refrule{r-done}. The only
cases left are when neither $P_1$ nor $P_2$ is a client or $\Nil\x$.
Then, $P_1$ and $P_2$ must be $x$-guards beginning with dual actions which
can synchronize using one of the rules \refrule{r-close}, \refrule{r-comm}
or \refrule{r-case}, possibly with the help of an application of
\refrule{s-par-comm}.
\end{proof}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:

\begin{thebibliography}{10}

[1]
Krzysztof~R. Apt, Nissim Francez, and Shmuel Katz.
\newblock Appraising fairness in languages for distributed programming.
\newblock In {\em Conference Record of the Fourteenth Annual {ACM} Symposium on
Principles of Programming Languages, Munich, Germany, January 21-23, 1987},
pages 189--198. {ACM} Press, 1987.
\newblock \href {https://doi.org/10.1145/41625.41642}

[2]
David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin.
\newblock Bouncing threads for circular and non-wellfounded proofs.
\newblock In {\em Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS, 2022}, 2022.
\newblock URL: \url{https://arxiv.org/abs/2005.08257}.

[3]
David Baelde, Amina Doumane, and Alexis Saurin.
\newblock Infinitary proof theory: the multiplicative additive case.
\newblock In Jean{-}Marc Talbot and Laurent Regnier, editors, {\em 25th {EACSL}
Annual Conference on Computer Science Logic, {CSL} 2016, August 29 -
September 1, 2016, Marseille, France}, volume~62 of {\em LIPIcs}, pages
42:1--42:17. Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik, 2016.
\newblock \href {https://doi.org/10.4230/LIPIcs.CSL.2016.42}

[4]
Stephanie Balzer and Frank Pfenning.
\newblock Manifest sharing with session types.
\newblock {\em Proc. {ACM} Program. Lang.}, 1({ICFP}):37:1--37:29, 2017.
\newblock \href {https://doi.org/10.1145/3110281} {\path{doi:10.1145/3110281}}.

[5]
Stephanie Balzer, Bernardo Toninho, and Frank Pfenning.
\newblock Manifest deadlock-freedom for shared session types.
\newblock In Lu{\'{\i}}s Caires, editor, {\em Programming Languages and Systems
- 28th European Symposium on Programming, {ESOP} 2019, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS} 2019,
Prague, Czech Republic, April 6-11, 2019, Proceedings}, volume 11423 of {\em
Lecture Notes in Computer Science}, pages 611--639. Springer, 2019.
\newblock \href {https://doi.org/10.1007/978-3-030-17184-1\_22}

[6]
Lu{\'{\i}}s Caires, Frank Pfenning, and Bernardo Toninho.
\newblock Linear logic propositions as session types.
\newblock {\em Math. Struct. Comput. Sci.}, 26(3):367--423, 2016.
\newblock \href {https://doi.org/10.1017/S0960129514000218}

[7]
Luca Ciccone and Luca Padovani.
\newblock An infinitary proof theory of linear logic ensuring fair termination
in the linear {\(\pi\)}-calculus.
\newblock In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, {\em
33rd International Conference on Concurrency Theory, {CONCUR} 2022, September
12-16, 2022, Warsaw, Poland}, volume 243 of {\em LIPIcs}, pages 36:1--36:18.
Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik, 2022.
\newblock \href {https://doi.org/10.4230/LIPIcs.CONCUR.2022.36}

[8]
Amina Doumane.
\newblock {\em On the infinitary proof theory of logics with fixed points.
(Th{\'{e}}orie de la d{\'{e}}monstration infinitaire pour les logiques
{\`{a}} points fixes)}.
\newblock PhD thesis, Paris Diderot University, France, 2017.
\newblock URL: \url{https://tel.archives-ouvertes.fr/tel-01676953}.

[9]
Nissim Francez.
\newblock {\em Fairness}.
\newblock Texts and Monographs in Computer Science. Springer, 1986.
\newblock \href {https://doi.org/10.1007/978-1-4612-4886-6}

[10]
Jean{-}Yves Girard and Yves Lafont.
\newblock Linear logic and lazy computation.
\newblock In Hartmut Ehrig, Robert~A. Kowalski, Giorgio Levi, and Ugo
Montanari, editors, {\em TAPSOFT'87: Proceedings of the International Joint
Conference on Theory and Practice of Software Development, Pisa, Italy, March
23-27, 1987, Volume 2: Advanced Seminar on Foundations of Innovative Software
Development {II} and Colloquium on Functional and Logic Programming and
Specifications {(CFLP)}}, volume 250 of {\em Lecture Notes in Computer
Science}, pages 52--66. Springer, 1987.
\newblock \href {https://doi.org/10.1007/BFb0014972}

[11]
Jean{-}Yves Girard, Andre Scedrov, and Philip~J. Scott.
\newblock Bounded linear logic: {A} modular approach to polynomial-time
\newblock {\em Theor. Comput. Sci.}, 97(1):1--66, 1992.
\newblock \href {https://doi.org/10.1016/0304-3975(92)90386-T}

[12]
Orna Grumberg, Nissim Francez, and Shmuel Katz.
\newblock Fair termination of communicating processes.
\newblock In {\em Proceedings of the Third Annual ACM Symposium on Principles
of Distributed Computing}, PODC '84, pages 254--265, New York, NY, USA, 1984.
Association for Computing Machinery.
\newblock \href {https://doi.org/10.1145/800222.806752}

[13]
Kohei Honda.
\newblock Types for dyadic interaction.
\newblock In Eike Best, editor, {\em {CONCUR} '93, 4th International Conference
on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings},
volume 715 of {\em Lecture Notes in Computer Science}, pages 509--523.
Springer, 1993.
\newblock \href {https://doi.org/10.1007/3-540-57208-2\_35}

[14]
Kohei Honda, Vasco~Thudichum Vasconcelos, and Makoto Kubo.
\newblock Language primitives and type discipline for structured
communication-based programming.
\newblock In Chris Hankin, editor, {\em Programming Languages and Systems -
ESOP'98, 7th European Symposium on Programming, Held as Part of the European
Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon,
Portugal, March 28 - April 4, 1998, Proceedings}, volume 1381 of {\em Lecture
Notes in Computer Science}, pages 122--138. Springer, 1998.
\newblock \href {https://doi.org/10.1007/BFb0053567}

[15]
Hans H{\"{u}}ttel, Ivan Lanese, Vasco~T. Vasconcelos, Lu{\'{\i}}s Caires, Marco
Carbone, Pierre{-}Malo Deni{\'{e}}lou, Dimitris Mostrous, Luca Padovani,
Ant{\'{o}}nio Ravara, Emilio Tuosto, Hugo~Torres Vieira, and Gianluigi
\newblock Foundations of session types and behavioural contracts.
\newblock {\em {ACM} Comput. Surv.}, 49(1):3:1--3:36, 2016.
\newblock \href {https://doi.org/10.1145/2873052} {\path{doi:10.1145/2873052}}.

[16]
Wen Kokke, J.~Garrett Morris, and Philip Wadler.
\newblock Towards races in linear logic.
\newblock {\em Log. Methods Comput. Sci.}, 16(4), 2020.
\newblock URL: \url{https://lmcs.episciences.org/6979}.

[17]
Leslie Lamport.
\newblock Fairness and hyperfairness.
\newblock {\em Distributed Comput.}, 13(4):239--245, 2000.
\newblock \href {https://doi.org/10.1007/PL00008921}

[18]
Sam Lindley and J.~Garrett Morris.
\newblock Talking bananas: structural recursion for session types.
\newblock In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, {\em
Proceedings of the 21st {ACM} {SIGPLAN} International Conference on
Functional Programming, {ICFP} 2016, Nara, Japan, September 18-22, 2016},
pages 434--447. {ACM}, 2016.
\newblock \href {https://doi.org/10.1145/2951913.2951921}

[19]
Zesen Qian, G.~A. Kavvos, and Lars Birkedal.
\newblock Client-server sessions in linear logic.
\newblock {\em Proc. {ACM} Program. Lang.}, 5({ICFP}):1--31, 2021.
\newblock \href {https://doi.org/10.1145/3473567} {\path{doi:10.1145/3473567}}.

[20]
Philip Wadler.
\newblock Propositions as sessions.
\newblock {\em J. Funct. Program.}, 24(2-3):384--418, 2014.
\newblock \href {https://doi.org/10.1017/S095679681400001X}

\end{thebibliography}

\end{document}