11institutetext:  Department of Computing, Imperial College London, United
Kingdom

# On Polymorphic Sessions and Functions

A Tale of Two (Fully Abstract) Encodings

Bernardo Toninho  Nobuko Yoshida

###### Abstract

This work exploits the logical foundation of session types to determine what
kind of type discipline for the $\pi$-calculus can exactly capture, and is
captured by, $\lambda$-calculus behaviours. Leveraging the proof theoretic
content of the soundness and completeness of sequent calculus and natural
deduction presentations of linear logic, we develop the first _mutually
inverse_ and _fully abstract_ processes-as-functions and functions-as-
processes encodings between a polymorphic session $\pi$-calculus and a linear
formulation of System F. We are then able to derive results of the session
calculus from the theory of the $\lambda$-calculus: (1) we obtain a
characterisation of inductive and coinductive session types via their
algebraic representations in System F; and (2) we extend our results to
account for _value_ and _process_ passing, entailing strong normalisation.

##  1 Introduction

Dating back to Milner's seminal work [29], encodings of $\lambda$-calculus
into $\pi$-calculus are seen as essential benchmarks to examine expressiveness
of various extensions of the $\pi$-calculus. Milner's original motivation was
to demonstrate the power of link mobility by decomposing higher-order
computations into pure name passing. Another goal was to analyse functional
behaviours in a broad computational universe of concurrency and non-
determinism. While _operationally_ correct encodings of many higher-order
constructs exist, it is challenging to obtain encodings that are precise wrt
behavioural equivalence: the semantic distance between the $\lambda$-calculus
and the $\pi$-calculus typically requires either restricting process
behaviours [45] (e.g. via typed equivalences [5]) or enriching the
$\lambda$-calculus with constants that allow for a suitable characterisation
of the term equivalence induced by the behavioural equivalence on processes
[43].

Encodings in $\pi$-calculi also gave rise to new typing disciplines: Session
types [20, 22], a typing system that is able to ensure deadlock-freedom for
communication protocols between two or more parties [23], were originally
motivated ``from process encodings of various data structures in an
asynchronous version of the $\pi$-calculus'' [21]. Recently, a propositions-
as-types correspondence between linear logic and session types [8, 9, 54] has
produced several new developments and logically-motivated techniques [49, 54,
7, 26] to augment both the theory and practice of session-based message-
passing concurrency. Notably, parametric session polymorphism [7] (in the
sense of Reynolds [41]) has been proposed and a corresponding abstraction
theorem has been shown.

Our work expands upon the proof theoretic consequences of this propositions-
as-types correspondence to address the problem of how to exactly match the
behaviours induced by session $\pi$-calculus encodings of the
$\lambda$-calculus with those of the $\lambda$-calculus. We develop mutually
inverse and fully abstract encodings (up to typed observational congruences)
between a polymorphic session-typed $\pi$-calculus and the polymorphic
$\lambda$-calculus. The encodings arise from the proof theoretic content of
the equivalence between sequent calculus (i.e. the session calculus) and
natural deduction (i.e. the $\lambda$-calculus) for _second-order_
intuitionistic linear logic, greatly generalising [49]. While fully abstract
encodings between $\lambda$-calculi and $\pi$-calculi have been proposed (e.g.
[5, 43]), our work is the first to consider a two-way, _both_ mutually inverse
_and_ fully abstract embedding between the two calculi by crucially exploiting
the linear logic-based session discipline. This also sheds some definitive
light on the nature of concurrency in the (logical) session calculi, which
exhibit ``don't care'' forms of non-determinism (e.g. processes may race on
stateless replicated servers) rather than ``don't know'' non-determinism
(which requires less harmonious logical features [2]).

In the spirit of Gentzen [14], we use our encodings as a tool to study non-
trivial properties of the session calculus, deriving them from results in the
$\lambda$-calculus: We show the existence of inductive and coinductive
sessions in the polymorphic session calculus by considering the representation
of initial $F$-algebras and final $F$-coalgebras [28] in the polymorphic
$\lambda$-calculus [1, 19] (in a linear setting [6]). By appealing to full
abstraction, we are able to derive processes that satisfy the necessary
algebraic properties and thus form adequate _uniform_ representations of
inductive and coinductive session types. The derived algebraic properties
enable us to reason about standard data structure examples, providing a
logical justification to typed variations of the representations in [30].

We systematically extend our results to a session calculus with $\lambda$-term
and process passing (the latter being the core calculus of [50], inspired by
Benton's LNL [4]). By showing that our encodings naturally adapt to this
setting, we prove that it is possible to encode higher-order process passing
in the first-order session calculus fully abstractly, providing a typed and
proof-theoretically justified re-envisioning of Sangiorgi's encodings of
higher-order $\pi$-calculus [46]. In addition, the encoding instantly provides
a strong normalisation property of the higher-order session calculus.

Contributions and the outline of our paper are as follows:

§ 3.1

develops a functions-as-processes encoding of a linear formulation of System
F, Linear-F, using a logically motivated polymorphic session $\pi$-calculus,
Poly$\pi$, and shows that the encoding is operationally sound and complete.

§ 3.2

develops a processes-as-functions encoding of Poly$\pi$ into Linear-F, arising
from the completeness of the sequent calculus wrt natural deduction, also
operationally sound and complete.

§ 3.3

studies the relationship between the two encodings, establishing they are
_mutually inverse_ and _fully abstract_ wrt typed congruence, the first two-
way embedding satisfying _both_ properties.

§ 4

develops a _faithful_ representation of inductive and coinductive session
types in Poly$\pi$ via the encoding of initial and final (co)algebras in the
polymorphic $\lambda$-calculus. We demonstrate a use of these algebraic
properties via examples.

§ 4.2,4.3

study term-passing and process-passing session calculi, extending our
encodings to provide embeddings into the first-order session calculus. We show
full abstraction and mutual inversion results, and derive strong normalisation
of the higher-order session calculus from the encoding.

In order to introduce our encodings, we first overview Poly$\pi$, its typing
system and behavioural equivalence (§ 2). We discuss related work and conclude
with future work (§ 5). Detailed proofs can be found in [52].

##  2 Polymorphic Session $\pi$-Calculus

This section summarises the polymorphic session $\pi$-calculus [7], dubbed
Poly$\pi$, arising as a process assignment to second-order linear logic [15],
its typing system and behavioural equivalences.

###  2.1 Processes and Typing

Syntax.  Given an infinite set $\Lambda$ of names $x,y,z,u,v$, the grammar of
processes $P,Q,R$ and session types $A,B,C$ is defined by:

$\begin{array}[]{l}\begin{array}[]{lclllllllllllllllll}P,Q,R&::=&x\langle
y\rangle.P&\mid&x(y).P&\mid&P\mid
Q&\mid&(\mathbf{\nu}y)P&\mid&[x\leftrightarrow y]&\mid&{\bf 0}\\\\[2.84526pt]
&\mid&x\langle
A\rangle.P&\mid&x(Y).P&\mid&x.\mathsf{inl};P&\mid&x.\mathsf{inr};P&\mid&x.\mathsf{case}(P,Q)&\mid&!x(y).P\\\\[2.84526pt]
\end{array}\\\\[2.84526pt] \begin{array}[]{lcl}A,B&::=&\mathbf{1}\mid
A\multimap B\mid A\otimes B\mid A\with B\mid A\oplus B\mid\,\,!A\mid\forall
X.A\mid\exists X.A\mid X\end{array}\end{array}$

$x\langle y\rangle.P$ denotes the output of channel $y$ on $x$ with
continuation process $P$; $x(y).P$ denotes an input along $x$, bound to $y$ in
$P$; $P\mid Q$ denotes parallel composition; $(\mathbf{\nu}y)P$ denotes the
restriction of name $y$ to the scope of $P$; ${\bf 0}$ denotes the inactive
process; $[x\leftrightarrow y]$ denotes the linking of the two channels $x$
and $y$ (implemented as renaming); $x\langle A\rangle.P$ and $x(Y).P$ denote
the sending and receiving of a _type_ $A$ along $x$ bound to $Y$ in $P$ of the
receiver process; $x.\mathsf{inl};P$ and $x.\mathsf{inr};P$ denote the
emission of a selection between the $\mathsf{l}$eft or $\mathsf{r}$ight branch
of a receiver $x.\mathsf{case}(P,Q)$ process; $!x(y).P$ denotes an input-
guarded replication, that spawns replicas upon receiving an input along $x$.
We often abbreviate $(\mathbf{\nu}y)x\langle y\rangle.P$ to
$\overline{x}\langle y\rangle.P$ and omit trailing ${\bf 0}$ processes. By
convention, we range over linear channels with $x,y,z$ and shared channels
with $u,v,w$.

The syntax of session types is that of (intuitionistic) linear logic
propositions which are assigned to channels according to their usages in
processes: $\mathbf{1}$ denotes the type of a channel along which no further
behaviour occurs; $A\multimap B$ denotes a session that waits to receive a
channel of type $A$ and will then proceed as a session of type $B$; dually,
$A\otimes B$ denotes a session that sends a channel of type $A$ and continues
as $B$; $A\with B$ denotes a session that offers a choice between proceeding
as behaviours $A$ or $B$; $A\oplus B$ denotes a session that internally
chooses to continue as either $A$ or $B$, signalling appropriately to the
communicating partner; $!A$ denotes a session offering an unbounded (but
finite) number of behaviours of type $A$; $\forall X.A$ denotes a polymorphic
session that receives a type $B$ and behaves uniformly as $A\\{B/X\\}$;
dually, $\exists X.A$ denotes an existentially typed session, which emits a
type $B$ and behaves as $A\\{B/X\\}$.

Operational Semantics.  The operational semantics of our calculus is presented
as a standard labelled transition system (Fig. 1) in the style of the _early_
system for the $\pi$-calculus [46].

In the remainder of this work we write $\equiv$ for a standard $\pi$-calculus
structural congruence extended with the clause $[x\leftrightarrow
y]\equiv[y\leftrightarrow x]$. In order to streamline the presentation of
observational equivalence [36, 7], we write $\equiv_{!}$ for structural
congruence extended with the so-called sharpened replication axioms [46],
which capture basic equivalences of replicated processes (and are present in
the proof dynamics of the exponential of linear logic). A transition
$P\xrightarrow{~{}\alpha~{}}Q$ denotes that $P$ may evolve to $Q$ by
performing the action represented by label $\alpha$. An action $\alpha$
($\overline{\alpha}$) requires a matching $\overline{\alpha}$ ($\alpha$) in
the environment to enable progress. Labels include: the silent internal action
$\tau$, output and bound output actions ($\overline{x\langle y\rangle}$ and
$\overline{(\nu z)x\langle z\rangle}$); input action $x(y)$; the binary choice
actions ($x.\mathsf{inl}$, $\overline{x.\mathsf{inl}}$, $x.\mathsf{inr}$, and
$\overline{x.\mathsf{inr}}$); and output and input actions of types
($\overline{x\langle A\rangle}$ and $x(A)$).

The labelled transition relation is defined by the rules in Fig. 1, subject to
the side conditions: in rule $(\mathsf{res})$, we require $y\not\in\mbox{\it
fn}(\alpha)$; in rule $(\mathsf{par})$, we require $\mbox{\it
bn}(\alpha)\cap\mbox{\it fn}(R)=\emptyset$; in rule $(\mathsf{close})$, we
require $y\not\in\mbox{\it fn}(Q)$. We omit the symmetric versions of
$(\mathsf{par})$, $(\mathsf{com})$, $(\mathsf{lout})$, $(\mathsf{lin})$,
$(\mathsf{close})$ and closure under $\alpha$-conversion. We write
$\rho_{1}\rho_{2}$ for the composition of relations $\rho_{1},\rho_{2}$. We
write $\xrightarrow{}$ to stand for $\xrightarrow{\tau}\equiv$. Weak
transitions are defined as usual: we write
$\stackrel{{\scriptstyle}}{{\Longrightarrow}}$ for the reflexive, transitive
closure of $\xrightarrow{\tau}$ and $\xrightarrow{}^{+}$ for the transitive
closure of $\xrightarrow{\tau}$. Given $\alpha\neq\tau$, notation
$\stackrel{{\scriptstyle\alpha}}{{\Longrightarrow}}$ stands for
$\stackrel{{\scriptstyle~{}}}{{\Longrightarrow}}\xrightarrow{\alpha}\stackrel{{\scriptstyle~{}}}{{\Longrightarrow}}$
and $\stackrel{{\scriptstyle\tau}}{{\Longrightarrow}}$ stands for
$\stackrel{{\scriptstyle}}{{\Longrightarrow}}$.

$\begin{array}[]{ccccc}{\vbox{\hbox{\hbox{\small\sc\mbox{{\scriptsize{{($\displaystyle\mathsf{out}$)}}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
22.60664pt\vbox{\vbox{}\hbox{\hskip-22.60663pt\hbox{\hbox{$\displaystyle\displaystyle{x\langle
y\rangle.P\xrightarrow{\overline{x\langle y\rangle}}P}$}}}}}}$}}}\hskip
8.5359pt{\vbox{\hbox{\hbox{\small\sc\mbox{{\scriptsize{{($\displaystyle\mathsf{in}$)}}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
40.2386pt\vbox{\vbox{}\hbox{\hskip-40.2386pt\hbox{\hbox{$\displaystyle\displaystyle{x(y).P\xrightarrow{x(z)}P\\{\raisebox{1.93748pt}{\small$\displaystyle
z$}\\!/\mbox{\small$\displaystyle y$}\\}}$}}}}}}$}}}\hskip
8.5359pt{\vbox{\hbox{\hbox{\small\sc\mbox{{\scriptsize{{($\displaystyle\mathsf{outT}$)}}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
23.61392pt\vbox{\vbox{}\hbox{\hskip-23.61392pt\hbox{\hbox{$\displaystyle\displaystyle{x\langle
A\rangle.P\xrightarrow{\overline{x\langle A\rangle}}P}$}}}}}}$}}}\hskip
8.5359pt{\vbox{\hbox{\hbox{\small\sc\mbox{{\scriptsize{{($\displaystyle\mathsf{inT}$)}}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
45.42505pt\vbox{\vbox{}\hbox{\hskip-45.42505pt\hbox{\hbox{$\displaystyle\displaystyle{x(Y).P\xrightarrow{x(B)}P\\{\raisebox{1.93748pt}{\small$\displaystyle
B$}\\!/\mbox{\small$\displaystyle Y$}\\}}$}}}}}}$}}}\\\\[2.84526pt]
\begin{array}[]{ll}\begin{array}[]{c}{\vbox{\hbox{\hbox{\small\sc\mbox{{\scriptsize{{($\displaystyle\mathsf{lout}$)}}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
22.60002pt\vbox{\vbox{}\hbox{\hskip-22.60002pt\hbox{\hbox{$\displaystyle\displaystyle{x.\mathsf{inl};P\xrightarrow{\overline{x.\mathsf{inl}}}P}$}}}}}}$}}}\hskip
8.5359pt{\vbox{\hbox{\hbox{\small\sc\mbox{{\scriptsize{{($\displaystyle\mathsf{id}$)}}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
52.91936pt\vbox{\vbox{}\hbox{\hskip-52.91934pt\hbox{\hbox{$\displaystyle\displaystyle{(\nu
x)([x\leftrightarrow y]\mid
P)\xrightarrow{\tau}P\\{\raisebox{1.93748pt}{\small$\displaystyle
y$}\\!/\mbox{\small$\displaystyle x$}\\}}$}}}}}}$}}}\\\\[2.84526pt]
{\vbox{\hbox{\hbox{\small\sc\mbox{{\scriptsize{{($\displaystyle\mathsf{lin}$)}}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
38.5044pt\vbox{\vbox{}\hbox{\hskip-38.5044pt\hbox{\hbox{$\displaystyle\displaystyle{x.\mathsf{case}(P,Q)\xrightarrow{x.\mathsf{inl}}P}$}}}}}}$}}}\hskip
8.5359pt{\vbox{\hbox{\hbox{\small\sc\mbox{{\scriptsize{{($\displaystyle\mathsf{rep}$)}}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
58.69226pt\vbox{\vbox{}\hbox{\hskip-58.69226pt\hbox{\hbox{$\displaystyle\displaystyle{!x(y).P\xrightarrow{x(z)}P\\{\raisebox{1.93748pt}{\small$\displaystyle
z$}\\!/\mbox{\small$\displaystyle y$}\\}\mid!x(y).P}$}}}}}}$}}}\\\\[2.84526pt]
\end{array}\quad\begin{array}[]{l}{\vbox{\hbox{\hbox{\small\sc\mbox{{\scriptsize{{($\displaystyle\mathsf{open}$)}}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
11.82158pt\vbox{\hbox{\hskip-11.82156pt\hbox{\hbox{$\displaystyle\displaystyle{P\xrightarrow{\overline{x\langle
y\rangle}}Q}$}}}\vbox{}}}\over\hbox{\hskip
19.91222pt\vbox{\vbox{}\hbox{\hskip-19.91222pt\hbox{\hbox{$\displaystyle\displaystyle{(\mathbf{\nu}y)P\xrightarrow{\overline{(\mathbf{\nu}y)x\langle
y\rangle}}Q}$}}}}}}$}}}\\\ \end{array}\\\ \end{array}\\\
{\vbox{\hbox{\hbox{\small\sc\mbox{{\scriptsize{{($\displaystyle\mathsf{close}$)}}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
32.46872pt\vbox{\hbox{\hskip-32.46872pt\hbox{\hbox{$\displaystyle\displaystyle{P\xrightarrow{\overline{(\mathbf{\nu}y)x\langle
y\rangle}}P^{\prime}\,\,Q\xrightarrow{x(y)}Q^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
36.33694pt\vbox{\vbox{}\hbox{\hskip-36.33694pt\hbox{\hbox{$\displaystyle\displaystyle{P\mid
Q\xrightarrow{\tau}(\mathbf{\nu}y)(P^{\prime}\mid
Q^{\prime})}$}}}}}}$}}}\hskip
8.5359pt{\vbox{\hbox{\hbox{\small\sc\mbox{{\scriptsize{{($\displaystyle\mathsf{par}$)}}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
12.20023pt\vbox{\hbox{\hskip-12.20021pt\hbox{\hbox{$\displaystyle\displaystyle{P\xrightarrow{\alpha}Q}$}}}\vbox{}}}\over\hbox{\hskip
25.10335pt\vbox{\vbox{}\hbox{\hskip-25.10333pt\hbox{\hbox{$\displaystyle\displaystyle{P\mid
R\xrightarrow{\alpha}Q\mid R}$}}}}}}$}}}\hskip
8.5359pt{\vbox{\hbox{\hbox{\small\sc\mbox{{\scriptsize{{($\displaystyle\mathsf{com}$)}}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
26.90778pt\vbox{\hbox{\hskip-26.90778pt\hbox{\hbox{$\displaystyle\displaystyle{P\xrightarrow{\overline{\alpha}}P^{\prime}\,\,Q\xrightarrow{\alpha}Q^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
24.7463pt\vbox{\vbox{}\hbox{\hskip-24.74629pt\hbox{\hbox{$\displaystyle\displaystyle{P\mid
Q\xrightarrow{\tau}P^{\prime}\mid Q^{\prime}}$}}}}}}$}}}\hskip
8.5359pt{\vbox{\hbox{\hbox{\small\sc\mbox{{\scriptsize{{($\displaystyle\mathsf{res}$)}}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
12.20023pt\vbox{\hbox{\hskip-12.20021pt\hbox{\hbox{$\displaystyle\displaystyle{P\xrightarrow{\alpha}Q}$}}}\vbox{}}}\over\hbox{\hskip
28.38152pt\vbox{\vbox{}\hbox{\hskip-28.3815pt\hbox{\hbox{$\displaystyle\displaystyle{(\mathbf{\nu}y)P\xrightarrow{\alpha}(\mathbf{\nu}y)Q}$}}}}}}$}}\par}\end{array}\vspace{-4ex}$
Figure 1: Labelled Transition System.

Typing System.  The typing rules of Poly$\pi$ are given in Fig. 2, following
[7]. The rules define the judgment $\Omega;\Gamma;\Delta\vdash P::z{:}A$,
denoting that process $P$ offers a session of type $A$ along channel $z$,
using the _linear_ sessions in $\Delta$, (potentially) using the unrestricted
or _shared_ sessions in $\Gamma$, with polymorphic type variables maintained
in $\Omega$. We use a well-formedness judgment $\Omega\vdash A\,\mathsf{type}$
which states that $A$ is well-formed wrt the type variable environment
$\Omega$ (i.e. $\mathit{fv}(A)\subseteq\Omega$). We often write $T$ for the
right-hand side typing $z{:}A$, $\cdot$ for the empty context and
$\Delta,\Delta^{\prime}$ for the union of contexts $\Delta$ and
$\Delta^{\prime}$, only defined when $\Delta$ and $\Delta^{\prime}$ are
disjoint. We write $\cdot\vdash P::T$ for $\cdot;\cdot;\cdot\vdash P::T$.

$\begin{array}[]{c}\raise
10.5pt\hbox{$\hbox{$\hbox{\small\sc$({{\multimap}\mathsf{R}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
48.95317pt\vbox{\hbox{\hskip-48.95316pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta,x{:}A\vdash
P::z{:}B}$}}}\vbox{}}}\over\hbox{\hskip
58.4938pt\vbox{\vbox{}\hbox{\hskip-58.4938pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta\vdash
z(x).P::z{:}A\multimap B}$}}}}}}$}}\hbox{}$}\quad\raise
11.0pt\hbox{$\hbox{$\hbox{\small\sc$({{\otimes}\mathsf{R}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
76.38904pt\vbox{\hbox{\hskip-76.38904pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta_{1}\vdash
P::y{:}A\quad\Omega;\Gamma;\Delta_{2}\vdash
Q::z{:}B}$}}}\vbox{}}}\over\hbox{\hskip
82.05086pt\vbox{\vbox{}\hbox{\hskip-82.05084pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta_{1},\Delta_{2}\vdash(\mathbf{\nu}x)z\langle
y\rangle.(P\mid Q)::z{:}A\otimes B}$}}}}}}$}}\hbox{}$}\\\\[9.00002pt] \raise
10.5pt\hbox{$\hbox{$\hbox{\small\sc$({{\forall}\mathsf{R}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
43.07347pt\vbox{\hbox{\hskip-43.07346pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega,X;\Gamma;\Delta\vdash
P::z{:}A}$}}}\vbox{}}}\over\hbox{\hskip
57.94534pt\vbox{\vbox{}\hbox{\hskip-57.94534pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta\vdash
z(X).P::z{:}\forall X.A}$}}}}}}$}}\hbox{}$}\quad\raise
11.0pt\hbox{$\hbox{$\hbox{\small\sc$({{\forall}\mathsf{L}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
90.71165pt\vbox{\hbox{\hskip-90.71165pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega\vdash
B\,\mathsf{type}\quad\Omega;\Gamma;\Delta,x{:}A\\{B/X\\}\vdash
P::z{:}C}$}}}\vbox{}}}\over\hbox{\hskip
70.03331pt\vbox{\vbox{}\hbox{\hskip-70.03331pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta,x{:}\forall
X.A\vdash x\langle B\rangle.P::z{:}C}$}}}}}}$}}\hbox{}$}\\\\[9.00002pt] \raise
11.0pt\hbox{$\hbox{$\hbox{\small\sc$({{\exists}\mathsf{R}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
79.97665pt\vbox{\hbox{\hskip-79.97665pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega\vdash
B\,\mathsf{type}\quad\Omega;\Gamma;\Delta\vdash
P::z{:}A\\{B/X\\}}$}}}\vbox{}}}\over\hbox{\hskip
57.89207pt\vbox{\vbox{}\hbox{\hskip-57.89206pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta\vdash
z\langle B\rangle.P::z{:}\exists X.A}$}}}}}}$}}\hbox{}$}\quad\raise
10.5pt\hbox{$\hbox{$\hbox{\small\sc$({{\exists}\mathsf{L}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
54.93346pt\vbox{\hbox{\hskip-54.93346pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega,X;\Gamma;\Delta,x{:}A\vdash
P::z{:}C}$}}}\vbox{}}}\over\hbox{\hskip
70.0866pt\vbox{\vbox{}\hbox{\hskip-70.08658pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta,x{:}\exists
X.A\vdash x(X).P::z{:}C}$}}}}}}$}}\hbox{}$}\\\\[9.00002pt] \raise
10.5pt\hbox{$\hbox{$\hbox{\small\sc$(\mathsf{id})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.75pt\vbox{\hbox{\hskip-0.75pt\hbox{\hbox{$\displaystyle\displaystyle{\,}$}}}\vbox{}}}\over\hbox{\hskip
53.78755pt\vbox{\vbox{}\hbox{\hskip-53.78754pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;x{:}A\vdash[x\leftrightarrow
z]::z{:}A}$}}}}}}$}}\hbox{}$}\quad\raise
10.5pt\hbox{$\hbox{$\hbox{\small\sc$(\mathsf{cut})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
91.93913pt\vbox{\hbox{\hskip-91.93912pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta_{1}\vdash
P::x{:}A\quad\Omega;\Gamma;\Delta_{2},x{:}A\vdash
Q::z{:}C}$}}}\vbox{}}}\over\hbox{\hskip
62.52763pt\vbox{\vbox{}\hbox{\hskip-62.52763pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta_{1},\Delta_{2}\vdash(\mathbf{\nu}x)(P\mid
Q)::z{:}C}$}}}}}}$}}\hbox{}$}\end{array}$ Figure 2: Typing Rules (Abridged –
See [52] for all rules).

