# SMART: Spatial Modeling Algorithms for Reactions and Transport

Justin G. Laughlin  Department of Mechanical and Aerospace Engineering,
University of California San Diego, La Jolla, CA, USA  Jørgen S. Dokken
Department of Numerical Analysis and Scientific Computing, Simula Research
Laboratory, Oslo, Norway  Henrik N.T. Finsberg  Department of Computational
Physiology, Simula Research Laboratory, Oslo, Norway  Emmet A. Francis
Department of Mechanical and Aerospace Engineering, University of California
San Diego, La Jolla, CA, USA  Christopher T. Lee  Department of Mechanical and
Aerospace Engineering, University of California San Diego, La Jolla, CA, USA
Marie E. Rognes  Department of Numerical Analysis and Scientific Computing,
Simula Research Laboratory, Oslo, Norway  Padmini Rangamani  Department of
Mechanical and Aerospace Engineering, University of California San Diego, La
Jolla, CA, USA

(June 2023)

## Summary

Recent advances in microscopy and 3D reconstruction methods have allowed for
characterization of cellular morphology in unprecedented detail, including the
irregular geometries of intracellular subcompartments such as membrane-bound
organelles. These geometries are now compatible with predictive modeling of
cellular function. Biological cells respond to stimuli through sequences of
chemical reactions generally referred to as _cell signaling pathways_. The
propagation and reaction of chemical substances in cell signaling pathways can
be represented by coupled nonlinear systems of reaction-transport equations.
These reaction pathways include numerous chemical species that react across
boundaries or interfaces (e.g., the cell membrane and membranes of organelles
within the cell) and domains (e.g., the bulk cell volume and the interior of
organelles). Such systems of multi-dimensional partial differential equations
(PDEs) are notoriously difficult to solve because of their high
dimensionality, non-linearities, strong coupling, stiffness, and potential
instabilities. In this work, we describe _Spatial Modeling Algorithms for
Reactions and Transport_ (SMART), a high-performance finite-element-based
simulation package for model specification and numerical simulation of
spatially-varying reaction-transport processes. SMART is based on the FEniCS
finite element library, provides a symbolic representation framework for
specifying reaction pathways, and supports geometries in 2D and 3D including
large and irregular cell geometries obtained from modern ultrastructural
characterization methods.

## Statement of need

SMART has been designed to fulfill the need for an open-source software
capable of modeling cell signaling pathways within complicated cell
geometries, including reactions and transport between different subcellular
surfaces and volumes. In SMART, the user specifies _species, reactions,
compartments, and parameters_ to define a high-level model representation.
This framework uses a similar convention to Systems Biology Markup Language
(SBML, [1]), making the software approachable to a wider user base. SMART
provides features for converting the model representation into appropriate
coupled systems of ordinary differential equations (ODEs) and PDEs, and for
solving these efficiently using finite element and finite difference
discretizations.

SMART has been designed for use by computational biologists and biophysicists.
SMART leverages state-of-the-art finite element software (FEniCS) [2, 3] which
is compatible with a variety of meshing software such as Gmsh [4] and GAMer 2
[5], allowing users to solve nonlinear systems of PDEs within complex cellular
geometries. Moreover, the design of SMART as a FEniCS-based package allows for
ease of extension and integration with additional physics, enabling, e.g.,
coupled simulations of cell signaling and mechanics or electrophysiology.
SMART complements several existing software tools that are used to assemble
and solve equations describing cell signaling networks such as VCell [6, 7],
COPASI [8], and MCell [9].

## Examples of SMART use

SMART offers unique opportunities to examine the behavior of signaling
networks in realistic cell geometries. As a proof of concept, we used SMART to
model a coupled volume-surface reaction-diffusion system on a mesh of a
dendritic spine generated by GAMer 2 (Fig 1, [5]). More recently, we
implemented a detailed model of neuron calcium dynamics in SMART (Fig 2). This
model describes $\mathrm{IP_{3}R}$\- and ryanodine receptor (RyR)-mediated
calcium release following stimulation by neurotransmitters. These SMART
simulations recapitulate the complex dynamics of calcium-induced calcium
release from the endoplasmic reticulum and predict strong spatial gradients of
calcium near regions of calcium release (Fig 2C).

Figure 1:  Simulation of a surface-volume reaction in a realistic dendritic
spine geometry using SMART. A) Diagram of the chosen surface-volume reaction,
in which cytosolic species, A, reacts with a species in the membrane, X, to
produce a new membrane species, B (originally described in [10]). Note that
this is the same reaction used in Example 2 of the SMART demos. B) Geometry-
preserving mesh of a neuronal dendritic spine attached to a portion of the
dendritic shaft, constructed from electron microscopy data of a mouse neuron
using GAMer 2. The mesh contains two domains - the surface, $\Gamma_{PM}$,
which represents the plasma membrane, and the inner volume, $\Omega_{Cyto}$,
which represents the cytosol. C) Concentration of product B on the plasma
membrane at $t=1.0$ s, with the diffusion coefficient of species A ($D_{A}$)
set to 10 $\mathrm{\upmu m^{2}}$/s. D) Range of concentrations of species B
over time for the simulation shown in (C), where the solid lines denote the
minimum and maximum concentrations at each time point and the dotted line
indicates the average concentration. This figure was adapated from Fig 10 in
[5]; additional parameters and details are given in the original paper.
Figure 2:  Model of calcium dynamics in a neuron using SMART (implemented in
Example 6). A) Diagram of the calcium signaling network in the main body
(soma) of a neuron. $\mathrm{IP_{3}}$ production at the plasma membrane (PM)
triggers the opening of $\mathrm{IP_{3}R}$ calcium channels in the endoplasmic
reticulum (ER) membrane, leading to calcium elevations in the cytosol. In
parallel, calcium entry through voltage-gated calcium channels (VGCCs) and
calcium release from the ER through ryanodine receptors (RyRs) also increase
cytosolic calcium levels, while calcium export through the plasma membrane
ATPase (PMCA) and sodium-calcium exchanger (NCX) and pumping of calcium back
into the ER via the sarco-endoplasmic reticulum ATPase (SERCA) counteract
these calcium increases. Calcium rapidly binds to other proteins in the
cytosol such as parvalbumin (PV) and calbindin-D28k (CD28k), which effectively
act as calcium buffers. For the mathematical details of this model, see
Example 6 in the SMART demos. The mesh depicted on the right shows the
”sphere-in-a-sphere” geometry tested in Example 6, in which the inner sphere
corresponds to the ER and the outer region corresponds to the cytosol in a
portion of the neuron soma. B) Plots of the time-dependent activation
functions, corresponding to calcium entry through VGCCs (upper plot) and
$\mathrm{IP_{3}}$ production at the plasma membrane. Patterns of calcium
influx were derived from those used in [11], and $\mathrm{IP_{3}}$ production
was fit to expected values from simulating a larger signaling network of
glutamate-dependent $\mathrm{IP_{3}}$ production. C) Cytosolic and ER calcium
concentrations plotted over the mesh at indicated time points. After the final
”simple spike” of calcium at $t=0.05$ s, $\mathrm{IP_{3}}$ production slowly
leads to a small amount of calcium release from the ER. However, once the
”complex spike” occurs at $t=0.1$ s, a larger amount of calcium is released
from the ER, manifesting as a sharp local gradient around the ER that is
visible at $t=0.111$ s. D) Plots of the average cytosolic calcium (upper plot)
and average ER calcium (lower plot) over time for the simulation shown in (C).
Note that the plots shown in (B) and (D) can be automatically generated by
running Example 6 in the SMART demos.

## Acknowledgements

The authors would like to acknowledge contributions from Yuan Gao and William
Xu during the early development of SMART.

MER acknowledges support and funding from the Research Council of Norway (RCN)
via FRIPRO grant agreement #324239 (EMIx), and the U.S.-Norway Fulbright
Foundation for Educational Exchange. EAF is supported by the National Science
Foundation under Grant #EEC-2127509 to the American Society for Engineering
Education. CTL is supported by a Kavli Institute for Brain and Mind
Postdoctoral Award. JGL, CTL, EAF, and PR further acknowledge support from
AFOSR MURI FA9550-18-1-0051 to PR.

## References

  * [1] James C. Schaff et al.  “SBML Level 3 Package: Spatial Processes, Version 1, Release 1”  In _Journal of Integrative Bioinformatics_ 20.1, 2023, pp. 20220054  DOI: 10.1515/jib-2022-0054
  * [2] “Automated Solution of Differential Equations by the Finite Element Method: The FEniCS Book” 84, Lecture Notes in Computational Science and Engineering  Berlin, Heidelberg: Springer Berlin Heidelberg, 2012  DOI: 10.1007/978-3-642-23099-8
  * [3] Martin Alnæs et al.  “The FEniCS Project Version 1.5”  In _Archive of Numerical Software_ Vol 3 University Library Heidelberg, 2015  DOI: 10.11588/ANS.2015.100.20553
  * [4] Christophe Geuzaine and Jean-François Remacle  “Gmsh: A 3-D Finite Element Mesh Generator with Built-in Pre- and Post-Processing Facilities: THE GMSH PAPER”  In _International Journal for Numerical Methods in Engineering_ 79.11, 2009, pp. 1309–1331  DOI: 10.1002/nme.2579
  * [5] Christopher T. Lee et al.  “3D Mesh Processing Using GAMer 2 to Enable Reaction-Diffusion Simulations in Realistic Cellular Geometries”  In _PLOS Computational Biology_ 16.4, 2020, pp. e1007756  DOI: 10.1371/journal.pcbi.1007756
  * [6] Ann E. Cowan, Ion I. Moraru, James C. Schaff, Boris M. Slepchenko and Leslie M. Loew  “Spatial Modeling of Cell Signaling Networks”  In _Methods in Cell Biology_ 110 Elsevier, 2012, pp. 195–221  DOI: 10.1016/B978-0-12-388403-9.00008-4
  * [7] J. Schaff, C.C. Fink, B. Slepchenko, J.H. Carson and L.M. Loew  “A General Computational Framework for Modeling Cellular Structure and Function”  In _Biophysical Journal_ 73.3, 1997, pp. 1135–1146  DOI: 10.1016/S0006-3495(97)78146-3
  * [8] Stefan Hoops et al.  “COPASI—a COmplex PAthway SImulator”  In _Bioinformatics_ 22.24, 2006, pp. 3067–3074  DOI: 10.1093/bioinformatics/btl485
  * [9] Rex A. Kerr et al.  “Fast Monte Carlo Simulation Methods for Biological Reaction-Diffusion Systems in Solution and on Surfaces”  In _SIAM Journal on Scientific Computing_ 30.6, 2008, pp. 3126–3149  DOI: 10.1137/070692017
  * [10] Padmini Rangamani et al.  “Decoding Information in Cell Shape”  In _Cell_ 154.6, 2013, pp. 1356–1369  DOI: 10.1016/j.cell.2013.08.026
  * [11] Tomokazu Doi, Shinya Kuroda, Takayuki Michikawa and Mitsuo Kawato  “Inositol 1,4,5-Trisphosphate-Dependent Ca 2+ Threshold Dynamics Detect Spike Timing in Cerebellar Purkinje Cells”  In _The Journal of Neuroscience_ 25.4, 2005, pp. 950–961  DOI: 10.1523/JNEUROSCI.2727-04.2005


Termination in Concurrency, Revisited

Joseph W. N. Paulus

University of Groningen
1 Thørväld Circle
The Netherlands

Jorge A. Pérez

University of Groningen
1 Thørväld Circle
The Netherlands

Daniele Nantes-Sobrinho

Imperial College London
1 Thørväld Circle

University of Brasília, Brazil

Termination is a central property in sequential programming models: a term is terminating if all its reduction sequences are finite.
Termination is also important in concurrency in general, and for message-passing programs in particular.
A variety of type systems that enforce termination by typing have been developed.

In this paper, we rigorously compare several type systems for $\pi$-calculus processes from the unifying perspective of termination.
Adopting session types as reference framework, we consider two different type systems: one follows Deng and Sangiorgi's weight-based approach; the other is Caires and Pfenning's Curry-Howard correspondence between linear logic and session types.
Our technical results precisely connect these very different type systems, and shed light on the classes of client/server interactions they admit as correct.

<concept_desc>Theory of computation Process calculi</concept_desc>
<concept_desc>Theory of computation Type structures</concept_desc>

[500]Theory of computation Process calculi
[500]Theory of computation Type structures

§ INTRODUCTION

The purpose of this paper is to present the first comparative study of type systems that enforce termination for message-passing processes in the $\pi$-calculus, the paradigmatic model of concurrency.

Termination is a cornerstone of sequential programming models: a term is terminating if all its reduction sequences are finite.
Termination is also an important property in concurrency in general, and in message-passing programs in particular.
In such a setting, infinite sequences of internal steps are rather undesirable, as they could jeopardize the reliable interaction between a process and its environment.
That is, we would like processes that exhibit infinite sequences of observable actions, possibly intertwined with finite sequences of internal/unobservable steps (i.e., reductions).

In the (un)typed  $\pi$-calculus, infinite behavior can be  expressed via operators for recursion (or recursive definitions) or replication.
We are interested in replication, and in particular in input-guarded replication, denoted $!x(y).P$.
Input-guarded replication neatly captures the essence of servers that are persistently available to spawn interactive behavior upon invocations by concurrent clients.
This way, it   precisely expresses the controlled invocation of (shared) resources.
To understand its operation, let us write $x\langle z\rangle$ to denote an output prefix, intended as an invocation to a server such as $!x(y).P$.
The corresponding reduction rule is then roughly as follows:

$$!x(y).P \pp x\langle z\rangle.Q ~\longrightarrow~ !x(y).P \pp P\substj{z}{y} \pp Q $$

Thus, after a synchronization on $x$, the server $!x(y).P$ continues to be available, and a copy of $P$ is spawned (where $\substj{z}{y}$ denotes the substitution of $y$ with $z$, as usual), enabling interaction with $Q$.

In this setting, an obvious source of non-terminating behaviors is when clients and servers invoke each other indefinitely.
This situation arises, in particular,  when client invocations occur in the body of a server, which can easily trigger infinite “ping-pong” reductions, as in the following process (where $\nil$ denotes inaction):

\begin{equation}
!x(y).x\langle y\rangle.\nil \pp x\langle w\rangle.\nil ~\longrightarrow~ !x(y).x\langle y\rangle.\nil \pp x\langle w\rangle.\nil \pp \nil ~\longrightarrow~ \cdots
\label{eq:ping}
\end{equation}

