# An Output-Based Semantics of Λμ with Explicit Substitution in the π-Calculus

Steffen Van Bakel, Maria Grazia Vigliotti

<figure><img src="image_1.png" /></figure>

## ► To cite this version:

Steffen Van Bakel, Maria Grazia Vigliotti. An Output-Based Semantics of Λμ with Explicit Substitution in the π-Calculus. 7th International Conference on Theoretical Computer Science (TCS), Sep 2012, Amsterdam, Netherlands. pp.372-387, 10.1007/978-3-642-33475-7_26 . hal-01556215

HAL Id: hal-01556215

https://inria.hal.science/hal-01556215

Submitted on 4 Jul 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>
# An output-based semantics of Λμ
with explicit substitution in the π-calculus
## Extended Abstract

Steffen van Bakel and Maria Grazia Vigliotti

Department of Computing, Imperial College London, 180 Queen's Gate, London SW7 2BZ, UK
s.vanbakel@imperial.ac.uk, maria.vigliotti@imperial.ac.uk

**Abstract.** We study the Λμ-calculus, extended with explicit substitution, and define a compositional *output*-based translation into a variant of the π-calculus with pairing. We show that this translation preserves single-step explicit head reduction with respect to contextual equivalence. We use this result to show operational soundness for head reduction, adequacy, and operational completeness. Using a notion of implicative type-context assignment for the π-calculus, we also show that assignable types are preserved by the translation. We finish by showing that termination is preserved.

## Introduction

Over the last two decades, the π-calculus [24] and its dialects have proven to give an interesting and expressive model of computation. Encodings of variants of the pure λ-calculus [14, 11] started with [24], which quickly led to more thorough investigations in [29, 31, 10] and also in the direction of object oriented calculi [21, 31].

For these encodings, over the years strong properties have been shown like soundness, completeness, termination, and full abstraction. The strength of these results has encouraged the investigation of encodings into the π-calculus of calculi that have their foundation in classical logic, as done in, for example, [22, 8, 15]. From these papers it might seem that the encoding of such calculi comes at a great price; for example, to encode typed λμ [25], [22] needs to consider a version of the π-calculus that is not only strongly typed, but, moreover, allows reduction under guard and under replication; [8] shows preservation of reduction in 𝒳 [9] only with respect to $⊆_c$, the contextual ordering; [15] defines a non-compositional encoding of $\overline{\lambda\mu\bar{\mu}}$ [17] that strongly depends on recursion, and does not regard the logical aspect at all.

In this paper, we will show that it is possible to define a intuitive, natural, logical encoding of λμ into the pure π-calculus that satisfies all the good properties. Although one could justifiably argue that calculi like 𝒳 and $\overline{\lambda\mu\bar{\mu}}$ are more expressive and, through their direct link to Gentzen's LK [18], more elegantly deal with negation and classical logic, they are also both symmetric in nature, which makes an accurate treatment in the π-calculus more intricate, as can be observed in [8, 15]. Moreover, as argued in [6, 5, 7], only for λμ is it possible to define a filter semantics, which seems to strengthen the case for that calculus even more.
Reduction in $\lambda\mu$ is confluent and non-symmetric; in fact, the main reduction rule (and the only cause for non-termination, for example) is the $\beta$-reduction rule of the $\lambda$-calculus. In addition to that rule, $\lambda\mu$ has structural rules, where elimination takes place for a type that is not the type of the term itself, but rather for one that appears in one of the alternative conclusions of the shape $\alpha:A$, where the Greek variable is the name given to a sub-term. For the naming feature, $\lambda\mu$ adds $[\alpha]M$ to the syntax which expresses that $\alpha$ serves as a pointer to the term $M$, and pairs this with a notion of $\mu$-abstraction $\mu\alpha.M$, which is used to redirect operands (terms) to those called $\alpha$. It is this naming feature, together with the structural rules, that make $\lambda\mu$ difficult to reason over; this is reflected in [20] and [9], where the encoding of $\lambda\mu$ into $\bar{\lambda}\mu\bar{\mu}$ and $\mathcal{X}$, respectively, does not respect normal reduction. In contrast, through our translation we will show that it is possible to give a process semantics for $\lambda\mu$ that very clearly shows that the context switch $\mu\alpha.[\beta]M$ is, essentially, just a variant of application.

For the construction of our translation, we will start with that defined in [10], that interprets terms under *output* rather than under *input*, by giving a name to the anonymous output of $\lambda$-terms; we will combine this with the inherent naming mechanism of $\lambda\mu$. To accurately define the notion of reduction that is modelled by our translation, we will define *untyped* $\Lambda\mu x$, a version with explicit substitution [1, 12] of the $\Lambda\mu$-calculus [19], itself a variant of $\lambda\mu$, together with a notion of *explicit head reduction*<fnref n="1" />, where reduction is also allowed under abstraction. We will define a new compositional semantic translation of $\Lambda\mu x$ into the $\pi$-calculus, and show that it fully respects each individual explicit head reduction step.

Perhaps surprisingly, we do not need to extend the kind of process calculus at all to accomodate our translation, but can build that directly on the standard $\pi$-calculus; in particular, the naming and $\mu$-binding features of $\lambda\mu$ are dealt with by the naming feature of the translation, and renaming, respectively. The only noteworthy change is that, when representing application $MN$, the communication needs to be replicated; the translation of application and structural substitution is almost identical.

The advantage of considering explicit substitution rather than the standard implicit substitution as considered in [31] has been strongly argued in [10]. That paper showed that communication in the $\pi$-calculus has a fine semantic level of granularity that ‘faithfully mimics’ explicit substitution, and not the implicit one; we stress this point again with the results presented in this paper.

# 1 The $\Lambda\mu$ calculus

The $\lambda\mu$-calculus is a proof-term syntax for classical logic, expressed in Natural Deduction, defined as an extension of the Curry type assignment system for the $\lambda$-calculus; we focus on de Groote’s $\Lambda\mu$, a variant that splits the naming from the $\mu$-binding. We will define in particular $\Lambda\mu x$, a variant of $\Lambda\mu$ with explicit substitution $\text{à la } \Lambda\mu x$ [12], and show our results for $\Lambda\mu x$; since $\Lambda\mu x$ implements $\Lambda\mu$-reduction, this implies that we also show some of our results for normal reduction (with implicit substitution).

<footnote n="1">¹ Called *spine reduction* in [10], and *head spine-reduction* in [32]; we prefer to use the terminology *head reduction* from [33].</footnote>
**Definition 1 (Syntax of Λμ).** The Λμ-terms we consider are defined over the set of term variables represented by Roman characters, and names, or context variables, represented by Greek characters, through the grammar:

$$ M, N ::= \begin{array}{l} x \mid \lambda x.M \mid MN \mid \mu\alpha.M \mid [\beta]M \\ \text{variable} \quad \text{abstraction} \quad \text{application} \quad \text{context abstraction} \quad \text{naming} \end{array} $$

The notion of free and bound names is defined as can be expected, taking both λ and μ as binders, and we assume Barendregt's convention.

Simple type assignment for Λμ is defined as follows:

**Definition 2 (Types, Contexts, and Typing).** 1. Types are defined by:

$$ A, B ::= \varphi \mid \bot \mid A \to B \quad (A \neq \bot) $$

where φ is a basic type of which there are infinitely many.

2. A context of inputs Γ is a mapping from term variables to types, denoted as a finite set of statements x:A, such that the subjects of the statements (x) are distinct. We write Γ₁, Γ₂ for the compatible union of Γ₁ and Γ₂ (if x:A₁ ∈ Γ₁ and x:A₂ ∈ Γ₂, then A₁ = A₂), and write Γ, x:A for Γ, {x:A}.

3. Contexts of outputs Δ, and the notions Δ₁, Δ₂ and α:A, Δ are defined similarly.

4. Type assignment for Λμ is defined by the following natural deduction system.

$$ (Ax) : \frac{\Gamma, x:A \vdash x : A \mid \Delta}{\mu} : \frac{\Gamma \vdash M : \bot \mid \alpha : A, \Delta}{\Gamma \vdash \mu\alpha.M : A \mid \Delta} (\bot) : \frac{\Gamma \vdash M : A \mid \beta : A, \Delta}{\Gamma \vdash [\beta]M : \bot \mid \beta : A, \Delta} $$

$$ (\to I) : \frac{\Gamma, x:A \vdash M : B \mid \Delta}{\Gamma \vdash \lambda x.M : A \to B \mid \Delta} \quad (\to E) : \frac{\Gamma \vdash M : A \to B \mid \Delta \quad \Gamma \vdash N : A \mid \Delta}{\Gamma \vdash MN : B \mid \Delta} $$

In Λμ, reduction of terms is expressed via implicit substitution; as usual, M[N/x] stands for the substitution of all occurrences of x in M by N, and M[N·γ/α], the structural substitution, stands for the term obtained from M in which every sub-term of the form [α]M' is replaced by [γ](M'N).

We have the following rules of computation in λμ:

**Definition 3 (Λμ reduction).** Λμ has two computational rules:

$$ \begin{array}{l} \textit{logical } (\beta) : (\lambda x.M)N \to M[N/x] \\ \textit{structural } (\mu) : (\mu\alpha.M)N \to \mu\gamma.M[N\cdot\gamma/\alpha] \quad \gamma \textit{ fresh} \end{array} $$

as well as the simplification rules:

$$ \textit{renaming} : \mu\alpha.[\beta]\mu\gamma.M \to \mu\alpha.M[\beta/\gamma] $$

$$ \textit{erasing} : \mu\alpha.[\alpha]M \to M \quad \text{if } \alpha \text{ does not occur in } M. $$

(which are added mainly to simplify the presentation of results), and the contextual rules. We use $\to_{\beta\mu}$ for this reduction, and $\to_{\beta\mu}^*$ for its reflexive and transitive closure.

[26] has shown that typeable terms are strongly normalisable. It also defines extensional rules, that we do not consider here: the model we present through our translation is not extensional, and we can therefore not show that those rules are preserved by the translation. That this notion of reduction is confluent was shown in [28].
## 2 The synchronous π-calculus with pairing

The notion of π-calculus that we consider in this paper is similar to the one used also in [2], and is different from other systems studied in the literature [21] in that it adds pairing, and uses a *let*-construct to deal with inputs of pairs of names that get distributed.

As already argued in [10], the main reason for the addition of pairing [2] lies in preservation of (implicate, or functional) type assignment; therefore *data* is introduced as a structure over names, such that not only names but also pairs of names can be sent.

**Definition 4 (Processes).** *Channel names and data are defined by:*

$a, b, c, d, x, y, z$ names

$p ::= a \mid \langle a, b \rangle$ data

Notice that pairing is *not* recursive. Processes are defined by:

$$P, Q ::= 0 \mid P \mid Q \mid !P \mid (va) P \mid a(x).P \mid \bar{a}\langle p \rangle .P \mid \text{let } \langle x,y \rangle = p \text{ in } P$$

A context $C[\cdot]$ is a process with a hole $[]$; we call $a(x)$ and $\bar{a}\langle p \rangle$ *guards*, and call $P$ in $a(x)$. $P$ and $\bar{a}\langle p \rangle$. $P$ a process *under guard*.

We abbreviate $a(x)$. $\text{let } \langle y,z \rangle = x$ in $P$ by $a(y,z)$. $P$, as well as $(vm)(vn)P$ by $(vmn)P$, and write $\bar{a}\langle p \rangle$ for $\bar{a}\langle p \rangle$. $0$, and $\bar{a}\langle c,d \rangle$. $P$ for $\bar{a}\langle\langle c,d \rangle\rangle$. $P$. Notice that $\text{let } \langle x,y \rangle = a$ in $P$ (where $a$ is not a variable) is *stuck*.

**Definition 5 (Congruence).** The structural congruence is the smallest equivalence relation closed under contexts defined by the following rules:

$P \mid 0 \equiv P$

$$ (P \mid Q) \mid R \equiv P \mid (Q \mid R) $$

$P \mid Q \equiv Q \mid P$

$$(vn)0 \equiv 0 $$

$!P \equiv P \mid !P$

$$(vm)(vn)P \equiv (vn)(vm)P $$

$!P \equiv !P \mid !P$

$$(vn)(P \mid Q) \equiv P \mid (vn)Q \quad \text{if } n \notin \mathit{fn}(P) $$

$$ \text{let } \langle x,y \rangle = \langle a,b \rangle \text{ in } P \equiv P[a/x, b/y] $$

As usual, we will consider processes modulo congruence and modulo α-convergence: this implies that we will not deal explicitly with the process $\text{let } \langle x,y \rangle = \langle a,b \rangle$ in $P$, but rather with $P[a/x, b/y]$. We write $a \leftrightarrow b$ for the *forwarder* [31] $a(x).\bar{b}\langle x \rangle$.

Computation in the π-calculus with pairing is expressed via the exchange of *data*.

**Definition 6 (Reduction).** The *reduction relation* over the processes of the π-calculus is defined by the following (elementary) rules:

$$ \bar{a}\langle p \rangle . P \mid a(x).Q \quad \rightarrow_{\pi} \quad P \mid Q[p/x] $$

$$ P \rightarrow_{\pi} P' \Rightarrow (vn)P \rightarrow_{\pi} (vn)P' $$

$$ P \rightarrow_{\pi} P' \Rightarrow P \mid Q \rightarrow_{\pi} P' \mid Q $$