As in [8, 9, 36, 54], the typing discipline enforces that channel outputs
always have as object a _fresh_ name, in the style of the internal mobility
$\pi$-calculus [44]. We clarify a few of the key rules: Rule
${{\forall}\mathsf{R}}$ defines the meaning of (impredicative) universal
quantification over session types, stating that a session of type $\forall
X.A$ inputs a type and then behaves uniformly as $A$; dually, to use such a
session (rule ${{\forall}\mathsf{L}}$), a process must output a type $B$ which
then warrants the use of the session as type $A\\{B/X\\}$. Rule
${{\multimap}\mathsf{R}}$ captures session input, where a session of type
$A\multimap B$ expects to receive a session of type $A$ which will then be
used to produce a session of type $B$. Dually, session output (rule
${{\otimes}\mathsf{R}}$) is achieved by producing a fresh session of type $A$
(that uses a disjoint set of sessions to those of the continuation) and
outputting the fresh session along $z$, which is then a session of type $B$.
Linear composition is captured by rule $\mathsf{cut}$ which enables a process
that offers a session $x{:}A$ (using linear sessions in $\Delta_{1}$) to be
composed with a process that _uses_ that session (amongst others in
$\Delta_{2}$) to offer $z{:}C$. As shown in [7], typing entails Subject
Reduction, Global Progress, and Termination.

Observational Equivalences.  We briefly summarise the typed congruence and
logical equivalence with polymorphism, giving rise to a suitable notion of
relational parametricity in the sense of Reynolds [41], defined as a
contextual logical relation on typed processes [7]. The logical relation is
reminiscent of a typed bisimulation. However, extra care is needed to ensure
well-foundedness due to impredicative type instantiation. As a consequence,
the logical relation allows us to reason about process equivalences where type
variables are not instantiated with _the same_ , but rather _related_ types.

Typed Barbed Congruence ($\cong$).  We use the typed contextual congruence
from [7], which preserves _observable_ actions, called barbs. Formally,
_barbed congruence_ , noted $\cong$, is the largest equivalence on well-typed
processes that is $\tau$-closed, barb preserving, and contextually closed
under typed contexts; see [7] and [52] for the full definition.

Logical Equivalence ($\approx_{\mathtt{L}}$).  The definition of logical
equivalence is no more than a typed contextual bisimulation with the following
intuitive reading: given two open processes $P$ and $Q$ (i.e. processes with
non-empty left-hand side typings), we define their equivalence by inductively
closing out the context, composing with equivalent processes offering
appropriately typed sessions. When processes are closed, we have a single
distinguished session channel along which we can perform observations, and
proceed inductively on the structure of the offered session type. We can then
show that such an equivalence satisfies the necessary fundamental properties
(Theorem 2.1).

The logical relation is defined using the candidates technique of Girard [16].
In this setting, an _equivalence candidate_ is a relation on typed processes
satisfying basic closure conditions: an equivalence candidate must be
compatible with barbed congruence and closed under forward and converse
reduction.

######  Definition 2.1 (Equivalence Candidate)

An _equivalence candidate_ $\mathcal{R}$ at $z{:}A$ and $z{:}B$, noted
$\mathcal{R}::z{:}A\\!\Leftrightarrow\\!B$, is a binary relation on processes
such that, for every $(P,Q)\in\mathcal{R}::z{:}A\\!\Leftrightarrow\\!B$ both
$\cdot\vdash P::z{:}A$ and $\cdot\vdash Q::z{:}B$ hold, together with the
following (we often write $(P,Q)\in\mathcal{R}::z{:}A\\!\Leftrightarrow\\!B$
as $P\,\mathcal{R}\,Q::z{:}A\\!\Leftrightarrow\\!B$):

  1. 1.

If $(P,Q)\in\mathcal{R}::z{:}A\\!\Leftrightarrow\\!B$, $\cdot\vdash P\cong
P^{\prime}::z{:}A$, and $\cdot\vdash Q\cong Q^{\prime}::z{:}B$ then
$(P^{\prime},Q^{\prime})\in\mathcal{R}::z{:}A\\!\Leftrightarrow\\!B$.

  2. 2.

If $(P,Q)\in\mathcal{R}::z{:}A\\!\Leftrightarrow\\!B$ then, for all $P_{0}$
such that $\cdot\vdash P_{0}::z{:}A$ and
$P_{0}\stackrel{{\scriptstyle}}{{\Longrightarrow}}P$, we have
$(P_{0},Q)\in\,\mathcal{R}::z{:}A\\!\Leftrightarrow\\!B$. Symmetrically for
$Q$.

To define the logical relation we rely on some auxiliary notation, pertaining
to the treatment of type variables arising due to impredicative polymorphism.
We write $\omega:\Omega$ to denote a mapping $\omega$ that assigns a closed
type to the type variables in $\Omega$. We write $\omega(X)$ for the type
mapped by $\omega$ to variable $X$. Given two mappings $\omega:\Omega$ and
$\omega^{\prime}:\Omega$, we define an equivalence candidate assignment $\eta$
between $\omega$ and $\omega^{\prime}$ as a mapping of equivalence candidate
$\eta(X)::{-}{:}\omega(X)\\!\Leftrightarrow\\!\omega^{\prime}(X)$ to the type
variables in $\Omega$, where the particular choice of a distinguished right-
hand side channel is _delayed_ (i.e. to be instantiated later on). We write
$\eta(X)(z)$ for the instantiation of the (delayed) candidate with the name
$z$. We write $\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}$ to denote that
$\eta$ is a candidate assignment between $\omega$ and $\omega^{\prime}$; and
$\hat{\omega}(P)$ to denote the application of mapping $\omega$ to $P$.

We define a sequent-indexed family of process relations, that is, a set of
pairs of processes $(P,Q)$, written $\Gamma;\Delta\vdash
P\approx_{\mathtt{L}}Q::T[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]$,
satisfying some conditions, typed under $\Omega;\Gamma;\Delta\vdash T$, with
$\omega:\Omega$, $\omega^{\prime}:\Omega$ and
$\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}$. Logical equivalence is
defined inductively on the size of the typing contexts and then on the
structure of the right-hand side type. We show only select cases (see [52] for
the full definition).

######  Definition 2.2 (Logical Equivalence)

(Base Case) Given a type $A$ and mappings $\omega,\omega^{\prime},\eta$, we
define _logical equivalence_ , noted
$P\approx_{\mathtt{L}}Q::z{:}A[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]$,
as the smallest symmetric binary relation containing all pairs of processes
$(P,Q)$ such that (i) $\cdot\vdash\hat{\omega}(P)::z{:}\hat{\omega}(A)$; (ii)
$\cdot\vdash\hat{\omega}^{\prime}(Q)::z{:}\hat{\omega}^{\prime}(A)$; and (iii)
satisfies the conditions given below:

  * •

$P\approx_{\mathtt{L}}Q::z{:}X[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]\text{
iff }(P,Q)\in\eta(X)(z)$

  * •

$P\approx_{\mathtt{L}}Q::z{:}A\multimap
B[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]$ iff $\forall
P^{\prime},y.~{}(P\xrightarrow{z(y)}P^{\prime})\Rightarrow\exists
Q^{\prime}.Q\stackrel{{\scriptstyle z(y)}}{{\Longrightarrow}}Q^{\prime}$ s.t.
$\forall
R_{1},R_{2}.R_{1}\approx_{\mathtt{L}}R_{2}::y{:}A[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}](\nu
y)(P^{\prime}\,|\,R_{1})\approx_{\mathtt{L}}(\nu
y)(Q^{\prime}\,|\,R_{2})::z{:}B[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]$

  * •

$P\approx_{\mathtt{L}}Q::z{:}A\otimes
B[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]$ iff $\forall
P^{\prime},y.~{}~{}(P\xrightarrow{\overline{(\nu y)z\langle
y\rangle}}P^{\prime})\Rightarrow\exists
Q^{\prime}.Q\stackrel{{\scriptstyle\overline{(\nu y)z\langle
y\rangle}}}{{\Longrightarrow}}Q^{\prime}$ s.t. $\exists
P_{1},P_{2},Q_{1},Q_{2}.\ P^{\prime}\equiv_{!}P_{1}\mid P_{2}\wedge
Q^{\prime}\equiv_{!}Q_{1}\mid Q_{2}\wedge
P_{1}\approx_{\mathtt{L}}Q_{1}::y{:}A[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]\wedge
P_{2}\approx_{\mathtt{L}}Q_{2}::z{:}B[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]$

  * •

$P\approx_{\mathtt{L}}Q::z{:}\forall
X.A[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]$ iff $\forall
B_{1},B_{2},P^{\prime},\mathcal{R}::{-}{:}B_{1}\\!\Leftrightarrow\\!B_{2}.~{}~{}(P\xrightarrow{z(B_{1})}P^{\prime})$
implies $\exists Q^{\prime}.Q\stackrel{{\scriptstyle
z(B_{2})}}{{\Longrightarrow}}Q^{\prime},~{}P^{\prime}\approx_{\mathtt{L}}Q^{\prime}::z{:}A[\eta[X\mapsto\mathcal{R}]:\omega[X\mapsto
B_{1}]\\!\Leftrightarrow\\!\omega^{\prime}[X\mapsto B_{2}]]$

(Inductive Case) Let $\Gamma,\Delta$ be non empty. Given
$\Omega;\Gamma;\Delta\vdash P::T$ and $\Omega;\Gamma;\Delta\vdash Q::T$, the
binary relation on processes $\Gamma;\Delta\vdash
P\approx_{\mathtt{L}}Q::T[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]$
(with $\omega,\omega^{\prime}:\Omega$ and
$\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}$) is inductively defined as:

$\begin{array}[]{lcl}\Gamma;\Delta,y:A\vdash
P\approx_{\mathtt{L}}Q::T[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]&\mbox{
iff }&\forall R_{1},R_{2}.\mbox{ s.t.
}R_{1}\approx_{\mathtt{L}}R_{2}::y{:}A[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}],\\\
&&\Gamma;\Delta\vdash(\nu
y)(\hat{\omega}(P)\mid\hat{\omega}(R_{1}))\approx_{\mathtt{L}}(\nu
y)(\hat{\omega}^{\prime}(Q)\mid\hat{\omega}^{\prime}(R_{2}))::T[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]\\\\[2.84526pt]
\Gamma,u:A;\Delta\vdash
P\approx_{\mathtt{L}}Q::T[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]&\mbox{
iff }&\forall R_{1},R_{2}.\mbox{ s.t.
}R_{1}\approx_{\mathtt{L}}R_{2}::y{:}A[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}],\\\
&&\Gamma;\Delta\vdash(\mathbf{\nu}u)(\hat{\omega}(P)\mid!u(y).\hat{\omega}(R_{1}))\approx_{\mathtt{L}}(\mathbf{\nu}u)(\hat{\omega}^{\prime}(Q)\mid!u(y).\hat{\omega}^{\prime}(R_{2}))::T[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]\end{array}$

For the sake of readability we often omit the
$\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}$ portion of
$\approx_{\mathtt{L}}$, which is henceforth implicitly universally quantified.
Thus, we write $\Omega;\Gamma;\Delta\vdash P\approx_{\mathtt{L}}Q::z{:}A$ (or
$P\approx_{\mathtt{L}}Q$) iff the two given processes are logically equivalent
for all consistent instantiations of its type variables.

It is instructive to inspect the clause for type input ($\forall X.A$): the
two processes must be able to match inputs of any pair of _related_ types
(i.e. types related by a candidate), such that the continuations are related
at the open type $A$ with the appropriate type variable instantiations,
following Girard [16]. The power of this style of logical relation arises from
a combination of the extensional flavour of the equivalence and the fact that
polymorphic equivalences do not require the same type to be instantiated in
both processes, but rather that the types are _related_ (via a suitable
equivalence candidate relation).

######  Theorem 2.1 (Properties of Logical Equivalence [7])

Parametricity:

If $\Omega;\Gamma;\Delta\vdash P::z{:}A$ then, for all
$\omega,\omega^{\prime}:\Omega$ and
$\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}$, we have
$\Gamma;\Delta\vdash\hat{\omega}(P)\approx_{\mathtt{L}}\hat{\omega^{\prime}}(P)::z{:}A[\eta:\omega\\!\Leftrightarrow\\!\omega^{\prime}]$.

