---
abstract: 'Recently, Wadler presented a continuation-passing translation from a session-typed functional language, GV, to a process calculus based on classical linear logic, CP. However, this translation is one-way: CP is more expressive than GV. We propose an extension of GV, called [HGV]{}, and give translations showing that it is as expressive as CP. The new translations shed light both on the original translation from GV to CP, and on the limitations in expressiveness of GV.'
author:
- 'Sam Lindley J. Garrett Morris'
bibliography:
- 'cpgv.bib'
title: Sessions as Propositions
---

Introduction {#sect:introduction}
============

Linear logic has long been regarded as a potential typing discipline for concurrency. Girard [@Girard87] observes that the connectives of linear logic can be interpreted as parallel computation. Abramsky [@Abramsky92] and Bellin and Scott [@BellinScott94] interpret linear logic proofs as $\pi$-calculus processes. While they provide $\pi$-calculus interpretations of all linear logic proofs, they do not provide a proof-theoretic interpretation for arbitrary $\pi$-calculus terms. Caires and Pfenning [@CairesPfenning10] give a propositions-as-types correspondence between intuitionistic linear logic and session types, interpreting linear logic propositions as session types for a restricted $\pi$-calculus, $\pi$DILL. Of particular importance to this work, they interpret the multiplicative connectives as prefixing, and the exponentials as replicated processes.

Wadler [@Wadler12] adapts Caires and Pfenning’s work to classical linear logic, interpreting proofs as processes in a restricted $\pi$-calculus, CP. Additionally, Wadler shows that a core session-typed linear functional language, GV, patterned after a similar language due to Gay and Vasconcelos [@GayVasconcelos10], may be translated into CP. However, GV is less expressive than CP: there are proofs which do not correspond to any GV program.

Our primary contribution is [HGV]{}(Harmonious GV), a version of GV extended with constructs for session forwarding, replication, and polymorphism. We identify [HGV$\pi$]{}, the session-typed fragment of [HGV]{}, and give a type-preserving translation from [HGV]{}to [HGV$\pi$]{}(${({-})^\star}$); this translation depends crucially on the new constructs of [HGV]{}. We show that [HGV]{}is sufficient to express all linear logic proofs by giving type-preserving translations from [HGV$\pi$]{}to CP (${\llbracket{-}\rrbracket}$), and from CP to [HGV$\pi$]{}(${\llparenthesis{-}\rrparenthesis}$). Factoring the translation of [HGV]{}into CP through ${({-})^\star}$ simplifies the presentation, and illuminates regularities that are not apparent in Wadler’s original translation of GV into CP. Finally, we show that [HGV]{}, [HGV$\pi$]{}, and CP are all equally expressive.

The [HGV]{}Language {#sect:hgv}
===================

This section describes our session-typed language [HGV]{}, contrasting it with Gay and Vasconcelos’s functional language for asynchronous session types [@GayVasconcelos10], which we call [LAST]{}, and Wadler’s GV [@Wadler12]. In designing [HGV]{}, we have opted for programming convenience over uniformity, while insisting on a tight correspondence with linear logic. The session types of [HGV]{}are given by the following grammar:

S & ::= & [.[S]{}]{} [.[S]{}]{} [[end]{}\_!]{}[[end]{}\_?]{} X [\[[X]{}\].[S]{}]{} [\[[X]{}\].[S]{}]{}

Types for input (${\mathord{?}{T}.{S}}$), output (${\mathord{!}{T}.{S}}$), selection (${\oplus {{\{ {l}_i:S_i \}}_{i}}}$) and choice (${\binampersand {{\{ {l}_i:S_i \}}_{i}}}$) are standard. Like GV, but unlike [LAST]{}, we distinguish output (${{\mathsf}{end}_!}$) and input (${{\mathsf}{end}_?}$) session ends; this matches the situation in linear logic, where there is no conveniently self-dual proposition to represent the end of a session. Variables and their duals ($X,{\overline{X}}$) and type input (${\mathord{?}[{X}].{S}}$) and output (${\mathord{!}[{X}].{S}}$), permit definition of polymorphic sessions. We include a notion of replicated sessions, corresponding to exponentials in linear logic: a channel of type ${\sharp {S}}$ is a “service”, providing any number of channels of type $S$; a channel of type ${\flat {S}}$ is the “server” providing such a service. Each session type $S$ has a dual ${\overline{S}}$ (with the obvious dual for variables $X$): $${{\begin{array}}{@{}c@{}}}{\overline{{\mathord{!}{T}.{S}}}} = {\mathord{?}{T}.{{\overline{S}}}}
\qquad
  {\overline{{\oplus {{\{ {l}_i:S_i \}}_{i}}}}} = {\binampersand {{\{ {l}_i:{\overline{S_i}} \}}_{i}}}
\qquad
  {\overline{{{\mathsf}{end}_!}}} = {{\mathsf}{end}_?}\qquad
  {\overline{{\mathord{!}[{X}].{S}}}} = {\mathord{?}[{X}].{{\overline{S}}}}
\qquad
  {\overline{{\sharp {S}}}} = {\flat {{\overline{S}}}}
\\
  {\overline{{\mathord{?}{T}.{S}}}} = {\mathord{!}{T}.{{\overline{S}}}}
\qquad
  {\overline{{\binampersand {{\{ {l}_i:S_i \}}_{i}}}}} = {\oplus {{\{ {l}_i:{\overline{S_i}} \}}_{i}}}
\qquad
  {\overline{{{\mathsf}{end}_?}}} = {{\mathsf}{end}_!}\qquad
  {\overline{{\mathord{?}[{X}].{S}}}} = {\mathord{!}[{X}].{{\overline{S}}}}
\qquad
  {\overline{{\flat {S}}}} = {\sharp {{\overline{S}}}}
\\
{{\end{array}}}$$ Note that dualisation leaves input and output types unchanged. In addition to sessions, [HGV]{}’s types include linear pairs, and linear and unlimited functions: $$T,U,V ::= S \mid {{T} \otimes {U}} \mid {{T} {\multimap}{U}} \mid {{T} \to {U}}$$ Every type $T$ is either linear (${\mathit{lin}(T)}$) or unlimited (${\mathit{un}(T)}$); the only unlimited types are services (${\mathit{un}({\sharp {S}})}$), unlimited functions (${\mathit{un}({{T} \to {U}})}$), and end input session types (${\mathit{un}({{\mathsf}{end}_?})}$). In GV, ${{\mathsf}{end}_?}$ is linear. We choose to make it unlimited in [HGV]{}because then we can dispense with GV’s explicit ${\mathsf}{terminate}$ construct while maintaining a strong correspondence with CP—${{\mathsf}{end}_?}$ corresponds to ${\bot}$ in CP, for which weakening and contraction are derivable.

Structural rules

Lambda rules

Session rules

\

\

Figure \[fig:hgv-typing\] gives the terms and typing rules for [HGV]{}; the first block contains the structural rules, the second contains the (standard) rules for lambda terms, and the third contains the session-typed fragment. The ${\mathsf}{fork}$ construct provides session initiation, filling the role of GV’s ${\mathsf}{with}\dots{\mathsf}{connect}\dots{\mathsf}{to}\dots$ structure, but without the asymmetry of the latter. The two are interdefinable, as follows: $${{\mathsf}{fork}~{x}.{M}} \equiv {{\mathsf}{with}~{x}~{\mathsf}{connect}~{M}~{\mathsf}{to}~{x}} \qquad {{\mathsf}{with}~{x}~{\mathsf}{connect}~{M}~{\mathsf}{to}~{N}} \equiv {{\mathsf}{let}~{x}={{{\mathsf}{fork}~{x}.{M}}}~{\mathsf}{in}~{N}}$$ We add a construct ${{\mathsf}{link}~{M}~{N}}$ to implement channel forwarding; this form is provided in neither GV nor [LAST]{}, but is necessary to match the expressive power of CP. (Note that while we could define session forwarding in GV or LAST for any particular session type, it is not possible to do so in a generic fashion.) We add terms ${{\mathsf}{sendType}~{S}~{M}}$ and ${{\mathsf}{receiveType}~{X}.{M}}$ to provide session polymorphism, and ${{\mathsf}{serve}~{x}.{M}}$ and ${{\mathsf}{request}~{M}}$ for replicated sessions. Note that, as the body $M$ of ${{\mathsf}{serve}~{x}.{M}}$ may be arbitrarily replicated, it can only refer to the unlimited portion of the environment. Channels of type ${\sharp {S}}$ offer arbitrarily many sessions of type $S$; correspondingly, channels of type ${\flat {S}}$ must consume arbitrarily many $S$ sessions. The rule for ${{\mathsf}{serve}~{x}.{M}}$ parallels that for ${\mathsf}{fork}$: it defines the server (which replicates $M$) and returns the channel by which it may be used (of type ${\overline{{\flat {S}}}} =
{\sharp {{\overline{S}}}}$). As a consequence, there is no rule involving type ${\flat {S}}$. We experimented with having such a rule, but found that it was always used immediately inside a ${\mathsf}{fork}$, while providing no extra expressive power. Hence we opted for the rule presented here.

From [HGV]{}to [HGV$\pi$]{} {#sect:hgv-to-hgvpi}
===========================

The language [HGV$\pi$]{}is the restriction of [HGV]{}to session types, that is, [HGV]{}without ${\multimap}$, $\to$, or $\otimes$. In order to avoid $\otimes$, we disallow plain ${{\mathsf}{receive}~{M}}$, but do permit it to be fused with a pair elimination ${{{\mathsf}{let}~{{({x},{y})}}={{{\mathsf}{receive}~{M}}}~{\mathsf}{in}~{N}}}$. We can simulate all non-session types as session types via a translation from [HGV]{}to [HGV$\pi$]{}. The translation on types is given by the homomorphic extension of the following equations: $${({{{T} {\multimap}{U}}})^\star} = {\mathord{!}{{({T})^\star}}.{{({U})^\star}}} \qquad
{({{{T} \to {U}}})^\star} = {\sharp {({\mathord{!}{{({T})^\star}}.{{({U})^\star}}})}} \qquad
{({{{T} \otimes {U}}})^\star} = {\mathord{?}{{({T})^\star}}.{{({U})^\star}}}$$Each target type is the *interface* to the simulated source type. A linear function is simulated by input on a channel; its interface is output on the other end of the channel. An unlimited function is simulated by a server; its interface is the service on the other end of that channel. A tensor is simulated by output on a channel; its interface is input on the other end of that channel. This duality between implementation and interface explains the flipping of types in Wadler’s original CPS translation from GV to CP. The translation on terms is given by the homomorphic extension of the following equations:

[([[.[M]{}]{}]{})\^]{} &=& [[fork]{} [z]{}.[[[let]{} [[([x]{},[z]{})]{}]{}=[[[receive]{} [z]{}]{}]{} [in]{} [[[link]{} [[([M]{})\^]{}]{} [z]{}]{}]{}]{}]{}]{}\
[([[[L]{} [M]{}]{}]{})\^]{} &=& [[send]{} [[([M]{})\^]{}]{} [[([L]{})\^]{}]{}]{}\
[([M,N]{})\^]{} &=& [[fork]{} [z]{}.[[[link]{} [([[send]{} [[([M]{})\^]{}]{} [z]{}]{})]{} [[([N]{})\^]{}]{}]{}]{}]{}\
[([[[let]{} [[([x]{},[y]{})]{}]{}=[M]{} [in]{} [N]{}]{}]{})\^]{} &=& [[let]{} [[([x]{},[y]{})]{}]{}=[[[receive]{} [[([M]{})\^]{}]{}]{}]{} [in]{} [[([N]{})\^]{}]{}]{}\
[([L : [[T]{} ]{}]{})\^]{} &=& [[serve]{} [z]{}.[[[link]{} [[([L]{})\^]{}]{} [z]{}]{}]{}]{}\
[([L : [[T]{} [U]{}]{}]{})\^]{} &=& [[request]{} [[([L]{})\^]{}]{}]{}\
[([[[receive]{} [M]{}]{}]{})\^]{} &=& [([M]{})\^]{}\

Formally, this is a translation on derivations. We write type annotations to indicate $\to$ introduction and elimination. For all other cases, it is unambiguous to give the translation on plain term syntax. Each introduction form translates to an interface ${{\mathsf}{fork}~{z}.{M}}$ of type ${\overline{S}}$, where $M : {{\mathsf}{end}_!}$ provides the implementation, with $z : S$ bound in $M$. We can extend the translation on types to a translation on contexts:

[([x\_1:T\_1, …, x\_n:T\_n]{})\^]{} &=& x\_1:[([T\_1]{})\^]{}, …, x\_n:[([T\_n]{})\^]{}\

It is straightforward to verify that our translation preserves typing.

If ${{\Phi} \vdash {M} : {T}}$ then ${{{({\Phi})^\star}} \vdash {{({M})^\star}} : {{({T})^\star}}}$.

From [HGV$\pi$]{}to CP {#sect:hgvpi-to-cp}
======================

We present the typing rules of CP in Figure \[fig:cp-typing\]. Note that the propositions of CP are exactly those of classical linear logic, as are the cut rules (if we ignore the terms). Thus, CP enjoys all of the standard meta theoretic properties of classical linear logic, including confluence and weak normalisation. A minor syntactic difference between our presentation and Wadler’s is that our sum ($\oplus$) and choice ($\binampersand$) types are $n$-ary, matching the corresponding session types in [HGV]{}, whereas he presents binary and nullary versions of sum and choice. Duality on CP types (${{(-)}^\bot}$) is standard: $${{\begin{array}}{@{}c@{}}}{{({{A} \otimes {B}})}^\bot} \!=\! {{{{A}^\bot}} \mathbin{\bindnasrepma} {{{B}^\bot}}}
~~
  {{({\oplus {{\{ {l}_i:A_i \}}_{i}}})}^\bot} \!=\! {\binampersand {{\{ {l}_i:{{A_i}^\bot} \}}_{i}}}
~~
  {{{1}}^\bot} \!=\! {\bot}~~
  {{({\exists {X}.{B}})}^\bot} \!=\! {\forall {X}.{{{B}^\bot}}}
~~
  {{({\mathord{!}{A}})}^\bot} \!=\! {\mathord{?}{{{A}^\bot}}}
\\
  {{({{A} \mathbin{\bindnasrepma} {B}})}^\bot} \!=\! {{{{A}^\bot}} \otimes {{{B}^\bot}}}
~~
  {{({\binampersand {{\{ {l}_i:A_i \}}_{i}}})}^\bot} \!=\! {\oplus {{\{ {l}_i:{{A_i}^\bot} \}}_{i}}}
~~
  {{{\bot}}^\bot} \!=\! {1}~~
  {{({\forall {X}.{B}})}^\bot} \!=\! {\exists {X}.{{{B}^\bot}}}
~~
  {{({\mathord{?}{A}})}^\bot} \!=\! {\mathord{!}{{{A}^\bot}}}
\\
{{\end{array}}}$$

The semantics of CP terms follows the cut elimination rules in classical linear logic. We interpret the cut relation ${\longrightarrow}$ modulo $\alpha$-equivalence and structural cut equivalence:

[[x]{} ]{} && [[y]{} ]{}\
[.([P]{} )]{} && [.([Q]{} )]{}\
[.([[.([P]{} )]{}]{} )]{} && [.([P]{} )]{}\

The principal cut elimination rules correspond to communication between processes.

[.([[[w]{} ]{}]{} )]{} && [[P]{}\[[w]{}/[x]{}\]]{}\
[.([[[x]{}\[[y]{}\].([P]{} )]{}]{} )]{} && [.([P]{} )]{}\
[.([[[x]{}\[[[l]{}\_j]{}\].[P]{}]{}]{} )]{} && [.([P]{} )]{}\
[.([[![x]{}([y]{}).[P]{}]{}]{} )]{} && [.([P]{} )]{}\
[.([[![x]{}([y]{}).[P]{}]{}]{} )]{} && Q, x [(Q)]{}\
[.([[![x]{}([y]{}).[P]{}]{}]{} )]{} && [.([[![x]{}([y]{}).[P]{}]{}]{} )]{}\
[.([[[x]{}\[[A]{}\].[P]{}]{}]{} )]{} && [.([P]{} )]{}\
[.([[[x]{}\[\].0]{}]{} )]{} && P\

Finally, we provide commuting conversions, moving communication under unrelated prefixes.

[.([[[x]{}\[[y]{}\].([P]{} )]{}]{} )]{} && [[x]{}\[[y]{}\].([[.([P]{} )]{}]{} )]{}, z [(P)]{}\
[.([[[x]{}\[[y]{}\].([P]{} )]{}]{} )]{} && [[x]{}\[[y]{}\].([P]{} )]{}, z [(Q)]{}\
[.([[[x]{}([y]{}).[P]{}]{}]{} )]{} && [[x]{}([y]{}).[[.([P]{} )]{}]{}]{}\
[.([[[x]{}\[[[l]{}]{}\].[P]{}]{}]{} )]{} && [[x]{}\[[[l]{}]{}\].[[.([P]{} )]{}]{}]{}\
[.([[[x]{}.[case]{} [[[{ [l]{}\_i.Q\_i }]{}\_[i]{}]{}]{}]{}]{} )]{} && [[x]{}.[case]{} [[[{ [l]{}\_i.[.([Q\_i]{} )]{} }]{}\_[i]{}]{}]{}]{}\
[.([[![x]{}([y]{}).[P]{}]{}]{} )]{} && [![x]{}([y]{}).[[.([P]{} )]{}]{}]{}\
[.([[?[x]{}\[[y]{}\].[P]{}]{}]{} )]{} && [?[x]{}\[[y]{}\].[[.([P]{} )]{}]{}]{}\
[.([[[x]{}\[[A]{}\].[P]{}]{}]{} )]{} && [[x]{}\[[A]{}\].[[.([P]{} )]{}]{}]{}\
[.([[[x]{}([X]{}).[P]{}]{}]{} )]{} && [[x]{}([X]{}).[[.([P]{} )]{}]{}]{}\
[.([[[x]{}().[P]{}]{}]{} )]{} && [[x]{}().[[.([P]{} )]{}]{}]{}\

A fuller account of CP can be found in Wadler’s work [@Wadler12].

We now give a translation from [HGV$\pi$]{}to CP. Post composing this with the embedding of [HGV]{}in [HGV$\pi$]{}yields a semantics for [HGV]{}. The translation on session types is as follows: $${\begin{array}}{@{}c@{\qquad}c@{\qquad}c@{\qquad}c@{}}
{\begin{array}}{@{}r@{~}c@{~}l@{}}
{\llbracket{{\mathord{!}{T}.{S}}}\rrbracket}         &=& {{{{{\llbracket{T}\rrbracket}}^\bot}} \otimes {{\llbracket{S}\rrbracket}}} \\
{\llbracket{{\mathord{?}{T}.{S}}}\rrbracket}          &=& {{{\llbracket{T}\rrbracket}} \mathbin{\bindnasrepma} {{\llbracket{S}\rrbracket}}} \\
{\llbracket{{{\mathsf}{end}_!}}\rrbracket}  &=& {1}\\
{\end{array}}&
{\begin{array}}{@{}r@{~}c@{~}l@{}}
{\llbracket{{\oplus {{\{ {l}_i:S_i \}}_{i}}}}\rrbracket}   &=& {\oplus {{\{ {l}_i:{\llbracket{S_i}\rrbracket} \}}_{i}}} \\
{\llbracket{{\binampersand {{\{ {l}_i:S_i \}}_{i}}}}\rrbracket} &=& {\binampersand {{\{ {l}_i:{\llbracket{S_i}\rrbracket} \}}_{i}}} \\
{\llbracket{{{\mathsf}{end}_?}}\rrbracket}   &=& {\bot}\\
{\end{array}}&
{\begin{array}}{@{}r@{~}c@{~}l@{}}
{\llbracket{{\flat {S}}}\rrbracket}  &=& {\mathord{!}{{\llbracket{S}\rrbracket}}} \\
{\llbracket{{\sharp {S}}}\rrbracket} &=& {\mathord{?}{{\llbracket{S}\rrbracket}}} \\
{\llbracket{X}\rrbracket}                   &=& X \\
{\end{array}}&
{\begin{array}}{@{}r@{~}c@{~}l@{}}
{\llbracket{{\mathord{!}[{X}].{S}}}\rrbracket} &=& {\exists {X}.{{\llbracket{S}\rrbracket}}} \\
{\llbracket{{\mathord{?}[{X}].{S}}}\rrbracket}  &=& {\forall {X}.{{\llbracket{S}\rrbracket}}} \\
{\llbracket{{\overline{X}}}\rrbracket}          &=& {{X}^\bot} \\
{\end{array}}{\end{array}}$$ The translation is homomorphic except for output, where the output type is dualised. This accounts for the discrepancy between ${\overline{{\mathord{!}{T}.{S}}}} = {\mathord{?}{T}.{{\overline{S}}}}$ and ${{({{A} \otimes {B}})}^\bot} = {{{{A}^\bot}} \mathbin{\bindnasrepma} {{{B}^\bot}}}$.

The translation on terms is formally specified as a CPS translation on derivations as in Wadler’s presentation. We provide the full translations of weakening and contraction for ${{\mathsf}{end}_?}$, as these steps are implicit in the syntax of [HGV]{}terms. The other constructs depend only on the immediate syntactic structure, so we abbreviate their translations as mappings on plain terms:

z &=&\
z &=&\
z &=& z\
z &=& [.([[[x]{}\[[y]{}\].([y]{} )]{}]{} )]{}\
z &=& [.([y]{} )]{}\
z &=& [.([x]{} )]{}\
z &=& [.([x]{} )]{}\
z &=& [.([[.([y]{} )]{}]{} )]{}\
z &=& [[z]{}().[[.([x]{} )]{}]{}]{}\
z &=& [.([x]{} )]{}\
z &=& [.([x]{} )]{}\
z &=& [![z]{}([y]{}).[[.([x]{} )]{}]{}]{}\
z &=& [.([x]{} )]{}\

Channel $z$ provides a continuation, consuming the output of the process representing the original [HGV$\pi$]{}term. The translation on contexts is pointwise.

&=& x\_1:, …, x\_n:\

As with the translation from [HGV]{}to [HGV$\pi$]{}, we can show that this translation preserves typing.

If ${{\Phi} \vdash {M} : {S}}$ then ${{{\llbracket{M}\rrbracket}z} \vdash {{\llbracket{\Phi}\rrbracket},z:{{{\llbracket{S}\rrbracket}}^\bot}}}$.

From CP to [HGV$\pi$]{} {#sect:cp-to-hgvpi}
=======================

We now present the translation ${\llparenthesis{-}\rrparenthesis}$ from CP to [HGV$\pi$]{}. The translation on types is as follows: $${\begin{array}}{@{}c@{\qquad}c@{\qquad}c@{\qquad}c@{}}
{\begin{array}}{@{}r@{~}c@{~}l@{}}
{\llparenthesis{{{A} \otimes {B}}}\rrparenthesis} &=& {\mathord{!}{{\overline{{\llparenthesis{A}\rrparenthesis}}}}.{{\llparenthesis{B}\rrparenthesis}}} \\
{\llparenthesis{{{A} \mathbin{\bindnasrepma} {B}}}\rrparenthesis}   &=& {\mathord{?}{{\llparenthesis{A}\rrparenthesis}}.{{\llparenthesis{B}\rrparenthesis}}} \\
{\llparenthesis{{1}}\rrparenthesis}         &=& {{\mathsf}{end}_!}\\
{\end{array}}&
{\begin{array}}{@{}r@{~}c@{~}l@{}}
{\llparenthesis{{\oplus {{\{ {l}_i:A_i \}}_{i}}}}\rrparenthesis} &=& {\oplus {{\{ {l}_i:{\llparenthesis{A_i}\rrparenthesis} \}}_{i}}}  \\
{\llparenthesis{{\binampersand {{\{ {l}_i:A_i \}}_{i}}}}\rrparenthesis} &=& {\binampersand {{\{ {l}_i:{\llparenthesis{A_i}\rrparenthesis} \}}_{i}}} \\
{\llparenthesis{{\bot}}\rrparenthesis}      &=& {{\mathsf}{end}_?}\\
{\end{array}}&
{\begin{array}}{@{}r@{~}c@{~}l@{}}
{\llparenthesis{{\exists {X}.{A}}}\rrparenthesis} &=& {\mathord{!}[{X}].{{\llparenthesis{A}\rrparenthesis}}} \\
{\llparenthesis{{\forall {X}.{A}}}\rrparenthesis} &=& {\mathord{?}[{X}].{{\llparenthesis{A}\rrparenthesis}}} \\
{\llparenthesis{X}\rrparenthesis}               &=& X \\
{\end{array}}&
{\begin{array}}{@{}r@{~}c@{~}l@{}}
{\llparenthesis{{\mathord{?}{A}}}\rrparenthesis}    &=& {\sharp {{\llparenthesis{A}\rrparenthesis}}} \\
{\llparenthesis{{\mathord{!}{A}}}\rrparenthesis}  &=& {\flat {{\llparenthesis{A}\rrparenthesis}}} \\
{\llparenthesis{{{X}^\bot}}\rrparenthesis}      &=& {\overline{X}} \\
{\end{array}}{\end{array}}$$ The translation on terms makes use of ${\mathsf}{let}$ expressions to simplify the presentation; these are expanded to [HGV$\pi$]{}as follows: $${{\mathsf}{let}~{x}={M}~{\mathsf}{in}~{N}} \equiv {({(\lambda x.N) M})^\star} \equiv {{\mathsf}{send}~{M}~{({{\mathsf}{fork}~{z}.{{{{\mathsf}{let}~{{({x},{z})}}={{{\mathsf}{receive}~{z}}}~{\mathsf}{in}~{{{\mathsf}{link}~{N}~{z}}}}}}})}}.$$ $${\begin{array}}{@{}r@{~}c@{~}l@{}}
  {\llparenthesis{{{x}[{y}].({P} \mid {Q})}}\rrparenthesis} &=&
  {{\mathsf}{let}~{x}={{{\mathsf}{send}~{({{\mathsf}{fork}~{y}.{{\llparenthesis{P}\rrparenthesis}}})}~{x}}}~{\mathsf}{in}~{{\llparenthesis{Q}\rrparenthesis}}} \\
{\llparenthesis{{{x}({y}).{P}}}\rrparenthesis} &=&
  {{\mathsf}{let}~{{({y},{x})}}={{{\mathsf}{receive}~{x}}}~{\mathsf}{in}~{{\llparenthesis{P}\rrparenthesis}}} \\
{\llparenthesis{{{x}[{{l}}].{P}}}\rrparenthesis} &=&
  {{\mathsf}{let}~{x}={{{\mathsf}{select}~{{l}}~{x}}}~{\mathsf}{in}~{{\llparenthesis{P}\rrparenthesis}}} \\
{\llparenthesis{{{x}.{\mathsf}{case}~{{{\{ {l}_i.P_i \}}_{i}}}}}\rrparenthesis} &=&
  {{\mathsf}{case}~{x}~{\mathsf}{of}~{{{\{ {l}_i(x).{\llparenthesis{P_i}\rrparenthesis} \}}_{i}}}} \\
{\llparenthesis{{{x}[].0}}\rrparenthesis} &=& x \\
{\llparenthesis{{{x}().{P}}}\rrparenthesis} &=& {\llparenthesis{P}\rrparenthesis} \\
{\llparenthesis{{\nu {x}.({P} \mid {Q})}}\rrparenthesis} &=&
  {{\mathsf}{let}~{x}={{{\mathsf}{fork}~{x}.{{\llparenthesis{P}\rrparenthesis}}}}~{\mathsf}{in}~{{\llparenthesis{Q}\rrparenthesis}}} \\
{\llparenthesis{{{x} \leftrightarrow {y}}}\rrparenthesis} &=& {{\mathsf}{link}~{x}~{y}} \\

{\llparenthesis{{{x}[{A}].{P}}}\rrparenthesis} &=&
  {{\mathsf}{let}~{x}={{{\mathsf}{sendType}~{{\llparenthesis{A}\rrparenthesis}}~{x}}}~{\mathsf}{in}~{{\llparenthesis{P}\rrparenthesis}}} \\
{\llparenthesis{{{x}({X}).{P}}}\rrparenthesis} &=&
  {{\mathsf}{let}~{x}={{{\mathsf}{receiveType}~{X}.{x}}}~{\mathsf}{in}~{{\llparenthesis{P}\rrparenthesis}}} \\

{\llparenthesis{{!{s}({x}).{P}}}\rrparenthesis} &=&
  {{\mathsf}{link}~{s}~{({{\mathsf}{serve}~{x}.{{\llparenthesis{P}\rrparenthesis}}})}} \\
{\llparenthesis{{?{s}[{x}].{P}}}\rrparenthesis} &=&
  {{\mathsf}{let}~{x}={{{\mathsf}{request}~{s}}}~{\mathsf}{in}~{{\llparenthesis{P}\rrparenthesis}}} \\
{\end{array}}$$ Again, we can extend the translation on types to a translation on contexts, and show that the translation preserves typing.

If ${{P} \vdash {{\Gamma}}}$ then ${{{\llparenthesis{{\Gamma}}\rrparenthesis}} \vdash {{\llparenthesis{P}\rrparenthesis}} : {{{\mathsf}{end}_!}}}$.

Correctness {#sect:correctness}
===========

If we extend ${\llbracket{-}\rrbracket}$ to non-session types, as in Wadler’s original presentation (Figure \[fig:hgvcp-ext\]), then it is straightforward to show that this monolithic translation factors through ${({-})^\star}$.

\[th:factor\] ${\llbracket{{({M})^\star}}\rrbracket}z {\longrightarrow}^* {\llbracket{M}\rrbracket}z$ (where ${\longrightarrow}^*$ is the reflexive transitive closure of $\equiv{\longrightarrow}\equiv$).

The key soundness property of our translations is that if we translate a term from CP to [HGV$\pi$]{}and back, then we obtain a term equivalent to the one we started with.

\[th:soundness\] If ${{P} \vdash {{\Gamma}}}$ then ${\nu {z}.({{{z}[].0}} \mid {{\llbracket{{\llparenthesis{P}\rrparenthesis}}\rrbracket}z})} {\longrightarrow}^* P$.

Together, Theorem \[th:factor\] and \[th:soundness\] tell us that [HGV]{}, [HGV$\pi$]{}, and CP are equally expressive, in the sense that every $X$ program can always be translated to an equivalent $Y$ program, where $X,Y \in \{$[HGV]{}, [HGV$\pi$]{}, CP$\}$.

Here our notion of expressivity is agnostic to the nature of the translations. It is instructive also to consider Felleisen’s more refined notion of expressivity [@Felleisen91]. Both ${({-})^\star}$ and ${\llparenthesis{-}\rrparenthesis}$ are local translations, thus both [HGV]{}and CP are *macro-expressible* [@Felleisen91] in [HGV$\pi$]{}. However, the need for a global CPS translation from [HGV$\pi$]{}to CP illustrates that [HGV$\pi$]{}is not macro-expressible in CP; hence [HGV$\pi$]{}is more expressive, in the Felleisen sense, than CP.

$${\begin{array}}{@{}cc@{}}
{\begin{array}}{@{}r@{~}c@{~}l@{}}
\multicolumn{3}{@{}l@{}}{\textbf{Types}} \\
\multicolumn{3}{@{}l@{}}{{\llbracket{T}\rrbracket} = {{{\llceil{T}\rrceil}}^\bot}, T \text{ not a session type}} \\
\multicolumn{3}{@{}l@{}}{\text{where}} \\
\quad{\llceil{{{T} {\multimap}{U}}}\rrceil} &=& {{{{{\llceil{T}\rrceil}}^\bot}} \mathbin{\bindnasrepma} {{\llceil{U}\rrceil}}} \\
\quad{\llceil{{{T} \to {U}}}\rrceil} &=& {\mathord{!}{({{{{{\llceil{T}\rrceil}}^\bot}} \mathbin{\bindnasrepma} {{\llceil{U}\rrceil}}})}} \\
\quad{\llceil{{{T} \otimes {U}}}\rrceil} &=& {{{\llceil{T}\rrceil}} \otimes {{\llceil{U}\rrceil}}} \\
\quad{\llceil{S}\rrceil} &=& {\llbracket{S}\rrbracket} \\
{\end{array}}&
{\begin{array}}{@{}r@{~}c@{~}l@{}}
\multicolumn{3}{@{}l@{}}{\textbf{Terms}} \\
{\llbracket{{\lambda {x}.{N}}}\rrbracket}z &=& {{z}({x}).{{\llbracket{N}\rrbracket}z}} \\
{\llbracket{{{L}~{M}}}\rrbracket}z &=& {\nu {y}.({{\llbracket{L}\rrbracket}y} \mid {{{y}[{x}].({{\llbracket{M}\rrbracket}x} \mid {{{y} \leftrightarrow {z}}})}})} \\
{\llbracket{L : {{T} \to {U}}}\rrbracket}z &=& {!{z}({y}).{{\llbracket{L}\rrbracket}y}} \\
{\llbracket{L : {{T} {\multimap}{U}}}\rrbracket}z &=& {\nu {y}.({{\llbracket{L}\rrbracket}y} \mid {{?{y}[{x}].{{{x} \leftrightarrow {z}}}}})} \\
{\llbracket{{({M},{N})}}\rrbracket}z &=& {{z}[{y}].({{\llbracket{M}\rrbracket}y} \mid {{\llbracket{N}\rrbracket}z})} \\
{\llbracket{{{\mathsf}{let}~{{({x},{y})}}={M}~{\mathsf}{in}~{N}}}\rrbracket}z
  &=& {\nu {y}.({{\llbracket{M}\rrbracket}y} \mid {{{y}({x}).{{\llbracket{N}\rrbracket}z}}})} \\
{\end{array}}{\end{array}}$$

Conclusions and Future Work {#sect:conclusion}
===========================

We have proposed a session-typed functional language, [HGV]{}, building on similar languages of Wadler [@Wadler12] and of Gay and Vasconcelos [@GayVasconcelos10]. We have shown that [HGV]{}is sufficient to encode arbitrary linear logic proofs, completing the correspondence between linear logic and session types. We have also given an embedding of all of [HGV]{}into its session-typed fragment, simplifying translation from [HGV]{}to CP.

Dardha et al [@DardhaGS12] offers an alternative foundation for session types through a CPS translation of $\pi$-calculus with session types into a linear $\pi$-calculus. There appear to be strong similarities between their CPS translation and ours. We would like to make the correspondence precise by studying translations between their systems and ours.

In addition we highlight several other areas of future work. First, the semantics of [HGV]{}is given only by cut elimination in CP. We would like to give [HGV]{}a semantics directly, in terms of reductions of configurations of processes, and then prove a formal correspondence with cut elimination in CP. Second, replication has limited expressive power compared to recursion; in particular, it cannot express services whose behaviour changes over time or in response to client requests. We believe that the study of fixed points in linear logic provides a mechanism to support more expressive recursive behaviour without sacrificing the logical interpretation of [HGV]{}. Finally, as classical linear logic proofs, and hence CP processes, enjoy confluence, [HGV]{}programs are deterministic. We hope to identify natural extensions of [HGV]{}that give rise to non-determinism, and thus allow programs to exhibit more interesting concurrent behaviour, while preserving the underlying connection to linear logic.

#### Acknowledgements

We would like to thank Philip Wadler for his suggestions on the direction of this work, and for his helpful feedback on the results. This work was funded by EPSRC grant number EP/K034413/1.

\[sect:bib\]