$$ P \equiv Q \ \& \ Q \rightarrow_{\pi} Q' \ \& \ Q' \equiv P' \Rightarrow P \rightarrow_{\pi} P' $$

As usual, we write $\rightarrow_{\pi}^{+}$ for the transitive closure of $\rightarrow_{\pi}$, and $\rightarrow_{\pi}^{*}$ for its reflexive and transitive closure; we write $\rightarrow_{\pi}(a)$ if we want to point out that a synchronisation took place over channel $a$, and write $\rightarrow_{\pi}(=_{\alpha})$ if we want to point out that α-conversion has taken place during the synchronisation.

$$ \text{Notice that } \bar{a}\langle b,c \rangle \mid a(x,y).Q \rightarrow_{\pi} Q[b/x, c/y]. $$
**Definition 7.** 1. We write $P \downarrow n$ and say that $P$ outputs on $n$ (or $P$ exhibits an output barb on $n$) if $P \equiv (vb_1) \dots b_m (\bar{n} \langle p \rangle | Q)$ for some $Q$, where $n \neq b_1 \dots b_m$.

2. We write $P \downarrow n$ ($P$ may output on $n$) if there exists $Q$ such that $P \xrightarrow{\pi} Q$ and $Q \downarrow n$.

3. We write $P \sim_C Q$ ($P$ and $Q$ are contextually equivalent) if, for all $C[\cdot]$, and for all $n$, $C[P] \downarrow n$ if and only if $C[Q] \downarrow n$.

4. We write $\sim_G$ (called garbage collection) when we ignore a process because it is contextually equivalent to 0; notice that $\sim_G \subset \sim_C$.

The following is a well-known result.

**Proposition 8.** Let $P, Q$ not contain $a$, then

$$ \begin{align*} (va) (\bar{a} \langle b \rangle . P | a(x) . Q) &\sim_C P | Q[b/x] \\ (va) (!\bar{a} \langle b \rangle . P | a(x) . Q) &\sim_C, \sim_G Q[b/x] \end{align*} $$

The $\pi$-calculus is equipped with a rich type theory [31], from the basic type system for counting the arity of channels [27] to sophisticated linear types in [22]. The notion of type assignment we use here is the one first defined in [8] and differs from systems presented in the past in that types do not contain channel information, and in that it expresses implication, i.e. has functional types and describes the 'input-output interface' of a process.

**Definition 9 (Context assignment for $\pi$ [8]).** Functional type assignment for the $\pi$-calculus is defined by the following sequent system:

$$ (o) : \underline{o : \Gamma \vdash \Delta} \quad (!) : \frac{P : \Gamma \vdash \Delta}{!P : \Gamma \vdash \Delta} \quad (in) : \frac{P : \Gamma, x : A \vdash x : A, \Delta}{a(x) . P : \Gamma, a : A \vdash \Delta} $$

$$ (v) : \frac{P : \Gamma, a : A \vdash a : A, \Delta}{(va) P : \Gamma \vdash \Delta} \quad (out) : \frac{P : \Gamma, b : A \vdash b : A, \Delta}{\bar{a} \langle b \rangle . P : \Gamma, b : A \vdash a : A, b : A, \Delta} \quad (a \neq b) $$

$$ (l) : \frac{P : \Gamma \vdash \Delta \quad Q : \Gamma \vdash \Delta}{P | Q : \Gamma \vdash \Delta} \quad (pair-out) : \frac{P : \Gamma, b : A \vdash c : B, \Delta}{\bar{a} \langle b, c \rangle . P : \Gamma, b : A \vdash a : A \rightarrow B, c : B, \Delta} \quad (b \notin \Delta; a, c \notin \Gamma) $$

$$ (W) : \frac{P : \Gamma \vdash \Delta}{P : \Gamma' \vdash \Delta'} (\Gamma' \supset \Gamma, \Delta' \supset \Delta) \quad (let) : \frac{P : \Gamma, y : B \vdash x : A, \Delta}{let \langle x, y \rangle = z \text{ in } P : \Gamma, z : A \rightarrow B \vdash \Delta} (y, z \notin \Delta; x \notin \Gamma) $$

We adjust the system for the type constant $\perp$ by allowing that only in right-hand contexts. We write $P : \Gamma \vdash_{\pi} \Delta$ if there exists a derivation using these rules that has this expression in the conclusion.

We should perhaps stress that it is not known if this system has a relation with logic.

The following rule is derivable:

$$ (pair-in) : \frac{P : \Gamma, y : B \vdash_{\pi} x : A, \Delta}{a(x, y) . P : \Gamma, a : A \rightarrow B \vdash_{\pi} \Delta} (y, a \notin \Delta, x \notin \Gamma) $$

The soundness result is stated as:

**Theorem 10 (Witness reduction [8]).** If $P : \Gamma \vdash_{\pi} \Delta$ and $P \to \pi Q$, then $Q : \Gamma \vdash_{\pi} \Delta$.
### 3 Context and background of this paper