Soundness:

If $\Omega;\Gamma;\Delta\vdash P\approx_{\mathtt{L}}Q::z{:}A$ then
$\mathcal{C}[P]\cong\mathcal{C}[Q]::z{:}A$, for any closing $\mathcal{C}[-]$.

Completeness:

If $\Omega;\Gamma;\Delta\vdash P\cong Q::z{:}A$ then
$\Omega;\Gamma;\Delta\vdash P\approx_{\mathtt{L}}Q::z{:}A$.

##  3 To Linear-F and Back

We now develop our mutually inverse and fully abstract encodings between
Poly$\pi$ and a linear polymorphic $\lambda$-calculus [55] that we dub
Linear-F. We first introduce the syntax and typing of the linear
$\lambda$-calculus and then proceed to detail our encodings and their
properties (we omit typing ascriptions from the existential polymorphism
constructs for readability).

######  Definition 3.1 (Linear-F)

The syntax of terms $M,N$ and types $A,B$ of Linear-F is given below.

$\small\begin{array}[]{lcl}M,N&::=&\lambda x{:}A.M\mid M\,N\mid\langle
M\otimes N\rangle\mid\mathsf{let}\,x\otimes
y=M\,\mathsf{in}\,N\mid\,!M\mid\mathsf{let}\,!u=M\,\mathsf{in}\,N\mid\Lambda
X.M\\\\[2.84526pt]
&\mid&M[A]\mid\mathsf{pack}\,A\,\mathsf{with}\,M\mid\mathsf{let}\,(X,y)=M\,\mathsf{in}\,N\mid\mathsf{let}\,\mathbf{1}=M\,\mathsf{in}\,N\mid\langle\rangle\mid\mathsf{T}\mid\mathsf{F}\\\\[4.5pt]
A,B&::=&A\multimap B\mid A\otimes B\mid\,!A\mid\forall X.A\mid\exists X.A\mid
X\mid\mathbf{1}\mid\mathbf{2}\end{array}$

The syntax of types is that of the multiplicative and exponential fragments of
second-order intuitionistic linear logic: $\lambda x{:}A.M$ denotes linear
$\lambda$-abstractions; $M\,N$ denotes the application; $\langle M\otimes
N\rangle$ denotes the multiplicative pairing of $M$ and $N$, as reflected in
its elimination form $\mathsf{let}\,x\otimes y=M\,\mathsf{in}\,N$ which
simultaneously deconstructs the pair $M$, binding its first and second
projection to $x$ and $y$ in $N$, respectively; $!M$ denotes a term $M$ that
does not use any linear variables and so may be used an arbitrary number of
times; $\mathsf{let}\,!u=M\,\mathsf{in}\,N$ binds the underlying exponential
term of $M$ as $u$ in $N$; $\Lambda X.M$ is the type abstraction former;
$M[A]$ stands for type application; $\mathsf{pack}\,A\,\mathsf{with}\,M$ is
the existential type introduction form, where $M$ is a term where the
existentially typed variable is instantiated with $A$;
$\mathsf{let}\,(X,y)=M\,\mathsf{in}\,N$ unpacks an existential package $M$,
binding the representation type to $X$ and the underlying term to $y$ in $N$;
the multiplicative unit $\mathbf{1}$ has as introduction form the nullary pair
$\langle\rangle$ and is eliminated by the construct
$\mathsf{let}\,\mathbf{1}=M\,\mathsf{in}\,N$, where $M$ is a term of type
$\mathbf{1}$. Booleans (type $\mathbf{2}$ with values $\mathsf{T}$ and
$\mathsf{F}$) are the basic observable.

The typing judgment in Linear-F is given as $\Omega;\Gamma;\Delta\vdash M:A$,
following the DILL formulation of linear logic [3], stating that term $M$ has
type $A$ in a linear context $\Delta$ (i.e. bindings for linear variables
$x{:}B$), intuitionistic context $\Gamma$ (i.e. binding for intuitionistic
variables $u{:}B$) and type variable context $\Omega$. The typing rules are
standard [7]. The operational semantics of the calculus are the expected call-
by-name semantics with commuting conversions [27]. We write $\Downarrow$ for
the evaluation relation. We write $\cong$ for the largest typed congruence
that is consistent with the observables of type $\mathbf{2}$ (i.e. a so-called
Morris-style equivalence as in [5]).

###  3.1 Encoding Linear-F into Session $\pi$-Calculus

We define a translation from Linear-F to Poly$\pi$ generalising the one from
[49], accounting for polymorphism and multiplicative pairs. We translate
typing derivations of $\lambda$-terms to those of $\pi$-calculus terms (we
omit the full typing derivation for the sake of readability).

Proof theoretically, the $\lambda$-calculus corresponds to a proof term
assignment for natural deduction presentations of logic, whereas the session
$\pi$-calculus from § 2 corresponds to a proof term assignment for sequent
calculus. Thus, we obtain a translation from $\lambda$-calculus to the session
$\pi$-calculus by considering the proof theoretic content of the constructive
proof of soundness of the sequent calculus wrt natural deduction. Following
Gentzen [14], the translation from natural deduction to sequent calculus maps
introduction rules to the corresponding right rules and elimination rules to a
combination of the corresponding left rule, cut and/or identity.

Since typing in the session calculus identifies a distinguished channel along
which a process offers a session, the translation of $\lambda$-terms is
parameterised by a ``result'' channel along which the behaviour of the
$\lambda$-term is implemented. Given a $\lambda$-term $M$, the process
$\llbracket M\rrbracket_{z}$ encodes the behaviour of $M$ along the session
channel $z$. We enforce that the type $\mathbf{2}$ of booleans and its two
constructors are consistently translated to their polymorphic Church encodings
before applying the translation to Poly$\pi$. Thus, type $\mathbf{2}$ is first
translated to $\forall X.!X\\!\multimap\,!X\\!\multimap X$, the value
$\mathsf{T}$ to $\Lambda X.\lambda u{:}!X.\lambda
v{:}!X.\mathsf{let}\,!x=u\,\mathsf{in}\,\mathsf{let}\,!y=v\,\mathsf{in}\,x$
and the value $\mathsf{F}$ to $\Lambda X.\lambda u{:}!X.\lambda
v{:}!X.\mathsf{let}\,!x=u\,\mathsf{in}\,\mathsf{let}\,!y=v\,\mathsf{in}\,y$.
Such representations of the booleans are adequate up to parametricity [6] and
suitable for our purposes of relating the session calculus (which has no
primitive notion of value or result type) with the $\lambda$-calculus
precisely due to the tight correspondence between the two calculi.

######  Definition 3.2 (From Linear-F to Poly$\pi$)

$\llbracket\Omega\rrbracket;\llbracket\Gamma\rrbracket;\llbracket\Delta\rrbracket\vdash\llbracket
M\rrbracket_{z}::z{:}A$ denotes the translation of contexts, types and terms
from Linear-F to the polymorphic session calculus. The translations on
contexts and types are the identity function. Booleans and their values are
first translated to their Church encodings as specified above. The translation
on $\lambda$-terms is given below:

$\begin{array}[]{lcllcl}\llbracket
x\rrbracket_{z}&\triangleq&[x\leftrightarrow z]&\llbracket
M\,N\rrbracket_{z}\triangleq&&(\mathbf{\nu}x)(\llbracket
M\rrbracket_{x}\mid(\mathbf{\nu}y)x\langle y\rangle.(\llbracket
N\rrbracket_{y}\mid[x\leftrightarrow z]))\\\ \llbracket
u\rrbracket_{z}&\triangleq&(\mathbf{\nu}x)u\langle x\rangle.[x\leftrightarrow
z]&\llbracket\mathsf{let}\,!u=M\,\mathsf{in}\,N\rrbracket_{z}&\triangleq&(\mathbf{\nu}x)(\llbracket
M\rrbracket_{x}\mid\llbracket N\rrbracket_{z}\\{x/u\\})\\\ \llbracket\lambda
x{:}A.M\rrbracket_{z}&\triangleq&z(x).\llbracket
M\rrbracket_{z}&\llbracket\langle M\otimes
N\rangle\rrbracket_{z}&\triangleq&(\mathbf{\nu}y)z\langle y\rangle.(\llbracket
M\rrbracket_{y}\mid\llbracket N\rrbracket_{z})\\\
\llbracket!M\rrbracket_{z}&\triangleq&!z(x).\llbracket
M\rrbracket_{x}&\llbracket\mathsf{let}\,x\otimes
y=M\,\mathsf{in}\,N\rrbracket_{z}&\triangleq&(\mathbf{\nu}w)(\llbracket
M\rrbracket_{y}\mid y(x).\llbracket N\rrbracket_{z})\\\ \llbracket\Lambda
X.M\rrbracket_{z}&\triangleq&z(X).\llbracket M\rrbracket_{z}&\llbracket
M[A]\rrbracket_{z}&\triangleq&(\mathbf{\nu}x)(\llbracket M\rrbracket_{x}\mid
x\langle A\rangle.[x\leftrightarrow z])\\\
\llbracket\mathsf{pack}\,A\,\mathsf{with}\,M\rrbracket_{z}&\triangleq&z\langle
A\rangle.\llbracket
M\rrbracket_{z}&\llbracket\mathsf{let}\,(X,y)=M\,\mathsf{in}\,N\rrbracket_{z}&\triangleq&(\mathbf{\nu}x)(\llbracket
M\rrbracket_{y}\mid y(X).\llbracket N\rrbracket_{z})\\\
\llbracket\langle\rangle\rrbracket_{z}&\triangleq&{\bf
0}&\llbracket\mathsf{let}\,\mathbf{1}=M\,\mathsf{in}\,N\rrbracket_{z}&\triangleq&(\mathbf{\nu}x)(\llbracket
M\rrbracket_{x}\mid\llbracket N\rrbracket_{z})\par\par\end{array}$

To translate a (linear) $\lambda$-abstraction $\lambda x{:}A.M$, which
corresponds to the proof term for the introduction rule for $\multimap$, we
map it to the corresponding ${{\multimap}\mathsf{R}}$ rule, thus obtaining a
process $z(x).\llbracket M\rrbracket_{z}$ that inputs along the result channel
$z$ a channel $x$ which will be used in $\llbracket M\rrbracket_{z}$ to access
the function argument. To encode the application $M\,N$, we compose (i.e.
$\mathsf{cut}$) $\llbracket M\rrbracket_{x}$, where $x$ is a fresh name, with
a process that provides the (encoded) function argument by outputting along
$x$ a channel $y$ which offers the behaviour of $\llbracket N\rrbracket_{y}$.
After the output is performed, the type of $x$ is now that of the function's
codomain and thus we conclude by forwarding (i.e. the $\mathsf{id}$ rule)
between $x$ and the result channel $z$.

The encoding for polymorphism follows a similar pattern: To encode the
abstraction $\Lambda X.M$, we receive along the result channel a type that is
bound to $X$ and proceed inductively. To encode type application $M[A]$ we
encode the abstraction $M$ in parallel with a process that sends $A$ to it,
and forwards accordingly. Finally, the encoding of the existential package
$\mathsf{pack}\,A\,\mathsf{with}\,M$ maps to an output of the type $A$
followed by the behaviour $\llbracket M\rrbracket_{z}$, with the encoding of
the elimination form $\mathsf{let}\,(X,y)=M\,\mathsf{in}\,N$ composing the
translation of the term of existential type $M$ with a process performing the
appropriate type input and proceeding as $\llbracket N\rrbracket_{z}$.

######  Example 3.1 (Encoding of Linear-F)

Consider the following $\lambda$-term corresponding to a polymorphic pairing
function (recall that we write $\overline{z}\langle w\rangle.P$ for
$(\mathbf{\nu}w)z\langle w\rangle.P$):

$\small\begin{array}[]{lcllcl}M\triangleq\Lambda X.\Lambda Y.\lambda
x{:}X.\lambda y{:}Y.\langle x\otimes
y\rangle&\mbox{and}&N\triangleq((M[A][B]\,M_{1})\,M_{2})\end{array}$

Then we have, with $\tilde{x}=x_{1}x_{2}x_{3}x_{4}$:

$\small\begin{array}[]{rcll}\llbracket
N\rrbracket_{z}&\equiv&(\mathbf{\nu}\tilde{x})(&\llbracket
M\rrbracket_{x_{1}}\mid x_{1}\langle A\rangle.[x_{1}\leftrightarrow x_{2}]\mid
x_{2}\langle B\rangle.[x_{2}\leftrightarrow x_{3}]\mid\\\
&&&\overline{x_{3}}\langle x\rangle.(\llbracket
M_{1}\rrbracket_{x}\mid[x_{3}\leftrightarrow
x_{4}])\mid\overline{x_{4}}\langle y\rangle.(\llbracket
M_{2}\rrbracket_{y}\mid[x_{4}\leftrightarrow z]))\\\
&\equiv&(\mathbf{\nu}\tilde{x})(&x_{1}(X).x_{1}(Y).x_{1}(x).x_{1}(y).\overline{x_{1}}\langle
w\rangle.([x\leftrightarrow w]\mid[y\leftrightarrow x_{1}])\mid x_{1}\langle
A\rangle.[x_{1}\leftrightarrow x_{2}]\mid\\\ &&&x_{2}\langle
B\rangle.[x_{2}\leftrightarrow x_{3}]\mid\overline{x_{3}}\langle
x\rangle.(\llbracket M_{1}\rrbracket_{x}\mid[x_{3}\leftrightarrow
x_{4}])\mid\overline{x_{4}}\langle y\rangle.(\llbracket
M_{2}\rrbracket_{y}\mid[x_{4}\leftrightarrow z]))\end{array}$

We can observe that $N\xrightarrow{}^{+}(((\lambda x{:}A.\lambda y{:}B.\langle
x\otimes y\rangle)\,M_{1})\,M_{2})\xrightarrow{}^{+}\langle M_{1}\otimes
M_{2}\rangle$. At the process level, each reduction corresponding to the redex
of type application is simulated by two reductions, obtaining:

$\small\begin{array}[]{lcll}\llbracket
N\rrbracket_{z}&\xrightarrow{}^{+}&(\mathbf{\nu}x_{3},x_{4})(&x_{3}(x).x_{3}(y).\overline{x_{3}}\langle
w\rangle.([x\leftrightarrow w]\mid[y\leftrightarrow x_{3}])\mid\\\
&&&\overline{x_{3}}\langle x\rangle.(\llbracket
M_{1}\rrbracket_{x}\mid[x_{3}\leftrightarrow
x_{4}])\mid\overline{x_{4}}\langle y\rangle.(\llbracket
M_{2}\rrbracket_{y}\mid[x_{4}\leftrightarrow z]))=P\end{array}$

The reductions corresponding to the $\beta$-redexes clarify the way in which
the encoding represents substitution of terms for variables via fine-grained
name passing. Consider $\llbracket\langle M_{1}\otimes
M_{2}\rangle\rrbracket_{z}\triangleq\overline{z}\langle w\rangle.(\llbracket
M_{1}\rrbracket_{w}\mid\llbracket M_{2}\rrbracket_{z})$ and

$\small\begin{array}[]{rcl}P&\xrightarrow{}^{+}&(\mathbf{\nu}x,y)(\llbracket
M_{1}\rrbracket_{x}\mid\llbracket M_{2}\rrbracket_{y}\mid\overline{z}\langle
w\rangle.([x\leftrightarrow w]\mid[y\leftrightarrow z]))\end{array}$

The encoding of the pairing of $M_{1}$ and $M_{2}$ outputs a fresh name $w$
which will denote the behaviour of (the encoding of) $M_{1}$, and then the
behaviour of the encoding of $M_{2}$ is offered on $z$. The reduct of $P$
outputs a fresh name $w$ which is then identified with $x$ and thus denotes
the behaviour of $\llbracket M_{1}\rrbracket_{w}$. The channel $z$ is
identified with $y$ and thus denotes the behaviour of $\llbracket
M_{2}\rrbracket_{z}$, making the two processes listed above equivalent. This
informal reasoning exposes the insights that justify the operational
correspondence of the encoding. Proof-theoretically, these equivalences simply
map to commuting conversions which push the processes $\llbracket
M_{1}\rrbracket_{x}$ and $\llbracket M_{2}\rrbracket_{z}$ under the output on
$z$.

######  Theorem 3.1 (Operational Correspondence)

  * •

If $\Omega;\Gamma;\Delta\vdash M:A$ and $M\xrightarrow{}N$ then $\llbracket
M\rrbracket_{z}\stackrel{{\scriptstyle}}{{\Longrightarrow}}P$ such that
$\llbracket N\rrbracket_{z}\approx_{\mathtt{L}}P$

  * •

If $\llbracket M\rrbracket_{z}\xrightarrow{}P$ then $M\xrightarrow{}^{+}N$ and
$\llbracket N\rrbracket_{z}\approx_{\mathtt{L}}P$

###  3.2 Encoding Session $\pi$-calculus to Linear-F

Just as the proof theoretic content of the soundness of sequent calculus wrt
natural deduction induces a translation from $\lambda$-terms to session-typed
processes, the _completeness_ of the sequent calculus wrt natural deduction
induces a translation from the session calculus to the $\lambda$-calculus.
This mapping identifies sequent calculus right rules with the introduction
rules of natural deduction and left rules with elimination rules combined with
(type-preserving) substitution. Crucially, the mapping is defined on _typing
derivations_ , enabling us to consistently identify when a process uses a
session (i.e. left rules) or, dually, when a process offers a session (i.e.
right rules).