The challenge of statically ruling out processes such as (<ref>) while enabling expressive client/server interactions has been addressed by multiple authors via various type systems, see, e.g., <cit.>.
Their underlying approaches are vastly diverse.
For instance,
Yoshida et al. <cit.> adopt a type-theoretical approach  based on logical relations and linear action types.
Deng and Sangiorgi <cit.> transport ideas from rewriting systems (well-founded measures) into a $\pi$-calculus with simple types.
Caires and Pfenning's Curry-Howard correspondence between linear logic and session types <cit.> represents yet another approach: their type system enforces termination based purely on proof-theoretical principles, by  interpreting the exponential `$!A$' as the type of a server and by connecting cut elimination with process synchronization.
Several natural questions arise. How do these type disciplines compare? What are their relative strengths? More concretely, are there terminating processes detected as such by one type system but not by some other? If so, where is the difference?

As inviting and intriguing these questions are, a technical approach to a formal comparison is far from obvious.
An immediate obstacle concerns the underlying formal models: all the type systems mentioned above operate on different dialects of the $\pi$-calculus, involving, e.g., synchronous/asynchronous communication, and monadic/polyadic message passing. These differences quickly escalate at the level of the respective type systems, with the presence/absence of linearity unsurprisingly playing a key distinguishing role. How do we even start formulating the intended comparison?

We frame our formal comparison as follows.
As baseline for comparison we take the   $\pi$-calculus processes typable with Vasconcelos's session type system <cit.>.  This is a quite liberal type system, which induces a  broad class of session processes (including non-terminating ones), which is convenient for our purposes.
In the following, this baseline class of processes is denoted $\vaslang$.

We then consider two representative classes of processes, both terminating by typing. One is based on Deng and Sangiorgi's weight-based type system; the other is Caires and Pfenning's linear-logic type system. Because these type systems are so different from Vasconcelos's, to connect them with we require  typed translations. This leads to two classes of terminating processes:

* contains all processes in (i.e., typable under
Vasconcelos's type system) which are also typable (up to a translation) under the weight-based type system.

* contains all processes in which are also typable (up to another translation) by the Curry-Howard correspondence.

This way, because Vasconcelos's  system can type non-terminating processes, both $\lvllang \subset \vaslang$ and $\dilllang \subset \vaslang$ hold by definition.
Our technical contributions are two-fold.

* Because the type systems by Vasconcelos and by Deng and Sangiorgi are so different, to define we develop a new weight-based type system that combines elements from both: it ensures termination by enforcing well-founded measures (as Deng and Sangiorgi's) while accounting for linearity and sessions (as Vasconcelos's). The translation involved in bridging and this new type system determines a technique for ensuring termination of session-typed processes, which is new and of independent interest.

* We prove that $\dilllang \subset \lvllang$
$\lvllang \not \subset \dilllang$, thus determining the exact relationship between  these classes of typed processes.
Our discovery is that there are terminating session-typed processes that are typable with the weight-based approach but not under the Curry-Howard correspondence.
In other words, techniques based on well-founded measures turn out to be more powerful for enforcing termination than proof-theoretical foundations.

Next, we introduce the class .
<Ref> develops the new weight-based type system and <Ref> studies its corresponding class .
The Curry-Howard correspondence for concurrency is recalled in <Ref>, and its corresponding class is presented in <Ref>.
Finally, <Ref> collects concluding remarks.

§ THE CLASS $\VASLANG$ OF SESSION PROCESSES

We present the process language that we shall consider as reference in our comparisons, and its corresponding session type system.
We distinguish between (i) the processes induced by this process model and (ii) the class of well-typed processes (<Ref>); in the following, these classes are denoted by and $\vaslang$, respectively.
We consider the type system by Vasconcelos <cit.>, which ensures communication safety and session fidelity, but not progress/deadlock-freedom nor termination.
Our presentation closely follows <cit.>, pointing out differences where appropriate.

§.§ The Process Model

Let  $x, y, \ldots$ range over variables, denoting channel names (or session endpoints), and $v, v', \ldots$ over values;
for simplicity, the sets of values and variables coincide.

Also, let  $P, Q, \ldots$ range over processes, defined by the grammar of <Ref>, which induces the class .

\[
\begin{aligned}
P,Q ::= &								&& \mbox{(Processes)}\\
&  \vasout{x}{v}{P}				&& \mbox{(output)}
&&  \vasin{q}{x}{y}{P}			&& \mbox{(input)} \\
&  \vaspara{P}{Q}  		  		&& \mbox{(composition)}
&&  \vasres{xy}{P}				&& \mbox{(restriction)} \\
&  \nil	     					&& \mbox{(inaction)} \\
q   ::= &								&& \mbox{(Qualifiers)}\\
& \lin 							&& \mbox{(linear)}
&& \un 							&& \mbox{(unrestricted)}\\
v	::= &								&& \mbox{(Values)}\\
& x								&& \mbox{(variables)}\\
\end{aligned}
\]

Syntax of the session $\pi$-calculus

The output process $\vasout{x}{v}{P}$ sends value $v$ across channel $x$ and then continues as $P$.
In the input process $ \vasin{q}{x}{y}{P}$, the qualifier $q$ can be either $\lin$ (denoting a linear input) or $\un$ (denoting an unrestricted input, i.e., a replicated server).
In either case, $x$ expects to receive a value that will replace free occurrences of $y$ in $P$.
Parallel composition $\vaspara{P}{Q}$ denotes the concurrent execution of processes $P$ and $Q$.
The process $\vasres{xy}{P}$ denotes the restriction of the co-variables $x$ and $y$ with scope $P$. This declares them as dual endpoints, which are expected to behave complementarily to each other.
We write $\res {zv:S} P $ when either $z$ or $v$ have session type $S$ in $P$.
As we will see, a synchronization  always occurs across a pairs of co-variables.
Finally, the inactive process is denoted as $\nil$.

As usual, the set of free variables in a process $P$ is denoted $\fv{P}$, and similarly $\bv{P}$ for bound variables.
The capture-free substitution of the variable $z$ by the value $v$ is denoted as $\substj{v}{z}$. We adopt Barendregt's variable convention.

With respect to <cit.>, the above the process syntax leaves out boolean values, conditional expressions, and labeled choices, which are all inessential for our comparative study of termination.

The reduction relation $\vasred$ of is defined in <Ref>.

[leftmargin = -3mm, rightmargin = -3mm]

\[
\begin{aligned}
\vaspara{P}{Q} &\equiv \vaspara{Q}{P}
\vaspara{P}{\nil} & \equiv P
\\
\vaspara{(\vaspara{P}{Q})}{R} &\equiv \vaspara{P}{(\vaspara{Q}{R})}
\vasres{xy}{\nil} & \equiv \nil
\\
\vasres{xy}\vasres{zw}{P} & \equiv \vasres{zw}\vasres{xy}{P}
\!\!\vasres{xy}{P} & \equiv \vasres{yx}{P}~
\\
\vaspara{(\vasres{xy}P)}{Q} & \equiv \vasres{xy}(\vaspara{P}{Q}) \,\text{[$x,y \not \in \fv{Q}$]}
\end{aligned}
\]

\[
\begin{array}{rll}
\Did{R-LinCom} &
\vasres{xy}{(
\vaspara{\vasout{x}{v}{P}}
\\
& \quad \vasred \vasres{xy}{(
\vaspara{P}

\\[1mm]
\Did{R-UnCom} &
\vasres{xy}{(
\vaspara{\vasout{x}{v}{P}}
\\
& \qquad \vasred
\vasres{xy}{(
\vaspara{P}
\\[1mm]
\Did{R-Par}&		{P\vasred Q}\Longrightarrow
{\vaspara{P}{R} \vasred \vaspara{Q}{R}}
\\[1mm]
\Did{R-Res}&	{P\vasred Q} \Longrightarrow
{\vasres{xy}{P} \vasred \vasres{xy}{Q}}
\\[1mm]
\Did{R-Str}& 	{P\equiv P',\ P\vasred Q,\ Q'\equiv Q}
\Longrightarrow
{P'\vasred Q'} &
%								\vspace{2mm}\\
\end{array}
\]

Reduction semantics for

The reduction semantics for follows standard lines for (session) $\pi$-calculi; it is closed under a structural congruence, denoted $\equiv$, which captures expected principles for parallel composition and restriction.
The reduction rule $\Did{R-LinCom}$ captures the linear communication across co-variables $x$ and $y$, appropriately declared by restriction, in which value $v$ is exchanged.
Similarly, rule $\Did{R-UnCom}$ denotes unrestricted communication across co-variables; in this case, the input prefix is persistent, and remains ready for further synchronizations after reduction.
The contextual rules $\Did{R-Par}$ and $\Did{R-Res}$ express that concurrent processes can reduce within the scope of parallel composition and restriction. Finally, rule $\Did{R-Str}$  denotes that reductions are closed under structural congruence.

§.§ Session Types

We endow with the session type system by Vasconcelos <cit.>, which ensures that well-typed processes respect their protocols but does not ensure deadlock-freedom nor termination guarantees.
With respect to the syntax of types in <cit.>,  we only consider channel endpoint types (no ground types such as ).

The syntax of session types ($T, S, \ldots$) is given in <Ref>.

\[
%	\begin{aligned}
%		q   ::= &								&& \mbox{(Qualifiers)}\\
%				& \lin 							&& \mbox{(linear)}\\
%				& \un 							&& \mbox{(unrestricted)}\\
%		p   ::= &								&& \mbox{(Pretypes)}\\
%				& \vasreci{T}{S}				&& \mbox{(receive)}\\
%				& \vassend{T}{S}				&& \mbox{(send)}\\
%		T,S ::= &								&& \mbox{(Types)}\\
%				& \nilT 						&& \mbox{(termination)}\\
%				& q \ p 						&& \mbox{(qualified pretypes)}\\
%				& a 							&& \mbox{(type variable)}\\
%				& \Rec{a}{T}					&& \mbox{(recursive types)}\\
%		\Gamma ::= &							&& \mbox{(Contexts)}\\
%				& \emptyset						&& \mbox{(empty context)}\\
%				& \Gamma , x:T					&& \mbox{(assumption)}\\
%	\end{aligned}
\begin{aligned}
q   ::= &	&
\mbox{(Qualifiers)}
& &
T,S ::= &	&							 \mbox{(Types)} &&
\\
& \lin 							& \mbox{(linear)}
& & &
\nilT 						& \mbox{(termination)}
\\
& \un 							& \mbox{(unrestricted)}
& & & q \ p  & \mbox{(pretypes)}
\\
p   ::= &								& \mbox{(Pretypes)}
& & &
a & \mbox{(type variable)}
\\
& \vasreci{T}{S}				& \mbox{(receive)}
& & &
\Rec{a}{T}	 & \mbox{(recursive types)}
\\
& \vassend{T}{S}				& \mbox{(send)}
& & &
\\
\Gamma	 ::= &  						& \mbox{(Contexts)}
& & & &
\\
& \emptyset						& \mbox{(empty)}
& & & &
\\
& \Gamma , x:T
& \mbox{(assumption)} &
\end{aligned}
\]

Session Types of

Session types $T, S$ describe protocols as sequences of actions for an endpoint; they do not admit the parallel usage of an endpoint.
They have the following forms:

* Type $\nilT$ is given to an endpoint with a completed protocol.

* Type $ q \ p $ denotes pre-type $p$ with qualifier $q$, which indicates either a linear or an unrestricted behavior ($\lin$ and $\un$, respectively).
The pre-type $\wn T.S$ is given to an endpoint that first receives a value of type $T$ and then continues according to type $S$.
Dually, the pre-type $\oc T.S$ is intended for an endpoint that first outputs a value of type $T$ and then continues according to  $S$.

* Type $\Rec{a}{T}$ is a recursive type, with type variable $a$. A recursive type is required to be contractive, i.e., it contains no subexpression of type $\Rec{a_1}\ldots \Rec{a_n}a_1$; and $a$ is bound with scope $T$. Notions of bound and free type variables, alpha-conversion and capture-avoiding substitutions (denoted $\substj{S}{a}$) is defined as usual. Type equality is based on regular infinite trees <cit.>.

Recursive types that are tail-recursive are expressive enough to type servers and clients; we have a dedicated notation for them.

[Server and Client Types]
We shall write $\recur{\wn T}$ to denote the server type $ \Rec{a}{\un\  \wn T.a}$, where variable $a$ does not occur in $T$.
Similarly, we write $\recur{\oc T}$ to denote the client type $ \Rec{a}{\un\  \oc T.a}$

In the following, we shall work  with tail-recursive types only.
A central notion in session-based concurrency is  duality,
which relates session types offering opposite (i.e., complementary) behaviors; it stands at the basis of communication safety and session fidelity.

Given a (tail-recursive) session type $T$, its dual type $\dual{T}$ is defined as follows:

=          T.S    =    T .S       T    =     T

q  p    =    q  p
T.S    =    T.S
T    =    T

We now collect definitions and results from <cit.> that will lead to state the main properties of typable processes.

We consider two predicates on types, denoted $\contlin{T}$ and $\contun{T}$, defined as follows:

* $\contun{T}$ if and only if $T = \nilT$ or $T = \un \ p$.

* $\contlin{T}$ if and only if $\ttrue$.

The definition extends to contexts as follows: we write
$q(\Gamma)$ if and only if $x:T \in \Gamma$ implies $q(T)$.

This way, to express that $T$ defines strictly linear behavior we write $\neg \contun{T}$ (and similarly for a context $\Gamma$).
The following notation is useful to separate the linear and unrestricted portions of a context:

We write $\Gamma \vaslinunsplit \Gamma'$ if $\contun{\Gamma} \land \neg \contun{\Gamma'}$.

The split and update operations on contexts, denoted $\contcomp$ and $+$, are defined as follows.

Γ_1 Γ_2 = Γ
Γ, x:T = ( Γ_1 , x:T ) ( Γ_2 , x: T )

Γ_1 Γ_2 = Γ
Γ, x:   p = (Γ_1 , x:   p) Γ_2

Γ_1 Γ_2 = Γ
Γ, x:   p = Γ_1 ( Γ_2 , x:  p )

x:U ∉Γ
Γ+ x:T = Γ, x:T

( Γ, x:T ) + x:T = ( Γ, x:T  )

The typing system considers two kinds of judgments, for processes and for variables, denoted  $\Gamma \st P$ and $\Gamma\st x:T$, respectively.
We write $~ \st P$ when $\Gamma$ is empty.
The typing rules are given in <Ref>.

We will explain Rule In: it  is parametric on the qualifiers $q_1$ and $q_2$  and  covers three different behaviours depending on whether $q_i$ is $\lin$ or $\un$, for $i=1,2$. In the case $q_1=\lin$, to prove $\Gamma_1 \contcomp \Gamma_2 \st\lin\ x\inp y.P$, we need to prove $\Gamma_1 \st x: q_2 \wn T.S $ and $ (\Gamma_2 + x: S), y:T \st P$; note  that $\lin (\Gamma_1\contcomp \Gamma_2)$ is true, by <Ref>.   In the case $q_2=\lin$, both judgments hold if $\Gamma_1=\Gamma_1',  x: \lin \wn T.S$, the assignment $x: \lin \wn T.S$ does not occur in $\Gamma_2$, by <Ref>,  and $x:S$ is added to $\Gamma_2$ for the continuation.
Differently, when $q_2=\un$, both judgments hold if $\Gamma_1=\Gamma_1',  x: \recur{\wn T}$, the assignment $x: \recur{\wn T}$ also occurs in $\Gamma_2$ which with the addition of $x:S$ in $\Gamma_2$ implies $S = \recur{\wn T}$. Notice that the case $q_1=\un$ and $q_2=\lin$ is not possible since $\un (\Gamma_1\contcomp \Gamma_2)$ implies that all assignments in $\Gamma_1\contcomp \Gamma_2$ have types $\nilT$ or with `$\un$'; thus, in that case we cannot prove $\Gamma_1 \st x: \lin \wn T.S $.

Similarly, Rule Out is parametric on the qualifier $q$.

* [ left = Var ] Γ
Γ, x:T x:T

* [ left = Nil ] Γ

*[ left =Par ] Γ_1 P
Γ_2 Q
Γ_1 Γ_2 P Q

*[ left =Res ] Γ, x:T ,y: T P
Γxy P

[In ] q_1(Γ_1 Γ_2 )
Γ_1 x: q_2 T.S
(Γ_2 + x: S), y:T P
Γ_1 Γ_2 q_1 xy.P

* [ left = Out ] Γ_1 x: q T.S
Γ_2 v:T
Γ_3 + x:S P
Γ_1 Γ_2 Γ_3 xv.P

Typing rules for (cf. <cit.>).

The main property of the type system concerns well-formed processes, which are defined next.

A redex is a process of the form $ \vasin{q}{x}{v}{P} \pp \vasout{y}{z}{Q}$.
Processes of the form $ \vasin{q}{x}{v}{P}$ and $\vasout{y}{z}{Q}$ have prefix $x$ and $y$, respectively.

A process is well-formed if, for each of its structurally congruent processes of the form $ \res {x_1y_1} \cdots \res {x_ny_n} (P \pp Q \pp R) $, the following conditions hold. (1) If $P$ and $Q$ are processes prefixed at the same variable, then they are of
the same nature (input, output). (2) If $P$ is prefixed at $x_1$ and $Q$ is prefixed at $y_1$ then $P \pp Q$ is a redex.

The type system satisfies the following properties (see <cit.> for details):

* If $\Gamma \st P$ and $P \equiv Q$, then $\Gamma \st Q$.

* If $\Gamma \st P$ and $P \vasred  Q$, then $\Gamma \st Q$.

* If $~\st P$ then $P$ is well-formed.

For technical convenience, we rely on the refined typing rules for input and output in <Ref>, which are equivalent (but more fine-grained) than those in <Ref>.

[Lin-In_1 ]
Γ_1 , x : TS x: TS

Γ_2 , x: S , y : T P
Γ_1 , x: TS Γ_2 xyP

* [ left = Lin-In_2 ]
Γ_1 , x: T x: T

Γ_2 , x: T , y : T P

(Γ_1 , x: T) (Γ_2 , x: T) xyP

* [ left = Un-In ]
Γx: T

Γ, y : T P

* [ left = Un-Out ]
Γ_1 x: T
Γ_2 v: T

Γ_3 P

Γ_1 Γ_2 Γ_3 xvP

[Lin-Out ]
Γ_1 x:  TS
Γ_2 v: T

Γ_3, x:S P

Γ_1 Γ_2 Γ_3 xvP

Refined typing rules for input and output.

We close this section by defining the class of processes .

We define $ \vaslang = \{ P \in \vasco \mid  \exists \Gamma \ s.t. \ \Gamma \st P  \}$.

[A Non-Terminating Process in ]

Consider the process $P_{\ref{ex:infinite}} =  \vasres{xy}{( \vaspara{\vasout{y}{w}{\nil}}{\vasin{\un}{x}{z}{\vasout{y}{w}{\nil}}} )}$,   which invokes itself ad infinitum.
Process $P_{\ref{ex:infinite}}$ is in $\vaslang$ because $w: \nilT \st P_{\ref{ex:infinite}}$ holds with the following derivation:

Γyw xzyw

w: xy( ywxzyw )

with 	 $  \Gamma = x:\recur{\wn \nilT} , y: \recur{\oc \nilT}, w: \nilT $ and $\Pi$ is the derivation

Γ' y:

Γ' w:

Γ' yw

with $ \Gamma' = x:\recur{\wn \nilT} , y: \recur{\oc \nilT}, w: \nilT, z: \nilT $.

§ A WEIGHT-BASED APPROACH TO TERMINATING PROCESSES

We move on to consider a type system that ensures termination for a class of $\pi$-calculus processes.
Following Deng and Sangiorgi <cit.>, the type system uses weights (or levels) to avoid infinite reduction sequences.
This type system will induce a class of terminating  $\vasco$ processes, denoted (<Ref>), obtained via appropriate translations on processes and types.
To ease the definition of such translations, here we define a type system that mildly modifies the system of <cit.> to account for linearity and synchronous/polyadic (tuple-based) communication.
Our main result is that the weight-based system ensures termination (<Ref>).

§.§ Processes

We introduce a process model for the weight-based type system, denoted , formally defined next.
In the following, we write $\tilde{y}$ to stand for the finite tuple $y_1,\cdots, y_n$.

The syntax of processes is given by the grammar in <Ref> (top).

is designed to stand in between and the process model in <cit.>.
Communication in is polyadic, i.e., exchanges involve a tuple of names, rather than a single name as in  <Ref> and <cit.>.
We shall often consider tuples of length two (i.e., dyadic communication), as this suffices for a continuation-passing encoding of sessions <cit.>.
Another difference with respect to <cit.> is that inputs can be linear or  unrestricted; this will facilitate the formal connection with and its type system.
The role of linearity is more prominent at the level of types, defined later on.

We give the operational semantics of in terms of the (early)
labeled transition system (LTS), with the following labels for input, output, bound output, and silent transitions (synchronizations):

$$\alpha ::= x(\tilde{v}) \,|\, \ov x\out { \tilde{y} } \,|\, \res {y,\widetilde{b}}\ov x\out { \tilde{v} } \,|\, \tau $$

The rules, given in <Ref>, are standard. Rules Par and Tau can be applied symmetrically across parallel composition.

[In ]
xyzP x ṽ Pv_1y_1v_2y_2

[Par ] P α P'
α ∩Q = ∅
P Q α P'Q

[Res ] P  α P'
x ∉α
xP  α xP'

[Rep ]
x  ỹ .P x  ṽ  x  ỹ.P  Pv_1y_1

[Out ]
xyzP  x ỹ   P

[Tau ] P   bx ṽ   P'
Q  x ṽ   Q'
b ∩Q = ∅
P Q  τ b (P'Q')

[Open ] P  bx ṽ   P'
y ∈(v_1 ∪v_2) - { b , x }
yP  y,bx ṽ   P'

An LTS for

§.§ Types

The syntax of weight-based types for is given by the grammar in <Ref> (bottom).

As in <cit.>, our link types  for are simple, i.e., they do not admit the sequencing of actions enabled by session types.
Our syntax of types extends that in <cit.> to account for (i) dyadic communication and (ii) explicit types for clients and servers.
Concerning (ii), we purposefully adopt the tail-recursive types for clients and servers defined for , rather than more general recursive types.

\[
\begin{aligned}
P,Q ::= &								&& \mbox{(Processes)}\\
&  \lvlout{x}{y_1}{y_2}{P}		&& \mbox{(output)}
%&  \ov x^{\un} \out { y^q,z^p }.P	&& \mbox{(unrestricted output)}\\
&&  \lvlin{x}{y_1}{y_2}{P}					&& \mbox{(linear input)}
\\
& P \pp Q  	    		  		&& \mbox{(parallel)}
&&  \lvlserv{x}{y_1}{y_2}{P}			&& \mbox{(server)}\\
%&  \ov x^{p} \out { y^q,z^p }.P		&& \mbox{(output)}\\
%&  \ov x^{\un} \out { y^q,z^p }.P	&& \mbox{(unrestricted output)}\\
%&  x^p\inp {y^q , z^p}.P				&& \mbox{(linear input)}\\
%&  \bang x^p \inp {y^q , z^p }.P		&& \mbox{(unrestricted input)}\\
& \res {x}P						&& \mbox{(restriction)}
&& \nil	     					&& \mbox{(inaction)}\\
\end{aligned}
\]

\[
\begin{aligned}
S,T,V,L ::= &								&& \mbox{(Link Types)}\\
%		& V								&& \mbox{(value)} \\
%		& L								&& \mbox{(link)} \\
%V	::= &								&& \mbox{(value types)}\\
%		& L								&& \mbox{(link)}\\
%& 								&& \mbox{(reserved for any other types such as bool, nat)}\\
%L   ::= &								&& \mbox{(link types)}\\
& \lvlint{n}{V_1}{V_2}			&& \mbox{(linear input type)}\\
& \lvloutt{n}{V_1}{V_2}			&& \mbox{(linear output type)}\\
& \lvlunst{n}{V}				&& \mbox{(unrestricted server type)}\\
& \lvlunct{n}{V}				&& \mbox{(unrestricted client type)}\\
%& q \#^n \widetilde{V} =
%	\begin{cases}
%		q = \ast \quad \widetilde{V} = V \\
%		q = \circ \quad \widetilde{V} = (V_1 , V_2)
%	\end{cases}								&&
%	\begin{aligned}
%	& \mbox{(unrestricted link type)} \\
%	& \mbox{(linear link type)}
%	\end{aligned}
%& \level{n}{V_1}{V_2} 			&& \mbox{(linear comunication)}\\
%& \rlevel{n}{V}	 				&& \mbox{(unrestricted comunication)}\\
& \lvlnilT							&& \mbox{(termination)}
%v	::= &								&& \mbox{(Values)}\\
%		& x								&& \mbox{(variables)}\\
\\
n ::= & ~1, 2, \cdots && \mbox{(weights)}
\end{aligned}
\]

Syntax of processes and types for .

We introduce some notions borrowed from the  type system from <Ref>: duality, contexts, predicates on types, operations on contexts.

Duality on linked types is defined as:

\[
\begin{aligned}
\dual{\lvlint{n}{V_1}{V_2}}	& = \lvloutt{n}{\dual{V_1}}{\dual{V_2}}		&
\dual{\lvloutt{n}{V_1}{V_2}} & = \lvlint{n}{\dual{V_1}}{\dual{V_2}}	& \dual{\lvlnilT} & = \lvlnilT
\\
\dual{\lvlunst{n}{V}} & = \lvlunct{n}{\dual{V}}
\dual{\lvlunct{n}{V}} & = \lvlunst{n}{\dual{V}}
%\dual{\lvlnilT} & = \lvlnilT\\
%\tilde{\dual{V}} & = \dual{V_1} , \dual{V_2} \quad \text{where } \tilde{V} = V_1 , V_2\\
\end{aligned}
\]

Contexts are given by the grammar:

\[
\Gamma , \Delta :: = \cdot \sep \Gamma , x:V \sep \Gamma , x:\dualjoin{V}{\dual{V}}
\]

where $\Gamma , x:L$ and $\Gamma , x:\dualjoin{L}{\dual{L}}$ imply $x \not \in \dom{\Gamma}$.

Following the sorts of <cit.>, the assignment
$x:\dualjoin{L}{\dual{L}}$ denotes the pairing of $x$  with two complementary protocols, where $\dualjoin{L}{\dual{L}} = \dualjoin{\dual{L}}{L}$.
We use xL to stand for $x:\dualjoin{L}{\dual{L}}$ when $L$ is the main object of interest.
We write $x\lvlass T $ if either $x:T$ or $x::T$ holds (i.e., $\lvlass \in \{ : , :: \}$).

Predicate $\contun{T}$ holds if $T = \lvlunst{n}{V}$, $T = \lvlunct{n}{V}$, $T = \lvlnilT$, or x:LL with $\contun{L}$. We write $\contun{\Gamma}$ if $\contun{T}$ holds for every $x \lvlass T \in \Gamma$.

Following <Ref>, the following definitions
gives a relation to split contexts into two parts.

The relation $\contcomp$ on contexts is defined in <Ref>.

Γ_1 Γ_2 = Γ
Γ, x: T = ( Γ_1 , x: T  ) ( Γ_2 , x: T  )

Γ_1 Γ_2 = Γ
Γ, x:VV = ( Γ_1 , x:VV  ) ( Γ_2 , x:VV  )

Γ_1 Γ_2 = Γ
Γ, x:VV = (Γ_1 , x: V) (Γ_2 , x: V)

Γ_1 Γ_2 = Γ
Γ, x:VV = (Γ_1 , x:VV) Γ_2

Γ_1 Γ_2 = Γ
Γ, x:VV = Γ_1  (Γ_2 , x:VV)

Γ_1 Γ_2 = Γ
Γ, x: T = (Γ_1 , x: T) Γ_2

Γ_1 Γ_2 = Γ
Γ, x: T = Γ_1 ( Γ_2 , x: T )

Splitting of Contexts for

We now introduce notions on processes that are essential to Deng and Sangiorgi's approach to termination by typing.

Let $\mathcal{N}$ denote the set of all names.
We define the function $\levelof{\cdot}: \mathcal{N} \to \mathbb{N}$ to map names of a process (free and bound) to naturals.
We assume $\alpha$-conversion is silently used to avoid name capture and ensure uniqueness of bound names.
Given a (typed) process, we define this function as follows:

\levelof{x} = \begin{cases}
%	n & \text{if $x \diamond \lvlint{n}{V_1}{V_2},x\diamond\lvloutt{n}{V_1}{V_2} , x\diamond\lvlunst{n}{V} $ or $x\diamond\lvlunct{n}{V} $}
n & \text{if $x : T$ or $x ::T$}
\\
& \text{with $T \in \{\lvlint{n}{V_1}{V_2},\lvloutt{n}{V_1}{V_2}, \lvlunst{n}{V}, \lvlunct{n}{V}\}$}
\\
m & \text{if $x: \lvlnilT$, for any $m \in \mathbb{N}$}
\end{cases}

Given a process $P$, the set of names with active outputs $\outsubj{P}$ is  defined inductively:

\[
\begin{aligned}
\outsubj{\lvloutpoly{x}{y}{z}{P}} & = \{x\} \cup \outsubj{P}
\outsubj{\lvlinpoly{x}{y}{z}{P}} & = \outsubj{P}\\
\outsubj{P \pp Q } & = \outsubj{P} \cup \outsubj{Q}
\outsubj{\res {x}P	} & = \outsubj{P}\\
\outsubj{\nil} & = \emptyset
\outsubj{\lvlservpoly{x}{y}{z}{P}} & = \emptyset
\end{aligned}
\]

[Var_1 ] Γ
Γ, x:V x:V

[Var_2 ] Γ
Γ, x: VV x:V

[Nil ] Γ

[Par ]Γ_1 P
Γ_2 Q
Γ_1 Γ_2 P Q

[Res ] Γ, x: VV  P

* [ left = Lin-In_1 ] Γ_1 , x: nV_1V_2 x: nV_1V_2
Γ_2 ,  y_1:V_1, y_2:V_2 P
x = y_2
Γ_1 , x: nV_1V_2 Γ_2  xy_1y_2P

* [ left = Lin-In_2 ]
Γ_1 , x: nV x: nV

Γ_2 , x: nV , y_1:V , y_2: P
( Γ_1 , x: nV) (Γ_2 , x: nV) xy_1y_2P

* [ left = Lin-In_3 ]
Γ, xnV x:nV

Γ, x nV ,   y_1:V  , y_2: P
Γ, xnV xy_1y_2P

* [ left = Lin-Out ]
Γ_1 ,  x: nV_1V_2 x: nV_1V_2

Γ_2 , y_1:V_1 y_1:V_1

Γ_3 , y_2:V_2 P
x = y_2
(Γ_1 , x: nV_1V_2) (Γ_2 , y_1:V_1) (Γ_3, y_2 V_2 ) xy_1y_2P

* [ left = Un-Out_1 ]
Γ_1 , x:  nV x:  nV

Γ_2, x:  nV , y: V y: V

Γ_3, x:  nV , y_2: P

( Γ_1 , x:  nV )(Γ_2, x:  nV , y: V) (Γ_3, x:  nV)

* [ left = Un-Out_2 ]
Γ_1, x nV x:  nV

Γ_2, x nV , y: V y: V

Γ_3 , x nV , y_2: P

(Γ_1 , x nV) (Γ_2, x nV , y: V) (Γ_3, x nV) xy_1y_2P

* [ left = Un-In_1 ]
Γ, x: nV x: nV

Γ, x: nV, y_1:V , y_2: P
∀b ∈P,  b < n
Γ, x: nV xy_1y_2P

* [ left = Un-In_2 ]
Γ, x nV x: nV

Γ, x nV, y_1:V , y_2: P
∀b ∈P,  b < n
Γ, xnV xy_1y_2P

Typing rules for

Typing judgments are of the form $\Gamma \lt P$, with corresponding typing given in <Ref>.

Typability is contingent on a level function: we say a process $P$ is well-typed if there exists a level function $\levelof{\cdot}$ such that a typing derivation $\Gamma \lt P$ holds, for some $\Gamma$.

We comment on some of the rules in <Ref> for , contrasting them with those in <Ref> for .
Rule Var_1 is similar to rule Var.
Rule Var_2 is the corresponding rule for complementary interaction:   if $x:\dualjoin{V}{\dual{V}}$, then we can assign the type $x:V$. Intuitively, name $x$ encapsulates the types of its two endpoints, denoted as $V$ and $\dual{V}$. As long as $x$ respects one of these types, the channel is considered correctly typed.

Rule Lin-In_1 acts as the linear counterpart to In. Importantly, there is no direct counterpart for $x$ as a linear complementary interaction. Instead, the context split $\Gamma , x:\dualjoin{V}{\dual{V}} = (\Gamma_1 , x:{V}) \contcomp (\Gamma_2 , x:{\dual{V}})$ allows for the application of rule Lin-In_1. This structural mechanism operates silently within the rules where $V$ is linear, achieved through context split. As a result, this disallows linear channels from consuming linear complementary interactions.

Rules Lin-In_2 and Lin-In_3, the first with `:' and the second with `::',  are  counterparts to rule In for  unrestricted types with linear qualifier.
Similarly, Lin-Out, Un-Out_1, and Un-Out_2 represent the rule Out.
Furthermore, Un-In_1 and Un-In_2 are the unrestricted counterparts to rule In with unrestricted qualifier.
These rules adopt the main condition from <cit.>, i.e., the weight of types of the active outputs must be strictly less than the weight of the type of the channel of the server providing them.
Finally, rule Res types a restricted channel through a complementary interaction.

We state the type preservation property:

Suppose $\Gamma \lt P$ for a level function $l$. If $ P \lts{\tau} P' $ then $\Gamma \lt P'$ for the same level function $l$.

§.§ Termination by Typing

A process terminates if all its reduction sequences are finite.
We show that our formulation of the type system in <cit.> also enforces termination by typing. The proof follows the same lines as in <cit.>:
a weight is associated with a well-typed process; this weight is then shown to strictly reduce when the the process synchronizes.
The weight is actually a vector constructed from the observable active outputs  of a channel within a typed process.

We define vectors and their operations:

* Given $k \geq 1$, we write $\zerovec_i$ to denote the vector $\langle n_k , n_{k-1} , \cdots ,  n_1  \rangle $ where $n_i = 1$ and $ n_j = 0$ for every other $j$. Also, $\zerovec$ denotes the zero vector where  $n_i = 0$ for every $i$.

* Given vectors $v_1 =\langle n_k , n_{k-1} ,\cdots ,  n_1  \rangle$ and $v_2 = \langle m_l , m_{l-1}  ,\cdots ,  m_1  \rangle $,  with $k \geq l$, the sum  $v_1+v_2$ is defined in two steps.
Firstly, if $k > l$ then the shorter vector $v_2$ is extended into $v'_2$ by adding  zeroes to match the size of $v_1$, i.e., $v'_2 =\langle m_k , m_{k-1} ,\cdots , m_l  ,\cdots ,  m_1  \rangle $, with $ \langle m_k , m_{k-1} ,\cdots , m_{l+1} \rangle = \zerovec$.
Then, addition of $ v_1 $ and $ v'_2 $ is applied pointwise.

* Given vectors $v_1 = \langle n_k , n_{k-1} ,\cdots ,  n_1 \rangle$ and $v_2 = \langle m_k , m_{k-1} ,\cdots ,  m_1 \rangle$ of equal size $k$, the ordering $v_1 \wtless v_2$ is defined iff $\exists i \leq k, \ n_i < m_i $ and $\forall j > i, \ n_j = m_j$.

Using vectors, we define the weight of a well-typed process:

Given a well-typed process $P$ with level function $l$, the weight of  $P$ is the vector defined inductively as:

\[
\begin{aligned}
\weight{\nil} & = 0 &
\weight{\bang x \inp { \tilde{y}}.P	}&  = 0
\\
\weight{x\inp { \tilde{y}}.P} & = \weight{P} &
\weight{\ov x\out { \tilde{y} }.P} & = \weight{P} + \zerovec_{\levelof{x}}
\\
\weight{P \pp Q} & = \weight{P} + \weight{Q} &
\weight{\res {x}P} & = \weight{P} &
\end{aligned}
\]

We have the following  results, whose proof is as in <cit.>:

If $ \Gamma \lt P $ and $ P \lts{\tau} P' $ then $ \weight{P'} \wtless \weight{P}$.

If $\Gamma \lt P$ then $P$ terminates.

§ : A CLASS OF TERMINATING PROCESSES

Here we define and study , a class of terminating processes induced by the weight-based type system given in <Ref>, which leverages
translations on processes and types/contexts, denoted $\sttoltp{\cdot}{}$ and $\sttoltt{\cdot}{l}{}$, respectively.
Concretely, is defined as follows:

We define:

$$ \lvllang = \{ P \in \vasco \mid  \exists \Gamma , l \ s.t. \ (\Gamma \st P) \land  \ %\sttoltj{\Gamma \st P}{l}{} =
\sttoltt{\Gamma}{l}{} \lt \sttoltp{P}{}     \} $$

Hence, contains those processes from $\vaslang$ (<Ref>) whose translation gives typable $\pilvl$ processes.
By <Ref>,   $\lvllang$ thus provides a characterization of terminating processes in $\vaslang$.
In the following we formally define the translations $\sttoltp{\cdot}{}$ and $\sttoltt{\cdot}{l}{}$, and establish their main properties.
Our main result is that $\lvllang \subset \vaslang$ (<Ref>): there are typable processes in $\vaslang$ which are not terminating under the weight-based approach.

§.§ The Typed Translation

Our translation is typed, i.e., the translation of a process depends on its associated (session) types.
We first present the translation on processes and types separately; then, we   combine them to define the translation of a typing judgment.

The translation   $\sttoltp{\cdot}{}: \vasco \to \pilvl $ is given in <Ref> (top), where we assume $z$ is fresh.

We discuss some interesting cases in the translation of processes:

* The shape of process $\sttoltp{  \vasin{\lin}{x}{y}{P}  }{} $ depends on whether  $x$ has a linear or an unrestricted type: this is due to rule $\vastype{In}$ (<Ref>) which depends on a qualifier $q_2$ that can be linear or unrestricted. If $x: \lin \wn T.S$ then the translation is  $\lvlin{x}{y}{z}{\sttoltp{P\substj{z}{x}}{}}$, with the continuation along $z$; otherwise, in case $x: \recur{\wn T}$, the translation is $\lvlin{x}{y}{z}{\sttoltp{P}{}}$, since there is no continuation in $x$, as explained in the description of rule In in <Ref>.

* The process $\sttoltp{   \vasin{\un}{x}{y}{P}  }{} $ is simply an unrestricted input process $\lvlserv{x}{y}{z}{\sttoltp{P}{}} $.

* The process $\sttoltp{ \vasout{x}{y}{P}  }{} $, the translation of a bound send, also depends on the type of $x$ and the justification for it is similar to the translation of linear inputs described above.

* The process $ \sttoltp{\res {xy}P}{}  $ is simply $ \res {z} \sttoltp{P\substj{z}{x}\substj{z}{y}}{}$: the co-variables $x,y$ are replaced by the restricted (fresh) name $z$. The duality between the types of $x$ and $y$, say $x:L$ and $y:\dual{L}$, must be preserved by the type of $z$ in $\pilvl$. This correspondence will become evident when discussing the translation of judgements (<Ref>).

\[
\begin{aligned}
\sttoltp{ \nil  }{} &=  \nil  \\
\sttoltp{  P \pp Q  }{} 	&=  \sttoltp{P}{} \pp \sttoltp{Q}{}  \\
\sttoltp{  \res {xy} P  }{} 	&=   \res {z} \sttoltp{P\substj{z}{x}\substj{z}{y}}{}  \\
\sttoltp{  \vasin{\lin}{x}{y}{P}  }{} 	&=
\begin{cases}
\lvlin{x}{y}{z}{\sttoltp{P\substj{z}{x}}{}} & \text{If } x: \lin \wn T.S \\
\lvlin{x}{y}{z}{\sttoltp{P}{}} & \text{If } x: \recur{\wn T}\\
\end{cases}  \\
\sttoltp{   \vasin{\un}{x}{y}{P}  }{} 	&=  \lvlserv{x}{y}{z}{\sttoltp{P}{}}  \\
\sttoltp{ \vasout{x}{y}{P}  }{} 	&=
\begin{cases}
\res{z} \lvlout{x}{y}{z}{\sttoltp{P\substj{z}{x}}{}} & \text{If }x: \lin \oc T.S \\
\lvlout{x}{y}{z}{\sttoltp{P}{}} & \text{If }x: \recur{\oc T} \\
\end{cases}
\end{aligned}
\]

\[
\begin{aligned}
\sttoltt{ \Gamma }{l}{} 	&= \sttoltt{ x_1 : T_1}{l}{} , \cdots , \sttoltt{x_n : T_n }{l}{}\\
\sttoltt{x : T}{l}{}		&= x : \sttoltt{ T }{l}{x}\\
\sttoltt{\nilT}{l}{x} &=  \lvlnilT \\
\sttoltt{ \lin\  \vasreci{T}{S} }{l}{x}	&= \lvlint{\levelof{x}}{\sttoltt{T}{l}{\alpha}}{\sttoltt{S}{l}{x}}\\
\sttoltt{ \lin\  \vassend{T}{S} }{l}{x}	&= \lvloutt{\levelof{x}}{\sttoltt{T}{l}{\beta}}{\sttoltt{S}{l}{x}}\\
\sttoltt{ \recur{\wn T} }{x}{l}	&= \lvlunst{\levelof{x}}{\sttoltt{T}{l}{\gamma}}\\
\sttoltt{ \recur{\oc T} }{x}{l}	&=\lvlunct{\levelof{x}}{\sttoltt{T}{l}{\gamma}}\\
\end{aligned}
\]

From to (<Ref>)

The translation  $\sttoltt{-}{l}{}$ of session types and contexts is given in <Ref> (bottom).
The translation of  contexts
is parametric on a level function $l$.  In particular, the translation of a type assignment $\sttoltt{x:T}{l}{}$, relies on an auxiliary translation $x:\sttoltt{T}{l}{x}$, which is deemed to be assigned a level $l(x)$ in the translated type $\sttoltt{T}{l}{x}$, depending on the shape of $T$. Other names, denoted $\alpha, \beta,\gamma\ldots$, are necessary when translating within types.

The translation $\sttoltt{-}{l}{}$ follows  the continuation-passing approach of <cit.> to encode session types into link types.
The translation of tail-recursive types is rather direct, and self-explanatory.

By combining the translations of types and processes in <Ref> we obtain a translation of type judgements / derivations in $\vasco$ into type judgements / derivations in $\pilvl$.
We use an auxiliary notation:

The translation of a type judgment for $\vasco$ into a type judgment for $\pilvl$ is parametric on the level function  $l:\mathcal{N} \to \mathbb{N}$, and is defined as:

\begin{align*}
\sttoltj{\Gamma \st P}{l}{}& =\sttoltt{\Gamma}{l}{} \lt \sttoltp{P}{}
\\
\sttoltj{\Gamma, x:T \st x:T}{l}{} &= \sttoltt{\Gamma}{l}{}, x:\sttoltt{T}{l}{x}  \lt x:\sttoltt{T}{l}{x}
\end{align*}

This translation induces  an inductive construction of the translation  of type  derivations in $\pilvl$ from type derivations in $\vasco$, denoted as:

Rule Υ_i
∀i ∈IΓPl  =
Rule Υ_il
∀i ∈I Γl P

where $\Upsilon_i$ denotes a set of derivations used to prove $\Gamma \st P$.

The translation, of which  <Ref> gives an excerpt, relies on analyzing the last rule Rule applied in the derivation $\Gamma \st P$ and the unfolding of the translation of judgements, mapping to a derivation $ \sttoltt{\Gamma}{l}{} \lt \sttoltp{P}{}$ in  $\pilvl$,  in which the last rule applied is rule.

\begin{array}{|c|}
\hline
\textbf{Case: Input}\\
\hline
\begin{array}{lcl}
%\vastype{Lin-In_1} && \lvltype{Lin-In_1}\\
\mprset{flushleft}
\sttoltj{
\inferrule[\vastype{Lin-In_1} ]
{\Gamma_1' \st x: \lin \vasreci{T}{S}   \\
\Gamma_2 , x: S , y : T \st P }
{ \Gamma_1'  \contcomp \Gamma_2 \st  \vasin{\lin}{x}{y}{P}  }
}{l}{} & = &
\mprset{flushleft}
\inferrule*[left= \lvltype{Lin-In_1}] {
\sttoltt{\Gamma_1'}{l}{}  \lt x: \lvlint{l(x)}{\sttoltt{T}{l}{y}}{\sttoltt{S}{l}{z}} \\\\
\sttoltt{\Gamma_2}{l}{} ,   y:\sttoltt{T}{l}{y} , z:\sttoltt{S}{l}{z}  \lt \sttoltp{P\substj{z}{x}}{}  \\ l(x) = l(z) }
\sttoltt{\Gamma_1'}{l}{} 	\contcomp
\sttoltt{\Gamma_2}{l}{}
\lt  x \inp {y , z}.\sttoltp{P\substj{z}{x}}{}
\text{where }\Gamma_1'=\Gamma_1,  x : \lin \vasreci{T}{S}&& 	\text{where } \sttoltt{\Gamma_1'}{l}{}=\sttoltt{\Gamma_1}{l}{} , x: \lvlint{l(x)}{\sttoltt{T}{l}{y}}{\sttoltt{S}{l}{z}}	\\[.2cm]
\hdashline
\mprset{flushleft}
\sttoltj{
\inferrule[\vastype{Lin-In_2}]
{  \Gamma_1' \st x: \recur{\wn T}  \\
\Gamma_2', y : T \st P
{  \Gamma_1' \contcomp \Gamma_2'  \st  \vasin{\lin}{x}{y}{P} }
}{l}{}  &=&
\mprset{flushleft}
\mprset{flushleft}
\inferrule*[left=\lvltype{Lin-In_2}]
\sttoltt{\Gamma_1'}{l}{}  \lt x: \lvlunst{l(x)}{\sttoltt{T}{l}{y}} \\
\sttoltt{\Gamma_2'}{l}{} ,  z:\lvlnilT  \lt \sttoltp{P}{}  }
{  \sttoltt{\Gamma_1'}{l}{}
\contcomp
\sttoltt{\Gamma_2'}{l}{}
\lt x\inp {y , z}.\sttoltp{P}{}
\text{ where }\Gamma_1'= \Gamma_1 , x: \recur{\wn T} \text{ and }	\Gamma_2'= \Gamma_2 , x: \recur{\wn T} &&  \text{where }\sttoltt{ \Gamma_1'}{l}{}= \sttoltt{\Gamma_1}{l}{} , x: \lvlunst{l(x)}{\sttoltt{T}{l}{y}} \text{ and } \sttoltt{ \Gamma_2'}{l}{}= \sttoltt{\Gamma_2}{l}{} , x: \lvlunst{l(x)}{\sttoltt{T}{l}{y}}\\[.2cm]
%\qquad \quad \Gamma_2'= \Gamma_2 , x: \recur{\wn T}, 	&&  \qquad \quad \sttoltt{ \Gamma_2'}{l}{}= \sttoltt{\Gamma_2}{l}{} , x: \lvlunst{l(x)}{\sttoltt{T}{l}{y}}\\[.2cm]
\hdashline
%\vastype{Un-In}&& \lvltype{Un-In_1}\\
\sttoltj{
\mprset{flushleft}
\inferrule[\vastype{Un-In}]
\Gamma' \st x: \recur{\wn T} \\
\Gamma' , y : T \st P }
{  \Gamma, x: \recur{\wn T} \st   \vasin{\un}{x}{y}{P}  }}{l}{}
& = &
\mprset{flushleft}
\inferrule*[left= \lvltype{Un-In_1}]
\sttoltt{\Gamma'}{l}{} \lt x:\lvlunst{l(x)}{\sttoltt{T}{l}{y}} \\\\
\sttoltt{\Gamma'}{l}{} , y:\sttoltt{T}{l}{y},  z : \lvlnilT   \lt \sttoltp{P}{}  \\
\forall b \in \outsubj{\sttoltp{P}{}}, \ \levelof{b} < \levelof{x}
\sttoltt{\Gamma}{l}{} ,  x:\lvlunst{l(x)}{\sttoltt{T}{l}{y}}  \lt \bang x \inp {y , z}.\sttoltp{P}{}
\text{ where } \Gamma'=\Gamma, x: \recur{\wn T}&&\text{ where }\sttoltt{\Gamma'}{l}{} =\sttoltt{\Gamma}{l}{} , x: \rlevel{l(x)}{\sttoltt{T}{l}{y}} \\[2mm]
\end{array}\\
\hline
\textbf{Case: Output}\\
\hline
\\
\begin{array}{lcl}
%\vastype{Lin-Out} &&\lvltype{Lin-Out}\\
\sttoltj{
\mprset{flushleft}
\inferrule[\vastype{Lin-Out} ]
\Gamma_1' \st x: \lin \vassend{T}{S} \\
\Gamma_2' \st y: T \\
\Gamma_3, x:S \st P
{ \Gamma_1' \contcomp	\Gamma_2'\contcomp \Gamma_3 \st   \vasout{x}{y}{P}}
\mprset{flushleft}
\inferrule*[left=\lvltype{Lin-Out}]
\sttoltt{\Gamma_1'}{l}{} \lt x: \lvloutt{l(x)}{\sttoltt{T}{l}{y}}{\sttoltt{S}{l}{z}}\\\\
\sttoltt{\Gamma_2'}{l}{} \lt  y:\sttoltt{T}{l}{y} \\
\sttoltt{\Gamma_3}{l}{} , z : \sttoltt{S}{l}{z} \lt \sttoltp{P\substj{z}{x}}{}    \\ \levelof{x} = \levelof{z}
\sttoltt{(\Gamma_1'}{l}{}\contcomp \sttoltt{\Gamma_2'}{l}{} \contcomp \sttoltt{\Gamma_3}{l}{}),
\lvlsplit{z}{\sttoltt{S}{l}{z}}  \lt \ov x \out { y,z }.(\sttoltp{P\substj{z}{x}}{})
{\sttoltt{\Gamma_1'}{l}{}\contcomp \sttoltt{\Gamma_2'}{l}{} \contcomp \sttoltt{\Gamma_3}{l}{}
\lt \res{z} \ov x \out { y,z }.(\sttoltp{P\substj{z}{x}}{})
\text{ where } \Gamma_1'=\Gamma_1, x: \lin \vassend{T}{S} \text{ and } \Gamma'_2=\Gamma_2, y: T&&\text{where }\sttoltt{\Gamma_1'}{l}{}=  \sttoltt{\Gamma_1}{l}{}, x: \lvloutt{l(x)}{\sttoltt{T}{l}{y}}{\sttoltt{S}{l}{z}} \text{ and } \sttoltt{\Gamma_2'}{l}{}= \sttoltt{\Gamma_2}{l}{}, y:\sttoltt{T}{l}{y}\\[2mm]
%\qquad \quad \Gamma'_2=\Gamma_2, y: T &&\qquad \quad \sttoltt{\Gamma_2'}{l}{}= \sttoltt{\Gamma_2}{l}{}, y:\sttoltt{T}{l}{y}\\[2mm]
\hdashline
%\vastype{Un-Out} && \lvltype{Un-Out_1}\\
\sttoltj{
\mprset{flushleft}
\inferrule[\vastype{Un-Out}]
\Gamma_1' \st x: \recur{\oc T}	\\
\Gamma_2' \st y: T\\
\Gamma_3' \st P
{  \Gamma_1'\contcomp	\Gamma_2' \contcomp \Gamma_3' \st   \vasout{x}{y}{P}}
\mprset{flushleft}
\inferrule*[left=\lvltype{Un-Out_1}]
\sttoltt{\Gamma_1'}{l}{} \lt x: \rlevel{l(x)}{\sttoltt{T}{l}{y}}\\\\
\sttoltt{\Gamma_2'}{l}{} \lt y:\sttoltt{T}{l}{y}\\ \\
\sttoltt{\Gamma_3'}{l}{}, z: \lvlnilT\lt \sttoltp{P}{} }
\sttoltt{\Gamma_1'}{l}{} \contcomp	\sttoltt{\Gamma_2'}{l}{}
\contcomp \sttoltt{\Gamma_3'}{l}{}
\lt \ov x \out { y,z }.\sttoltp{P}{}
\text{ where } \Gamma_1'= \Gamma_1 , x: \recur{\oc T}, \  \Gamma_2'= \Gamma_2 , x: \recur{\oc T}, y: T  && \text{where } \sttoltt{\Gamma_1'}{l}{} =\sttoltt{\Gamma_1}{l}{} , x: \rlevel{l(x)}{\sttoltt{T}{l}{y}}, \  \sttoltt{\Gamma_2'}{l}{}=\sttoltt{\Gamma_2}{l}{}, x: \rlevel{l(x)}{\sttoltt{T}{l}{y}} , y:\sttoltt{T}{l}{y}\\
%\qquad \quad \Gamma_2'= \Gamma_2 , x: \recur{\oc T}, y: T   && \qquad \quad \sttoltt{\Gamma_2'}{l}{}=\sttoltt{\Gamma_2}{l}{}, x: \rlevel{l(x)}{\sttoltt{T}{l}{y}} , y:\sttoltt{T}{l}{y} \\
\qquad \quad \Gamma_3'= \Gamma_3 , x: \recur{\oc T} &&  \qquad \quad \sttoltt{\Gamma_3'}{l}{} =\sttoltt{\Gamma_3}{l}{} , x: \rlevel{l(x)}{\sttoltt{T}{l}{y}}\\[2mm]
\end{array}\\
\hline
\end{array}

From derivations in to derivations in (excerpt, cf. <Ref>)

§.§ Results

In general, the translation of a $P \in \vaslang$ is not necessarily typable in $\pilvl$; this occurs when, e.g., $P$ is non-terminating.
We focus on processes in $\vaslang$ that are typable in $\pilvl$, and therefore, are terminating.

We write $\sttoltt{\Gamma}{l}{} \lt \sttoltp{P}{}$ if $\sttoltj{\Gamma \st P}{l}{}$ holds, for some $l$.

Our translations are correct, in the following sense:

Let $ P \in \lvllang$ such that  $\sttoltt{\Gamma}{l}{} \lt \sttoltp{P}{}$,  for some level function $l$. Then there exists $R \in \lvllang$ such that $P \vasred Q \implies\sttoltp{P}{}{} \lts{ \tau } \sttoltp{R}{}{}$  and $R \equiv Q$.

Let $P \in \lvllang$ with  $\sttoltt{\Gamma}{l}{} \lt \sttoltp{P}{}$, for some level function $l$. If  $\sttoltp{P}{}{} \lts{ \tau } U$ Then there exists $R,Q \in \lvllang$ such that $P \vasred Q \land R \equiv Q \land U = \sttoltp{R}{}{} $.

An immediate corollary of <Ref> is that our translation preserves (non-)terminating behaviour, i.e.,  does not map non-terminating processes in $\vaslang$ into terminating processes in $\pilvl$.

$\sttoltp{\cdot}{}$ preserves (non-)terminating behaviour.

The following result corroborates our informal intuitions about $\vaslang$ and $\lvllang$. It also precisely characterizes a class of terminating processes based on our correct translations  $\sttoltp{\cdot}{}$ and $\sttoltt{\cdot}{l}{}$.

$\lvllang \subset \vaslang$.

The inclusion $\lvllang \subseteq \vaslang$ is immediate by definition.
To prove that the inclusion is strict, we consider a counterexample, i.e., a process $P$ typable in $\vasco$ but not typable in $\pilvl$.
Process $P_{\ref{ex:infinite}}$ from <Ref> suffices for this purpose.

§ PROPOSITIONS AS SESSIONS

We now introduce $\pidill$, the process model induced by the Curry-Howard correspondence between linear types and session types  (propositions-as-sessions) <cit.>.
is a synchronous $\pi$-calculus extended with (binary) guarded choice and forwarding.

Processes  in $\pidill$ are given by the grammar in <Ref> (top).
Types coincide with linear logic propositions, as given in the grammar in <Ref> (bottom).

The reduction semantics of is defined in <Ref> (bottom), relying on structural congruence, the least congruence relation defined in <Ref> (top).

\[
\begin{aligned}
P,Q ::= &								&& \mbox{(Processes)}\\
&  \dillout{x}{y}{P}		&& \mbox{(output)}
&&  \dillin{x}{y}{P}					&& \mbox{(linear input)}\\
&  \dillserv{x}{y}{P}			&& \mbox{(server)}
&& P \pp Q  	    		  		&& \mbox{(composition)}\\
& \res {x}P						&& \mbox{(restriction)}
&& \nil	     					&& \mbox{(inaction)}\\
& \dillchoice{x}{P}{Q}			&& \mbox{(branching)}
&& \dillseler{x}{P}				&& \mbox{(select right)}\\
& \dillselel{x}{P}				&& \mbox{(select left)}
&& \dillforward{x}{y}			&& \mbox{(forwarding)}
\end{aligned}
\]

\[
\begin{aligned}
A,B ::= &								&& \mbox{(Types)}
\\
& \dillnilT						&& \mbox{(Termination)}
&& \dillunt{A}					&& \mbox{(Shared)}
\\
& \dillint{A}{B}				&& \mbox{(Receive)}
&& \dilloutt{A}{B}				&& \mbox{(Send)}
\\
& \dillchoicet{A}{B}			&& \mbox{(Selection)}
&& \dillselet{A}{B}				&& \mbox{(Branching)}
\end{aligned}
\]

Processes and types of the session $\pi$-calculus $\pidill$

\[
\begin{aligned}
P \pp \nil &\equiv P
P \equiv_\alpha Q &\implies P \equiv Q
P \pp Q &\equiv Q \pp P
\\
\res{x} \nil &\equiv \nil
P \pp (Q \pp R) &\equiv (P \pp Q) \pp R
&\!\!\res{x} \res{y} P &\equiv \res{y} \res{x} P
\end{aligned}\\
x \not \in \fn{P} & \implies P \pp \res{x}Q \equiv \res{x} (P \pp Q)
\end{aligned}
\end{aligned}
\]

\[
\begin{array}{rll}
\Did{R$\leftrightarrow$} &
\res{x} (\dillforward{x}{y}	\pp P)
\dillred
P\substj{y}{x} \quad \text{if } x \not = y
\\[1mm]
\Did{RC} &
\dillout{x}{y}{P} \pp \dillin{x}{z}{Q}
\dillred
P \pp Q\substj{y}{z}
\\[1mm]
\Did{R!} &
\dillin{x}{y}{P} \pp \dillserv{x}{z}{Q}
\dillred
P \pp \vaspara{Q\substj{y}{z}}  \dillserv{x}{z}{Q}
\\[1mm]
\Did{RL}&
\dillselel{x}{P} \pp  \dillchoice{x}{Q}{R}
\dillred
P \pp Q
\\[1mm]
\Did{RR}&
\dillseler{x}{P}  \pp  \dillchoice{x}{Q}{R}\
\dillred
P \pp R
\\[1mm]
\Did{R$\pp$}&
Q \dillred R
\implies
P \pp Q \dillred P \pp R
\\[1mm]
\Did{R$\nu$}&
P \dillred Q
\implies
\res{x} P \dillred \res{x} Q
\\[1mm]
\Did{R$\equiv$}&
P \equiv P' \land P' \dillred Q' \land Q' \equiv Q
\implies
P \dillred Q
\\[1mm]
\end{array}
\]

Structural congruence and reductions for $\pidill$

[Process Abbreviations]
We adopt the following abbreviations for bound outputs and replicated forwarders:

\begin{align*}
\dillbout{x}{z}{P} &=  \res{z}\dillout{x}{z}{P}
\\
\dillfwdbang{x}{y}  & = \dillserv{y}{z}{
\dillbout{x}{k}{	\dillforward{k}{z}}}
\end{align*}

As usual, a type environment is a collection of type assignments $x : A $ where $x$ is a name and $A$ a type, the names being pairwise disjoint.
The empty environment is denoted `$\cdot$'.
We consider  unrestricted environments (denoted $\Gamma,\Gamma'$) and  linear environments  (denoted as $\Delta,\Delta'$); while the former satisfy weakening and contraction, the latter do not.

We denote by $dom(\Gamma)$, the domain of  $\Gamma$, the set of names whose type assignments are in $\Gamma$, i.e., $dom(\Gamma)=\{x \mid x:A \in \Gamma\}$.  Also,  $\Gamma(x)$ denotes the type of the name $x\in dom(\Gamma)$, i.e., $\Gamma(x)=A$, if $x:A\in \Gamma$. The domain of $\Delta$  and $\Delta(x)$ are similarly defined.

Typing judgments for $\pidill$ are of the form $\Gamma ; \Delta    \dill P \ :: x:A$.
Such a judgment is intuitively read as: “$P$ provides protocol $A$ along $x$ by using the protocols described in the assignments in $\Gamma$ and $\Delta$”. The domains of  $\Gamma$, $\Delta$ and $x:A$ are pairwise disjoint.
The corresponding type
rules  are given  in <Ref>.
Each logical operator is represented by right and left rules: the former explains how to offer a behavior (according to the operator's interpretation, cf. <Ref> (bottom)); the latter explains how to make use of a behavior typed with the operator.
In particular, the behavior of clients and servers is governed by four typing rules:
L, and

The Curry-Howard correspondence connects the logical principle of cut elimination with process synchronization. As a result, we have  the fundamental property ensured by typing:

If $\Gamma ; \Delta    \dill P \ :: x:A$
and $P \dillred Q$
$\Gamma ; \Delta    \dill Q \ :: x:A$.

The type system enforces also progress and termination. The latter property can be proven using logical relations <cit.>.

* [ left = L ]  Γ; ΔP :: T
Γ; Δ, x : P :: T

* [ left = R ]
Γ; ·::   x :

* [ left = fwd ]
Γ; x:A  xy ::   y : A

* [ left =  L ] Γ; Δ, y:A , x:B P :: T
Γ; Δ, x :AB xyP :: T

* [ left =  R ] Γ; Δ_1 P :: y : A
Γ; Δ_2 Q :: x : B
Γ; Δ_1, Δ_2  xy(P Q) ::   x : AB

* [ left = cut ] Γ; Δ_1 P :: x: A
Γ; Δ_2 , x:A Q ::T
Γ; Δ_1 ,  Δ_2  x(P Q) ::  T

* [ left = cut^! ]  Γ; ·P :: y: A
Γ, u:A ; ΔQ ::T
Γ;   Δu(uyP Q) ::  T

* [ left = copy ] Γ, u:A ; Δ, y:A P  :: T
Γ, u:A ; ΔuyP ::  T

* [ left =  L ] Γ, u:A ; ΔP ux :: T
Γ; Δ, x: A P :: T

* [ left =  R ] Γ; ·Q :: y:A
Γ; ·xyQ ::   x : A

*[left= L_1 ] Γ; Δ, x:A P :: T
Γ; Δ, x:AB      xP :: T

* [ left =  L ] Γ; Δ, x:A P :: T   Γ; Δ, x:B P :: T
Γ; Δ, x:AB xPQ :: T

*[left= R_2 ] Γ; ΔP ::  x:B
Γ; Δ    xP :: x:AB

Type rules for $\pidill$ (selection)

§ : A CLASS OF TERMINATING PROCESSES

We now study , another class of terminating processes.
This class is induced by the Curry-Howard system given in <Ref>, which leverages
translations on processes and types/contexts, denoted $\sttodillp{\cdot}{}$ and $\sttodillt{\cdot}$, respectively.
Roughly, is defined as follows:

$$ \dilllang = \{ P \in \vasco \mid  \ \Gamma \vaslinunsplit \Delta \st P ~\land~
{\sttodillt{\Gamma}};   \sttodillt{\Delta}  \dill \sttodillp{{P}}  :: u: \sttodillt{\dual{S}} 	\}

<Ref> will give a formal definition.
In the following we define the translations $\sttodillp{\cdot}{}$ and $\sttodillt{\cdot}$, and establish their properties.
Our main result is that
$\dilllang \subset \lvllang$
$\lvllang \not \subset \dilllang$
(<Ref>): there are terminating processes detected as such by the weight-based approach but not by the Curry-Howard correspondence.

We require some auxiliary definitions.

The following predicates say whether a session type contains client or server behaviors.

Given a session type $T$, we define predicates $\server{{T}}$ and $\client{{T}}$ as follows:

\[
\begin{array}{rl@{\hspace{2cm}}rl}
\server{\recur{\wn T}} &  = \ttrue
\client{\recur{\oc T}} &  = \ttrue
\\
\server{\nilT} &  = \ffalse
\client{\nilT} &  = \ffalse
\\
\server{q \ \vassend{S}{T}} &  = \server{T}
\client{q \ \vassend{S}{T}} &  = \client{T}
\\
\server{q \ \vasreci{S}{T}} &  = \server{T}
\client{q \ \vasreci{S}{T}} &  = \client{T}
\\
\server{\recur{\oc T}} &  =  \server{T}
\client{\recur{\wn T}} &  = \client{T}
\end{array}
\]

These predicates extend to contexts $\Gamma$ as expected. This way, e.g., $\server{\Gamma}$ stands for $\bigwedge_{x\in dom(\Gamma)} \Gamma(x)$.

Also, we write $\server{\Gamma;P}$ to stand for $ \bigwedge_{x \in (\fn{P} \cap dom(\Gamma) )} \server{\Gamma(x)}$, returning $\ttrue$ when $(\fn{P} \cap dom(\Gamma)) = \emptyset$.
Analogous definitions for $\client{\cdot}$ , $\notserver{\cdot} $, and $ \notclient{\cdot} $ arise similarly.

This way, intuitively:

* $\notserver{T}\land \notclient{T}$ means that $T$ is an always-linear behavior, i.e., it does not contain server and client actions.

* $\server{T} \land \notclient{T}$ means that $T$ contains some server behavior and that it does not contain client behaviors.

* $\notserver{T}\land \client{T}$ means that $T$ will at some point exhibit client behaviors and that it does not contain server behaviors.

Also, $\server{T} \land \client{T}$ means that $T$ contains both server and client actions; this combination, however, is excluded by typing.

We further illustrate <Ref> by example:

$T$     $\server{T}$     $\client{T}$

1    $\recur{ \oc ( \lin \  \vassend{(\recur{\oc S})}{(\lin \ \vasreci{(\recur{\wn R})}{(\recur{\wn T_0})})})}$

2    $\lin \ \vassend{(\recur{\oc S})}{(\lin \ \vasreci{(\recur{\wn R})}{(\recur{\wn T_0})})}$

3    $\recur{\oc (\lin \ \vassend{(\recur{\oc S})}{(\lin \ \vasreci{(\recur{\wn R})}{\nilT})})}$

4    $\lin \ \vassend{(\recur{\oc S})}{(\lin \ \vasreci{(\recur{\wn R})}{\nilT})}$

Both $(1)$ and $(2)$ return for $\server{T}$ because of their final behavior (i.e., `$\recur{\wn T_0}$'), whereas $(3)$ and $(4)$ return , because their final  behavior is $\nilT$.
Both $(1)$ and $(3)$ return for $\client{T}$ as their initial type behavior (i.e., `$\recur{\oc T'}$') is that of a client, whereas $(2)$ and $(4)$ return as they do not contain any client behavior.

§.§ The Typed Translation

The translation $\sttodillp{\cdot}: \vasco \to \pidill$ is given in <Ref>.

\[
\begin{aligned}
\sttodillp{\vasout{x}{y}{P}} & =
\begin{cases}
\dillbout{x}{z}{( \dillforward{y}{z}  \pp  \sttodillp{{P}}   )}
& \text{If $ x: \lin \oc (T).S \land \neg \contun{T}\land \notserver{T}$.}
\\
\dillbout{x}{z}{( \dillfwdbang{y}{z}  \pp  \sttodillp{{P}}   )}
& \text{If $ x: \lin \oc (T).S \land \contun{T} \land \notserver{T}$.}
\\
%\res{z} \dillout{x}{z}{ \dillselel{z}{
%	\res{w} \dillout{z}{w}{
%		( \dillfwdbang{v}{w}  \pp  \sttodillp{{P}}   )
%	}
%} \\
\dillbout{x}{z}{
\dillbout{z}{w}{
( \dillforward{y}{w}  \pp  \sttodillp{{P}}   )
\text{If $ x: \recur{\oc T} \land \neg \contun{T} \land  \notserver{T} \land \client{T}$}
\\
\dillbout{x}{z}{
\dillbout{z}{w}{
( \dillfwdbang{y}{w}  \pp  \sttodillp{{P}}   )
\text{If $ x: \recur{\oc T} \land \contun{T} \land \notserver{T} \land \client{T}$}
\\
\dillbout{x}{z}{ \dillselel{z}{
\dillbout{z}{w}{
( \dillfwdbang{y}{w}  \pp  \sttodillp{{P}}   )
\text{If $ x: \recur{\oc T} \land \contun{T}\land \notserver{T} \land \notclient{T} $}
\\
\dillbout{x}{z}{ \dillselel{z}{
\dillbout{z}{w}{
( \dillforward{y}{w}  \pp  \sttodillp{{P}}   )
\text{If $ x: \recur{\oc T} \land \neg \contun{T}\land \notserver{T} \land \notclient{T} $}
\end{cases}\\
\sttodillp{\res{xy}\vasout{z}{y}{P}  } & =
\begin{cases}
\dillbout{z}{x}{\dillseler{x}{\sttodillp{P}}}  & \text{If $z:\recur{\oc T} \land \notserver{T} \land \notclient{T} $.}\\
\dillbout{z}{x}{\sttodillp{P}} & \text{If $z:\recur{\oc T} \land \server{T} \land \notclient{T} $.}
\end{cases}
\\
\sttodillp{\res{xy}\vasout{z}{x}{(P \pp Q)}} & =
\dillbout{z}{y}{(\sttodillp{P} \pp \sttodillp{Q})}
\quad \text{If $z:  \lin \vassend{T}{S} \wedge z \not \in \fn{P} \land y \not \in \fn{Q}$}
\\
\sttodillp{\vasin{\lin}{x}{y}{P}} & =
\dillin{x}{y}{\sttodillp{P}} \quad \text{If $x: \lin \vasreci{T}{S}$}\\
\sttodillp{\vasin{\un}{x}{{y}}{P}} & =
\begin{cases}
\dillserv{x}{z}{\sttodillp{P\substj{z}{y}}}
& \text{If $ x: \recur{\wn T} \land\server{T}\land \notclient{T} $.} \\
\dillserv{x}{z}{ \dillin{z}{y}{ \sttodillp{P} }
& \text{If $ x: \recur{\wn T} \land\notserver{T}\land \client{T} $.} \\
\dillserv{x}{z}{
\dillchoice{z}{	\dillin{z}{y}{ \sttodillp{P} }	}{	\sttodillp{P\substj{z}{y}} }
& \text{If $ x: \recur{\wn T} \land\notserver{T}\land \notclient{T} $.}
\end{cases}\\
\sttodillp{\res{x y}(P \pp Q)} & =
\res{x}( \sttodillp{P} \pp \sttodillp{Q}\substj{x}{y}) \quad \text{If $ y \not \in \fn{P} \land x \not \in \fn{Q}$}\\
\sttodillp{P \pp Q} & = \res{w} ( \sttodillp{P} \pp \sttodillp{Q}   ) \quad \text{With $ w $ fresh}
\\
\sttodillp{\nil} & = \nil
\end{aligned}
\]

Translating processes in into $\pidill$

The translation of processes relies on type information; in particular, the translation of outputs and unrestricted inputs depends on whether the overall behavior of channels exhibits server or client behaviors (cf. <Ref>).
In translating  outputs, we check whether the output is free or bound.
The translation of free outputs is further influenced by whether the sender is associated with a linear connection or acts as a client connected to a server. There are 5 cases to consider, and the translated processes are designed to preserve typability.
Similar conditions apply to the translation of bound outputs.

To ensure typability of the translated process, we explain some of the choices in <Ref>:

* In a free output $\vasout{x}{z}{P}$ the value $z$   cannot have a server behavior. In <Ref>, this is ensured using the predicate $\notserver{T}$.

* In an unrestricted bound output $\res{xy}\vasout{z}{y}{P} $,  the value $y$ cannot have a client behavior. In <Ref>, this is ensured using the predicate $\notclient{T}$.

We illustrate what we mean by “client behavior” above. Consider the process $P=\res{xy}( \res{wv}\vasout{x}{v}{\vasin{\un}{w}{a}{\nil}}\pp \vasin{\un}{y}{c}{\vasout{c}{b}{\nil}})$.
In $P$, the output action on $x$ is an unrestricted bound output, whose object $v$ has a client behavior: after one reduction, an output on $v$ will be ready to invoke the server on $w$.
Notice that $P \in \vaslang$, as $P$ is typable with $b:\nilT\st P$ and $x:\recur{\oc (\recur{\oc \nilT})}, y:\recur{\wn (\recur{\oc \nilT})}, w:\recur{\wn \nilT}$ and $ v:\recur{\oc \nilT}$.

We want a typable  translation of the judgement $\sttodillj{\Gamma \st P}_u$. Consider the partial translation of $P$, i.e., $\sttodillp{P}=\res{x}(\sttodillp{P_1}\pp \sttodillp{Q_1}\substj{x}{y})$,

where we use the abbreviations

* $P_1= \res{wv}\vasout{x}{v}{\vasin{\un}{w}{a}{\nil}}$, and

* $Q_1= \vasin{\un}{y}{c}{\vasout{c}{b}{\nil}}$.

Suppose we can apply cut, then there are derivations $\Pi_1$ and $\Pi_2$ such that

Π_1b:; ·Q_1xy:: y: !( )  Π_2b:; x:!( )P_1 :: u:T

b:;·x( P_1Q_1xy)::u:T

Consider the partial translation $\sttodillp{\res{wv}\vasout{x}{v}{\vasin{\un}{w}{a}{\nil}}}= \dillbout{x}{w}{(\dillserv{w}{a'}{P_1'})}$ for some $P_1'$ that we will leave opaque for now.

Notice, however, that the following derivation is not possible: to type $\dillserv{w}{a'}{P_1'}$ we would need $u=w$ to apply $\dilltype{\dillunt{}R}$ (above the application of $\dilltype{copy}$), but $w$ already occurs in the context and this contradicts the domain restriction of $\dill$ judgements.

b:, x:( );w:( ) !w(a).0::u:T
b:, x:( );·wa'P_1'::u:T
b:; x:!( )xw(wa'P_1')::u:T

A similar argument and example can be used to justify the first item of this remark.

While the translation of linear inputs is straightforward, in translating unrestricted inputs we check whether the synchronization concerns a bound or free output.
When the unrestricted input cannot discern the client or server behavior from the type, it offers both behaviors using a branching construct; the synchronizing party (i.e. the translation of output, free or bound) then determines the desired behavior using a corresponding selection construct.

Consider $P=\res{xy}(  \vasin{\un}{ x}{z}{\nil}\pp  \vasout{y}{w}{\nil})$, a $\vasco$ process that implements a simple  server-client communication.  As in <Ref>, one can verify that
$x:\recur{\wn \nilT}, y:\recur{\oc \nilT}$, $w:\nilT$ and $z:\nilT$, which  entail $w:\nilT \st P$. Since $y\notin \fn{\vasin{\un}{x}{z}{\nil}}$ and $x\notin \fn{\vasout{y}{w}{\nil}}$, the translation of $P$ is as:

\[
\begin{aligned}
\sttodillp{P}= \res{x}(\sttodillp{\vasin{\un}{x}{z}{\nil}}\pp \sttodillp{\vasout{x}{w}{\nil}})
\end{aligned}
\]

Note that $\notclient{\nilT}\wedge \notserver{\nilT}\wedge \contun{\nilT}$ holds (cf. <Ref> and <Ref>). Thus,

\[
\begin{aligned}
\sttodillp{\vasin{\un}{x}{z}{\nil}} &=\dillserv{x}{v}{
\dillchoice{v}{	\dillin{v}{z}{ \nil }	}{\nil }
} \\
\sttodillp{\vasout{x}{w}{\nil}} &= \dillbout{x}{z}{ \dillselel{z}{
\dillbout{z}{v}{
( \dillfwdbang{w}{v}  \pp  \nil   )
\end{aligned}
\]

Given a session type/linear logic proposition $A$, we write $\dillnotunsingular{{A}}$ to denote $A$ without
top-level occurrences of ` $\bang$ ', i.e., $\dillnotunsingular{\dillunt{A}} =  A$ and is  the identity function otherwise.

The translation $\sttodillt{\cdot }$ from session types in $\vasco$ to logic propositions in $\pidill$ is given in <Ref>.
The translation of types extends to contexts as expected;
we shall write $\dillnotun{\sttodillt{\Gamma}}$ to stand for  $\dillnotunsingular{\sttodillt{\Gamma}}$.

\[
\begin{aligned}
\sttodillt{\nilT} &  = \dillunt{\dillnilT} \\
\sttodillt{\lin \vassend{S}{T}} &  =  \dillint{\sttodillt{S}}{\sttodillt{T}}\\
\sttodillt{\lin \vasreci{S}{T}} &  = \dilloutt{\sttodillt{S}}{\sttodillt{T}} \\
\sttodillt{\recur{\wn T}} &  =
\begin{cases}
\dillunt{\sttodillt{T}} & \text{If $\server{T}\land \notclient{T} $.}\\
\dillunt{(\dilloutt{\sttodillt{T}}{\dillnilT})} & \text{If $\notserver{T}\land \client{T} $.}\\
\dillunt{(\dillchoicet{(\dilloutt{\sttodillt{T}}{\dillnilT})}{\sttodillt{T}})} & \text{If $\notserver{T}\land \notclient{T} $.}
%\text{Undefined} & \text{If $\server{T}\land \client{T} $.}
\end{cases}\\
\sttodillt{\recur{\oc T}} &  =
\begin{cases}
\dillunt{\sttodillt{\dual{T}}} & \text{If $\server{T}\land \notclient{T} $.} \\
\dillunt{({\dillint{\sttodillt{T}}{\dillnilT}})} & \text{If $\notserver{T}\land \client{T} $.}\\
\dillunt{(\dillselet{(\dillint{\sttodillt{T}}{\dillnilT})}{\sttodillt{\dual{T}}})} & \text{If $\notserver{T}\land \notclient{T} $.}
%\text{Undefined}  & \text{If $\server{T}\land \client{T} $.}
\end{cases}\\
\end{aligned}
\]

Translating session types into logical propositions

The translation of $\nilT$ and linear input/output types is standard.
As for client and servers, the translation of types follows the translation of processes.
When the type of the client or server exhibits a server behavior, the type is encoded into an unrestricted type.
Notice that a client type $\recur{\oc T}$ is translated into its dual behavior $\dillunt{\sttodillt{\dual{T}}} $, but a server is not.
This has to do with the left/right interpretation of judgments in : servers always occur on the right-hand side; to provide a dual behavior, the client should itself be dual.

[Cont. <Ref>]
Consider the type assignments
$x:\recur{\wn \nilT}, y:\recur{\oc \nilT}$, $w:\nilT$ and $z:\nilT$. Since  $\notclient{\nilT}\wedge \notserver{\nilT}$, the translation in <Ref> gives:

* $x:\sttodillt{\recur{\wn\nilT}}=\dillunt{(\dillchoicet{(\dilloutt{\sttodillt{\nilT}}{\dillnilT})}{\sttodillt{
\nilT}})}=\dillunt{(\dillchoicet{(\dilloutt{\dillunt{\dillnilT}}{\dillnilT})}{\dillnilT})}$;

* $y:\sttodillt{\recur{\oc \nilT}}=\dillunt{(\dillselet{(\dillint{\sttodillt{\nilT}}{\dillnilT})}{\sttodillt{\dual{\nilT}}})}=\dillunt{(\dillselet{(\dillint{\dillunt{\dillnilT}}{\dillnilT})}{~\dillnilT})}$

The translations to $z:\dillnilT$ and $w:\dillnilT$ are trivial.

Armed with the translations of processes and types given in <Ref> and  <Ref>,
we are now ready to translate a judgment $\Gamma, \Delta \st P$ into $\dillnotun{\sttodillt{\Gamma}{}{}} ;  \sttodillt{\Delta}{}{} \dill \sttodillp{P}{} :u:: A$, for some name $u$.
This translation requires that $\contun{\Gamma}$ and $\neg \contun{\Delta}$, i.e., $\Gamma$ is unrestricted and $\Delta$ is `not' unrestricted; this is the abbreviation $\Gamma \vaslinunsplit \Delta$ (<Ref>).

The following auxiliary notion relates contexts that may differ in exactly one assignment:

Given contexts  $\Gamma , \Gamma'$, we write  $\Gamma \dillcontrel{z}{T} \Gamma' $ if $(\Gamma = \Gamma' \land z \not \in \dom{\Gamma}) \lor (\Gamma = \Gamma' , z:T) $ for some type $T$.

Given a judgment $\Gamma \vaslinunsplit \Delta \st P$
and a name $u$, 	its translation   $\sttodillj{\Gamma \vaslinunsplit \Delta \st P}_{u}{}$ is defined as

$$ \dillnotun{\sttodillt{\Gamma'}{}{}} ;  \sttodillt{\Delta'}{}{} \dill \sttodillp{P}{} :: u: A$$

where $\Gamma'$, $\Delta'$, and $A$ are subject to one of the following conditions:

* $A= \sttodillt{\dual{T}}{}{}$ when $\{ u: T \} \subset \Gamma , \Delta$ with $ (\Gamma \dillcontrel{u}{T} \Gamma') \land (\Delta \dillcontrel{u}{T} \Delta')$; or

* $A= \dillnilT $ when $ u \not\in \dom{\Gamma , \Delta}$ with $ (\Gamma = \Gamma') \land (\Delta = \Delta')$.

<Ref> defines the translation by induction on $P$, assuming that the contexts satisfy the appropriate requirements, i.e., $\contun{\Gamma,\Gamma'} \land \neg \contun{\Delta , \Delta_1,\Delta' }$ and $A,\Gamma'$ and $\Delta'$ are as one of the cases above.

c]| p.2cm | c | l |

$\Gamma \vaslinunsplit \Delta \st P$
$\dillnotun{\sttodillt{\Gamma}} ;  \sttodillt{\Delta} \dill \sttodillp{P} :: u : A$

{ \Gamma  \vaslinunsplit \cdot  \st \nil  }

{ \dillnotun{\sttodillt{\Gamma}} ;  \cdot \dill \nil :: u : \dillnilT }

\Gamma \vaslinunsplit \Delta_1 , \Delta \st P \pp Q

\begin{array}{ll}
\dillnotun{\sttodillt{\Gamma'}} ; \sttodillt{\Delta_1} , \sttodillt{\Delta'}   \dill \res{w} ( \sttodillp{P} \pp \sttodillp{Q}   )  ::  u: A
\text{if } w \not \in \dom{\Gamma, \Delta_1, \Delta}  \land u \notin \fn{P}
%				(
%					\abconditionO{u}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}
%					\lor \abconditionT{u}{R}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}
%				)
\end{array}

\begin{array}{l}
\Gamma \vaslinunsplit  \Delta_1 ,  \Delta \st
\res {zv:V} (P \pp Q)
\end{array}

\begin{array}{l}
\text{If }
(u\notin \fn{P})
\land
( (\neg \contun{V}) \lor
( \contun{V} \land v \not \in \fn{P} \land z \not \in \fn{Q} )) \
%				\land (
%					\abconditionO{u}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}
%					\lor
%					\abconditionT{u}{R}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}
%				)
\\

\dillnotun{\sttodillt{\Gamma'}} ; \sttodillt{\Delta_1} , \sttodillt{\Delta'}  \dill \res{z}( \sttodillp{P} \pp \sttodillp{Q}\substj{z}{v} ) ::  u: A
%\text{if } \neg \contun{V} \land
%	\abconditionO{u}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}
%	\lor
%	\abconditionTstar{u}{R}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}{P}{u}
\end{array}

\begin{array}{ll}
\Gamma , x: \recur{\wn T} \vaslinunsplit \cdot \st
\vasin{\un}{x}{y}{P}
\end{array}

\begin{array}{l}
\text{If } u = x \land x \not \in \fn{P} \text{ and one of the following holds:}
\\
\begin{tabular}{ll}
%\text{if } \notserver{T}\land \notclient{T}
\dillnotun{\sttodillt{\Gamma}} ; \cdot  \dill   \dillserv{x}{w}{
\dillchoice{w}{	\dillin{w}{y}{ \sttodillp{P} }	}{	\sttodillp{P\substj{w}{y}} }}
:: u: \dillunt{(\dillselet{(\dillint{\sttodillt{T}}{\dillnilT})}{\sttodillt{\dual{T}}})} $
$\text{if } \notserver{T}\land \notclient{T}
\smallskip
\\
\hdashline
\noalign{\smallskip}
$\dillnotun{\sttodillt{\Gamma}} ; \cdot  \dill   \dillserv{x}{w}{
{ \sttodillp{P\substj{w}{y}} }} ::  u: \dillunt{\sttodillt{\dual{T}}} $
\text{if } $\server{T} \land \notclient{T} $
\smallskip
\\
\hdashline
\noalign{\smallskip}
$\dillnotun{\sttodillt{\Gamma}} ; \cdot  \dill   \dillserv{x}{w}{
\dillin{w}{y}{ \sttodillp{P} }	} ::  u: \dillunt{(\dillint{\sttodillt{T}}{\dillnilT})}$
\text{if } $\notserver{T} \land \client{T}$
\smallskip
\end{tabular}
\end{array}

\begin{array}{l}
\Gamma \vaslinunsplit  x: \lin \vasreci{T}{S} , \Delta \st
\vasin{\lin}{x}{y}{P}
\end{array}

$\dillnotun{\sttodillt{\Gamma}} ; \sttodillt{\Delta} \dill \dillin{x}{y}{\sttodillp{P}}  :: u:\dillint{\sttodillt{T}}{\sttodillt{\dual{S}}}$     if $u = x$

$\dillnotun{\sttodillt{\Gamma'}} ; \sttodillt{\Delta'} , x:\dilloutt{\sttodillt{T}}{\sttodillt{S}}  \dill \dillin{x}{y}{\sttodillp{P}} :: u: A$

\begin{aligned}
& \Gamma , z: \recur{\oc T} \vaslinunsplit \Delta  \st
\res{xy}\vasout{z}{y}{P}
\end{aligned}

\begin{array}{l}
\text{If } (\neg \contun{T}) \lor (y \not \in \fn{P} \land \contun{T}) \text{ and:}
\\
\begin{tabular}{ll}
$\dillnotun{\sttodillt{\Gamma'}} , z:\dillselet{\dillint{\sttodillt{T}}{\sttodillt{\dillnilT}}}{\sttodillt{\dual{T}}}  ; \sttodillt{\Delta'}  \dill
\dillbout{z}{x}{
\dillseler{x}{\sttodillp{P}}} ::  u: A
\text{if } \notserver{T} \land \notclient{T}
%\land (\abconditionO{u}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A} \lor \abconditionT{u}{R}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A} )
\smallskip
\\
\hdashline
\noalign{\smallskip}
$ \dillnotun{\sttodillt{\Gamma'}} , z:\sttodillt{\dual{T}}  ; \sttodillt{\Delta'}  \dill  \dillbout{z}{x}{
\sttodillp{P}} :: u: A $
\text{if } $\server{T} \land \notclient{T}
%					\land
%					(\abconditionO{u}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A} \lor \abconditionT{u}{R}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A} )
\smallskip
\end{tabular}
\end{array}

\begin{array}{l}
\Gamma \vaslinunsplit z: \lin \vassend{T}{S} , \Delta_1, \Delta \st \\
\quad   \res{xy}\vasout{z}{x}{(P \pp Q)}
\end{array}

$\text{If } (\neg \contun{T}) \lor (x \not \in \fn{P} \cup \fn{Q} \land \contun{T}) \text{ and:}$

\begin{array}{ll}
%\text{If }z = u \land u,z \not \in \fn{P} \land y \not \in \fn{Q}
\dillnotun{\sttodillt{\Gamma}} ; \sttodillt{\Delta_1} , \sttodillt{\Delta} \dill
\dillbout{z}{y}{(\sttodillp{P} \pp \sttodillp{Q})} ::   z : \dilloutt{\sttodillt{T}}{\sttodillt{\dual{S}}} & \qquad \quad  \text{if }z = u \land u,z \not \in \fn{P} \land y \not \in \fn{Q}
\end{array}

\begin{array}{ll}
%\text{If }{z \not = u} \land {u,z \not \in \fn{P}}\land y \not \in \fn{Q}
%\land ( u \notin \fn{P})
%						\land
%						(
%							\abconditionO{u}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}
%							\lor
%							\abconditionT{u}{R}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}
%						)
\dillnotun{\sttodillt{\Gamma'}} ; \sttodillt{\Delta_1} , \sttodillt{\Delta'}  , z : \dillint{\sttodillt{T}}{\sttodillt{S}} \dill
\dillbout{z}{y}{(\sttodillp{P} \pp \sttodillp{Q})} :: u: A  & \text{if }{z \not = u} \land {u,z \not \in \fn{P}}\land y \not \in \fn{Q}
\end{array}

\begin{array}{l}
\smallskip
\Gamma  \vaslinunsplit v:T, x: \lin \oc (T).S , \Delta
\st \ov x\out v.P
\end{array}

$ \dillnotun{\sttodillt{\Gamma}} ;  v: \sttodillt{T}, \sttodillt{\Delta}   \dill \dillbout{x}{y}{(\dillforward{v}{y}  \pp  \sttodillp{P})} ::   u : \dilloutt{\sttodillt{T}}{\sttodillt{\dual{S}}} $     if $u = x \land \neg \contun{T} \land \notserver{T}$

$ \dillnotun{\sttodillt{\Gamma'}} ;  v: \sttodillt{T},  \sttodillt{\Delta'}  , x : \dillint{\sttodillt{T}}{\sttodillt{S}}  \dill \dillbout{x}{y}{(\dillforward{v}{y} \pp P)} ::  u: \sttodillt{\dual{R}}  $    	if  $\neg \contun{T} \land \notserver{T} $

\begin{array}{l}
\Gamma,  v:T \vaslinunsplit x: \lin \oc (T).S , \Delta
\st \ov x\out v.P
\end{array}

$  \dillnotun{\sttodillt{\Gamma}} , v: \sttodillt{T} ;  \sttodillt{\Delta} \dill \dillbout{x}{y}{(\dillfwdbang{v}{y}  \pp  \sttodillp{P})} ::   x : \dilloutt{\sttodillt{T}}{\sttodillt{\dual{S}}}$     if $u = x \land \contun{T} \land \notserver{T}$

$ \dillnotun{\sttodillt{\Gamma'}},  v:T  ; \sttodillt{\Delta'}  , x : \dillint{\sttodillt{T}}{\sttodillt{S}}  \dill \dillbout{x}{y}{(\dillfwdbang{v}{y} \pp P)} ::  u: A $     if  $\contun{T} \land \notserver{T}$

\begin{aligned}
& \Gamma , x: \recur{\oc T} \vaslinunsplit v:T , \Delta
\st \ov x\out v.P
\end{aligned}

If $\notserver{T} \land \notclient{T}  \land \neg \contun{T} \land z \not \in \fn{P}$  $
%				\land
%				(
%					\abconditionO{u}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}
%					\lor
%					\abconditionT{u}{R}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}
%				)

$ \dillnotun{\sttodillt{\Gamma'}} , x:\dillselet{\dillint{\sttodillt{T}}{\dillnilT}}{\sttodillt{\dual{T}}} ;  v:\sttodillt{T} , \sttodillt{\Delta'} \dill \dillbout{x}{z}{ \dillselel{z}{ \dillbout{z}{w}{( \dillforward{v}{w}  \pp  \sttodillp{{P}} )}}} :: u: A$

If $\notserver{T} \land \client{T}  \land \neg \contun{T} \land z \not \in \fn{P}$ $
%				\land
%				(
%					\abconditionO{u}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}
%					\lor
%					\abconditionT{u}{R}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}
%				)

$ \dillnotun{\sttodillt{\Gamma'}} , x:\dillint{\sttodillt{T}}{\dillnilT} ;  v:\sttodillt{T} , \sttodillt{\Delta'}   \dill \dillbout{x}{z}{ \dillbout{z}{w}{ ( \dillforward{v}{w}  \pp  \sttodillp{{P}} )} } ::  u: A $

& \Gamma , x: \recur{\oc T}, v:T\vaslinunsplit \Delta
\st \ov x\out v.P
\end{aligned}

\begin{array}{l}
\text{If } \notserver{T} \land \notclient{T} \land \contun{T}\land z \notin \fn{P}\\
\dillnotun{\sttodillt{\Gamma'}} , x:\dillselet{\dillint{\sttodillt{T}}{\dillnilT}}{\sttodillt{\dual{T}}} ; v:\sttodillt{T} ; \sttodillt{\Delta'} \dill \dillbout{x}{z}{ \dillselel{z}{ \dillbout{z}{w}{( \dillfwdbang{v}{w}  \pp  \sttodillp{{P}} )}}} :: u: A		\smallskip
\\
\hdashline
\text{If  } \notserver{T} \land \client{T} \land \contun{T} \land z \not \in \fn{P}
%				 \land
%				(
%					\abconditionO{u}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}
%					\lor
%					\abconditionT{u}{R}{\Gamma}{\Delta}{\Gamma'}{\Delta'}{A}
%				)
\\
\begin{aligned}
& \dillnotun{\sttodillt{\Gamma'}} , x:\dillint{\sttodillt{T}}{\dillnilT} , v:\sttodillt{T};   \sttodillt{\Delta'}  \dill \dillbout{x}{z}{
\dillbout{z}{w}{
( \dillfwdbang{v}{w}  \pp  \sttodillp{{P}}   )
} :: u: A
\end{aligned}
\end{array}

From judgments in to judgments in (<Ref>).

Using this translation of judgments, a translation of derivations can be defined exactly as in <Ref>.

We discuss some entries in <Ref> with the following example.

[Cont. <Ref>]

The translation of judgments defined in <Ref> relies on the typability in the source language () to determine the exact conditions to the typability of the translated process in $\pidill$. First, the type derivation of $w:\nilT\st \res{xy}(  \vasin{\un}{ x}{z}{\nil}\pp  \vasout{y}{w}{\nil})$ is essential to build a type derivation for the translated judgment (if one exists):

Γ, z:Γxz

Γ xzyw

w:xy ( xzyw)

where $\Gamma= x:\recur{\wn \nilT}, y:\recur{\oc \nilT}, w:\nilT$

Second, the translation  $\sttodillj{w:\nilT\st \res{xy}(  \vasin{\un}{ x}{z}{\nil}\pp  \vasout{y}{w}{\nil})}_u$
corresponds to entry 3 of <Ref>,

w:;·x( xzxw)::u:A

and we have previously observed that the side conditions hold. Since $u$ is not in the type context, we have $A=\dillnilT$. Now we proceed to build a type derivation for the translated judgment by applying rule $\dilltype{cut}$:

w:; · xz::x:  B

w:,y :B; ·yw)::u:w:; x :B xw)::u:

w:;·x( xzxw)::u:

and we will show that there exist derivations $\Pi_1$ and $\Pi_2$  such that the derivation holds.  We recall the translations $\sttodillp{\vasin{\un}{x}{z}{0}}$ and $\sttodillp{\vasout{x}{w}{
\nil}}$ in <Ref>.

Third, the left premise is the translation $\sttodillj{\Gamma\st \vasin{\un}{x}{z}{\nil}}_x$  and corresponds to entry (4) of the <Ref>. We  recall <Ref> for $\dillnotun{\sttodillt{\Gamma}}=w:\dillnilT, x:  (\dillchoicet{(\dilloutt{\dillunt{\dillnilT}}{\dillnilT})}{\dillnilT}) , y: (\dillselet{(\dillint{\dillunt{\dillnilT}}{\dillnilT})}{\dillnilT})$ and use the abbreviation $B=(\dillselet{(\dillint{\dillunt{\dillnilT}}{\dillnilT})}{\dillnilT})$ and strengthening of $\dillnotun{\sttodillt{\Gamma}}$. The derivation $\Pi_1$ is as follows:

w:; ·:: v:
w:; z::: v:

w:; ·vz ::v:

w:; ·:: v:
w:; ·v	vz
:: v: ()

w:; ·xv  v	vz  ::x: (())

Fourth, the right premise is the translation $\sttodillj{\Gamma\st \vasout{y}{w}{0}\substj{x}{y}}_u$ and  corresponds to the entry (11a) of the <Ref>. The derivation $\Pi_2$ is as follows:

Γ' ; ·wv :: v :  Γ' ; z::: u :
Γ' ; z:()   zv( wv  ) :: u :
Γ' ; z:()   z zv( wv  ) :: u:
Γ'  ; ·yz z zv( wv  ) :: u:

where we strengthen $\dillnotun{\sttodillt{\Gamma}}$ to  $\dillnotun{\sttodillt{\Gamma'}}= y: (\dillselet{(\dillint{\dillunt{\dillnilT}}{\dillnilT})}{\dillnilT}), w:{\dillnilT}$.

We have the following property, which holds by definition of the entries of <Ref>:

If $\Gamma \vaslinunsplit \Delta \st P$ then $ \dillnotun{\sttodillt{\Gamma'}{}{}} ;  \sttodillt{\Delta'}{}{} \dill \sttodillp{P}{} :: u: A$ is well-typed in , with  $A, \Gamma'$ and $\Delta'$ as in <Ref>.

Notice that the translations of typable processes are not necessarily typable in .
We shall concentrate on  processes in $\vaslang$ that are typable in $\pidill$:

We write $\dillnotun{\sttodillt{\Gamma'}};   \sttodillt{\Delta'}  \dill \sttodillp{{P}}  :: u: \sttodillt{\dual{S}} $ whenever $\sttodillj{\Gamma ,\Delta  \st P}_u$  holds, with $\Gamma \dillcontrel{u}{S} \Gamma'$ and $\Delta \dillcontrel{u}{S} \Delta'$.

We can finally define $\dilllang$:

Let $u$ be a name.	We define:

\begin{align*}
\dilllang = \{ P \in \vasco \mid &  \ \Gamma \vaslinunsplit \Delta \st P \land 	\Gamma \dillcontrel{u}{S} \Gamma'
\land  \Delta \dillcontrel{u}{S} \Delta'  \\	& \land \dillnotun{\sttodillt{\Gamma'}};   \sttodillt{\Delta'}  \dill \sttodillp{{P}}  :: u: \sttodillt{\dual{S}} 	\}
\end{align*}

where contexts and types mentioned are existentially quantified.

§.§ Results

Let $P\in \vaslang$ such that $\Gamma \st P$, for some context $\Gamma$. If there exists $  u$  such that  $\sttodillj{\Gamma \st P}_u $ holds, then there exists $l$ such that $ \sttoltj{\Gamma \st P}{l}{}$ holds.

The proof of <Ref> is
by induction on the structure of $P$.
We exploit a number of invariant properties for the type systems for and , including:

* In $\pidill$, judgments for typed processes never exhibit servers on the left-hand side.

* In , levels for types that do not exhibit server behavior can be decreased at will.

* The type system of ensures that the name on the right-hand side is not guarded by servers.

$\exists P \in \lvllang$  with $\Gamma \st P$ and $\sttoltj{\Gamma \st P}{l}{} $ for some $l$  such that $ \nexists  \ z \ s.t. \ \sttodillj{\Gamma \st P}_z $.

To prove <Ref>, it suffices to consider the process

\[
P =
\vasres{xy}{(
\vaspara{
\vasin{\lin}{x}{z}{\vasin{\un}{z}{w}{\nil}}
\vasres{st}{
\vasout{y}{s}{(
\vaspara{
\vasres{uv}{(\vasout{t}{u}{\nil})}
\nil
\]

Clearly, $P$ is terminating:

\[
\begin{aligned}
P &\redd
\vasres{st}{(
\vaspara{
\vasin{\un}{s}{w}{\nil}
\vasres{uv}{(\vasout{t}{u}{\nil})}
\redd
\vasres{st}{
\vasin{\un}{s}{w}{\nil}
\end{aligned}
\]

Process $P$ can be typed so as to establish $P \in  \vaslang$.
Also, there is a level function that makes its translation into typable. Hence, $P \in \lvllang$.
However, its translation into is not typable, so $P \not\in \dilllang$.

§ CLOSING REMARKS

We presented a comparative study of type systems for concurrent processes in the $\pi$-calculus, from the unifying perspective of termination and session types.
To our knowledge, this is the first study of its kind.
Even by focusing on only three different type systems, we were confronted with technical challenges connected with the intrinsic differences between them.
The typed process model  <cit.>, focused on session-based concurrency, admits a rather broad class of processes, exploiting a clear distinction between linear and unrestricted resources, implemented via context splitting.
The typed process model combines features from type systems that target the termination property <cit.> and type systems for sessions.
Finally, the typed process model  <cit.> rests upon a firm logical foundation, and its control of clients and servers is directly inherited from the logical principles of the exponential $!A$.
Notice that is unique among type systems for the $\pi$-calculus in that it ensures  protocol fidelity, deadlock-freedom, confluence, and strong normalization/termination for typed processes.

The main take-away message is that the Curry-Howard correspondence is strictly weaker than weight-based approaches for enforcing the termination property.
Hence, the  control of server/client interactions that is elegantly enabled by the copying semantics of  $!A$ turns out to be rather implicit when contrasted to weight-based techniques.
Interestingly,  Dardha and Pérez arrived to a similar conclusion in their comparative study of type systems focused on the deadlock-freedom property <cit.>: type systems based on the Curry-Howard correspondence can detect strictly less deadlock-free processes than other, more sophisticated type systems.
Notice that the study in <cit.> considers only finite processes, without input-guarded replication (so all process are terminating).

Immediate items for current and future work include incorporating other type systems into our formal comparisons.
The type systems by Sangiorgi <cit.> and by Yoshida et al. <cit.> are very appealing candidates.
Also, Deng and Sangiorgi proposed several type systems for termination.
Here we considered only the simplest variant, which induces the class and is already different from ; it would be interesting to consider the other variants.

§ ACKNOWLEDGMENTS

We  acknowledge the support of
the Dutch Research Council (NWO) under project No. 016.Vidi.189.046 (Unifying Correctness for Communicating Software).
Daniele Nantes-Sobrinho has been supported by the EPSRC Fellowship `VeTSpec: Verified Trustworthy Software Specification' (EP/R034567/1) and Edital DPI/DPG n. 03/2020.

We are grateful to
Davide Sangiorgi,
Nobuko Yoshida,  and
the anonymous reviewers for useful suggestions and remarks.