In the past, there have been several investigations of encoding from the $\lambda$-calculus [11] into the $\pi$-calculus [24, 29]. Research in this direction started by Milner's encoding $[\cdot]_M^\lambda$ of $\lambda$-terms [24]; Milner's encoding is *input* based and the translation of closed $\lambda$-terms respects large-step *lazy reduction* $\rightarrow_L$ [3] to normal form up to substitution. Standard operational soundness result hold for this translation, and full abstraction has been shown by in [29] for an (input-based, as Milner's) encoding $\mathcal{H}[\cdot]_L \langle \cdot \rangle$, of the lazy $\lambda$-calculus into the higher-order $\pi$-calculus (where in synchronisation not names are sent, but processes).

In [10], we presented a *logical, output-based* translation $[\cdot]_L^S$ that interprets abstraction $\lambda x.M$ not using *input*, but via an asynchronous *output* which leaves the translation of the body $M$ free to reduce. That translation is defined as:

$$ 
\begin{align*}
[\cdot]_{\llbracket}^S a &\triangleq x(w).\bar{a}\langle w \rangle \\
[\lambda x.M_{\llbracket}^S] a &\triangleq (vxb)([\cdot]_{\llbracket}^H b | \bar{a}\langle x, b \rangle) \\
[\mathit{MN}_{\llbracket}^S] a &\triangleq (vc)([\cdot]_{\llbracket}^H c | c(v,d). (![\cdot]_{\llbracket}^H v | d \rightarrow a)) \\
[\mathit{M}\langle x := N \rangle_{\llbracket}^S] a &\triangleq (vx)([\cdot]_{\llbracket}^H a | ![\cdot]_{\llbracket}^H x)
\end{align*}
$$

For this translation, [10] showed (using $\uparrow$ to denote non-termination)

1. $M \uparrow \Rightarrow [\cdot]_{\llbracket}^S a \uparrow$, and $M \rightarrow_{xH} N \Rightarrow [\cdot]_{\llbracket}^S a \rightarrow_{\pi}^* \sim_C [\cdot]_{\llbracket}^H a$.

2. $\Gamma \vdash M : A \Rightarrow [\cdot]_{\llbracket}^S a : \Gamma \vdash_{\pi} a : A$.

As argued in [10], to show the above result, which formulates a direct step-by-step relation between $\beta$-reduction and the synchronisation in the $\pi$-calculus, it is necessary to make the substitution explicit. This is a direct result of the fact that, in the $\pi$-calculus, $\lambda$'s implicit substitution gets 'implemented' *one variable at the time*, rather than all in one fell swoop. Since we aim to show a similar result for $\Lambda\mu$, we will therefore define a notion of explicit substitution. Although termination is not studied in that paper, it is easily achieved through restricting the notion of reduction in the $\pi$-calculus by not allowing reduction to take place inside processes whose output cannot be received, or by placing a guard on the replication as we do in this paper.

A natural extension of this line of research is to see if the $\pi$-calculus can be used to interpret more complex calculi as well, as for example calculi that relate not to intuitionistic logic, but to classical logic, as $\lambda\mu$, $\bar{\lambda}\mu\bar{\mu}$, or $\mathcal{X}$. There are, to date, a number of papers on this topic. In [22] an interpretation of Call-by-Value $\lambda\mu$ is defined that is based on Milner's. The authors consider *typed processes only*, and use a much more liberal notion of reduction on processes by allowing reduction *under* guards, making the resulting calculus very different from the original $\pi$-calculus. Types for processes prescribe usage of names

In [8] an interpretation into $\pi$ of the sequent calculus $\mathcal{X}$ is defined that enjoys the Curry-Howard isomorphism for Gentzen's LK [18], which is shown to respect reduction. However, this result is only partial, as it is formulated as "if $P \rightarrow_X Q$, then $[P] \sqsubseteq [Q]$, allowing $[P]$ to have more observable behaviour than $[Q]$. Although in [8] it is reasoned that this is natural in the context of non-confluent, symmetric sequent calculi, and is shown that the interpretation preserves types, it is a weaker result than could perhaps be expected.
An encoding of $\bar{\lambda}\mu\tilde{\mu}$ is studied in [15]; the interpretation defined there strongly depends on recursion, is not compositional, and preserves only outermost reduction; no relation with types is shown.

# 4 $\Lambda\mu$ with explicit substitution

One of the main achievements of [10] is that it establishes a strong link between reduction in the $\pi$-calculus and step-by-step explicit substitution for the $\lambda$-calculus, by formulating a result not only with respect to explicit head reduction and the spine encoding defined there, but also for Milner's encoding with respect to explicit lazy reduction.

In view of this, we decided to study a variant of $\Lambda\mu$ with explicit substitution as well, and present here $\Lambda\mu x$. Explicit substitution treats substitution as a first-class operator, both for the logical and the structural substitution, and describes all the necessary steps to effectuate both.

**Definition 11 ($\Lambda\mu x$).** 1. The syntax of the explicit $\Lambda\mu$ calculus, $\Lambda\mu x$, is defined by:

$$M, N ::= x \mid \lambda x.M \mid MN \mid M \langle x := N \rangle \mid \mu\alpha.M \mid [\beta]M \mid M \langle \alpha := N \cdot \gamma \rangle$$

We call a term *pure* if it does not contain explicit substitution.

2. The reduction relation $\rightarrow_x$ on terms in $\Lambda\mu x$ is defined as the compatible closure of the rules (we only show the important ones):

(a) Main reduction rules:

$$\begin{array}{lcl}
(\lambda x.M)N & \rightarrow & M \langle x := N \rangle \qquad N \text{ pure} \\
(\mu\alpha.M)N & \rightarrow & \mu\gamma.M \langle \alpha := N \cdot \gamma \rangle \qquad N \text{ pure} \\
\mu\beta.[\beta]M & \rightarrow & M \qquad \text{if } \beta \notin \text{fn}(M) \\
\mu\beta.[\delta]\mu\gamma.M & \rightarrow & \mu\beta.M[\delta/\gamma]
\end{array}$$

(b) Term substitution rules, like

$$\begin{array}{lcl}
x \langle x := N \rangle & \rightarrow & N \\
M \langle x := N \rangle & \rightarrow & M \quad x \notin \text{fv}(M)
\end{array}$$

(c) Structural rules, like

$$\begin{array}{lcl}
([\alpha]M) \langle \alpha := N \cdot \gamma \rangle & \rightarrow & [\gamma](M \langle \alpha := N \cdot \gamma \rangle)N \\
([\beta]M) \langle \alpha := N \cdot \gamma \rangle & \rightarrow & [\beta](M \langle \alpha := N \cdot \gamma \rangle) \qquad \alpha \neq \beta \\
M \langle \alpha := N \cdot \gamma \rangle & \rightarrow & M \qquad \alpha \notin \text{fn}(M)
\end{array}$$

(d) Contextual rules, like

$$M \rightarrow N \Rightarrow \left\{ \begin{array}{lcl} ML & \rightarrow & NL \\ LM & \rightarrow & LN \\ M \langle x := L \rangle & \rightarrow & N \langle x := L \rangle \\ L \langle \alpha := M \cdot \gamma \rangle & \rightarrow & L \langle \alpha := N \cdot \gamma \rangle \end{array} \right.$$

3. We define $\rightarrow_\alpha$ as the notion of reduction where the main reduction rules are not used, and $\Rightarrow_x$ as the smallest equivalence relation generated by $\rightarrow_x$.

Notice that this is a system different from that of [4], where a version with explicit substitution is defined for a variant of $\lambda\mu$ that uses de Bruijn indices [13].

Explicit substitution describes explicitly the process of executing a $\beta\mu$-reduction, i.e. expresses syntactically the details of the computation as a succession of atomic steps (like in a first-order rewriting system), where the implicit substitution of each $\beta\mu$-reduction step is split up into reduction steps. Thereby the following is straightforward:
**Proposition 12 (Λμx implements Λμ-reduction).** 1. $M \to_{βμ} N \Rightarrow M \to_x^* N$.

2. $M \in \Lambda\mu \ \& \ M \to_x N \Rightarrow \exists L \in \Lambda\mu [N \to_{:=} L]$.

The notion of type assignment on Λμx is a natural extension of the system for the Λμ-calculus of Def. 2 by adding rules (T-cut) and (C-cut).

**Definition 13.** *Using the notion of type assignment in Def. 2, type assignment for Λμx is defined by adding:*

$$ (T-cut) : \frac{\Gamma, x:A \vdash M:B \mid \Delta \quad \Gamma \vdash N:A \mid \Delta}{\Gamma \vdash M \langle x := N \rangle : B \mid \Delta} $$

$$ (C-cut) : \frac{\Gamma \vdash M:C \mid \alpha:A \to B, \gamma:B, \Delta \quad \Gamma \vdash N:A \mid \gamma:B, \Delta}{\Gamma \vdash M \langle \alpha := N \cdot \gamma \rangle : C \mid \Delta} $$

We write $\Gamma \vdash_{\mu x} M : A$ for judgements derivable in this system.

We also consider the notion of head reduction;

**Definition 14.** 1. We define head reduction $\to_H$ as a restriction of $\to_{βμ}$ by removing the contextual rule $M \to N \Rightarrow LM \to LN$.

2. The Λμ and Λμx head-normal forms are defined through the grammar:

$$ \mathbf{H} ::= xM_1 \cdots M_n \ (n \ge 0) \mid \lambda x.\mathbf{H} \mid [\alpha]\mathbf{H} \\ \phantom{\mathbf{H} ::=} | \mu\alpha.\mathbf{H} \ (\mathbf{H} \ne [\alpha]\mathbf{H}' \ \& \ \alpha \notin \mathbf{H}', \mathbf{H} \ne [\beta]\gamma.\mathbf{H}') $$

3. The head variable of M, $hv(M)$, and head name $hn(M)$ are defined as expected.

The following is straightforward:

**Proposition 15 (→<sub>H</sub> implements Λμ's head reduction).** If $M \to_{βμ}^* N$ with $N$ in head-normal form, then there exists $L$ in $\to_H$-normal form such that $M \to_H^* L$, and $L \to_{βμ}^* N$, and none of these last steps are reductions in $\to_H$.

Notice that $\lambda f.(\lambda x.f(xx))(\lambda x.f(xx)) \to_H \lambda f.f((\lambda x.f(xx))(\lambda x.f(xx)))$ and this last term is in head-normal form, and in $\to_H$-normal form.

In the context of head reduction, we can economise further on how substitution is executed, and perform only those replacements of variables by terms that are essential for the continuation of reduction. We will therefore limit substitution to allow it to only replace the head variable or name of a term. We will show that this is exactly the kind of reduction that the π-calculus naturally encodes.

**Definition 16 (Explicit head reduction cf. [10]).** We define explicit head reduction $\to_{xH}$ on Λμx as $\to_x$, but for:

1. To avoid looping unnecessarily, application of all term substitution (resp. structural) rules on $M \langle x := N \rangle$ (resp. $M \langle \alpha := N \cdot \gamma \rangle$) is only allowed if $hv(M) = x$ (resp. $hn(M) = \alpha$); the only exception are the garbage collection rules, i.e. when $x \notin fv(M)$ ($\alpha \notin fn(M)$).
2. We change two cases:

$$ (PQ) \langle x := N \rangle \rightarrow (P \langle x := N \rangle Q) \langle x := N \rangle \quad (x = hv(P)) $$

$$ (PQ) \langle \alpha := N \cdot \gamma \rangle \rightarrow (P \langle \alpha := N \cdot \gamma \rangle Q) \langle \alpha := N \cdot \gamma \rangle \quad (\alpha = hn(P)) $$

3. We add two substitution rules:

$$ M \langle x := N \rangle \langle y := L \rangle \rightarrow M \langle y := L \rangle \langle x := N \rangle \langle y := L \rangle \quad (y = hv(M)) $$

$$ M \langle \alpha := N \cdot \gamma \rangle \langle \beta := L \cdot \delta \rangle \rightarrow M \langle \beta := L \cdot \delta \rangle \langle \alpha := N \cdot \gamma \rangle \langle \beta := L \cdot \delta \rangle \quad (\alpha = hn(P)) $$

4. We remove the contextual rules:

$$ M \rightarrow N \Rightarrow \begin{cases} LM & \rightarrow LN \\ L \langle x := M \rangle & \rightarrow L \langle x := N \rangle \\ L \langle \alpha := M \cdot \gamma \rangle & \rightarrow L \langle \alpha := N \cdot \gamma \rangle \end{cases} $$

Notice that, for example, in case 2, the first of the two clauses postpones the substitution $\langle x := N \rangle$ on $Q$ until such time that an occurrence of the variable $x$ in $Q$ becomes the head-variable. It is straightforward to show that this notion of reduction is confluent; remember that in $M \langle x := N \rangle$ and $M \langle \alpha := N \cdot \gamma \rangle$, $N$ is a pure term.

The following proposition states the relation between explicit head reduction, head reduction, and explicit reduction.

**Proposition 17.** 1. If $M \xrightarrow{\cdot}^* N$, then there exists $L$ such that $M \xrightarrow{\cdot}^* L$ and $N \xrightarrow{\cdot}^* L$.

2. If $M \xrightarrow{\cdot}^* N$ and $N$ is in $\rightarrow_H$-normal form, then there exists $L$ such that $M \xrightarrow{\cdot}^* L$ and $N \xrightarrow{\cdot}^* L$.

3. If $M \xrightarrow{\cdot}^* N$ with $M \in \Lambda\mu$ and $N$ is in $\rightarrow_{xH}$-normal form, then there exists $L \in \Lambda\mu$ such that $N \xrightarrow{\cdot} L$, and $L$ is in $\Lambda\mu$ head-normal form.

This result gives that we can show our main results for $\Lambda\mu x$ for reductions that reduce to head-normal form, that are naturally defined as follows:

**Definition 18 (cf. [23]).** The normal forms with respect to $\rightarrow_{xH}$ are defined through:

$$ \begin{array}{l} N ::= xM_1 \cdots M_n \ (n \ge 0) \quad | \quad \lambda x.N \quad | \quad [\alpha]N \\ | \quad \mu\alpha.N \quad (N \neq [\alpha]N' \ \& \ \alpha \notin N', N \neq [\beta]\gamma.N') \\ | \quad N \langle x := M \rangle \quad (hv(N) \neq x) \\ | \quad N \langle \alpha := M \cdot \gamma \rangle \quad (hn(N) \neq \alpha) \end{array} $$

Notice that, for example, under head reduction, any term of the shape $(\lambda x.P)Q$ in one of the $M_i$ in $xM_1 \cdots M_n$ is not considered a redex.

# 5 A logical translation of $\Lambda\mu x$ to $\pi$

We will now define our logical, output-based translation $\Gamma \cdot \downarrow \cdot$ of the $\Lambda\mu x$-calculus into the $\pi$-calculus. The main idea behind the translation, as in [10], is to give a name to the anonymous output of terms; it combines this with the inherent naming mechanism of $\Lambda\mu$. In the definition below, for readability, we use the symbol $\bullet$ as a channel name to represent an output that cannot be received from.

**Definition 19 (Logical translation of $\Lambda\mu x$ terms).** The translation of $\Lambda\mu x$ terms into the $\pi$-calculus is defined in Fig. 1.
<figure><img src="image_3.png" /><figcaption>Fig. 1. The logical translation</figcaption></figure>

We would like to stress that, although inspired by logic, our translation does not depend on types *at all*; in fact, we can treat untypeable terms as well, and can show that $\Gamma(\lambda x.xx)(\lambda x.xx)\downarrow a$ (perhaps the prototype of a non-typeable term) runs to itself (this already holds for $\Gamma\cdot\downarrow^H$ of [10]).

Notice that, as is the case for Milner's translation and in contrast to the interpretation of [10], a guard is placed on the replicated terms. This is not only done with an eye on proving preservation of termination, but more importantly, to make sure that $(vx)(\Gamma x := N\downarrow) \sim_c o$: since a term can have named sub-terms, the translation will generate output not only for the term itself, but also for those named terms, so $(vx)(\Gamma x := N\downarrow)$ can have observable behaviour, in contrast to [10], where this process is equivalent to $o$.

We could have avoided the implicit renaming in the case for $\mu$-abstraction and defined $\Gamma\mu\gamma.M_\downarrow a = (\nu\bullet\gamma)(\Gamma M_\downarrow\bullet | !\gamma\to a)$, which is operationally (contextually) the same as $(\nu\bullet)((\Gamma M_\downarrow\bullet)[a/\gamma])$, but then we could not show that terms in head-normal form are translated to processes in normal form (Lem. 24). There is a strong relation between this encoding and the abstract machine defined in [16], but for the fact that that only represents lazy reduction.

Notice that $\Gamma\mu\gamma.[\beta]M_\downarrow a \triangleq (\nu\bullet)((\Gamma M_\downarrow\beta)[a/\gamma])$, so had we considered to just encode $\lambda\mu$, we could have defined

$$ \Gamma\mu\gamma.[\beta]M_\downarrow a \triangleq (\nu\bullet)((\Gamma M_\downarrow\beta)[a/\gamma]) = \Gamma M[a/\gamma]\downarrow\beta $$

so $\lambda\mu$'s binding-and-naming has no representation in $\pi$.

Moreover, notice the similarity between

$$ \Gamma MN_\downarrow a = (vc) (\Gamma M_\downarrow c | !c(v,d). (\Gamma v := N_\downarrow | !d \to a)) \\ \Gamma M \langle \beta := N \cdot \gamma \rangle_\downarrow a = (v\beta) (\Gamma M_\downarrow a | !\beta(v,d). (\Gamma v := N_\downarrow | !d \to \gamma)) $$

The first communicates $N$ via the output channel $c$ of $M$, whereas the second communicates with all the sub-terms that have $\beta$ as its output name<fnref n="2" />. This very elegantly expresses exactly what the structural substitution does: it ‘connects’ arguments with the correct position in a term; it also allows us to write $(vc)(\Gamma M_\downarrow c | \Gamma c := N \cdot a_\downarrow)$ for $\Gamma MN_\downarrow a$. This stresses that the $\pi$-calculus constitutes a very powerful abstract machine indeed: although the notion of structural reduction in $\lambda\mu$ is very different from normal $\beta$-reduction, no special measures had to be taken in order to be able to express it; the

<footnote n="2">² A similar observation can be made for the encoding of $\lambda\mu$ in $\mathcal{X}$; see [9].</footnote>
<figure><img src="image_4.png" /><figcaption>Fig. 2. The translation of a term with double output</figcaption></figure>

*Example 23.* The translation of a $\beta$-redex reduces as:

<figure><img src="image_5.png" /></figure>

This implies that $\beta$-reduction is implemented in $\pi$ by at least one $\pi$-reduction.

On the other hand, $\mu$-reduction consists of a reorganisation of the structure of a term by changing its applicative structure. Since application is essentially modelled through parallel composition, this implies that the translation of a $\mu$-redex is essentially dealt with by congruence and renaming. For example,

<figure><img src="image_6.png" /></figure>

We can show, using Lem. 20, this last process is contextually equivalent to

<figure><img src="image_7.png" /></figure>

(notice that we have separated out the outside name of the term $P$, being $\beta$, which we renamed to $\gamma$; this leaves two context substitutions, one dealing with the occurrences of $\beta$ inside $P$, and one with $\gamma^3$).

Translations of terms in $\rightarrow_{\mathbf{xH}}$-normal form are in normal form as well.

*Lemma 24.* $\mathbf{N}$ is a $\rightarrow_{\mathbf{xH}}$-nf implies $\Gamma\mathbf{N}\downarrow a$ is irreducible.

To illustrate the expressiveness of our translation, we give some examples:

*Example 25.* 1. In Fig. 2 we run $\Gamma(\lambda x.x)(\mu\alpha.[\alpha](\lambda q.q)(\mu\beta.[\alpha]\lambda y.y))\downarrow a$,

<footnote n="3">³ This corresponds to the behaviour of rule (x̄ imp-outs) in $\mathcal{X}$.</footnote>
as an example of a term that generates two outputs over $\alpha$, and highlights the need for the repeated use of replication.

2. $\Gamma PQR_\parallel a \stackrel{\Delta}{\equiv} (vcc') (\Gamma P_\parallel c' | !c'(v,d). (\Gamma v:=Q_\parallel | !d\to c) | !c(v,d). (\Gamma v:=R_\parallel | !d\to a))$

so components of applications are placed in parallel under the translation. Similarly,

$$ \Gamma M\langle\alpha := N\cdot\beta\rangle \langle\gamma := L\cdot\delta\rangle_\parallel a = (v\gamma\alpha)(\Gamma M_\parallel a | \Gamma\alpha := N\cdot\beta_\parallel | \Gamma\gamma := L\cdot\delta_\parallel) $$

so repeated structural substitutions are also placed in parallel under the translation and can be applied independently.

# 6 Soundness, completeness, and termination

As in [24, 31], we can now show a reduction preservation result for explicit head reduction for $\Lambda\mu x$, by showing that $\Gamma\cdot\parallel$ preserves $\to_{xH}$ up to $\rightsquigarrow_\pi^*$. Since reduction in interpreted terms takes place over hidden channels exclusively, by Lem. 8, $\rightsquigarrow_\pi^* \subseteq \sim_C$, so we could have shown the following result using $\sim_C$ as well, but the current formulation is more expressive; notice that we do not require the terms to be closed.

**Theorem 26 (Soundness).** $M \to_{xH} N \Rightarrow \Gamma M_\parallel a \rightsquigarrow_\pi^* \Gamma N_\parallel a$.

*PROOF.* We show only the interesting cases.

$$ \begin{align*} x \langle x := N \rangle \to N : \quad & \Gamma x \langle x := N \rangle_\parallel a & \stackrel{\Delta}{=} \\ & (v x) (\Gamma x_\parallel a | \Gamma x := N_\parallel) & \stackrel{\equiv}{=} \\ & (v x) (x(u).!u\to a | (v w) (\bar{x} \langle w \rangle . \Gamma N_\parallel w) | \Gamma x := N_\parallel) & \to_\pi (x) \\ & (v w) (!w\to a | \Gamma N_\parallel w) | (v x) (\Gamma x := N_\parallel) & \sim_{R, \sim_G} \Gamma N_\parallel a \end{align*} $$

$$ \begin{align*} (PQ) \langle x := N \rangle \to & (P \langle x := N \rangle Q) \langle x := N \rangle, x = h_v(P) : \Gamma (PQ) \langle x := N \rangle_\parallel a \stackrel{\Delta}{=} \\ & (v x) ((vc) (\Gamma P_\parallel c | !\Gamma c := Q \cdot a_\parallel) | \Gamma x := N_\parallel) & \sim_C (20) \\ & (v x) ((vc) ((vx) (\Gamma P_\parallel c | \Gamma x := N_\parallel) | !\Gamma c := Q \cdot a_\parallel) | \Gamma x := N_\parallel) & \stackrel{\Delta}{=} \\ & (v x) ((vc) (\Gamma P \langle x := N \rangle_\parallel c | !\Gamma c := Q \cdot a_\parallel) | \Gamma x := N_\parallel) & \stackrel{\Delta, \equiv}{=} \\ & (v x) (\Gamma P \langle x := N \rangle Q_\parallel a | \Gamma x := N_\parallel) & \stackrel{\Delta}{=} \\ & \Gamma (P \langle x := N \rangle Q) \langle x := N \rangle_\parallel a \end{align*} $$

$$ \begin{align*} (\mu\beta.M)N \to \mu\gamma.M \langle\beta := N\cdot\gamma\rangle, \gamma \text{ fresh : } & \Gamma (\mu\beta.M)N_\parallel a \stackrel{\Delta}{=} \\ & (vc) ((v\bullet)((\Gamma M_\parallel\bullet)[c/\beta]) | !c(v,d). (\Gamma v:=N_\parallel | !d\to a)) & =_\alpha \\ & (v\beta) ((v\bullet)(\Gamma M_\parallel\bullet) | !\beta(v,d). (\Gamma v:=N_\parallel | !d\to a)) & \equiv_\equiv \\ & (v\bullet)((v\beta)(\Gamma M_\parallel\bullet | !\beta(v,d). (\Gamma v:=N_\parallel | !d\to\gamma)))[a/\gamma] & \stackrel{\Delta}{=} \\ & \Gamma\mu\gamma.M\langle\beta := N\cdot\gamma\rangle_\parallel a \end{align*} $$

$$ \begin{align*} ([\alpha]M) \langle \alpha := N \cdot \gamma \rangle \to [\gamma] (M \langle \alpha := N \cdot \gamma \rangle) N : \quad & \Gamma ([\alpha]M) \langle \alpha := N \cdot \gamma \rangle_\parallel \stackrel{\Delta}{=} \\ & (v\alpha) (\Gamma M_\parallel \alpha | !\alpha(v,d). (\Gamma v := N_\parallel | !d \to \gamma)) & \sim_C (20) \\ & (vc) ((v\alpha) (\Gamma M_\parallel c | !\alpha(v,d). (\Gamma v := N_\parallel | !d \to \gamma)) | \\ & \phantom{((v\alpha) (\Gamma M_\parallel c | !\alpha(v,d). (\Gamma v := N_\parallel | !d \to \gamma)) |} !c(v,d). (\Gamma v := N_\parallel | !d \to \gamma)) & \stackrel{\Delta}{=} \\ & (vc) (\Gamma M \langle \alpha := N \cdot \gamma \rangle_\parallel c | !c(v,d). (\Gamma v := N_\parallel | !d \to \gamma)) & \stackrel{\Delta}{=} \\ & \Gamma [\gamma] M \langle \alpha := N \cdot \gamma \rangle N_\parallel \end{align*} $$

□

The main soundness result is formulated as:
**Theorem 27 (Operational Soundness for $\rightarrow_{xH}$).**
1. $M \rightarrow_{xH}^* N \Rightarrow \Gamma M \downarrow a \rightsquigarrow \pi_*^* \Gamma N \downarrow a$.

2. $M \uparrow_{xH} \Rightarrow \Gamma M \downarrow a \uparrow_{\pi}$.

Since $\rightsquigarrow_{\pi}^* \subseteq \sim_C$, which is symmetric, Thm. 27 gives that $\Gamma \cdot \downarrow \cdot$ preserves $\rightarrow_{xH}$ up to $\sim_C$.

**Corollary 28 (Adequacy).** $M \coloneqq_{xH} N \Rightarrow \Gamma M \downarrow a \sim_C \Gamma N \downarrow a$.

This result states that our encoding gives, in fact, a semantics for the explicit head reduction for $\Lambda\mu$. As for a full abstraction result, note that we cannot show the reverse of Cor. 28, since different unsolvable terms like $(\lambda x.xx)(\lambda x.xx)$ and $(\lambda w.www)(\lambda w.www)$ are not equivalent under $\coloneqq_{xH}$, but are contextually equivalent under $\Gamma \cdot \downarrow \cdot$, i.e. have the same observable behaviour, as is illustrated by the fact that their translations never exhibit an output.

We can also show operational completeness for $\rightarrow_{xH}$.

**Theorem 29 (Operational completeness for $\rightarrow_{xH}$).** If $\Gamma M \downarrow a \rightarrow_{\pi} P$ then there exists $N$ such that $P \rightsquigarrow_{\pi}^* \Gamma N \downarrow a$, and $M \rightarrow_{xH} N$.

This in turn can be used to show:

**Lemma 30.**
1. Let $M$ be a term in $\Lambda\mu x$. If $\Gamma M \downarrow a \rightarrow_{\pi}^* \Gamma N \downarrow a$ then $M \rightarrow_{xH}^* N$.

2. Let $M \in \Lambda\mu$, i.e. a (pure) $\Lambda\mu$-term. If $\Gamma M \downarrow a \rightarrow_{\pi} P$ then there exists $N \in \Lambda\mu x$ and $L \in \Lambda\mu$ such that $P \sim_C \Gamma N \downarrow a$, and $M \rightarrow_{xH}^* N$ and $N \rightarrow_{:=}^* L$.

We can show the following termination results:

**Theorem 31 (Termination).**
1. If $M \rightarrow_{xH}^* N$, with $N$ in explicit head-normal from, then $\Gamma M \downarrow a \downarrow_{\pi}$.

2. If $M \rightarrow_{\beta\mu}^* N$, with $N$ in head-normal from, then $\Gamma M \downarrow a \downarrow_{\pi}$.

3. Let $M \in \Lambda\mu$. If $\Gamma M \downarrow a \downarrow_{\pi}$ then there exists $N \in \Lambda\mu x$ and $L$ in $\rightarrow_{\lambda\mu}$-head normal form such that $\Gamma M \downarrow a \sim_C \Gamma N \downarrow a$, and $M \rightarrow_{xH}^* N$ and $N \rightarrow_{:=}^* L$.

Notice that, in the first case, the normal form of $\Gamma M \downarrow a$ need not be $\Gamma N \downarrow a$; a similar observation can be made with respect to Milner's encoding. Notice also that this result is stronger than the formulation of the termination result for Milner's encoding in [31], since it models reduction to head-normal form, not just normal form. However, since terms that have a normal form have a head-normal form as well, Thm. 31 immediately leads to:

**Corollary 32.** If $M \downarrow_{\beta\mu}$, then $\Gamma M \downarrow a \downarrow_{\pi}$.

## Conclusions

We have defined an output based, logic inspired translation of untyped $\Lambda\mu$ with explicit substitution into the $\pi$-calculus and shown that it respects step-by-step head-reduction, assignable types, head-conversion, and termination. We conjecture that we can show the results shown above also for head reduction with *implicit* substitution; for this we
would need to show that, if $M \to^* N$, then $\Gamma M \llcorner a \sim_C \Gamma N \llcorner a$. It seems that the approach via Levy-Longo trees is more suitable for that.

There are many alternatives to the approach we have chosen to follow here; especially our choice for contextual equivalence (inspired by λ-calculus semantics) could be replaced by branching semantics, or a bisimulation-like equivalence. The natural question is then, which of our properties would be affected? Would branching and non-branching equivalences to coincide, maybe by exploiting some confluence properties?

We leave these issues for future work.

## References

1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit Substitutions. JFP, 1(4):375–416, 1991.

2. M. Abadi and A. Gordon. A Calculus for Cryptographic Protocols: The Spi Calculus. CCS'97, pp 36–47, 1997.

3. S. Abramsky. The lazy lambda calculus. Research topics in functional programming, pages 65–116. Addison-Wesley, 1990.

4. P. Audebaud. Explicit Substitutions for the $\Lambda\mu$ Calculus. RR 94-26, ÉNS de Lyon, 1994.

5. S. van Bakel. Completeness and Partial Soundness Results for Intersection & Union Typing for $\bar{\lambda}\mu\bar{\mu}$. Annals of Pure and Applied Logic, 161:1400–1430, 2010.

6. S. van Bakel. Completeness and Soundness results for $\mathcal{X}$ with Intersection and Union Types. Fundamenta Informaticae, 2012. To appear.

7. S. van Bakel, F. Barbanera, and U' de Liguooro. A Filter Model for $\bar{\lambda}\mu$. TLCA'11, LNCS 6690, pp. 213–228, 2011.

8. S. van Bakel, L. Cardelli, and M.G. Vigliotti. From $\mathcal{X}$ to $\pi$; Representing the Classical Sequent Calculus in the $\pi$-calculus. CL&C'08, 2008.

9. S. van Bakel and P. Lescanne. Computation with Classical Sequents. MSCS, 18:555–609, 2008.

10. S. van Bakel and M.G. Vigliotti. A logical interpretation of the $\lambda$-calculus into the $\pi$-calculus, preserving spine reduction and types. CONCUR'09, LNCS 5710, pp 84–98, 2009.

11. H. Barendregt. The Lambda Calculus: its Syntax and Semantics. North-Holland, 1984.

12. R. Bloo and K.H. Rose. Preservation of Strong Normalisation in Named Lambda Calculi with Explicit Substitution and Garbage Collection. CSN'95, pp 62–72, 1995.

13. N.G. de Brujin. Lambda Calculus Notation with Nameless Dummies: A Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem. Ind. Math., 34:381–392, 1972.

14. A. Church. A Note on the Entscheidungsproblem. JSL, 1(1):40–41, 1936.

15. M. Cimini, C. Sacerdoti Coen, and D. Sangiorgi. $\bar{\lambda}\mu\bar{\mu}$ calculus, $\pi$-calculus, and abstract machines. EXPRESS'09, 2009.

16. T. Crolard. A confluent lambda-calculus with a catch/throw mechanism. JFP, 9(6):625–647, 1999.

17. P.-L. Curien and H. Herbelin. The Duality of Computation. ICFP'00, pp 233–243. ACM, 2000.

18. G. Gentzen. Investigations into logical deduction. The Collected Papers of Gerhard Gentzen. Ed M. E. Szabo, North Holland, 68ff (1969), 1935.

19. Ph. de Groote. On the relation between the $\lambda\mu$-calculus and the syntactic theory of sequential control. LPAR'94, LNCS 822, pp 31–43, 1994.

20. H. Herbelin. C'est maintenant qu'on calcule: au cœur de la dualité. Mémoire d'habilitation, Université Paris 11, 2005.

21. K. Honda and M. Tokoro. An object calculus for asynchronous communication. ECOOP'91, LNCS 512, pp 133–147, 1991.

22. K. Honda, N. Yoshida, and M. Berger. Control in the $\pi$-Calculus. CW'04, 2004.

23. S.B. Lassen. Head Normal Form Bisimulation for Pairs and the $\lambda\mu$-Calculus. LICS'06, pp 297–306, 2006.

24. R. Milner. Functions as processes. MSCS, 2(2):269–310, 1992.

25. M. Parigot. An algorithmic interpretation of classical natural deduction. LPAR'92, LNCS 624, pp 190–201, 1992.

26. M. Parigot. Strong Normalization for Second Order Classical Natural Deduction. LICS'93, pp 39–46, 1993.

27. B.C. Pierce and D. Sangiorgi. Typing and Subtyping for Mobile Processes. MSCS, 6(5):409–453, 1996.

28. W. Py. Confluence en $\lambda\mu$-calcul. PhD thesis, Univ. Savoie, 1998.

29. D. Sangiorgi. Expressing Mobility in Process Algebra: First Order and Higher Order Paradigms. PhD thesis, Univ. Edinburgh, 1992.

30. D. Sangiorgi. Lazy functions and mobile processes. RR 2515, INRIA, Sophia-Antipolis, France, 1995.

31. D. Sangiorgi and D. Walker. The Pi-Calculus. Cambridge University Press, 2001.

32. P. Sestoft. Demonstrating Lambda Calculus Reduction. The Essence of Computation, LNCS 2566, pp 420–435, 2001.

33. C.P. Wadsworth. The relation between computational and denotational properties for Scott's $D_\infty$-models of the lambda-calculus. SIAM JOC, 5:488–521, 1976.