${\footnotesize\begin{array}[]{l}\stretchleftright{\llparenthesis}{\raise
10.0pt\hbox{$\hbox{$\hbox{\small\sc$({{\multimap}\mathsf{R}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
34.56946pt\vbox{\hbox{\hskip-34.56946pt\hbox{\hbox{$\displaystyle\displaystyle{\Delta,x{:}A\vdash{\color[rgb]{0,0,1}P}::z{:}B}$}}}\vbox{}}}\over\hbox{\hskip
43.05003pt\vbox{\vbox{}\hbox{\hskip-43.05003pt\hbox{\hbox{$\displaystyle\displaystyle{\Delta\vdash{\color[rgb]{0,0,1}z(x).P}::z{:}A\multimap
B}$}}}}}}$}}\hbox{}$}}{\rrparenthesis}\triangleq\raise
10.01332pt\hbox{$\hbox{$\hbox{\small\sc$(\multimap
I)$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
42.8808pt\vbox{\hbox{\hskip-42.8808pt\hbox{\hbox{$\displaystyle\displaystyle{\Delta,x{:}A\vdash{\color[rgb]{0,0,1}\llparenthesis
P\rrparenthesis}_{\Delta,x{:}A\vdash z{:}B}:B}$}}}\vbox{}}}\over\hbox{\hskip
53.76971pt\vbox{\vbox{}\hbox{\hskip-53.76971pt\hbox{\hbox{$\displaystyle\displaystyle{\Delta\vdash{\color[rgb]{0,0,1}\lambda
x{:}A.\llparenthesis P\rrparenthesis}_{\Delta,x{:}A\vdash z{:}B}:A\multimap
B}$}}}}}}$}}\hbox{}$}\\\\[16.00003pt]
\stretchleftright{\llparenthesis}{{\vbox{\hbox{\hbox{\small\sc$\displaystyle({{\multimap}\mathsf{L}})$}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
63.888pt\vbox{\hbox{\hskip-63.888pt\hbox{\hbox{$\displaystyle\displaystyle{\Delta_{1}\vdash{\color[rgb]{0,0,1}P}::y{:}A\quad\Delta_{2},x{:}B\vdash{\color[rgb]{0,0,1}Q}::z{:}C}$}}}\vbox{}}}\over\hbox{\hskip
77.92137pt\vbox{\vbox{}\hbox{\hskip-77.92137pt\hbox{\hbox{$\displaystyle\displaystyle{\Delta_{1},\Delta_{2},x{:}A\multimap
B\vdash{\color[rgb]{0,0,1}(\mathbf{\nu}y)x\langle y\rangle.(P\mid
Q)}::z{:}C}$}}}}}}$}}}}{\rrparenthesis}\par\triangleq\\\\[16.00003pt]
{\vbox{\hbox{\hbox{\small\sc(subst)}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
125.67091pt\vbox{\hbox{\hskip-125.6709pt\hbox{\hbox{$\displaystyle\displaystyle{\Delta_{2},x{:}B\vdash{\color[rgb]{0,0,1}\llparenthesis
Q\rrparenthesis}_{\Delta_{2},x{:}B\vdash
z{:}C}:C\quad{\vbox{\hbox{\hbox{\small\sc$\displaystyle(\multimap
E)$}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
75.6542pt\vbox{\hbox{\hskip-75.65419pt\hbox{\hbox{$\displaystyle\displaystyle{x{:}A\multimap
B\vdash{\color[rgb]{0,0,1}x}{:}A\multimap
B\quad\Delta_{1}\vdash{\color[rgb]{0,0,1}\llparenthesis
P\rrparenthesis}_{\Delta_{1}\vdash y{:}A}:B}$}}}\vbox{}}}\over\hbox{\hskip
54.30835pt\vbox{\vbox{}\hbox{\hskip-54.30833pt\hbox{\hbox{$\displaystyle\displaystyle{\Delta_{1},x{:}A\multimap
B\vdash{\color[rgb]{0,0,1}x\,\llparenthesis P\rrparenthesis}_{\Delta_{1}\vdash
y{:}A}:B}$}}}}}}$}}}}$}}}\vbox{}}}\over\hbox{\hskip
94.41118pt\vbox{\vbox{}\hbox{\hskip-94.41116pt\hbox{\hbox{$\displaystyle\displaystyle{\Delta_{1},\Delta_{2},x{:}A\multimap
B\vdash{\color[rgb]{0,0,1}\llparenthesis
Q\rrparenthesis}_{\Delta_{2},x{:}B\vdash
z{:}C}{\color[rgb]{0,0,1}\\{(x\,\llparenthesis
P\rrparenthesis}_{\Delta_{1}\vdash
y{:}A}{\color[rgb]{0,0,1})/x\\}}:C}$}}}}}}$}}}\end{array}}$ Figure 3:
Translation on Typing Derivations (Excerpt – See [52])

######  Definition 3.3 (From Poly$\pi$ to Linear-F)

We write
$\llparenthesis\Omega\rrparenthesis;\llparenthesis\Gamma\rrparenthesis;\llparenthesis\Delta\rrparenthesis\vdash\llparenthesis
P\rrparenthesis:A$ for the translation from typing derivations in Poly$\pi$ to
derivations in Linear-F. The translations on types and contexts are the
identity function. The translation on processes is given below, where the
leftmost column indicates the typing rule at the root of the derivation (see
Fig. 3 for an excerpt of the translation on typing derivations, where we write
$\llparenthesis P\rrparenthesis_{\Omega;\Gamma;\Delta\vdash z{:}A}$ to denote
the translation of $\Omega;\Gamma;\Delta\vdash P::z{:}A$. We omit $\Omega$ and
$\Gamma$ when unchanged).

$\begin{array}[]{llclllcl}({{\mathbf{1}}\mathsf{R}})&\llparenthesis{\bf
0}\rrparenthesis&\triangleq&\langle\rangle&({{\multimap}\mathsf{L}})&\llparenthesis(\mathbf{\nu}y)x\langle
y\rangle.(P\mid Q)\rrparenthesis&\triangleq&\llparenthesis
Q\rrparenthesis\\{(x\,\llparenthesis P\rrparenthesis)/x\\}\\\
(\mathsf{id})&\llparenthesis[x\leftrightarrow
y]\rrparenthesis&\triangleq&x&({{\multimap}\mathsf{R}})&\llparenthesis
z(x).P\rrparenthesis&\triangleq&\lambda x{:}A.\llparenthesis
P\rrparenthesis\\\ ({{\mathbf{1}}\mathsf{L}})&\llparenthesis
P\rrparenthesis&\triangleq&\mathsf{let}\,\mathbf{1}=x\,\mathsf{in}\,\llparenthesis
P\rrparenthesis&({{\otimes}\mathsf{R}})&\llparenthesis(\mathbf{\nu}x)z\langle
x\rangle.(P\mid Q)\rrparenthesis&\triangleq&\langle\llparenthesis
P\rrparenthesis\otimes\llparenthesis Q\rrparenthesis\rangle\\\
({{!}\mathsf{R}})&\llparenthesis!z(x).P\rrparenthesis&\triangleq&!\llparenthesis
P\rrparenthesis&({{\otimes}\mathsf{L}})&\llparenthesis
x(y).P\rrparenthesis&\triangleq&\mathsf{let}\,x\otimes
y=x\,\mathsf{in}\,\llparenthesis P\rrparenthesis\\\
({{!}\mathsf{L}})&\llparenthesis
P\\{u/x\\}\rrparenthesis&\triangleq&\mathsf{let}\,!u=x\,\mathsf{in}\,\llparenthesis
P\rrparenthesis&(\mathsf{copy})&\llparenthesis(\mathbf{\nu}x)u\langle
x\rangle.P\rrparenthesis&\triangleq&\llparenthesis P\rrparenthesis\\{u/x\\}\\\
({{\forall}\mathsf{R}})&\llparenthesis z(X).P\rrparenthesis&\triangleq&\Lambda
X.\llparenthesis P\rrparenthesis&({{\forall}\mathsf{L}})&\llparenthesis
x\langle B\rangle.P\rrparenthesis&\triangleq&\llparenthesis
P\rrparenthesis\\{(x[B])/x\\}\\\ ({{\exists}\mathsf{R}})&\llparenthesis
z\langle
B\rangle.P\rrparenthesis&\triangleq&\mathsf{pack}\,B\,\mathsf{with}\,\llparenthesis
P\rrparenthesis&({{\exists}\mathsf{L}})&\llparenthesis
x(Y).P\rrparenthesis&\triangleq&\mathsf{let}\,(Y,x)=x\,\mathsf{in}\,\llparenthesis
P\rrparenthesis\\\ (\mathsf{cut})&\llparenthesis(\mathbf{\nu}x)(P\mid
Q)\rrparenthesis&\triangleq&\llparenthesis Q\rrparenthesis\\{\llparenthesis
P\rrparenthesis/x\\}&(\mathsf{cut}^{!})&\llparenthesis(\mathbf{\nu}u)(!u(x).P\mid
Q)\rrparenthesis&\triangleq&\llparenthesis Q\rrparenthesis\\{\llparenthesis
P\rrparenthesis/u\\}\\\ \end{array}$

For instance, the encoding of a process $z(x).P::z{:}A\multimap B$, typed by
rule ${{\multimap}\mathsf{R}}$, results in the corresponding $\multimap\\!I$
introduction rule in the $\lambda$-calculus and thus is $\lambda
x{:}A.\llparenthesis P\rrparenthesis$. To encode the process
$(\mathbf{\nu}y)x\langle y\rangle.(P\mid Q)$, typed by rule
${{\multimap}\mathsf{L}}$, we make use of substitution: Given that the sub-
process $Q$ is typed as $\Omega;\Gamma;\Delta^{\prime},x{:}B\vdash Q::z{:}C$,
the encoding of the full process is given by $\llparenthesis
Q\rrparenthesis\\{(x\,\llparenthesis P\rrparenthesis)/x\\}$. The term
$x\,\llparenthesis P\rrparenthesis$ consists of the application of $x$ (of
function type) to the argument $\llparenthesis P\rrparenthesis$, thus ensuring
that the term resulting from the substitution is of the appropriate type. We
note that, for instance, the encoding of rule ${{\otimes}\mathsf{L}}$ does not
need to appeal to substitution – the $\lambda$-calculus $\mathsf{let}$ style
rules can be mapped directly. Similarly, rule ${{\forall}\mathsf{R}}$ is
mapped to type abstraction, whereas rule ${{\forall}\mathsf{L}}$ which types a
process of the form $x\langle B\rangle.P$ maps to a substitution of the type
application $x[B]$ for $x$ in $\llparenthesis P\rrparenthesis$. The encoding
of existential polymorphism is simpler due to the $\mathsf{let}$-style
elimination. We also highlight the encoding of the $\mathsf{cut}$ rule which
embodies parallel composition of two processes sharing a linear name, which
clarifies the use/offer duality of the intuitionistic calculus – the process
that offers $P$ is encoded and substituted into the encoded user $Q$.

######  Theorem 3.2 ()

If $\Omega;\Gamma;\Delta\vdash P::z{:}A$ then
$\llparenthesis\Omega\rrparenthesis;\llparenthesis\Gamma\rrparenthesis;\llparenthesis\Delta\rrparenthesis\vdash\llparenthesis
P\rrparenthesis:A$.

######  Example 3.2 (Encoding of Poly$\pi$)

Consider the following processes

$\small\begin{array}[]{l}P\triangleq z(X).z(Y).z(x).z(y).\overline{z}\langle
w\rangle.([x\leftrightarrow w]\mid[y\leftrightarrow z])\quad Q\triangleq
z\langle\mathbf{1}\rangle.z\langle\mathbf{1}\rangle.\overline{z}\langle
x\rangle.\overline{z}\langle y\rangle.z(w).[w\leftrightarrow r]\end{array}$

with $\vdash P::z{:}\forall X.\forall Y.X\multimap Y\multimap X\otimes Y$ and
$z{:}\forall X.\forall Y.X\multimap Y\multimap X\otimes Y\vdash
Q::r{:}\mathbf{1}$. $\small\begin{array}[]{ll}\mbox{Then:}&\llparenthesis
P\rrparenthesis=\Lambda X.\Lambda Y.\lambda x{:}X.\lambda y{:}Y.\langle
x\otimes y\rangle\quad\quad\llparenthesis
Q\rrparenthesis=\mathsf{let}\,x\otimes
y=z[\mathbf{1}][\mathbf{1}]\,\langle\rangle\,\langle\rangle\,\mathsf{in}\,\mathsf{let}\,\mathbf{1}=y\,\mathsf{in}\,x\\\
&\llparenthesis(\mathbf{\nu}z)(P\mid Q)\rrparenthesis=\mathsf{let}\,x\otimes
y=(\Lambda X.\Lambda Y.\lambda x{:}X.\lambda y{:}Y.\langle x\otimes
y\rangle)[\mathbf{1}][\mathbf{1}]\,\langle\rangle\,\langle\rangle\,\mathsf{in}\,\mathsf{let}\,\mathbf{1}=y\,\mathsf{in}\,x\end{array}$
By the behaviour of $(\mathbf{\nu}z)(P\mid Q)$, which consists of a sequence
of cuts, and its encoding, we have that $\llparenthesis(\mathbf{\nu}z)(P\mid
Q)\rrparenthesis\xrightarrow{}^{+}\langle\rangle$ and $(\mathbf{\nu}z)(P\mid
Q)\xrightarrow{}^{+}{\bf 0}=\llparenthesis\langle\rangle\rrparenthesis$.

In general, the translation of Def. 3.3 can introduce some distance between
the immediate operational behaviour of a process and its corresponding
$\lambda$-term, insofar as the translations of cuts (and left rules to non
$\mathsf{let}$-form elimination rules) make use of substitutions that can take
place deep within the resulting term. Consider the process at the root of the
following typing judgment
$\Delta_{1},\Delta_{2},\Delta_{3}\vdash(\mathbf{\nu}x)(x(y).P_{1}\mid(\mathbf{\nu}y)x\langle
y\rangle.(P_{2}\mid w(z).{\bf 0}))::w{:}\mathbf{1}\multimap\mathbf{1}$,
derivable through a $\mathsf{cut}$ on session $x$ between instances of
${{\multimap}\mathsf{R}}$ and ${{\multimap}\mathsf{L}}$, where the
continuation process $w(z).{\bf 0}$ offers a session
$w{:}\mathbf{1}\multimap\mathbf{1}$ (and so must use rule
${{\mathbf{1}}\mathsf{L}}$ on $x$). We have that:
$(\mathbf{\nu}x)(x(y).P_{1}\mid(\mathbf{\nu}y)x\langle y\rangle.(P_{2}\mid
w(z).{\bf 0}))\xrightarrow{}(\mathbf{\nu}x,y)(P_{1}\mid P_{2}\mid w(z).{\bf
0})$. However, the translation of the process above results in the term
$\lambda z{:}\mathbf{1}.\mathsf{let}\,\mathbf{1}=((\lambda
y{:}A.\llparenthesis P_{1}\rrparenthesis)\,\llparenthesis
P_{2}\rrparenthesis)\,\mathsf{in}\,\mathsf{let}\,\mathbf{1}=z\,\mathsf{in}\,\langle\rangle$,
where the redex that corresponds to the process reduction is present but
hidden under the binder for $z$ (corresponding to the input along $w$). Thus,
to establish operational completeness we consider full $\beta$-reduction,
denoted by $\xrightarrow{}_{\beta}$, i.e. enabling $\beta$-reductions under
binders.

######  Theorem 3.3 (Operational Completeness)

Let $\Omega;\Gamma;\Delta\vdash P::z{:}A$. If $P\xrightarrow{}Q$ then
$\llparenthesis P\rrparenthesis\xrightarrow{}_{\beta}^{*}\llparenthesis
Q\rrparenthesis$.

In order to study the soundness direction it is instructive to consider typed
process $x{:}\mathbf{1}\multimap\mathbf{1}\vdash\overline{x}\langle
y\rangle.(\mathbf{\nu}z)(z(w).{\bf 0}\mid\overline{z}\langle w\rangle.{\bf
0})::v{:}\mathbf{1}$ and its translation:

$\small\begin{array}[]{c}\llparenthesis\overline{x}\langle
y\rangle.(\mathbf{\nu}z)(z(w).{\bf 0}\mid\overline{z}\langle w\rangle.{\bf
0})\rrparenthesis=\llparenthesis(\mathbf{\nu}z)(z(w).{\bf
0}\mid\overline{z}\langle w\rangle.{\bf
0})\rrparenthesis\\{(x\,\langle\rangle)/x\\}\\\
=\mathsf{let}\,\mathbf{1}=(\lambda
w{:}\mathbf{1}.\mathsf{let}\,\mathbf{1}=w\,\mathsf{in}\,\langle\rangle)\,\langle\rangle\,\mathsf{in}\,\mathsf{let}\,\mathbf{1}=x\,\langle\rangle\,\mathsf{in}\,\langle\rangle\end{array}$

The process above cannot reduce due to the output prefix on $x$, which cannot
synchronise with a corresponding input action since there is no provider for
$x$ (i.e. the channel is in the left-hand side context). However, its encoding
can exhibit the $\beta$-redex corresponding to the synchronisation along $z$,
hidden by the prefix on $x$. The corresponding reductions hidden under
prefixes in the encoding can be _soundly_ exposed in the session calculus by
appealing to the commuting conversions of linear logic (e.g. in the process
above, the instance of rule ${{\multimap}\mathsf{L}}$ corresponding to the
output on $x$ can be commuted with the $\mathsf{cut}$ on $z$).

As shown in [36], commuting conversions are sound wrt observational
equivalence, and thus we formulate operational soundness through a notion of
_extended_ process reduction, which extends process reduction with the
reductions that are induced by commuting conversions. Such a relation was also
used for similar purposes in [5] and in [26], in a classical linear logic
setting. For conciseness, we define extended reduction as a relation on
_typed_ processes modulo $\equiv$.

######  Definition 3.4 (Extended Reduction [5])

We define $\mapsto$ as the type preserving relations on typed processes modulo
$\equiv$ generated by:

  1. 1.

$\mathcal{C}[(\mathbf{\nu}y)x\langle y\rangle.P]\mid
x(y).Q\mapsto\mathcal{C}[(\mathbf{\nu}y)(P\mid Q)]$;

  2. 2.

$\mathcal{C}[(\mathbf{\nu}y)x\langle
y\rangle.P]\mid\,!x(y).Q\mapsto\mathcal{C}[(\mathbf{\nu}y)(P\mid
Q)]\mid\,!x(y).Q$; and (3) $(\mathbf{\nu}x)(!x(y).Q)\mapsto\mathbf{0}$

where $\mathcal{C}$ is a (typed) process context which does not capture the
bound name $y$.

######  Theorem 3.4 (Operational Soundness)

Let $\Omega;\Gamma;\Delta\vdash P::z{:}A$ and $\llparenthesis
P\rrparenthesis\xrightarrow{}M$, there exists $Q$ such that $P\mapsto^{*}Q$
and $\llparenthesis Q\rrparenthesis=_{\alpha}M$.

###  3.3 Inversion and Full Abstraction

Having established the operational preciseness of the encodings to-and-from
Poly$\pi$ and Linear-F, we establish our main results for the encodings.
Specifically, we show that the encodings are mutually inverse up-to
behavioural equivalence (with fullness as its corollary), which then enables
us to establish full abstraction for _both_ encodings.

######  Theorem 3.5 (Inverse)

If $\Omega;\Gamma;\Delta\vdash M:A$ then
$\Omega;\Gamma;\Delta\vdash\llparenthesis\llbracket
M\rrbracket_{z}\rrparenthesis\cong M:A$. Also, if $\Omega;\Gamma;\Delta\vdash
P::z{:}A$ then $\Omega;\Gamma;\Delta\vdash\llbracket\llparenthesis
P\rrparenthesis\rrbracket_{z}\approx_{\mathtt{L}}P::z{:}A$

######  Corollary 3.1 (Fullness)

Let $\Omega;\Gamma;\Delta\vdash P::z{:}A$. $\exists M$ s.t.
$\Omega;\Gamma;\Delta\vdash M:A$ and $\Omega;\Gamma;\Delta\vdash\llbracket
M\rrbracket_{z}\approx_{\mathtt{L}}P::z{:}A$ Also, let
$\Omega;\Gamma;\Delta\vdash M:A$. $\exists P$ s.t. $\Omega;\Gamma;\Delta\vdash
P::z{:}A$ and $\Omega;\Gamma;\Delta\vdash\llparenthesis P\rrparenthesis\cong
M:A$

We now state our full abstraction results. Given two Linear-F terms of the
same type, equivalence in the image of the $\llbracket{-}\rrbracket_{z}$
translation can be used as a proof technique for contextual equivalence in
Linear-F. This is called the _soundness_ direction of full abstraction in the
literature [18] and proved by showing the relation generated by $\llbracket
M\rrbracket_{z}\approx_{\mathtt{L}}\llbracket N\rrbracket_{z}$ forms $\cong$;
we then establish the _completeness_ direction by contradiction, using
fullness.

######  Theorem 3.6 (Full Abstraction)

$\Omega;\Gamma;\Delta\vdash M\cong N:A$ iff
$\Omega;\Gamma;\Delta\vdash\llbracket
M\rrbracket_{z}\approx_{\mathtt{L}}\llbracket N\rrbracket_{z}::z{:}A$.

We can straightforwardly combine the above full abstraction with Theorem 3.5
to obtain full abstraction of the $\llparenthesis{-}\rrparenthesis$
translation.

######  Theorem 3.7 (Full Abstraction)

$\Omega;\Gamma;\Delta\vdash P\approx_{\mathtt{L}}Q::z{:}A$ iff
$\Omega;\Gamma;\Delta\vdash\llparenthesis P\rrparenthesis\cong\llparenthesis
Q\rrparenthesis:A$.

##  4 Applications of the Encodings

In this section we develop applications of the encodings of the previous
sections. Taking advantage of full abstraction and mutual inversion, we apply
non-trivial properties from the theory of the $\lambda$-calculus to our
session-typed process setting.

In § 4.1 we study inductive and coinductive sessions, arising through
encodings of initial $F$-algebras and final $F$-coalgebras in the polymorphic
$\lambda$-calculus.

In § 4.2 we study encodings for an extension of the core session calculus with
term passing, where terms are derived from a simply-typed $\lambda$-calculus.
Using the development of § 4.2 as a stepping stone, we generalise the
encodings to a _higher-order_ session calculus (§ 4.3), where processes can
send, receive and execute other processes.We show full abstraction and mutual
inversion theorems for the encodings from higher-order to first-order. As a
consequence, we can straightforwardly derive a strong normalisation property
for the higher-order process-passing calculus.

###  4.1 Inductive and Coinductive Session Types

The study of polymorphism in the $\lambda$-calculus [1, 19, 40, 6] has shown
that parametric polymorphism is expressive enough to encode both inductive and
coinductive types in a precise way, through a faithful representation of
initial and final (co)algebras [28], without extending the language of terms
nor the semantics of the calculus, giving a logical justification to the
Church encodings of inductive datatypes such as lists and natural numbers. The
polymorphic session calculus can express fairly intricate communication
behaviours, including generic protocols through both existential and universal
polymorphism (i.e. protocols that are parametric in their sub-protocols).
Using our fully abstract encodings between the two calculi, we show that
session polymorphism is expressive enough to encode inductive and coinductive
sessions, ``importing'' the results for the $\lambda$-calculus, which may then
be instantiated to provide a session-typed formulation of the encodings of
data structures in the $\pi$-calculus of [30].

Inductive and Coinductive Types in System F.  Exploring an algebraic
interpretation of polymorphism where types are interpreted as functors, it can
be shown that given a type $F$ with a free variable $X$ that occurs only
positively (i.e. occurrences of $X$ are on the left-hand side of an even
number of function arrows), the polymorphic type $\forall X.((F(X)\rightarrow
X)\rightarrow X)$ forms an initial $F$-algebra [42, 1] (we write $F(X)$ to
denote that $X$ occurs in $F$). This enables the representation of
_inductively_ defined structures using an algebraic or categorical
justification. For instance, the natural numbers can be seen as the initial
$F$-algebra of $F(X)=\mathbf{1}+X$ (where $\mathbf{1}$ is the unit type and
$+$ is the coproduct), and are thus _already present_ in System F, in a
precise sense, as the type $\forall X.((\mathbf{1}+X)\rightarrow X)\rightarrow
X$ (noting that both $\mathbf{1}$ and $+$ can also be encoded in System F). A
similar story can be told for _coinductively_ defined structures, which
correspond to final $F$-coalgebras and are representable with the polymorphic
type $\exists X.(X\rightarrow F(X))\times X$, where $\times$ is a product
type. In the remainder of this section we assume the positivity requirement on
$F$ mentioned above.

While the complete formal development of the representation of inductive and
coinductive types in System F would lead us to far astray, we summarise here
the key concepts as they apply to the $\lambda$-calculus (the interested
reader can refer to [19] for the full categorical details).

|
---
(a)
|
---
(b)
Figure 4: Diagrams for Initial $F$-algebras and Final $F$-coalgebras

To show that the polymorphic type $T_{i}\triangleq\forall X.((F(X)\rightarrow
X)\rightarrow X)$ is an initial $F$-algebra, one exhibits a pair of
$\lambda$-terms, often dubbed $\mathsf{fold}$ and $\mathsf{in}$, such that the
diagram in Fig. 4(a) commutes (for any $A$, where $F(f)$, where $f$ is a
$\lambda$-term, denotes the functorial action of $F$ applied to $f$), and,
crucially, that $\mathsf{fold}$ is _unique_. When these conditions hold, we
are justified in saying that $T_{i}$ is a least fixed point of $F$. Through a
fairly simple calculation, it is easy to see that:

$\small\begin{array}[]{rcl}\mathsf{fold}&\triangleq&\Lambda X.\lambda
x{:}F(X)\rightarrow X.\lambda t{:}T_{i}.t[X](x)\\\
\mathsf{in}&\triangleq&\lambda x{:}F(T_{i}).\Lambda X.\lambda
y{:}F(X)\rightarrow X.y\,(F(\mathsf{fold}[X](x))(x))\end{array}$

satisfy the necessary equalities. To show uniqueness one appeals to
_parametricity_ , which allows us to prove that any function of the
appropriate type is equivalent to $\mathsf{fold}$. This property is often
dubbed initiality or universality.

The construction of final $F$-coalgebras and their justification as _greatest_
fixed points is dual. Assuming products in the calculus and taking
$T_{f}\triangleq\exists X.(X\rightarrow F(X))\times X$, we produce the
$\lambda$-terms

$\small\begin{array}[]{rcl}\mathsf{unfold}&\triangleq&\Lambda X.\lambda
f{:}X\rightarrow F(X).\lambda
x{:}T_{f}.\mathsf{pack}\,X\,\mathsf{with}\,(f,x)\\\
\mathsf{out}&\triangleq&\lambda
t:T_{f}.\mathsf{let}\,(X,(f,x))=t\,\mathsf{in}\,F(\mathsf{unfold}[X](f))\,(f(x))\end{array}$

such that the diagram in Fig. 4(b) commutes and $\mathsf{unfold}$ is unique
(again, up to parametricity). While the argument above applies to System F, a
similar development can be made in Linear-F [6] by considering
$T_{i}\triangleq\forall X.!(F(X)\multimap X)\multimap X$ and
$T_{f}\triangleq\exists X.!(X\multimap F(X))\otimes X$. Reusing the same names
for the sake of conciseness, the associated _linear_ $\lambda$-terms are:

$\small\begin{array}[]{rcl}\mathsf{fold}&\triangleq&\Lambda X.\lambda
u{:}!(F(X)\multimap X).\lambda y{:}T_{i}.(y[X]\,u):\forall X.!(F(X)\multimap
X)\multimap T_{i}\multimap X\\\ \mathsf{in}&\triangleq&\lambda
x{:}F(T_{i}).\Lambda X.\lambda y{:}!(F(X)\multimap
X).\mathsf{let}\,!u=y\,\mathsf{in}\,k\,(F\,(\mathsf{fold}[X](!u))(x)):F(T_{i})\multimap
T_{i}\\\ \mathsf{unfold}&\triangleq&\Lambda X.\lambda u{:}!(X\multimap
F(X)).\lambda x{:}X.\mathsf{pack}\,X\,\mathsf{with}\,\langle u\otimes
x\rangle:\forall X.!(X\multimap F(X))\multimap X\multimap T_{f}\\\
\mathsf{out}&\triangleq&\lambda
t:T_{f}.\mathsf{let}\,(X,(u,x))=t\,\mathsf{in}\,\mathsf{let}\,!f=u\,\mathsf{in}\,F(\mathsf{unfold}[X](!f))\,(f(x)):T_{f}\multimap
F(T_{f})\end{array}$

Inductive and Coinductive Sessions for Free.  As a consequence of full
abstraction we may appeal to the $\llbracket{-}\rrbracket_{z}$ encoding to
derive representations of $\mathsf{fold}$ and $\mathsf{unfold}$ that satisfy
the necessary algebraic properties. The derived processes are (recall that we
write $\overline{x}\langle y\rangle.P$ for $(\mathbf{\nu}y)x\langle
y\rangle.P$):

$\small\begin{array}[]{rcl}\llbracket\mathsf{fold}\rrbracket_{z}&\triangleq&z(X).z(u).z(y).(\mathbf{\nu}w)((\mathbf{\nu}x)([y\leftrightarrow
x]\mid x\langle X\rangle.[x\leftrightarrow w])\mid\overline{w}\langle
v\rangle.([u\leftrightarrow v]\mid[w\leftrightarrow z]))\\\
\llbracket\mathsf{unfold}\rrbracket_{z}&\triangleq&z(X).z(u).z(x).z\langle
X\rangle.\overline{z}\langle y\rangle.([u\leftrightarrow
y]\mid[x\leftrightarrow z])\\\ \end{array}$

We can then show universality of the two constructions. We write $P_{x,y}$ to
single out that $x$ and $y$ are free in $P$ and $P_{z,w}$ to denote the result
of employing capture-avoiding substitution on $P$, substituting $x$ and $y$ by
$z$ and $w$. Let:

$\small\begin{array}[]{rcl}\mathsf{foldP}(A)_{y_{1},y_{2}}&\triangleq&(\mathbf{\nu}x)(\llbracket\mathsf{fold}\rrbracket_{x}\mid
x\langle A\rangle.\overline{x}\langle v\rangle.(\overline{u}\langle
y\rangle.[y\leftrightarrow v]\mid\overline{x}\langle
z\rangle.([z\leftrightarrow y_{1}]\mid[x\leftrightarrow y_{2}])))\\\
\mathsf{unfoldP}(A)_{y_{1},y_{2}}&\triangleq&(\mathbf{\nu}x)(\llbracket\mathsf{unfold}\rrbracket_{x}\mid
x\langle A\rangle.\overline{x}\langle v\rangle.(\overline{u}\langle
y\rangle.[y\leftrightarrow v]\mid\overline{x}\langle
z\rangle.([z\leftrightarrow y_{1}]\mid[x\leftrightarrow y_{2}])))\end{array}$

where $\mathsf{foldP}(A)_{y_{1},y_{2}}$ corresponds to the application of
$\mathsf{fold}$ to an $F$-algebra $A$ with the associated morphism
$F(A)\multimap A$ available on the shared channel $u$, consuming an ambient
session $y_{1}{:}T_{i}$ and offering $y_{2}{:}A$. Similarly,
$\mathsf{unfoldP}(A)_{y_{1},y_{2}}$ corresponds to the application of
$\mathsf{unfold}$ to an $F$-coalgebra $A$ with the associated morphism
$A\multimap F(A)$ available on the shared channel $u$, consuming an ambient
session $y_{1}{:}A$ and offering $y_{2}{:}T_{f}$.

######  Theorem 4.1 (Universality of $\mathsf{foldP}$)

$\forall Q$ such that $X;u{:}F(X)\multimap X;y_{1}{:}T_{i}\vdash Q::y_{2}{:}X$
we have $X;u{:}F(X)\multimap X;y_{1}{:}T_{i}\vdash
Q\approx_{\mathtt{L}}\mathsf{foldP}(X)_{y_{1},y_{2}}::y_{2}{:}X$

######  Theorem 4.2 (Universality of $\mathsf{unfoldP}$)

$\forall Q$ and $F$-coalgebra $A$ s.t $\cdot;\cdot;y_{1}{:}A\vdash
Q::y_{2}{:}T_{f}$ we have that $\cdot;u{:}F(A)\multimap A;y_{1}{:}A\vdash
Q\approx_{\mathtt{L}}\mathsf{unfoldP}(A)_{y_{1},y_{2}}::y_{2}::T_{f}$.

######  Example 4.1 (Natural Numbers)

We show how to represent the natural numbers as an inductive session type
using $F(X)=\mathbf{1}\oplus X$, making use of $\mathsf{in}$:

$\small\begin{array}[]{c}\mathsf{zero}_{x}\triangleq(\mathbf{\nu}z)(z.\mathsf{inl};{\bf
0}\mid\llbracket\mathsf{in}(z)\rrbracket_{x})\quad\mathsf{succ}_{y,x}\triangleq(\mathbf{\nu}s)(s.\mathsf{inr};[y\leftrightarrow
s]\mid\llbracket\mathsf{in}(s)\rrbracket_{x})\end{array}$

with $\mathsf{Nat}\triangleq\forall X.!((\mathbf{1}\oplus X)\multimap
X)\multimap X$ where $\vdash\mathsf{zero}_{x}::x{:}\mathsf{Nat}$ and
$y{:}\mathsf{Nat}\vdash\mathsf{succ}_{y,x}::x{:}\mathsf{Nat}$ encode the
representation of $0$ and successor, respectively. The natural $1$ would thus
be represented by
$\mathsf{one}_{x}\triangleq(\mathbf{\nu}y)(\mathsf{zero}_{y}\mid\mathsf{succ}_{y,x})$.
The behaviour of type $\mathsf{Nat}$ can be seen as a that of a sequence of
internal choices of arbitrary (but finite) length. We can then observe that
the $\mathsf{foldP}$ process acts as a recursor. For instance consider:

$\small\begin{array}[]{l}\mathsf{stepDec}_{d}\triangleq
d(n).n.\mathsf{case}(\mathsf{zero}_{d},[n\leftrightarrow
d])\quad\mathsf{dec}_{x,z}\triangleq(\mathbf{\nu}u)(!u(d).\mathsf{stepDec}_{d}\mid\mathsf{foldP}(\mathsf{Nat})_{x,z})\end{array}$

with
$\mathsf{stepDec}_{d}::d{:}(\mathbf{1}\oplus\mathsf{Nat})\multimap\mathsf{Nat}$
and $x{:}\mathsf{Nat}\vdash\mathsf{dec}_{x,z}::z{:}\mathsf{Nat}$, where
$\mathsf{dec}$ decrements a given natural number session on channel $x$. We
have that:

$\small\begin{array}[]{l}(\mathbf{\nu}x)(\mathsf{one}_{x}\mid\mathsf{dec}_{x,z})\equiv(\mathbf{\nu}x,y.u)(\mathsf{zero}_{y}\mid\mathsf{succ}_{y,x}!u(d).\mathsf{stepDec}_{d}\mid\mathsf{foldP}(\mathsf{Nat})_{x,z})\approx_{\mathtt{L}}\mathsf{zero}_{z}\end{array}$

We note that the resulting encoding is reminiscent of the encoding of lists of
[30] (where $\mathsf{zero}$ is the empty list and $\mathsf{succ}$ the cons
cell). The main differences in the encodings arise due to our primitive
notions of labels and forwarding, as well as due to the generic nature of
$\mathsf{in}$ and $\mathsf{fold}$.

######  Example 4.2 (Streams)

We build on Example 4.1 by representing _streams_ of natural numbers as a
coinductive session type. We encode infinite streams of naturals with
$F(X)=\mathsf{Nat}\otimes X$. Thus: $\mathsf{NatStream}\triangleq\exists
X.!(X\multimap(\mathsf{Nat}\otimes X))\otimes X$. The behaviour of a session
of type $\mathsf{NatStream}$ amounts to an infinite sequence of outputs of
channels of type $\mathsf{Nat}$. Such an encoding enables us to construct the
stream of all naturals $\mathsf{nats}$ (and the stream of all non-zero
naturals $\mathsf{oneNats}$):

$\small\begin{array}[]{lcl}\mathsf{genHdNext}_{z}&\triangleq&z(n).\overline{z}\langle
y\rangle.(\overline{n}\langle n^{\prime}\rangle.[n^{\prime}\leftrightarrow
y]\mid\,!z(w).\overline{n}\langle
n^{\prime}\rangle.\mathsf{succ}_{n^{\prime},w})\\\
\mathsf{nats}_{y}&\triangleq&(\mathbf{\nu}x,u)(\mathsf{zero}_{x}\mid\,!u(z).\mathsf{genHdNext}_{z}\mid\mathsf{unfoldP}(!\mathsf{Nat})_{x,y})\\\
\mathsf{oneNats}_{y}&\triangleq&(\mathbf{\nu}x,u)(\mathsf{one}_{x}\mid\,!u(z).\mathsf{genHdNext}_{z}\mid\mathsf{unfoldP}(!\mathsf{Nat})_{x,y})\end{array}$

with
$\mathsf{genHdNext}_{z}::z{:}!\mathsf{Nat}\multimap\mathsf{Nat}\otimes!\mathsf{Nat}$
and both $\mathsf{nats}_{y}$ and $\mathsf{oneNats}::y{:}\mathsf{NatStream}$.
$\mathsf{genHdNext}_{z}$ consists of a helper that generates the current head
of a stream and the next element. As expected, the following process
implements a session that ``unrolls'' the stream once, providing the head of
the stream and then behaving as the rest of the stream (recall that
$\mathsf{out}:T_{f}\multimap F(T_{f})$).

$(\mathbf{\nu}x)(\mathsf{nats}_{x}\mid\llbracket\mathsf{out}(x)\rrbracket_{y})::y{:}\mathsf{Nat}\otimes\mathsf{NatStream}$

We note a peculiarity of the interaction of linearity with the stream
encoding: a process that begins to deconstruct a stream has no way of
``bottoming out'' and stopping. One cannot, for instance, extract the first
element of a stream of naturals and stop unrolling the stream in a well-typed
way. We can, however, easily encode a ``terminating'' stream of all natural
numbers via $F(X)=(\mathsf{Nat}\otimes!X)$ by replacing the
$\mathsf{genHdNext}_{z}$ with the generator given as:

$\small\begin{array}[]{rcl}\mathsf{genHdNextTer}_{z}&\triangleq&z(n).\overline{z}\langle
y\rangle.(\overline{n}\langle n^{\prime}\rangle.[n^{\prime}\leftrightarrow
y]\mid\,!z(w).!w(w^{\prime}).\overline{n}\langle
n^{\prime}\rangle.\mathsf{succ}_{n^{\prime},w^{\prime}})\end{array}$

It is then easy to see that a usage of
$\llbracket\mathsf{out}(x)\rrbracket_{y}$ results in a session of type
$\mathsf{Nat}\otimes!\mathsf{NatStream}$, enabling us to discard the stream as
needed. One can replay this argument with the operator
$F(X)=(!\mathsf{Nat}\otimes X)$ to enable discarding of stream elements.
Assuming such modifications, we can then show:

$(\mathbf{\nu}y)((\mathbf{\nu}x)(\mathsf{nats}_{x}\mid\llbracket\mathsf{out}(x)\rrbracket_{y})\mid
y(n).[y\leftrightarrow
z])\approx_{\mathtt{L}}\mathsf{oneNats}_{z}::z{:}\mathsf{NatStream}$

###  4.2 Communicating Values – Sess$\pi\lambda$

We now consider a session calculus extended with a data layer obtained from a
$\lambda$-calculus (whose terms are ranged over by $M,N$ and types by
$\tau,\sigma$). We dub this calculus Sess$\pi\lambda$.

$\small\begin{array}[]{ll}\begin{array}[]{lcl}P,Q&::=&\dots\mid x\langle
M\rangle.P\mid x(y).P\\\ M,N&::=&\lambda x{:}\tau.M\mid M\,N\mid
x\end{array}&\quad\quad\begin{array}[]{lcl}A,B&::=&\dots\mid\tau\wedge
A\mid\tau\supset A\\\
\tau,\sigma&::=&\dots\mid\tau\rightarrow\sigma\end{array}\end{array}$

Without loss of generality, we consider the data layer to be simply-typed,
with a call-by-name semantics, satisfying the usual type safety properties.
The typing judgment for this calculus is $\Psi\vdash M:\tau$. We omit session
polymorphism for the sake of conciseness, restricting processes to
communication of data and (session) channels. The typing judgment for
processes is thus modified to $\Psi;\Gamma;\Delta\vdash P::z{:}A$, where
$\Psi$ is an intuitionistic context that accounts for variables in the data
layer. The rules for the relevant process constructs are (all other rules
simply propagate the $\Psi$ context from conclusion to premises):

$\small\begin{array}[]{c}\Psi;\Gamma;\Delta\vdash z\langle
M\rangle.P::z{:}\tau\wedge A\lx@proof@logical@and\Psi\vdash
M:\tau\Psi;\Gamma;\Delta\vdash P::z{:}A\quad\Psi;\Gamma;\Delta,x{:}\tau\wedge
A\vdash x(y).Q::z{:}C\Psi,y{:}\tau;\Gamma;\Delta,x{:}A\vdash
Q::z{:}C\\\\[4.5pt] \Psi;\Gamma;\Delta\vdash z(x).P::z{:}\tau\supset
A\Psi,x{:}\tau;\Gamma;\Delta\vdash
P::z{:}A\quad\Psi;\Gamma;\Delta,x{:}\tau\supset A\vdash x\langle
M\rangle.Q::z{:}C\lx@proof@logical@and\Psi\vdash
M:\tau\Psi;\Gamma;\Delta,x{:}A\vdash Q::z{:}C\end{array}$

With the reduction rule given by:111For simplicity, in this section, we define
the process semantics through a reduction relation. $x\langle M\rangle.P\mid
x(y).Q\xrightarrow{}P\mid Q\\{M/y\\}$. With a simple extension to our
encodings we may eliminate the data layer by encoding the data objects as
processes, showing that from an expressiveness point of view, data
communication is orthogonal to the framework. We note that the data language
we are considering is _not_ linear, and the usage discipline of data in
processes is itself also not linear.

#### To First-Order Processes

We now introduce our encoding for Sess$\pi\lambda$, defined inductively on
session types, processes, types and $\lambda$-terms (we omit the purely
inductive cases on session types and processes for conciseness). As before,
the encoding on processes is defined on _typing derivations_ , where we
indicate the typing rule at the root of the typing derivation.

$\small\begin{array}[]{l}\llbracket\tau\wedge
A\rrbracket\triangleq!\llbracket\tau\rrbracket\otimes\llbracket
A\rrbracket\qquad\llbracket\tau\supset
A\rrbracket\triangleq!\llbracket\tau\rrbracket\multimap\llbracket
A\rrbracket\qquad\llbracket\tau\rightarrow\sigma\rrbracket\triangleq!\llbracket\tau\rrbracket\multimap\llbracket\sigma\rrbracket\end{array}$
$\small\begin{array}[]{lrcllrcl}({{\wedge}\mathsf{R}})&\llbracket z\langle
M\rangle.P\rrbracket&\triangleq&\overline{z}\langle x\rangle.(!x(y).\llbracket
M\rrbracket_{y}\mid\llbracket P\rrbracket)&({{\wedge}\mathsf{L}})&\llbracket
x(y).P\rrbracket&\triangleq&x(y).\llbracket P\rrbracket\\\
({{\supset}\mathsf{R}})&\llbracket z(x).P\rrbracket&\triangleq&z(x).\llbracket
P\rrbracket&({{\supset}\mathsf{L}})&\llbracket x\langle
M\rangle.P\rrbracket&\triangleq&\overline{x}\langle y\rangle.(!y(w).\llbracket
M\rrbracket_{w}\mid\llbracket P\rrbracket)\end{array}$
$\small\begin{array}[]{lll}\llbracket
x\rrbracket_{z}\triangleq\overline{x}\langle y\rangle.[y\leftrightarrow
z]\quad\quad\quad\llbracket\lambda x{:}\tau.M\rrbracket_{z}\triangleq
z(x).\llbracket M\rrbracket_{z}\\\ \llbracket
M\,N\rrbracket_{z}\triangleq(\mathbf{\nu}y)(\llbracket
M\rrbracket_{y}\mid\overline{y}\langle x\rangle.(!x(w).\llbracket
N\rrbracket_{w}\mid[y\leftrightarrow z]))\end{array}$

The encoding addresses the non-linear usage of data elements in processes by
encoding the types $\tau\wedge A$ and $\tau\supset A$ as
$!\llbracket\tau\rrbracket\otimes\llbracket A\rrbracket$ and
$!\llbracket\tau\rrbracket\multimap\llbracket A\rrbracket$, respectively.
Thus, sending and receiving of data is codified as the sending and receiving
of channels of type $!$, which therefore can be used non-linearly. Moreover,
since data terms are themselves non-linear, the $\tau\rightarrow\sigma$ type
is encoded as $!\llbracket\tau\rrbracket\multimap\llbracket\sigma\rrbracket$,
following Girard's embedding of intuitionistic logic in linear logic [15].

At the level of processes, offering a session of type $\tau\wedge A$ (i.e. a
process of the form $z\langle M\rangle.P$) is encoded according to the
translation of the type: we first send a _fresh_ name $x$ which will be used
to access the encoding of the term $M$. Since $M$ can be used an arbitrary
number of times by the receiver, we guard the encoding of $M$ with a
replicated input, proceeding with the encoding of $P$ accordingly. Using a
session of type $\tau\supset A$ follows the same principle. The input cases
(and the rest of the process constructs) are completely homomorphic.

The encoding of $\lambda$-terms follows Girard's decomposition of the
intuitionistic function space [49]. The $\lambda$-abstraction is translated as
input. Since variables in a $\lambda$-abstraction may be used non-linearly,
the case for variables and application is slightly more intricate: to encode
the application $M\,N$ we compose $M$ in parallel with a process that will
send the ``reference'' to the function argument $N$ which will be encoded
using replication, in order to handle the potential for $0$ or more usages of
variables in a function body. Respectively, a variable is encoded by
performing an output to trigger the replication and forwarding accordingly.
Without loss of generality, we assume variable names and their corresponding
replicated counterparts match, which can be achieved through
$\alpha$-conversion before applying the translation. We exemplify our encoding
as follows:

$\small\begin{array}[]{c}\llbracket z(x).z\langle x\rangle.z\langle(\lambda
y{:}\sigma.x)\rangle.{\bf 0}\rrbracket=z(x).\overline{z}\langle
w\rangle.(!w(u).\llbracket x\rrbracket_{u}\mid\overline{z}\langle
v\rangle.(!v(i).\llbracket\lambda y{:}\sigma.x\rrbracket_{i}\mid{\bf 0}))\\\
\qquad\qquad\qquad\qquad=z(x).\overline{z}\langle
w\rangle.(!w(u).\overline{x}\langle y\rangle.[y\leftrightarrow
u]\mid\overline{z}\langle v\rangle.(!v(i).i(y).\overline{x}\langle
t\rangle.[t\leftrightarrow i]\mid{\bf 0}))\end{array}$

Properties of the Encoding.  We discuss the correctness of our encoding. We
can straightforwardly establish that the encoding preserves typing.

To show that our encoding is operationally sound and complete, we capture the
interaction between substitution on $\lambda$-terms and the encoding into
processes through logical equivalence. Consider the following reduction of a
process:

$\displaystyle(\mathbf{\nu}z)(z(x).z\langle x\rangle.z\langle(\lambda
y{:}\sigma.x)\rangle.{\bf 0}\mid z\langle\lambda w{:}\tau_{0}.w\rangle.P)$
$\displaystyle\hskip 85.35826pt\xrightarrow{}(\mathbf{\nu}z)(z\langle\lambda
w{:}\tau_{0}.w\rangle.z\langle(\lambda y{:}\sigma.\lambda
w{:}\tau_{0}.w)\rangle.{\bf 0}\mid P)$ (1)

Given that substitution in the target session $\pi$-calculus amounts to
renaming, whereas in the $\lambda$-calculus we replace a variable for a term,
the relationship between the encoding of a substitution $M\\{N/x\\}$ and the
encodings of $M$ and $N$ corresponds to the composition of the encoding of $M$
with that of $N$, but where the encoding of $N$ is guarded by a replication,
codifying a form of explicit non-linear substitution.

######  Lemma 4.1 (Compositionality)

Let $\Psi,x{:}\tau\vdash M:\sigma$ and $\Psi\vdash N:\tau$. We have that
$\llbracket
M\\{N/x\\}\rrbracket_{z}\approx_{\mathtt{L}}(\mathbf{\nu}x)(\llbracket
M\rrbracket_{z}\mid!x(y).\llbracket N\rrbracket_{y})$

Revisiting the process to the left of the arrow in Equation 1 we have:

$\small\begin{array}[]{l}\llbracket(\mathbf{\nu}z)(z(x).z\langle
x\rangle.z\langle(\lambda y{:}\sigma.x)\rangle.{\bf 0}\mid z\langle\lambda
w{:}\tau_{0}.w\rangle.P)\rrbracket\\\ =(\mathbf{\nu}z)(\llbracket
z(x).z\langle x\rangle.z\langle(\lambda y{:}\sigma.x)\rangle.{\bf
0}\rrbracket_{z}\mid\overline{z}\langle x\rangle.(!x(b).\llbracket\lambda
w{:}\tau_{0}.w\rrbracket_{b}\mid\llbracket P\rrbracket))\\\
\xrightarrow{}(\mathbf{\nu}z,x)(\overline{z}\langle
w\rangle.(!w(u).\overline{x}\langle y\rangle.[y\leftrightarrow
u]\mid\overline{z}\langle v\rangle.(!v(i).\llbracket\lambda
y{:}\sigma.x\rrbracket_{i}\mid{\bf 0})\mid\,!x(b).\llbracket\lambda
w{:}\tau_{0}.w\rrbracket_{b}\mid\llbracket P\rrbracket))\end{array}$

whereas the process to the right of the arrow is encoded as:

$\small\begin{array}[]{l}\llbracket(\mathbf{\nu}z)(z\langle\lambda
w{:}\tau_{0}.w\rangle.z\langle(\lambda y{:}\sigma.\lambda
w{:}\tau_{0}.w)\rangle.{\bf 0}\mid P)\rrbracket\\\
=(\mathbf{\nu}z)(\overline{z}\langle w\rangle.(!w(u).\llbracket\lambda
w{:}\tau_{0}.w\rrbracket_{u}\mid\overline{z}\langle
v\rangle.(!v(i).\llbracket\lambda y{:}\sigma.\lambda
w{:}\tau_{0}.w\rrbracket_{i}\mid\llbracket P\rrbracket)))\end{array}$

While the reduction of the encoded process and the encoding of the reduct
differ syntactically, they are observationally equivalent – the latter inlines
the replicated process behaviour that is accessible in the former on $x$.
Having characterised substitution, we establish operational correspondence for
the encoding.

######  Theorem 4.3 (Operational Correspondence)

  1. 1.

If $\Psi\vdash M:\tau$ and $\llbracket M\rrbracket_{z}\xrightarrow{}Q$ then
$M\xrightarrow{}^{+}N$ such that $\llbracket
N\rrbracket_{z}\approx_{\mathtt{L}}Q$

  2. 2.

If $\Psi;\Gamma;\Delta\vdash P::z{:}A$ and $\llbracket
P\rrbracket\xrightarrow{}Q$ then $P\xrightarrow{}^{+}P^{\prime}$ such that
$\llbracket P^{\prime}\rrbracket\approx_{\mathtt{L}}Q$

  3. 3.

If $\Psi\vdash M:\tau$ and $M\xrightarrow{}N$ then $\llbracket
M\rrbracket_{z}\stackrel{{\scriptstyle}}{{\Longrightarrow}}P$ such that
$P\approx_{\mathtt{L}}\llbracket N\rrbracket_{z}$

  4. 4.

If $\Psi;\Gamma;\Delta\vdash P::z{:}A$ and $P\xrightarrow{}Q$ then $\llbracket
P\rrbracket\xrightarrow{}^{+}R$ with $R\approx_{\mathtt{L}}\llbracket
Q\rrbracket$

The process equivalence in Theorem 4.3 above need not be extended to account
for data (although it would be relatively simple to do so), since the
processes in the image of the encoding are fully erased of any data elements.

#### Back to $\lambda$-Terms.

We extend our encoding of processes to $\lambda$-terms to Sess$\pi\lambda$.
Our extended translation maps processes to linear $\lambda$-terms, with the
session type $\tau\wedge A$ interpreted as a pair type where the first
component is replicated. Dually, $\tau\supset A$ is interpreted as a function
type where the domain type is replicated. The remaining session constructs are
translated as in § 3.2.

$\small\begin{array}[]{c}\llparenthesis\tau\wedge A\rrparenthesis\triangleq\
!\llparenthesis\tau\rrparenthesis\otimes\llparenthesis
A\rrparenthesis\quad\quad\llparenthesis\tau\supset A\rrparenthesis\triangleq\
!\llparenthesis\tau\rrparenthesis\multimap\llparenthesis
A\rrparenthesis\quad\quad\llparenthesis\tau\rightarrow\sigma\rrparenthesis\triangleq\
!\llparenthesis\tau\rrparenthesis\multimap\llparenthesis\sigma\rrparenthesis\end{array}$
$\small\begin{array}[]{llclllcl}({{\wedge}\mathsf{L}})&\llparenthesis
x(y).P\rrparenthesis&\triangleq&\mathsf{let}\,y\otimes
x=x\,\mathsf{in}\,\mathsf{let}\,!y=y\,\mathsf{in}\,\llparenthesis
P\rrparenthesis&({{\wedge}\mathsf{R}})&\llparenthesis z\langle
M\rangle.P\rrparenthesis&\triangleq&\langle!\llparenthesis
M\rrparenthesis\otimes\llparenthesis P\rrparenthesis\rangle\\\
({{\supset}\mathsf{R}})&\llparenthesis x(y).P\rrparenthesis&\triangleq&\lambda
x{:}!\llparenthesis\tau\rrparenthesis.\mathsf{let}\,!x=x\,\mathsf{in}\,\llparenthesis
P\rrparenthesis&({{\supset}\mathsf{L}})&\llparenthesis x\langle
M\rangle.P\rrparenthesis&\triangleq&\llparenthesis
P\rrparenthesis\\{(x\,!\llparenthesis M\rrparenthesis)/x\\}\end{array}$
$\begin{array}[]{c}\llparenthesis\lambda
x{:}\tau.M\rrparenthesis\triangleq\lambda
x{:}!\llparenthesis\tau\rrparenthesis.\mathsf{let}\,!x=x\,\mathsf{in}\,\llparenthesis
M\rrparenthesis\par\quad\llparenthesis
M\,N\rrparenthesis\triangleq\llparenthesis M\rrparenthesis\,!\llparenthesis
N\rrparenthesis\quad\llparenthesis x\rrparenthesis\triangleq x\end{array}$

The treatment of non-linear components of processes is identical to our
previous encoding: non-linear functions $\tau\rightarrow\sigma$ are translated
to linear functions of type $!\tau\multimap\sigma$; a process offering a
session of type $\tau\wedge A$ (i.e. a process of the form $z\langle
M\rangle.P$, typed by rule ${{\wedge}\mathsf{R}}$) is translated to a pair
where the first component is the encoding of $M$ prefixed with $!$ so that it
may be used non-linearly, and the second is the encoding of $P$. Non-linear
variables are handled at the respective binding sites: a process using a
session of type $\tau\wedge A$ is encoded using the elimination form for the
pair and the elimination form for the exponential; similarly, a process
offering a session of type $\tau\supset A$ is encoded as a
$\lambda$-abstraction where the bound variable is of type
$!\llparenthesis\tau\rrparenthesis$. Thus, we use the elimination form for the
exponential, ensuring that the typing is correct. We illustrate our encoding:

$\small\begin{array}[]{rcl}\llparenthesis z(x).z\langle
x\rangle.z\langle(\lambda y{:}\sigma.x)\rangle.{\bf 0}\rrparenthesis&=&\lambda
x{:}!\llparenthesis\tau\rrparenthesis.\mathsf{let}\,!x=x\,\mathsf{in}\,\langle!x\,\otimes\langle!\llparenthesis\lambda
y{:}\sigma.x\rrparenthesis\,\otimes\langle\rangle\rangle\rangle\\\ &=&\lambda
x{:}!\llparenthesis\tau\rrparenthesis.\mathsf{let}\,!x=x\,\mathsf{in}\,\langle!x\,\otimes\langle!(\lambda
y{:}!\llparenthesis\sigma\rrparenthesis.\mathsf{let}\,!y=y\,\mathsf{in}\,x)\,\otimes\langle\rangle\rangle\rangle\end{array}$

Properties of the Encoding.  Unsurprisingly due to the logical correspondence
between natural deduction and sequent calculus presentations of logic, our
encoding satisfies both type soundness and operational correspondence (c.f.
Theorems 3.2, 3.3, and 3.4). The full development can be found in [52].

#### Relating the Two Encodings.

We prove the two encodings are mutually inverse and preserve the full
abstraction properties (we write $=_{\beta}$ and $=_{\beta\eta}$ for $\beta$\-
and $\beta\eta$-equivalence, respectively).

######  Theorem 4.4 (Inverse)

If $\Psi;\Gamma;\Delta\vdash P::z{:}A$ then $\llbracket\llparenthesis
P\rrparenthesis\rrbracket_{z}\approx_{\mathtt{L}}\llbracket P\rrbracket$.
Also, if $\Psi\vdash M:\tau$ then $\llparenthesis\llbracket
M\rrbracket_{z}\rrparenthesis=_{\beta}\llparenthesis M\rrparenthesis$.

The equivalences above are formulated between the composition of the encodings
applied to $P$ (resp. $M$) and the process (resp. $\lambda$-term) _after_
applying the translation embedding the non-linear components into their linear
counterparts. This formulation matches more closely that of § 3.3, which
applies to linear calculi for which the _target_ languages of this section are
a strict subset (and avoids the formalisation of process equivalence with
terms). We also note that in this setting, observational equivalence and
$\beta\eta$-equivalence coincide [3, 31]. Moreover, the extensional flavour of
$\approx_{\mathtt{L}}$ includes $\eta$-like principles at the process level.

######  Theorem 4.5 ()

Let $\cdot\vdash M:\tau$ and $\cdot\vdash N:\tau$. $\llparenthesis
M\rrparenthesis=_{\beta\eta}\llparenthesis N\rrparenthesis$ iff $\llbracket
M\rrbracket_{z}\approx_{\mathtt{L}}\llbracket N\rrbracket_{z}$. Also, let
$\cdot\vdash P::z{:}A$ and $\cdot\vdash Q::z{:}A$. We have that $\llbracket
P\rrbracket\approx_{\mathtt{L}}\llbracket Q\rrbracket$ iff $\llparenthesis
P\rrparenthesis=_{\beta\eta}\llparenthesis Q\rrparenthesis$.

We establish full abstraction for the encoding of $\lambda$-terms into
processes (Theorem 4.5) in two steps: The completeness direction (i.e. from
left-to-right) follows from operational completeness and strong normalisation
of the $\lambda$-calculus. The soundness direction uses operational soundness.
The proof of Theorem 4.5 uses the same strategy of Theorem 3.7, appealing to
the inverse theorems.

###  4.3 Higher-Order Session Processes – Sess$\pi\lambda^{+}$

We extend the value-passing framework of the previous section, accounting for
process-passing (i.e. the higher-order) in a session-typed setting. As shown
in [50], we achieve this by adding to the data layer a _contextual monad_ that
encapsulates (open) session-typed processes as data values, with a
corresponding elimination form in the process layer. We dub this calculus
Sess$\pi\lambda^{+}$.

$\begin{array}[]{rclrcl}P,Q&::=&\dots\mid x\leftarrow
M\leftarrow\overline{y_{i}};Q&\quad\quad M.N&::=&\dots\mid\\{x\leftarrow
P\leftarrow\overline{y_{i}{:}A_{i}}\\}\\\
\tau,\sigma&::=&\dots\mid\\{\overline{x_{j}{:}A_{j}}\vdash
z{:}A\\}\end{array}$

The type $\\{\overline{x_{j}{:}A_{j}}\vdash z{:}A\\}$ is the type of a term
which encapsulates an open process that uses the linear channels
$\overline{x_{j}{:}A_{j}}$ and offers $A$ along channel $z$. This formulation
has the added benefit of formalising the integration of session-typed
processes in a functional language and forms the basis for the concurrent
programming language SILL [37, 50]. The typing rules for the new constructs
are (for simplicity we assume no shared channels in process monads):

$\begin{array}[]{c}\Psi\vdash\\{z\leftarrow
P\leftarrow\overline{x_{i}{:}A_{i}}\\}:\\{\overline{x_{i}{:}A_{i}}\vdash
z{:}A\\}\Psi;\cdot;\overline{x_{i}{:}A_{i}}\vdash P::z{:}A\\\\[4.5pt]
\Psi;\Gamma;\Delta_{1},\Delta_{2}\vdash x\leftarrow
M\leftarrow\overline{y_{i}};Q::z{:}C\lx@proof@logical@and\Psi\vdash
M:\\{\overline{x_{i}{:}A_{i}}\vdash
x{:}A\\}\Delta_{1}=\overline{y_{i}{:}A_{i}}\Psi;\Gamma;\Delta_{2},x{:}A\vdash
Q::z{:}C\end{array}$

Rule $\\{\\}I$ embeds processes in the term language by essentially quoting an
open process that is well-typed according to the type specification in the
monadic type. Dually, rule $\\{\\}E$ allows for processes to use monadic
values through composition that _consumes_ some of the ambient channels in
order to provide the monadic term with the necessary context (according to its
type). These constructs are discussed in substantial detail in [50]. The
reduction semantics of the process construct is given by (we tacitly assume
that the names $\overline{y}$ and $c$ do not occur in $P$ and omit the
congruence case):

$\begin{array}[]{c}(c\leftarrow\\{z\leftarrow
P\leftarrow\overline{x_{i}{:}A_{i}}\\}\leftarrow\overline{y_{i}};Q)\xrightarrow{}(\mathbf{\nu}c)(P\\{\overline{y}/\overline{x_{i}}\\{c/z\\}\\}\mid
Q)\end{array}$

The semantics allows for the underlying monadic term $M$ to evaluate to a
(quoted) process $P$. The process $P$ is then executed in parallel with the
continuation $Q$, sharing the linear channel $c$ for subsequent interactions.
We illustrate the higher-order extension with following typed process (we
write $\\{x\leftarrow P\\}$ when $P$ does not depend on any linear channels
and assume $\vdash Q::d{:}\mathsf{Nat}\wedge\mathbf{1}$):

$P\triangleq(\mathbf{\nu}c)(c\langle\\{d\leftarrow Q\\}\rangle.c(x).{\bf
0}\mid c(y).d\leftarrow y;d(n).c\langle n\rangle.{\bf 0})$ (2)

Process $P$ above gives an abstract view of a communication idiom where a
process (the left-hand side of the parallel composition) sends another process
$Q$ which potentially encapsulates some complex computation. The receiver then
_spawns_ the execution of the received process and inputs from it a result
value that is sent back to the original sender. An execution of $P$ is given
by:

$\small\begin{array}[]{rcl}P\xrightarrow{}(\mathbf{\nu}c)(c(x).{\bf 0}\mid
d\leftarrow\\{d\leftarrow Q\\};d(n).c\langle n\rangle.{\bf
0})&\xrightarrow{}&(\mathbf{\nu}c)(c(x).{\bf 0}\mid(\mathbf{\nu}d)(Q\mid
d(n).c\langle n\rangle.{\bf 0}))\\\
&\xrightarrow{}^{+}&(\mathbf{\nu}c)(c(x).{\bf 0}\mid c\langle 42\rangle.{\bf
0})\xrightarrow{}{\bf 0}\end{array}$

Given the seminal work of Sangiorgi [46], such a representation naturally begs
the question of whether or not we can develop a _typed_ encoding of higher-
order processes into the first-order setting. Indeed, we can achieve such an
encoding with a fairly simple extension of the encoding of § 4.2 to
Sess$\pi\lambda^{+}$ by observing that monadic values are processes that need
to be potentially provided with extra sessions in order to be executed
correctly. For instance, a term of type $\\{x{:}A\vdash y{:}B\\}$ denotes a
process that given a session $x$ of type $A$ will then offer $y{:}B$.
Exploiting this observation we encode this type as the session $A\multimap B$,
ensuring subsequent usages of such a term are consistent with this
interpretation.

$\small\begin{array}[]{lcl}\llbracket\\{\overline{x_{j}{:}A_{j}}\vdash
z{:}A\\}\rrbracket&\triangleq&\overline{\llbracket
A_{j}\rrbracket}\multimap\llbracket A\rrbracket\\\\[4.5pt]
\llbracket\\{x\leftarrow
P\rightarrow\overline{y_{i}}\\}\rrbracket_{z}&\triangleq&z(y_{0}).\dots.z(y_{n}).\llbracket
P\\{z/x\\}\rrbracket\quad(z\not\in\mbox{\it fn}(P))\\\\[4.5pt] \llbracket
x\leftarrow
M\leftarrow\overline{y_{i}};Q\rrbracket&\triangleq&(\mathbf{\nu}x)(\llbracket
M\rrbracket_{x}\mid\overline{x}\langle a_{0}\rangle.([a_{0}\leftrightarrow
y_{0}]\mid\dots\mid x\langle a_{n}\rangle.([a_{n}\leftrightarrow
y_{n}]\mid\llbracket Q\rrbracket)\dots))\end{array}$

To encode the monadic type $\\{\overline{x_{j}{:}A_{j}}\vdash z{:}A\\}$,
denoting the type of process $P$ that is typed by
$\overline{x_{j}{:}A_{j}}\vdash P::z{:}A$, we require that the session in the
image of the translation specifies a sequence of channel inputs with
behaviours $\overline{A_{j}}$ that make up the linear context. After the
contextual aspects of the type are encoded, the session will then offer the
(encoded) behaviour of $A$. Thus, the encoding of the monadic type is
$\llbracket A_{0}\rrbracket\multimap\dots\multimap\llbracket
A_{n}\rrbracket\multimap\llbracket A\rrbracket$, which we write as
$\overline{\llbracket A_{j}\rrbracket}\multimap\llbracket A\rrbracket$. The
encoding of monadic expressions adheres to this behaviour, first performing
the necessary sequence of inputs and then proceeding inductively. Finally, the
encoding of the elimination form for monadic expressions behaves dually,
composing the encoding of the monadic expression with a sequence of outputs
that instantiate the consumed names accordingly (via forwarding). The encoding
of process $P$ from Equation 2 is thus:

$\small\begin{array}[]{l}\llbracket P\rrbracket=(\mathbf{\nu}c)(\llbracket
c\langle\\{d\leftarrow Q\\}\rangle.c(x).{\bf 0}\rrbracket\mid\llbracket
c(y).d\leftarrow y;d(n).c\langle n\rangle.{\bf 0}\rrbracket)\\\
=(\mathbf{\nu}c)(\overline{c}\langle w\rangle.(!w(d).\llbracket
Q\rrbracket\mid c(x).{\bf 0})c(y).(\mathbf{\nu}d)(\overline{y}\langle
b\rangle.[b\leftrightarrow d]\mid d(n).\overline{c}\langle
m\rangle.(\overline{n}\langle e\rangle.[e\leftrightarrow m]\mid{\bf
0})))\end{array}$

#### Properties of the Encoding.

As in our previous development, we can show that our encoding for
Sess$\pi\lambda^{+}$ is type sound and satisfies operational correspondence.
The full development is omitted but can be found in [52].

We encode Sess$\pi\lambda^{+}$ into $\lambda$-terms, extending § 4.2 with:

$\small\begin{array}[]{l}\llparenthesis\\{\overline{x_{i}{:}A_{i}}\vdash
z{:}A\\}\rrparenthesis\triangleq\overline{\llparenthesis
A_{i}\rrparenthesis}\multimap\llparenthesis A\rrparenthesis\\\\[1.42262pt]
\llparenthesis x\leftarrow
M\leftarrow\overline{y_{i}};Q\rrparenthesis\triangleq\llparenthesis
Q\rrparenthesis\\{(\llparenthesis M\rrparenthesis\,\overline{y_{i}})/x\\}\
\quad\llparenthesis\\{x\leftarrow
P\leftarrow\overline{w_{i}}\\}\rrparenthesis\triangleq\lambda
w_{0}.\dots.\lambda w_{n}.\llparenthesis P\rrparenthesis\end{array}$

The encoding translates the monadic type $\\{\overline{x_{i}{:}A_{i}}\vdash
z{:}A\\}$ as a linear function $\overline{\llparenthesis
A_{i}\rrparenthesis}\multimap\llparenthesis A\rrparenthesis$, which captures
the fact that the underlying value must be provided with terms satisfying the
requirements of the linear context. At the level of terms, the encoding for
the monadic term constructor follows its type specification, generating a
nesting of $\lambda$-abstractions that closes the term and proceeding
inductively. For the process encoding, we translate the monadic application
construct analogously to the translation of a linear $\mathsf{cut}$, but
applying the appropriate variables to the translated monadic term (which is of
function type). We remark the similarity between our encoding and that of the
previous section, where monadic terms are translated to a sequence of inputs
(here a nesting of $\lambda$-abstractions). Our encoding satisfies type
soundness and operational correspondence, as usual. Further showcasing the
applications of our development, we obtain a novel strong normalisation result
for this higher-order session-calculus ``for free'', through encoding to the
$\lambda$-calculus.

######  Theorem 4.6 (Strong Normalisation)

Let $\Psi;\Gamma;\Delta\vdash P::z{:}A$. There is no infinite reduction
sequence starting from $P$.

######  Theorem 4.7 (Inverse Encodings)

If $\Psi;\Gamma;\Delta\vdash P::z{:}A$ then $\llbracket\llparenthesis
P\rrparenthesis\rrbracket_{z}\approx_{\mathtt{L}}\llbracket P\rrbracket$.
Also, if $\Psi\vdash M:\tau$ then $\llparenthesis\llbracket
M\rrbracket_{z}\rrparenthesis=_{\beta}\llparenthesis M\rrparenthesis$.

###### Theorem 4.8

Let $\vdash M:\tau$, $\vdash N:\tau$, $\vdash P::z{:}A$ and $\vdash Q::z{:}A$.
$\llparenthesis M\rrparenthesis=_{\beta\eta}\llparenthesis N\rrparenthesis$
iff $\llbracket M\rrbracket_{z}\approx_{\mathtt{L}}\llbracket N\rrbracket_{z}$
and $\llbracket P\rrbracket\approx_{\mathtt{L}}\llbracket Q\rrbracket$ iff
$\llparenthesis P\rrparenthesis=_{\beta\eta}\llparenthesis Q\rrparenthesis$.

##  5 Related Work and Concluding Remarks

Process Encodings of Functions.  Toninho et al. [49] study encodings of the
simply-typed $\lambda$-calculus in a logically motivated session
$\pi$-calculus, via encodings to the linear $\lambda$-calculus. Our work
differs since they do not study polymorphism nor reverse encodings; and we
provide deeper insights through applications of the encodings. Full
abstraction or inverse properties are not studied.

Sangiorgi [43] uses a fully abstract compilation from the higher-order
$\pi$-calculus (HO$\pi$) to the $\pi$-calculus to study full abstraction for
Milner's encodings of the $\lambda$-calculus. The work shows that Milner's
encoding of the lazy $\lambda$-calculus can be recovered by restricting the
semantic domain of processes (the so-called _restrictive_ approach) or by
enriching the $\lambda$-calculus with suitable constants. This work was later
refined in [45], which does not use HO$\pi$ and considers an operational
equivalence on $\lambda$-terms called _open applicative bisimulation_ which
coincides with Lévy-Longo tree equality. The work [47] studies general
conditions under which encodings of the $\lambda$-calculus in the
$\pi$-calculus are fully abstract wrt Lévy-Longo and Böhm Trees, which are
then applied to several encodings of (call-by-name) $\lambda$-calculus. The
works above deal with untyped calculi, and so reverse encodings are
unfeasible. In a broader sense, our approach takes the restrictive approach
using linear logic-based session typing and the induced observational
equivalence. We use a $\lambda$-calculus with booleans as observables and
reason with a Morris-style equivalence instead of tree equalities. It would be
an interesting future work to apply the conditions in [47] in our typed
setting.

Wadler [54] shows a correspondence between a linear functional language with
session types GV and a session-typed process calculus with polymorphism based
on classical linear logic CP. Along the lines of this work, Lindley and Morris
[26], in an exploration of inductive and coinductive session types through the
addition of least and greatest fixed points to CP and GV, develop an encoding
from a linear $\lambda$-calculus with session primitives (Concurrent $\mu$GV)
to a pure linear $\lambda$-calculus (Functional $\mu$GV) via a CPS
transformation. They also develop translations between $\mu$CP and Concurrent
$\mu$GV, extending [25]. Mapping to the terminology used in our work [17],
their encodings are shown to be operationally complete, but no results are
shown for the operational soundness directions and neither full abstraction
nor inverse properties are studied. In addition, their operational
characterisations do not compose across encodings. For instance, while strong
normalisation of Functional $\mu$GV implies the same property for Concurrent
$\mu$GV through their operationally complete encoding, the encoding from
$\mu$CP to $\mu$GV does not necessarily preserve this property.

Types for $\pi$-calculi delineate sequential behaviours by restricting
composition and name usages, limiting the contexts in which processes can
interact. Therefore typed equivalences offer a coarser semantics than untyped
semantics. Berger et al. [5] study an encoding of System F in a polymorphic
linear $\pi$-calculus, showing it to be fully abstract based on game semantics
techniques. Their typing system and proofs are more complex due to the fine-
grained constraints from game semantics. Moreover, they do not study a reverse
encoding.

Orchard and Yoshida [33] develop embeddings to-and-from PCF with parallel
effects and a session-typed $\pi$-calculus, but only develop operational
correspondence and semantic soundness results, leaving the full abstraction
problem open.

Polymorphism and Typed Behavioural Semantics.  The work of [7] studies
parametric session polymorphism for the intuitionistic setting, developing a
behavioural equivalence that captures parametricity, which is used (denoted as
$\approx_{\mathtt{L}}$) in our paper. The work [39] introduces a typed
bisimilarity for polymorphism in the $\pi$-calculus. Their bisimilarity is of
an intensional flavour, whereas the one used in our work follows the
extensional style of Reynolds [41]. Their typing discipline (originally from
[53], which also develops type-preserving encodings of polymorphic
$\lambda$-calculus into polymorphic $\pi$-calculus) differs significantly from
the linear logic-based session typing of our work (e.g. theirs does not ensure
deadlock-freedom). A key observation in their work is the coarser nature of
typed equivalences with polymorphism (in analogy to those for IO-subtyping
[38]) and their interaction with channel aliasing, suggesting a use of typed
semantics and encodings of the $\pi$-calculus for fine-grained analyses of
program behaviour.

F-Algebras and Linear-F.  The use of initial and final (co)algebras to give a
semantics to inductive and coinductive types dates back to Mendler [28], with
their strong definability in System F appearing in [1] and [19]. The
definability of inductive and coinductive types using parametricity also
appears in [40] in the context of a logic for parametric polymorphism and
later in [6] in a linear variant of such a logic. The work of [55] studies
parametricity for the polymorphic linear $\lambda$-calculus of this work,
developing encodings of a few inductive types but not the initial (or final)
algebraic encodings in their full generality. Inductive and coinductive
session types in a logical process setting appear in [51] and [26]. Both works
consider a calculus with built-in recursion – the former in an intuitionistic
setting where a process that offers a (co)inductive protocol is composed with
another that consumes the (co)inductive protocol and the latter in a classical
framework where composed recursive session types are dual each other.

Conclusion and Future Work.  This work answers the question of what kind of
type discipline of the $\pi$-calculus can exactly capture and is captured by
$\lambda$-calculus behaviours. Our answer is given by showing the first
mutually inverse and fully abstract encodings between two calculi with
polymorphism, one being the Poly$\pi$ session calculus based on intuitionistic
linear logic, and the other (a linear) System F. This further demonstrates
that the linear logic-based articulation of name-passing interactions
originally proposed by [8] (and studied extensively thereafter e.g. [50, 51,
36, 9, 54, 7, 25]) provides a clear and applicable tool for message-passing
concurrency. By exploiting the proof theoretic equivalences between natural
deduction and sequent calculus we develop mutually inverse and fully abstract
encodings, which naturally extend to more intricate settings such as process
passing (in the sense of HO$\pi$). Our encodings also enable us to derive
properties of the $\pi$-calculi ``for free''. Specifically, we show how to
obtain adequate representations of least and greatest fixed points in
Poly$\pi$ through the encoding of initial and final (co)algebras in the
$\lambda$-calculus. We also straightforwardly derive a strong normalisation
result for the higher-order session calculus, which otherwise involves non-
trivial proof techniques [13, 12, 36, 7, 5]. Future work includes extensions
to the classical linear logic-based framework, including multiparty session
types [10, 11]. Encodings of session $\pi$-calculi to the $\lambda$-calculus
have been used to implement session primitives in functional languages such as
Haskell (see a recent survey [32]), OCaml [34, 35, 24] and Scala [48].
Following this line of work, we plan to develop encoding-based implementations
of this work as embedded DSLs. This would potentially enable an exploration of
algebraic constructs beyond initial and final co-algebras in a session
programming setting. In particular, we wish to further study the meaning of
functors, natural transformations and related constructions in a session-typed
setting, both from a more fundamental viewpoint but also in terms of
programming patterns.

Acknowledgements. The authors would like to thank the reviewers for their
comments, suggestions and pointers to related works. This work is partially
supported by EPSRC EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1 and
EP/N028201/1.

## References

  * [1] Bainbridge, E.S., Freyd, P.J., Scedrov, A., Scott, P.J.: Functorial polymorphism. Theor. Comput. Sci. 70(1), 35–64 (1990)
  * [2] Balzer, S., Pfenning, F.: Manifest sharing with session types. In: ICFP (2017)
  * [3] Barber, A.: Dual intuitionistic linear logic. Tech. Rep. ECS-LFCS-96-347, School of Informatics, University of Edinburgh (1996)
  * [4] Benton, N.: A mixed linear and non-linear logic: Proofs, terms and models (extended abstract). In: CSL. pp. 121–135 (1994)
  * [5] Berger, M., Honda, K., Yoshida, N.: Genericity and the pi-calculus. Acta Inf. 42(2-3), 83–141 (2005)
  * [6] Birkedal, L., Møgelberg, R.E., Petersen, R.L.: Linear Abadi and Plotkin Logic. Logical Methods in Computer Science 2(5) (2006)
  * [7] Caires, L., Pérez, J.A., Pfenning, F., Toninho, B.: Behavioral polymorphism and parametricity in session-based communication. In: ESOP 2013\. pp. 330–349 (2013)
  * [8] Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: CONCUR 2010. pp. 222–236 (2010)
  * [9] Caires, L., Pfenning, F., Toninho, B.: Linear logic propositions as session types. Mathematical Structures in Computer Science 26(3), 367–423 (2016)
  * [10] Carbone, M., Lindley, S., Montesi, F., Schuermann, C., Wadler, P.: Coherence generalises duality: a logical explanation of multiparty session types. In: CONCUR'16. vol. 59, pp. 33:1–33:15. Sch. Dag. (2016)
  * [11] Carbone, M., Montesi, F., Schurmann, C., Yoshida, N.: Multiparty session types as coherence proofs. In: CONCUR 2015. vol. 42, pp. 412–426. Sch. Dag. (2015)
  * [12] Demangeon, R., Hirschkoff, D., Sangiorgi, D.: Mobile processes and termination. In: Semantics and Algebraic Specification. pp. 250–273 (2009)
  * [13] Demangeon, R., Hirschkoff, D., Sangiorgi, D.: Termination in higher-order concurrent calculi. J. Log. Algebr. Program. 79(7), 550–577 (2010)
  * [14] Gentzen, G.: Untersuchungen über das logische schließen. Mathematische Zeitschrift 39, 176–210 (1935)
  * [15] Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)
  * [16] Girard, J., Lafont, Y., Taylor, P.: Proofs and Types. C. U. P. (1989)
  * [17] Gorla, D.: Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208(9), 1031–1053 (2010)
  * [18] Gorla, D., Nestmann, U.: Full abstraction for expressiveness: history, myths and facts. Mathematical Structures in Computer Science 26(4), 639–654 (2016)
  * [19] Hasegawa, R.: Categorical data types in parametric polymorphism. Mathematical Structures in Computer Science 4(1), 71–109 (1994)
  * [20] Honda, K.: Types for dyadic interaction. In: CONCUR'93. pp. 509–523 (1993)
  * [21] Honda, K.: Session types and distributed computing. In: ICALP (2012)
  * [22] Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type disciplines for structured communication-based programming. In: ESOP'98. pp. 22–138 (1998)
  * [23] Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL'08. pp. 273–284 (2008)
  * [24] Imai, K., Yoshida, N., Yuen, S.: Session-ocaml: a session-based library with polarities and lenses . In: COORDINATION. LNCS, vol. 10319, pp. 99–118 (2017)
  * [25] Lindley, S., Morris, J.G.: A semantics for propositions as sessions. In: ESOP'15. pp. 560–584 (2015)
  * [26] Lindley, S., Morris, J.G.: Talking bananas: structural recursion for session types. In: ICFP 2016. pp. 434–447 (2016)
  * [27] Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name, call-by-value, call-by-need and the linear lambda calculus. T. C. S. 228(1-2), 175–210 (1999)
  * [28] Mendler, N.P.: Recursive types and type constraints in second-order lambda calculus. In: LICS'87. pp. 30–36 (1987)
  * [29] Milner, R.: Functions as processes. Math. Struct. in C.S. 2(2), 119–141 (1992)
  * [30] Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I and II. Inf. Comput. 100(1), 1–77 (1992)
  * [31] Ohta, Y., Hasegawa, M.: A terminating and confluent linear lambda calculus. In: RTA'06. pp. 166–180 (2006)
  * [32] Orchard, D., Yoshida, N.: Session types with linearity in Haskell. In: Behavioural Types: from Theory to Tools. River Publishers (2017)
  * [33] Orchard, D.A., Yoshida, N.: Effects as sessions, sessions as effects. In: POPL 2016. pp. 568–581 (2016)
  * [34] Padovani, L.: A Simple Library Implementation of Binary Sessions. JFP 27 (2016)
  * [35] Padovani, L.: Context-Free Session Type Inference. In: ESOP 2017 (2017)
  * [36] Pérez, J.A., Caires, L., Pfenning, F., Toninho, B.: Linear logical relations for session-based concurrency. In: ESOP. pp. 539–558 (2012)
  * [37] Pfenning, F., Griffith, D.: Polarized substructural session types. In: FoSSaCS. pp. 3–22 (2015)
  * [38] Pierce, B.C., Sangiorgi, D.: Typing and subtyping for mobile processes. Mathematical Structures in Computer Science 6(5), 409–453 (1996)
  * [39] Pierce, B.C., Sangiorgi, D.: Behavioral equivalence in the polymorphic pi-calculus. J. ACM 47(3), 531–584 (2000)
  * [40] Plotkin, G.D., Abadi, M.: A logic for parametric polymorphism. In: TLCA '93. pp. 361–375 (1993)
  * [41] Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress. pp. 513–523 (1983)
  * [42] Reynolds, J.C., Plotkin, G.D.: On functors expressible in the polymorphic typed lambda calculus. Inf. Comput. 105(1), 1–29 (1993)
  * [43] Sangiorgi, D.: An investigation into functions as processes. In: MFPS (1993)
  * [44] Sangiorgi, D.: Pi-calculus, internal mobility, and agent-passing calculi. Theor. Comput. Sci. 167(1&2), 235–274 (1996)
  * [45] Sangiorgi, D.: Lazy functions and mobile processes. In: Proof, Language, and Interaction, Essays in Honour of Robin Milner. pp. 691–720 (2000)
  * [46] Sangiorgi, D., Walker, D.: The pi-calculus: A theory of mobile processes (2001)
  * [47] Sangiorgi, D., Xu, X.: Trees from functions as processes. In: CONCUR (2014)
  * [48] Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In: ECOOP'17 (2017)
  * [49] Toninho, B., Caires, L., Pfenning, F.: Functions as session-typed processes. In: FOSSACS 2012. pp. 346–360 (2012)
  * [50] Toninho, B., Caires, L., Pfenning, F.: Higher-order processes, functions, and sessions: A monadic integration. In: ESOP. pp. 350–369 (2013)
  * [51] Toninho, B., Caires, L., Pfenning, F.: Corecursion and non-divergence in session-typed processes. In: TGC 2014. pp. 159–175 (2014)
  * [52] Toninho, B., Yoshida, N.: On polymorphic sessions and functions: A tale of two (fully abstract) encodings (long version). CoRR abs/1711.00878 (2017)
  * [53] Turner, D.: The polymorphic pi-calculus: Theory and implementation. Tech. Rep. ECS-LFCS-96-345, School of Informatics, University of Edinburgh (1996)
  * [54] Wadler, P.: Propositions as sessions. J. Funct. Program. 24(2-3), 384–418 (2014)
  * [55] Zhao, J., Zhang, Q., Zdancewic, S.: Relational parametricity for a polymorphic linear lambda calculus. In: APLAS. pp. 344–359 (2010)

Appendix

On Polymorphic Sessions and Functions

A Tale of Two (Fully Abstract) Encodings

Additional definitions and proofs of the main materials.

##  Appendix 0.A Appendix

###  0.A.1 Additional Definitions for § 2 – Structural Congruence

######  Definition 0.A.1 (Structural congruence)

is the least congruence relation generated by the following laws: $P\mid{\bf
0}\equiv P$; $P\equiv_{\alpha}Q\Rightarrow P\equiv Q$; $P\mid Q\equiv Q\mid
P$; $P\mid(Q\mid R)\equiv(P\mid Q)\mid R$;
$(\mathbf{\nu}x)(\mathbf{\nu}y)P\equiv(\mathbf{\nu}y)(\mathbf{\nu}x)P$;
$x\not\in\mbox{\it fn}(P)\Rightarrow
P\mid(\mathbf{\nu}x)Q\equiv(\mathbf{\nu}x)(P\mid Q)$; $(\mathbf{\nu}x){\bf
0}\equiv{\bf 0}$; and $[x\leftrightarrow y]\equiv[y\leftrightarrow x]$.

######  Definition 0.A.2 (Extended Structural Congruence)

We write $\equiv_{!}$ for the least congruence relation on processes which
results from extending structural congruence $\equiv$ (Def. 0.A.1) with the
following axioms, dubbed the Sharpened Replication Axioms [46]:

  1. 1.

$(\mathbf{\nu}u)(!u(z).P\mid(\nu y)(Q\mid R))\equiv_{!}(\nu y)((\nu
u)(!u(z).P\mid Q)\mid(\nu u)(!u(z).P\mid R))$

  2. 2.

$(\nu u)(!u(y).P\mid(\nu v)(!v(z).Q\mid R))\equiv_{!}(\nu v)((!v(z).(\nu
u)(!u(y).P\mid Q))\mid(\nu u)(!u(y).P\mid R))$

  3. 3.

$(\nu u)(!u(y).Q\mid P)\equiv_{!}P$ if $u\not\in\mbox{\it fn}(P)$

Axioms (1) and (2) represent principles for the distribution of shared servers
among processes, while (3) formalises the garbage collection of shared servers
which cannot be invoked by any process. The axioms embody distributivity,
contraction and weakening of shared resources and are sound wrt (typed)
observational equivalence [36].

###  0.A.2 Additional Definitions for § 2 – Typing Rules

Below we list the typing rules for the calculus of section § 2. We note that
the judgment $\Omega\vdash B\,\mathsf{type}$ simply requires that free
variables in $B$ be in $\Omega$. Moreover, typing treats processes quotiented
by structural congruence – given a well-typed process
$\Omega;\Gamma;\Delta\vdash P::T$, subject reduction ensures that for all
possible reductions $P\xrightarrow{\tau}P^{\prime}$, there exists a process
$Q$ where $P^{\prime}\equiv Q$ such that $\Omega;\Gamma;\Delta\vdash Q::T$.
Related properties hold wrt general transitions
$P\xrightarrow{\alpha}P^{\prime}$. We refer the reader to [9, 8] for
additional details on this matter.

$\begin{array}[]{c}\raise
11.0pt\hbox{$\hbox{$\hbox{\small\sc$(\mathsf{id})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.83331pt\vbox{\hbox{\hskip-0.83331pt\hbox{\hbox{$\displaystyle\displaystyle{\,}$}}}\vbox{}}}\over\hbox{\hskip
59.7636pt\vbox{\vbox{}\hbox{\hskip-59.7636pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;x{:}A\vdash[x\leftrightarrow
z]::z{:}A}$}}}}}}$}}\hbox{}$}\quad\raise
10.44444pt\hbox{$\hbox{$\hbox{\small\sc$({{\mathbf{1}}\mathsf{R}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.83331pt\vbox{\hbox{\hskip-0.83331pt\hbox{\hbox{$\displaystyle\displaystyle{\,}$}}}\vbox{}}}\over\hbox{\hskip
32.05894pt\vbox{\vbox{}\hbox{\hskip-32.05893pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\cdot\vdash{\bf
0}::z{:}\mathbf{1}}$}}}}}}$}}\hbox{}$}\quad\raise
10.44444pt\hbox{$\hbox{$\hbox{\small\sc$({{\mathbf{1}}\mathsf{L}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
41.2835pt\vbox{\hbox{\hskip-41.2835pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta\vdash
P::z{:}C}$}}}\vbox{}}}\over\hbox{\hskip
50.25224pt\vbox{\vbox{}\hbox{\hskip-50.25223pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta,x{:}\mathbf{1}\vdash
P::z{:}C}$}}}}}}$}}\hbox{}$}\\\\[10.00002pt] \raise
11.0pt\hbox{$\hbox{$\hbox{\small\sc$({{\multimap}\mathsf{R}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
54.3921pt\vbox{\hbox{\hskip-54.3921pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta,x{:}A\vdash
P::z{:}B}$}}}\vbox{}}}\over\hbox{\hskip
64.99284pt\vbox{\vbox{}\hbox{\hskip-64.99283pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta\vdash
z(x).P::z{:}A\multimap B}$}}}}}}$}}\hbox{}$}\quad\raise
11.0pt\hbox{$\hbox{$\hbox{\small\sc$({{\multimap}\mathsf{L}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
100.8318pt\vbox{\hbox{\hskip-100.8318pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta_{1}\vdash
P::y{:}A\quad\Omega;\Gamma;\Delta_{2},x{:}B\vdash
Q::z{:}C}$}}}\vbox{}}}\over\hbox{\hskip
107.60963pt\vbox{\vbox{}\hbox{\hskip-107.60962pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta_{1},\Delta_{2},x{:}A\multimap
B\vdash(\mathbf{\nu}y)x\langle y\rangle.(P\mid
Q)::z{:}C}$}}}}}}$}}\hbox{}$}\\\\[10.00002pt] \raise
11.0pt\hbox{$\hbox{$\hbox{\small\sc$({{\otimes}\mathsf{R}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
87.65411pt\vbox{\hbox{\hskip-87.65411pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta_{1}\vdash
P::y{:}A\quad\Omega;\Gamma;\Delta_{2}\vdash
Q::z{:}B}$}}}\vbox{}}}\over\hbox{\hskip
90.73523pt\vbox{\vbox{}\hbox{\hskip-90.73521pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta_{1},\Delta_{2}\vdash(\mathbf{\nu}x)z\langle
y\rangle.(P\mid Q)::z{:}A\otimes B}$}}}}}}$}}\hbox{}$}\quad\raise
11.0pt\hbox{$\hbox{$\hbox{\small\sc$({{\otimes}\mathsf{L}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
67.34296pt\vbox{\hbox{\hskip-67.34296pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta,y{:}A,x{:}B\vdash
P::z{:}C}$}}}\vbox{}}}\over\hbox{\hskip
76.03397pt\vbox{\vbox{}\hbox{\hskip-76.03395pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta,x{:}A\otimes
B\vdash x(y).P::z{:}C}$}}}}}}$}}\hbox{}$}\\\\[10.00002pt] \raise
11.0pt\hbox{$\hbox{$\hbox{\small\sc$({{\with}\mathsf{R}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
87.54617pt\vbox{\hbox{\hskip-87.54617pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta\vdash
P::z{:}A\quad\Omega;\Gamma;\Delta\vdash
Q::z{:}B}$}}}\vbox{}}}\over\hbox{\hskip
72.03941pt\vbox{\vbox{}\hbox{\hskip-72.03941pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta\vdash
z.\mathsf{case}(P,Q)::z{:}A\with B}$}}}}}}$}}\hbox{}$}\quad\raise
10.44444pt\hbox{$\hbox{$\hbox{\small\sc$({{\with}\mathsf{L}}_{1})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
54.27995pt\vbox{\hbox{\hskip-54.27994pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta,x{:}A\vdash
P::z{:}C}$}}}\vbox{}}}\over\hbox{\hskip
74.88237pt\vbox{\vbox{}\hbox{\hskip-74.88237pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta,x{:}A\with
B\vdash x.\mathsf{inl};P::z{:}C}$}}}}}}$}}\hbox{}$}\\\\[10.00002pt] \raise
10.44444pt\hbox{$\hbox{$\hbox{\small\sc$({{\with}\mathsf{L}}_{2})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
54.27995pt\vbox{\hbox{\hskip-54.27994pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta,x{:}A\vdash
P::z{:}C}$}}}\vbox{}}}\over\hbox{\hskip
75.45181pt\vbox{\vbox{}\hbox{\hskip-75.45181pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta,x{:}A\with
B\vdash x.\mathsf{inr};P::z{:}C}$}}}}}}$}}\hbox{}$}\quad\raise
10.44444pt\hbox{$\hbox{$\hbox{\small\sc$({{\oplus}\mathsf{R}}_{1})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
39.71341pt\vbox{\hbox{\hskip-39.7134pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta\vdash
P::z{:}A}$}}}\vbox{}}}\over\hbox{\hskip
62.96855pt\vbox{\vbox{}\hbox{\hskip-62.96855pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta\vdash
z.\mathsf{inl};P::z{:}A\oplus B}$}}}}}}$}}\hbox{}$}\\\\[10.00002pt] \raise
10.44444pt\hbox{$\hbox{$\hbox{\small\sc$({{\oplus}\mathsf{R}}_{2})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
41.39566pt\vbox{\hbox{\hskip-41.39565pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta\vdash
P::z{:}B}$}}}\vbox{}}}\over\hbox{\hskip
63.538pt\vbox{\vbox{}\hbox{\hskip-63.538pt\hbox{\hbox{$\displaystyle\displaystyle{\Omega;\Gamma;\Delta\vdash
z.\mathsf{inr};P::z{:}A\oplus B}$}}}}}}$}}\hbox{}$}\quad\raise
11.0pt\hbox{$\hbox{$\hbox{\small\sc$({{\oplus}\mathsf{L}})$}\,$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip