arXiv:1102.2339v1 [] 11 Feb 2011

A decompilation of the π-calculus
and its application to termination
Roberto M. Amadio
Université Paris Diderot
(UMR CNRS 7126)

March 20, 2018
Abstract
We study the correspondence between a concurrent lambda-calculus in administrative,
continuation passing style and a pi-calculus and we derive a termination result for the
latter.

1

Introduction

There are two complementary explanations of the π-calculus. The first one is to regard it
as an extension of a rather standard process calculus such as CCS while the second one
is to present it as an intermediate language for compiling higher-order languages including
various imperative/concurrent extensions of λ-calculi and object-oriented calculi. The first
view was put forward in the original presentation [10] and explains the transfer of effective
operational semantics techniques from CCS to the π-calculus. The second view gradually
emerged through a series of encodings starting from, e.g., [8] and it explains the expressivity
of the calculus while providing guidance in selecting its essential aspects.
Taking the second view, it has been stressed (see, e.g., [4]) that the translations from the
λ-calculus to the π-calculus can be understood as the composition of two familiar compilation
techniques. In the first step, the λ-term is put in an administrative form (AF) where all values
are explicitly named and in the second one a continuation passing style (CPS) translation is
applied so that the evaluation contexts are passed explicitly as an argument.
We note that neither the notion of administrative form nor that of CPS translation are
canonical. Our purpose here is to provide a concrete presentation of this approach for a
call-by-value λ-calculus and then for a parallel and concurrent extension of it. We show
that the two compilation steps commute nicely with the reduction relations and the typing
disciplines. Moreover, we identify languages which contain the image of the compilation and
are isomorphic to natural fragments of the π-calculus. The situation is summarized in table
1 where the λ-calculi in administrative form play a prominent role since on one hand the
ordinary λ-calculi can be regarded as a retraction of the administrative ones (symbol ⊳) and
on the other hand they contain sub-calculi (symbol ⊃) in CPS form which are isomorphic
(symbol ∼
=) to π-calculi. Also it is at this level, that it is natural to introduce a notion of
concurrent access to a resource, i.e., a definition. In this framework, one can decompile terms
of the π-calculus into familiar λ-terms. As an application of the correspondence, we show
that the termination of a (concurrent) λ-calculus entails the termination of a corresponding
1

Functional
∩
Concurrent

λ − notation
λ

⊳

Adm. Form (AF)
λa

⊃

AF in CPS style
λak

∼
=

π − notation
πf

λk

⊳

λak

⊃

λak
k

∼
=

π

Table 1: Overview of calculi and their relationships
(concurrent) π-calculus. Section 2 covers the functional case, section 3 generalizes it to the
parallel and concurrent case, and section 4 makes explicit the correspondence with the πcalculus. Omitted specifications, some concurrent programming examples, and proof sketches
of the main results are available in appendices A, B, and C, respectively.
Related work This work arises out of a long term effort of presenting the π-calculus to an
audience familiar with the λ-calculus but not necessarily with process calculi. We tried this
first in the context of a book [3] and then more recently in the context of a graduate course
[2]. The application to termination appears as a natural test for the presented compilation
techniques and can be regarded as a natural continuation of recent work on the termination of
(higher-order) concurrent calculi. In this respect, we find it remarkable that in the presented
approach one can drop completely the notion of stratified region [5, 1, 13, 6]. As far as the
π-calculus is concerned, we believe the presented approach complements those described in
[14, 12] in that we reduce the termination of a fragment of the π-calculus to the termination
of the λ-calculus by ‘elementary’ means. In particular, we do not need to develop reducibility
candidates/logical relations techniques for the π-calculus, nor do we require specific knowledge
of the operational semantics of the π-calculus.
Requirements The reader is supposed to be acquainted with the simply typed λ-calculus,
see, e.g., [7], its evaluation strategies and continuation passing style translations, see, e.g.,
[11], and to have some familiarity with the syntax of the π-calculus, see, e.g., [9] and its
reduction semantics. We shall make no use of the so called labelled transition systems and
related notions of bisimulation.
Renaming In the following calculi, all terms are manipulated up to α-renaming of bound
names. Whenever a structural congruence or a reduction rule is applied, it is assumed that
terms have been renamed so that all binders use distinct variables and these variables are
distinct from the free ones. Similar conventions are applied when performing a substitution,
say [T /x]T ′ , of a term T for a variable x in a term T ’. We denote with FV (T ) the set of
variables occurring free in a term T .
Syntax, Structural congruence, Reduction, and Typing For each calculus, we specify
the syntactic categories, the notion of structural congruence, the reduction rules, and the
typing rules. In all calculi, we assume a syntactic category id of identifiers (or variables)
which we denote with x, y, z, . . .. Structural congruence is the least equivalence relation,
denoted with ≡, which is induced by the displayed equations, α-renaming (which is always
left implicit), and closed under the operators of the language. The reduction relation is the
least binary relation → that includes the pairs given by the rewriting rules and such that
M → N if M ≡ M ′ → N ′ ≡ N . The basic judgment of the typing rules assigns a type to
2

Syntax
V
M
E
A

::= ∗ | (λid.M ) | id
::= V | (M M )
::= [ ] | E[[ ]M ] | E[V [ ]]
::= 1 | (A → A)

(values)
(terms)
(eval. contexts)
(types)

Reduction rule
(βV )

E[(λx.M )V ] → E[[V /x]M ]
Typing

(id)

(λ)

x:A∈Γ
Γ⊢x:A

Γ, x : A ⊢ M : B
Γ ⊢ λx.M : A → B

(∗)

(@)

Γ⊢∗:1

Γ⊢M :A→B Γ⊢N :A
Γ ⊢ MN : B

Table 2: A simply typed, call-by-value λ-calculus: λ
a term in a context Γ. The latter is a function mapping a finite set of variables to types.
When writing Γ, x : A it is assumed that x is not in the domain of definition of Γ. In the
parallel/concurrent extensions we distinguish between value types and types. The latter are
composed of value types plus a distinct behavior type b. Terms of a behavior type do not
return a result. As such a behavior type cannot occur in a context or as the type of the
argument of a function.
Vectorial notation We shall write X + (X ∗ ) for a non-empty (possibly empty) finite sequence X1 , . . . , Xn of symbols. By extension, λx+ .M stands for λx1 . . . λxn .M , A+ → B
stands for (A1 → · · · → (An → B) · · · ), [V + /x+ ]M stands for [V1 /x1 ](· · · [Vn /xn ]M · · · ), x+ :
A+ stands for x1 : A1 , . . . , xn : An , Γ ⊢ M + : A+ stands for Γ ⊢ M1 : A1 , . . . , Γ ⊢ Mn : An ,
and let (x = V )+ in M stands for let x1 = V1 in · · · let xn = Vn in M .

2

The functional case

In this section we explore the functional case, namely the upper part of table 1. This has at
least two advantages: first one can get an idea of the approach in a simple familiar framework
and second it clarifies the additions to be made to achieve parallelism and concurrency.
A λ-calculus To start with we introduce in table 2 a standard, simply typed, call-by-value
λ-calculus (λ). We specify, syntax, reduction and typing rules. We follow this pattern in the
following calculi too, possibly adding the specification of a structural congruence.
A λ-calculus in administrative form A corresponding calculus in administrative form
(λa ) is presented in table 3. The basic idea is to attribute a name to each value and to
compute by replacing names with names. Notice that in λa we restrict the values in a let
definition to be either abstractions or constants ‘∗’. Beyond values and terms, we introduce a
new syntactic category of ‘declarations’ which are terms possibly preceded by a list of value
declarations. Strictly speaking the application only applies to terms, however if Di = let (xi =
3

Syntax
V
D
M
E
A

::= ∗ | (λid + .D)
::= let (id = V )∗ in M
::= id | @(M, M + )
::= let (id = V )∗ in [ ] | E[@(id ∗ , [ ], M ∗ )]
::= N (1) | N (A+ → A)

(values)
(declarations)
(terms)
(eval. contexts)
(types)

Structural Congruence
(eq 1 )

let x1 = V1 in let x2 = V2 in D
≡ let x2 = V2 in let x1 = V1 in D
if x1 ∈
/ FV (V2 ), x2 ∈
/ FV (V1 )

(eq 2 )

let x = V in D ≡ D
if x ∈
/ FV (D)

Reduction rule
(βVa )

E[let x = λy + .D in E ′ [@(x, z + )]] → E[let x = λy + .D in E ′ [[z + /y + ]D]]
Typing
(id a )

(λa )

x:A∈Γ
Γ ⊢a x : A

(∗a )

Γ, y + : A+ ⊢a D′ : C
Γ, x : N (A+ → C) ⊢a D : B
Γ ⊢a let x = λy + .D′ in D : B

(@a )

Γ, x : N (1) ⊢ D : A
Γ ⊢a let x = ∗ in D : A
Γ ⊢a M : N (A+ → B)
Γ ⊢a N + : A +
Γ ⊢a @(M, N + ) : B

Table 3: The λ-calculus in administrative form: λa
Vi )∗ in Mi , for i = 1, . . . , n, then we regard @(D0 , D1 , . . . , Dn ) as an abbreviation for let (x0 =
V0 )∗ in · · · let (xn = Vn )∗ in @(M0 , . . . , Mn ) (the order of the declarations is immaterial up to
structural congruence). Similar care is needed when substituting a declaration D = let (x =
V )∗ in M in an evaluation context E. We remark that E can be written as let (x′ = V ′ )∗ in E ′
where E ′ does not start with a let declaration. Then by E[D] we mean the declaration
let (x = V )∗ in let (x′ = V ′ )∗ in E ′ [M ] where it is intended that the names x′∗ do not occur
free in E ′ . 1
We use N (A) for the type of names carrying values of type A; as the reader might have
guessed these names correspond to the channel names of the π-calculus. The λa -calculus is
polyadic in the sense that the application may have any finite, positive number of arguments.
This choice allows to represent directly the following CPS translation as a translation from
the λa calculus to a fragment of the λa calculus in ‘CPS form’ and moreover the latter
corresponds directly to a polyadic π-calculus. Nevertheless, we notice that the λa -calculus
contains a monadic sub-calculus that we denote with λam where the types are restricted as
follows:
A ::= N (1) | N (A → A)
(monadic types)
This sub-calculus is closed under reduction (provided we consider typable terms) and it suffices
to encode the simply typed λ-calculus.
Back and forth between λ and λa In table 4, we introduce a translation of λ-terms to
administrative forms along with a readback translation. Clearly, there are λa -terms which are
1
There is an alternative presentation where declarations and applications can be inter-mixed freely; we
found the current presentation more handy for our purposes.

4

Translation in AF
1 = N (1)
A → B = N (A → B)
∗ = let x = ∗ in x
λx.M = let x = λx.M in x

x=x

M N = @(M , N )

Readback
o

N (A1 → · · · → Ak → B)o = Ao1 → · · · → Aok → B o
∗o = ∗
(λy + .D)o = λy + .Do
o
o
(let x = V in D) = [V /x]Do
@(M, N1 , . . . , Nk )o = M o N1o · · · Nko

N (1) = 1
xo = x

Table 4: Translation in administrative form and readback
not structurally equivalent but are mapped to the same λ-term by the readback translation.
For instance, taking: V ≡ λz.z, M ≡ let x = V in @(x, x), and N ≡ let x = V in let y =
V in @(x, y), we have that M 6≡ N in λa but M o ≡ N o in λ. Thus we can regard the
administrative forms as notations for λ terms which differ in the amount of value sharing.
Conversely, given a λ-term such as V V , we can associate with it an administrative form
V V = @(let x = V in x, let y = V in y) ≡ N . Thus the translation ( ) in administrative form
makes no effort to share identical values. The translation and the related readback function
form a retraction pair which is ‘compatible’ with typing and reduction in a sense that is made
formal below. Thus, we can look at the λ-calculus as a retract of the λa calculus.
In establishing the simulations between λ and λa we cannot work directly with the translation ( ). For instance, taking M = (λx.x(xy))(λz.z), we have M → M ′ in λ and M 6→ M ′ .
Indeed in M ′ the term λz.z is duplicated while its translation is shared in M ′ . We get around
this difficulty by working with the readback operation.
Theorem 1 (read-back translation, functional case) The following properties hold.
1. If D1 ≡ D2 in λa then D1o ≡ D2o in λ.
2. If M is a term in λ then M o ≡ M .
3. If Γ ⊢ M : A in λ then Γ ⊢am M : A in λa .
4. If Γ ⊢a D : A in λa then Γo ⊢ D o : Ao in λ.
+

5. If Γ ⊢a D1 : A, M1 ≡ D1o and D1 → D2 in λa then M1 → M2 in λ and M2 ≡ D2o .
6. If Γ ⊢am D1 : A, M1 ≡ D1o and M1 → M2 in λ then D1 → D2 in λam and M2 ≡ D2o .
The first property states that the readback translation is invariant under structural congruence and the second that it is the left inverse of the function that puts a λ-term in
administrative form. The third and fourth properties state that typing is preserved by the
translations. The fifth property shows that any reduction in λa corresponds to a positive
number of reductions of the readback in λ (hence the following corollary). Finally, the sixth
property guarantees that the monadic administrative forms are indeed enough to simulate
the λ-calculus.
Corollary 2 The λa -calculus terminates.

5

Restricted CPS Syntax
V
D
M
E
A

::= ∗ | (λid + .D)
::= let (id = V )∗ in M
::= @(id, id + )
::= let (id = V )∗ in [ ]
::= N (1) | N (A+ → R)

(values)
(declarations)
(terms)
(eval. contexts)
(types)

Specialized typing rules
(∗a )

Γ, x : N (1) ⊢ D : R
x : N (A+ → R), y + : A+ ∈ Γ
(@a )
Γ ⊢a let x = ∗ in D : R
Γ ⊢a @(x, y + ) : R
+
+ a
′
+
Γ,
y
:
A
⊢
D
:
R
Γ,
x
:
N
(A
→ R) ⊢a D : R
(λa )
a
+
′
Γ ⊢ let x = λy .D in D : R

Table 5: Administrative forms in CPS style: λak
N (1)
N (A1 → · · · → An → B)

= N (1)
= N (A1 → · · · → An → K(B) → R)
where: K(B) = N (B → R)

ψ(∗)
ψ(λy + .D)
let (x = V )∗ in M : k
@(x∗ , @(M, M + ), N ∗ ) : k
@(x, x+ ) : k
x:k

=∗
= λy + .λk.(D : k)
= let (x = ψ(V ))∗ in M : k
= let k′ = λy.@(x∗ , y, N ∗ ) : k in @(M, M + ) : k′
= @(x, x+ , k)
= @(k, x)

Table 6: An optimized CPS translation on the administrative forms
Administrative forms in CPS style In table 5 we consider a restriction of the syntax of
the terms where we drop variables (functions are always applied to their arguments) and the
operator @ is only applied to variables. Evaluation contexts are then restricted accordingly.
The definition of structural congruence and reduction are inherited from λa and are omitted.
We restrict the syntax of types too by requiring, as it is common in CPS translations, that
there is a fixed type of results called R. The resulting language is called λak and it is a
subsystem of λa which inherits from λa the reduction and typing rules. In particular, the
terms in λak terminate because those in λa do.
CPS translation In table 6, we describe a CPS translation of the administrative language
λa into λak . The reader familiar with CPS translations, may appreciate the fact that the
translation has been optimized so as to have a simple statement and proof of the simulation
property. In particular, notice that the case for application is split into two cases.
Theorem 3 (CPS translation, functional case) The following properties hold.
1. If Γ ⊢a D : A then Γ, k : K(A) ⊢a (D : k) : R.
+

2. If Γ ⊢a D : A and D → D ′ in λa then (D : k) → (D ′ : k) in λak .

6

Syntax
V
M
E
A
α

::= ∗ | (λid.M ) | id
::= V | (M M ) | (M | M )
::= [ ] | E[[ ]M | E[V [ ]] | E[[ ] | M ] | E[M | [ ]]
::= 1 | (A → α)
::= A | b

(values)
(terms)
(eval. contexts)
(value types)
(types)

New typing rule
(|)

Γ ⊢ Mi : b i = 1, 2
Γ ⊢ (M1 | M2 ) : b

Table 7: Sketch of a parallel λ-calculus: λk

3

Parallel and Concurrent extensions

In this section, we explore the more general concurrent case, namely the lower part of table
1.
A parallel λ-calculus In table 7, we introduce a parallel version of the λ-calculus (cf.
appendix A, table 10). This amounts to introduce a binary parallel composition operator on
terms along with a special behavior type b which is attributed to terms running in parallel.
The reduction rule and the typing rules (id ), (∗), (λ), (@) are omitted since they are similar
to the ones in table 2. Terms running in parallel are not supposed to return a value. The
typing guarantees that they cannot occur under an application (neither as a function nor as
an argument). Notice that in this language terms running in parallel are not really competing
for the resources, i.e., the value declarations. This is because values are always available and
stateless (for this reason we call this calculus parallel rather than concurrent). An interesting
remark is that the termination of the parallel λ-calculus can be derived from the termination
of the simply typed λ-calculus.
Proposition 4 The λk -calculus terminates.

A concurrent λ-calculus in administrative form In table 8 we sketch an extension
of the administrative λ-calculus to accommodate the parallelism already introduced in the
λ-calculus (cf. appendix A, table 11). Thus once again we introduce parallel terms and a
special behavior type b. In order to have a form of concurrency or competition among the
parallel threads we associate a usage u with each declaration. A usage u varies over the set
{∞, 1, 0}. The (familiar) idea is that a declaration with usage ∞ is always available, one
with usage 1 can be used at most once, and one with usage 0 cannot be used at all. We
take the convention that when the usage is omitted the intended usage is ∞. We define an
operator ↓ to decrease usages as follows: ↓ ∞ = ∞, ↓ 1 = 0, and ↓ 0 is undefined. Modulo
this enrichment of the declarations with usages, the structural congruence is defined as in the
functional fragment of the language (table 3) and it is omitted. Notice that a reduction is
possible only if the usage of the corresponding definition is not 0 and in this case the effect of
the reduction is to decrease the usage. We omit the typing rules (id a ), (∗a ), and (@a ) which
are similar to the ones in table 3.
7

Syntax
V
D
M
E
A
α

::= ∗ | (λid + .D)
::= letu (id = V )∗ in M
::= id | @(M, M + ) | (M | M )
::= letu (id = V )∗ in [ ] | E[@(id ∗ , [ ], M ∗ )] | E[[ ] | M ] | E[M | [ ]]
::= N (1) | N (A+ → α)
::= A | b

(values)
(declarations)
(terms)
(eval. contexts)
(value types)
(types)

Reduction rule
(βVa )

E[letu x = λy + .D in E ′ [@(x, z + )]] → E[let↓u x = λy + .D in E ′ [[z + /y + ]D]]
New typing rules
(λa )

(λa0 )

u 6= 0

Γ, y

+

: A+ ⊢a D′ : α′ Γ, x : N (A+ → α′ ) ⊢a D : α
Γ ⊢a letu x = λy + .D′ in D : α

V 6= ∗ Γ, x : N (A+ → α′ ) ⊢a D : α
Γ ⊢a let0 x = V in D : α

(|a )

Γ ⊢a Mi : b i = 1, 2
Γ ⊢a (M1 | M2 ) : b

Table 8: Sketch of a concurrent λ-calculus in administrative form: λak
In the typing, we require that in letu x = ∗ in D, u is ∞. Also notice that in let0 x = V in D
we disregard the typing of the value V . Given a declaration D, we can obtain a declaration
D ′ by replacing all the usages with the usage ∞. It is clear that all reductions D may perform
can be simulated by D ′ . If the transformation must respect typing then we can just replace
the possibly ill-typed values in let0 by some well-typed value. Then, as far as termination
is concerned, it is enough to consider the sub-calculus where all usages are ∞; we denote
this calculus with λak,∞ . The administrative translation and the related readback translation
described in table 4 are extended to provide a retraction pair between the λk and the λak,∞
calculi. The translations are the identity on the behavior type b and distribute over parallel
compositions (cf. appendix A, table 12):
b
bo

=b
=b

M | M′
(M1 | M2 )o

= M | M′
= M1o | M2o

(translation in AF)
(readback)

Theorem 5 (read-back translation, parallel case) The following properties hold.
1. If D1 ≡ D2 in λak,∞ then D1o ≡ D2o in λ.
2. If M is a term in λk then M o ≡ M .
3. If Γ ⊢ M : α in λk then Γ ⊢am M : α in λam
k .
4. If Γ ⊢a D : α in λak,∞ then Γo ⊢ D o : αo in λk .
+

5. If If Γ ⊢a D1 : α, M1 ≡ D1o and D1 → D2 in λak,∞ then M1 → M2 in λk and M2 ≡ D2o .
am
o
6. If Γ ⊢am D1 : α in λam
k,∞ , M1 ≡ D1 and M1 → M2 in λk then D1 → D2 in λk,∞ and
o
M2 ≡ D2 .

8

Restricted CPS Syntax
V
D
M
E
A

::= ∗ | (λid + .D)
::= letu (id = V )∗ in M
::= @(id, id + ) | (M | M )
::= letu (id = V )∗ in [ ] | E[[ ] | M ] | E[M | [ ]]
::= N (1) | N (A+ → b)

(values)
(declarations)
(terms)
(eval. contexts)
(types)

New specialized typing rules
(λa )

(λa0 )

Γ, y + : A+ ⊢a D′ : b Γ, x : N (A+ → b) ⊢a D : b
Γ ⊢a letu x = λy + .D′ in D : b

V 6= ∗ Γ, x : N (A+ → b) ⊢a D : b
Γ ⊢a let0 x = V in D : b

(|a )

Γ ⊢ Mi : b i = 1, 2
Γ ⊢ (M1 | M2 ) : b

Table 9: Sketch of the concurrent administrative forms in CPS style: λak
k
By theorem 5(5), a reduction of a term in λak,∞ corresponds to a positive number of
reductions of the readback in λk . Hence, by recalling proposition 4, we obtain the following
corollary (cf. appendix B for concurrent programming examples).
Corollary 6 The λak -calculus terminates.
Concurrent λ-calculus in administrative, CPS form In table 9, we introduce the
concurrent λ-calculus in administrative and CPS form (cf. appendix A, table 13). The typing
rules (∗a ) and (@a ) are omitted as they are similar to the ones in table 5. The CPS translation
given in table 6 is extended to a translation from λak to λak
k . The behavior type is mapped to
itself, b = b, with a continuation type K(b) which is conventionally taken to be N (1), while
the optimized term translation distributes over parallel composition (M | M ′ ) : k = (M : k) |
(M ′ : k) (cf. appendix A, table 14). Then typing and reduction are preserved as follows.
Theorem 7 (CPS translation, concurrent case) The following properties hold.
1. If Γ ⊢a D : α in λak then Γ, k : K(α) ⊢a (D : k) : b in λak
k .
+

2. If Γ ⊢a D : α and D → D ′ in λak then (D : k) → (D ′ : k) in λak
k .

4

Correspondence with the π-calculus

In this section we consider the correspondence between the λak
k -calculus and the π-calculus.
To this end, we introduce the syntax of a π-calculus, π, where we write {. . .} to mean that the
symbols between curly brackets are optional. The ‘functional’ version of this calculus (called
πf in table 1) is obtained by dropping the (non-replicated) input prefix from the syntax and
it corresponds to the functional administrative CPS forms (table 5).
D
M
E
A

::= νid D | νid (id(id + ).D | D) | νid (!id (id + ).D | D) | M
::= id(id + ) | (M | M )
::= [ ] | E[νid([ ])] | E[νid({!}id (id + .D | [ ]) | E[[ ] | M ] | E[M | [ ]]
::= Ch(1) | Ch(A+ )

9

(declarations)
(terms)
(eval. contexts)
(types)

The following table provide a correspondence (a bidirectional translation) between λak
k
and π. Notice that declarations of the shape let∞ x = ∗ in D and let0 x = V in D both
correspond to declarations νx D. The structural congruence, the reduction rules, and the
typing rules of πr are exactly those of λak
k modulo this correspondence (cf. appendix A, table
15).
Types
Terms

λak
N (1)
N (A+ → b)
let∞ x = λy + .D in D′
let1 x = λy + .D in D′
let0 x = V in D
let∞ x = ∗ in D
M | M′
@(x, y + )

π
Ch(1)
Ch(A+ )
νx (!x(y + ).D | D′ )
νx (x(y + ).D | D′ )
νx D
νx D
M | M′
xy +

When applying the translation from πr to λak
k it is intended that: (i) D does not contain
a (possibly replicated) input prefix on the declared name x and (ii) the typing determines
the appropriate translation (recall that in λak the typing of V is disregarded). The reader
familiar with the π-calculus will recognize that communication is asynchronous (there is no
output prefix) and polyadic (we send vectors of names) and that for every (channel) name
x there is at most one associated definition (a process, possibly replicated, ready to input
on x). However these constraints are not enough to guarantee termination. For instance,
consider the following looping processes of the (untyped) π-calculus: P1 ≡ νx (!x(y).xy | xz),
P2 ≡ νx, x′ (!x(y).x′ y |!x′ (y).xy | xy). In the presented system, both processes are rejected,
the first because the definition of x refers to itself and the second because the definitions of x
and x′ are mutually recursive. The syntactic constraints and the typing rules guarantee that
the definitions can be linearly ordered so that each definition may only refer to previously
defined names.
Corollary 8 The typed π-calculus π described above terminates (cf. appendix A, table 15).

5

Conclusion

We have introduced a simply typed concurrent λ-calculus in administrative form, and shown
that a fragment of this calculus in continuation passing style corresponds to a simply typed
π-calculus. As an application of the correspondence, we have derived a termination result for
the π-calculus. We expect that the current framework can be extended in various directions
including: (i) polymorphic (second order) types, (ii) refinements towards linear logic/type
systems, and (iii) a synchronous/timed variants of the concurrency model.

References
[1] R.M. Amadio. On stratified regions. In Proc. APLAS, Springer LNCS 5905: 210-225, 2009.
[2] R.M. Amadio. Lectures on extensions of basic process calculi. MPRI course Concurrency, 2010, Université
Paris-Diderot.
[3] R.M. Amadio, P.-L. Curien. Domains and lambda calculi. Cambridge Tracts in Theoretical Computer
Science 46. 1998.

10

[4] G. Boudol. The π-calculus in direct style. In Proc. ACM-POPL: 228-241, 1997.
[5] G. Boudol. Typing termination in a higher-order concurrent imperative language. In Proc. CONCUR,
Springer LNCS 4703:272-286, 2007.
[6] R. Demangeon, D. Hirschkoff, D. Sangiorgi. Termination in impure concurrent languages. Proc. CONCUR
2010, SLNCS 6269: 328-342, 2010.
[7] J.-Y. Girard. Proofs and types. Cambridge University Press. 1989.
[8] R. Milner. Functions as processes. Mathematical Structures in Computer Science, 2(2): 119-141, 1992.
[9] R. Milner. Communicating and mobile systems: the pi calculus. Cambridge University Press. 1999.
[10] R. Milner, J. Parrow, D. Walker. A calculus of mobile processes, parts 1-2. Information and Computation,
100(1):1–77, 1992.
[11] G. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1(2):125-159,
1975.
[12] D. Sangiorgi. Termination of processes. Math. Struct. in Comp. Sci., 16:1-39, 2006.
[13] P. Tranquilli. Translating types and effects with state monads and linear logic. Manuscript, ENS Lyon,
January 2010,
[14] N. Yoshida, M. Berger, K. Honda. Strong normalisation in the π-calculus. Information and Computation,
191(2):145-202, 2004.

11

Syntax
V
M
E
A
α

::= ∗ | (λid.M ) | id
::= V | (M M ) | (M | M )
::= [ ] | E[[ ]M ] | E[V [ ]] | E[[ ] | M ] | E[M | [ ]]
::= 1 | (A → α)
::= A | b

(values)
(terms)
(eval. contexts)
(value types)
(types)

Reduction rule
(βV )

E[(λx.M )V ] → E[[V /x]M ]
Typing

(id)

(λ)

(|)

x:A∈Γ
Γ⊢x:A

Γ, x : A ⊢ M : α
Γ ⊢ λx.M : A → α

(∗)

(@)

Γ⊢∗:1

Γ⊢M :A→α Γ⊢N :A
Γ ⊢ MN : α

Γ ⊢ Mi : b i = 1, 2
Γ ⊢ (M1 | M2 ) : b

Table 10: A parallel λ-calculus: λk

A

Full specifications

This section contains the full specifications of the parallel/concurrent calculi and the related
translations as tables 10, 11, 12, 13, 14, and 15.

12

Syntax
::= ∗ | (λid + .D)
::= letu (id = V )∗ in M
::= id | @(M, M + ) | (M | M )
::= letu (id = V )∗ in [ ] | E[@(id ∗ , [ ], M ∗ )] | E[[ ] | M ] | E[M | [ ]]
::= N (1) | N (A+ → α)
::= A | b

V
D
M
E
A
α

(values)
(declarations)
(terms)
(eval. contexts)
(value types)
(types)

Structural Congruence
(eq 1 )

letu1 x1 = V1 in letu2 x2 = V2 in D
≡ letu2 x2 = V2 in letu1 x1 = V1 in D
if x1 ∈
/ FV (V2 ), x2 ∈
/ FV (V1 )

(eq 2 )

letu x = V in D ≡ D
if x ∈
/ FV (D)

Reduction rule
E[letu x = λy + .D in E ′ [@(x, z + )]] → E[let↓u x = λy + .D in E ′ [[z + /y + ]D]]

(βVa )

Typing
(id a )

x:A∈Γ
Γ ⊢a x : A

(∗a )

u 6= 0 Γ, y + : A+ ⊢a D′ : α′
Γ, x : N (A+ → α′ ) ⊢a D : α
Γ ⊢a letu x = λy + .D′ in D : α

a

(λ )

a

(@ )

(λa0 )

Γ ⊢a M : N (A+ → α)
Γ ⊢a N + : A +
Γ ⊢a @(M, N + ) : α

Γ, x : N (1) ⊢ D : α
Γ ⊢a let∞ x = ∗ in D : α

V 6= ∗ Γ, x : N (A+ → α′ ) ⊢a D : α
Γ ⊢a let0 x = V in D : α

(|a )

Γ ⊢a Mi : b i = 1, 2
Γ ⊢a (M1 | M2 ) : b

Table 11: A concurrent λ-calculus in administrative form: λak

Translation in AF
1 = N (1)
x=x

A → α = N (A → α)

b=b

∗ = let∞ x = ∗ in x
M N = @(M , N )

λx.M = let∞ x = λx.M in x
M | M′ = M | M′

Readback
N (1)o = 1

(let∞

bo = b

N (A1 → · · · → Ak → α)o = Ao1 → · · · → Aok → αo

∗o = ∗
(λy + .D)o = λy + .Do
xo = x
o
o
o
x = V in D) = [V /x]D
@(M, N1 , . . . , Nk )o = M o N1o · · · Nko
o
(M1 | M2 ) = M1o | M2o

Table 12: Translation in administrative form and readback: parallel case

13

Restricted CPS Syntax
V
D
M
E
A

::= ∗ | (λid + .D)
::= letu (id = V )∗ in M
::= @(id, id + ) | (M | M )
::= letu (id = V )∗ in [ ] | E[[ ] | M ] | E[M | [ ]]
::= N (1) | N (A+ → b)

(values)
(declarations)
(terms)
(eval. contexts)
(types)

Specialized typing rules
Γ, x : N (1) ⊢ D : b
Γ ⊢a let∞ x = ∗ in D : b

(∗a )

a

(λ )

(λa0 )

Γ, y + : A+ ⊢a D′ : b
Γ, x : N (A+ → b) ⊢a D : b
Γ ⊢a letu x = λy + .D′ in D : b
(|a )

(@a )

V 6= ∗ Γ, x : N (A+ → b) ⊢a D : b
Γ ⊢a let0 x = V in D : b
x : N (A+ → b), y + : A+ ∈ Γ
Γ ⊢a @(x, y + ) : b

Γ ⊢ Mi : b i = 1, 2
Γ ⊢ (M1 | M2 ) : b

Table 13: Concurrent administrative forms in CPS style: λak
k

N (1)
b
N (A1 → · · · → An → α)

= N (1)
=b
= N (A1 → · · · → An → K(α) → b)
where: K(A) = N (A → b), K(b) = N (1)

ψ(∗)
ψ(λy + .D)
letu (x = V )∗ in D : k
(M | M ′ ) : k
@(x∗ , @(M, M + ), N ∗ ) : k
@(x, x+ ) : k
x:k

=∗
= λy + .λk.(D : k)
= letu (x = ψ(V ))∗ in D : k
= (M : k) | (M ′ : k)
= letu k′ = λy.@(x∗ , y, N ∗ ) : k in @(M, M + ) : k′
= @(x, x+ , k)
= @(k, x)

(u 6= 0)

Table 14: An optimized CPS translation for the concurrent case

14

Syntax
D
M
E
A

::= νid D | νid (id(id + ).D | D) | νid (!id (id + ).D | D) | M
::= id(id + ) | (M | M )
::= [ ] | E[νid([ ])] | E[νid({!}id (id + .D | [ ]) | E[[ ] | M ] | E[M | [ ]]
::= Ch(1) | Ch(A+ )

(declarations)
(terms)
(eval. contexts)
(types)

Structural Congruence
(eq 1 )

νx1 ({{!}x1 (y1+ ).D1 |}νx2 ({{!}x2 (y2+ ).D2 |}D))
≡ νx2 ({{!}x2 (y2+ ).D2 |}νx1 ({{!}x1 (y1+ ).D1 |}D))
/ FV (λy2+ .D2 )
if x1 ∈
/ FV (λy1+ .D1 ), x2 ∈

(eq 2 )

νx ({{!}x(y + ).D′ |}D)
≡D
if x ∈
/ FV (D)

Reduction Rules
E[νx (!x(y + ).D | E ′ [xz + ])]
E[νx (x(y + ).D | E ′ [xz + ])]

→
→

E[νx (!x(y + ).D | E ′ [[z + /y + ]D])]
E[νx (E ′ [[z + /y + ]D])]

Typing Rules
Γ, x : A ⊢ D
Γ ⊢π νx D

π

(ν )

(out π )

x : Ch(A+ ), y + : A+ ∈ Γ
Γ ⊢π xy +

π

(ν − in )

(|π )

Γ, y + : A+ ⊢π D′
Γ, x : Ch(A+ ) ⊢π D
Γ ⊢π νx ({!}x(y + ).D′ | D)
Γ ⊢π Mi i = 1, 2
Γ ⊢π (M1 | M2 )

Table 15: A concurrent π-calculus: π

B

Expressivity

This section illustrates the expressivity of the λak -calculus (and therefore of the related λak
k and
π-calculi) as far as the programming of some familiar concepts in concurrent programming is
concerned.

B.1

Output prefix

An ‘output prefix’ @(x, y).D is simulated by the usual continuation passing trick:
let1 k = λw.D in
@(x, y, k)

B.2

Internal choice

We introduce an ‘internal choice’ operator ⊕ by defining M ⊕ N as follows (all variables being
fresh):
let x = ∗
in
let1 y = λk.@(@(k, y), x) in
let1 k1 = λw.M
in
let1 k2 = λw.N
in
(@(y, k1 ) | @(y, k2 ))

15

B.3

External choice

An ‘external choice’ between M and N based on a boolean value (coded as a projection) can
be defined as follows:
let x = ∗
in
let1 y = λz.@(@(z, λw.M, λw.N ), x) in
···

B.4

Multiple definitions

One can add to the language the possibility of having multiple definitions of the same name.
let x = V1 or
···
or
x = Vn in · · ·
where V1 , . . . , Vn do not depend on x. This does not compromise termination because a
multiple definition can be simulated by a unique definition that receives its arguments and
then performs an internal choice among the n branches.

B.5

Joined definitions

One can also add to the language the possibility of having joined definitions (in the direction
of Fournet and Gonthier join-calculus).
let x1 = V1 join
···
join
xn = Vn in · · ·
where Vi can only depend on x1 , . . . , xi−1 . The intended semantics is that the definitions of
x1 , . . . , xn can be used only simultaneously. Clearly, a joined definition can be simulated by
a usual one and thus the termination property is not compromised.

B.6

Lock/Unlock

One can use the joined definitions to define a lock/unlock mechanism:
let x = ∗
in
let unlock = λw. · · ·
join
let lock = λk.@(k, unlock ) in
(@(unlock , x) | M [lock ])
Here M [lock ] is composed of several threads that may invoke the lock definition. When the
lock is acquired the thread receives the name unlock and invoking it amounts to release the
lock (this is a rudimentary mechanism and no effort is made to to enforce a correct usage).

16

B.7

CCS channel manager

Another possible use of the joined definitions is to define a CCS channel manager:
let x = ∗
in
let in = λk.@(k, x) join
let out = λk.@(k, x) in
M [in, out ]
Here M is composed of parallel threads trying to synchronize on a channel.

C

Proofs

The functional case being a special case of the concurrent one, we focus directly on the proofs
of the latter. There is one exception: in the concurrent case in administrative, CPS form we
fix the type of results to be the behavior type b rather than an arbitrary (value) type R but
this does not affect the structure of the proofs.

C.1

Proof of proposition 4

The simple idea idea is to simulate the λk -calculus in an ordinary simply typed λ-calculus
equipped with a distinguished variable p of type (b → b) → b. More precisely, let λp be a
simply typed λ-calculus with two basic types 1 and b, a constant ∗, and a distinguished variable
p. It is well-known that such calculus terminates under an arbitrary reduction strategy. For
our purposes, it suffices to consider a reduction strategy where a call-by-value redex (λx.M )V
is reduced in a context that does not cross a λ.
Next let us define a translation h i from λk to to λp which is the identity on types (hαi =
α) and type contexts and commutes with all the operators of the terms but on parallel
composition where it is defined as follows:
hM | N i = (phM i)hN i .
The translation is also extended to evaluation contexts where in particular:
hE[[ ] | M ]i = hEi[(p[ ])hM i]

hE[M | [ ]]i = hEi[(phM i)[ ]]

Then it is easy to check the following properties:
1. If Γ ⊢ M : α then hΓi, p : b → (b → b) ⊢ hM i : α.
2. h[V /x]M i = [hV i/x]hM i.
3. hE[M ]i = hEi[hM i].
It follows that if M → N in λk then hM i → hN i in λp . Thus since λp terminates, λk must
terminate too.
✷

17

C.2

Proof of theorem 5

(1) As a preliminary remark notice that if V is a value and D a declaration in λak then
FV (V o ) ⊆ FV (V ) and FV (D o ) ⊆ FV (D). Then we proceed by case analysis on the structural congruence by applying the properties of substitutions.
(2) By induction on the structure of M term of λk .
(3) By induction on the typing of Γ ⊢ M : α in λk . For instance, suppose we derive
Γ ⊢ λx.M : A → α from Γ, x : A ⊢ M : α. Then by inductive hypothesis, Γ, x : A ⊢am M : α.
Also, Γ, x : A → α ⊢am x : A → α, where by definition A → α = N (A → α). Then we can
conclude Γ ⊢am let x = λx.M in x : A → α as required.
(4) First, we prove a substitution lemma for λk , namely: if Γ, x : A ⊢ M : α and Γ ⊢ V : A
then Γ ⊢ [V /x]M : α. Then we proceed by induction on the typing of Γ ⊢ D : α in λak,∞ .
(5) Let F and E be one hole contexts composed of parallel compositions and applications,
respectively:
F

E ::= [ ] | @(id ∗ , E, M ∗ ) .

::= [ ] | (F | M ) | (M | F ),

If D1 is well-typed and reduces then it has the shape:
let (x = V )∗ in F [E[@(x, z + )]]
and x is associated with a value λy + .D ′ . Then D1 → D2 where:
D2 ≡ let (x = V )∗ in F [E[[z + /y + ]D ′ ]] .
We extend the read-back translation to F and E by defining:
[ ]o = [ ] (F | M )o = F o | M o
(M | F )o = M o | F o
o) .
o
@(x1 , . . . , xn , E, M1 , . . . , Mm ) = (· · · (((x1 · · · xn )E o )M1o ) · · · Mm
Let σ be the (iterated) substitution [V o /x]∗ . We notice that:
M1 ≡ D1o = σ(F o [E o [xz + ]]) = (σF o )[σE o [σ(xz + )]] .
Recalling that (λy + .D ′ )o = λy + .(D ′ )o , we have that M1 performs as many reductions as there
are arguments z + and reduces to (assuming suitable renaming of bound variables):
M2 ≡ (σF o )[(σE o )[[σz + /y + ](σ(D ′ )o )] .
On the other hand, we notice that:
D2o ≡ (σF o )[(σE o )[σ([z + /y + ](D ′ )o )]] .
Knowing that the variables y + do not appear in the domain or codomain of the substitution
σ, we apply the properties of substitution to check that:
[σz + /y + ](σ(D ′ )o ) ≡ σ([z + /y + ](D ′ )o ) .

18

(6) Suppose D1 is typable in the monadic fragment λam
k . The following table describes how
o
the structure of the readback M1 ≡ (D1 ) determines D1 up to structural congruence.
M1
x
∗
λy.M ′
M1 M2
(M1 | M2 )

D1 ≡
x
let x = ∗ in x
let (x = V )∗ in let z = λy.D′ in z and M ′ ≡ (let (x = V )∗ in D′ )o
let (x = V )∗ in @(N1 , N2 ) and Mi ≡ (let (x = V )∗ in Ni )o , i = 1, 2
let (x = V )∗ in (N1 | N2 ) and Mi ≡ (let (x = V )∗ in Ni )o , i = 1, 2

Suppose M1 ≡ D1o . Notice that M1 is typable because the readback translation preserves
typing (property 4). Then if M1 reduces, it must have the shape M1 = F [E[(λx.M ′ )V ]],
where F ::= [ ] | (F | M ) | (M | F ) and E ::= [ ] | EM | V E. The reduced term is
M2 = F [E[[V /x]M ′ ]]. Let σ be the (iterated) substitution [V o /x]∗ . By the table above, we
derive that D1 must have the shape let (x = V )∗ in F ′ [E ′ [@(x1 , x2 )]] with:
σ(F ′ )o = F,
σ(x1 ) = λx.M ′ ,

σ(E ′ )o = E,
σ(x2 ) = V .

In particular, we see that the variable x1 must occur in the list of let declarations and it must
be associated with a λ-abstraction, say λx.D ′ where:
(let (x = V )∗ in D ′ )o ≡ σ(D ′ )o ≡ M ′ .
This means that D1 can also perform one reduction and reduce to
D2 ≡ let (x = V )∗ in F ′ [E ′ [[x2 /x]D ′ ]] .
We observe that:
D2o ≡ (σ(F ′ )o )[σ(E ′ )o [σ([x2 /x](D ′ )o )]]
Knowing that the variable x does not appear in the domain or codomain of the substitution
σ, we apply the properties of substitution to check that:
σ([x2 /x](D ′ )o ) ≡ [σ(x2 )/x](σ(D ′ )o ) ≡ [V /x]M ′ .
✷

C.3

Proof of theorem 7

(1) By induction on the proof of Γ ⊢a D : α and case analysis on the definition of D : k. We
spell out the following case:
Γ ⊢a @(M, M + ) : N (A+ → α) Γ ⊢a N + : A+
Γ ⊢a @(@(M, M + ), N + ) : α
We use the following abbreviations:
A′ ≡ N (A+ → α),

M ′ ≡ @(M, M + ),

Γ′ ≡ Γ, k : K(α) .

We have to show:
Γ′ ⊢a let k′ = λy.@(y, N + ) : k in (M ′ : k′ ) : b
19

By weakening, we derive Γ, y : A′ ⊢a @(y, N + ) : α. Then by induction hypothesis we have:
Γ′ , y : A′ ⊢a (@(y, N + ) : k) : b .
Also, by induction hypothesis on Γ ⊢a M ′ : A′ we derive:
Γ, k ′ : K(A′ ) ⊢a (M ′ : k′ ) : b .
Noticing that K(A′ ) = N (A′ → b) we conclude by applying the rule for the let.
(2) As a preliminary remark, we notice that structural congruence is preserved by the CPS
translation, namely D ≡ D ′ in λa entails (D : k) ≡ (D ′ : k). We introduce some additional
notation for evaluation contexts. We denote with F a one hole context composed of parallel
compositions:
F ::= [ ] | F | M | M | F .
We denote with H an elementary applicative context of the shape @(id ∗ , [ ], M ∗ ). If the
declaration D in λak is typable and reduces then it must have the following shape:
letu (x = V )∗ in F [H1 [· · · Hm [@(x, z + )] · · · ]]
where the name x is associated with a value λy + .D ′ . Then the reduced term is:
letu (x = V )∗ in F [H1 [· · · Hm [[z + /y + ]D ′ )] · · · ]]
The CPS translation of the declaration D has the following shape:
letu (x = ψ(V ))∗ in (F [H1 [· · · Hm [@(x, z + )] · · · ]] : k)
Recalling that the CPS translation distributes over parallel composition, we define:
[ ] : k = [ ],

(F | M ) : k = (F : k) | (M : k),

(M | F ) : k = (M : k) | (F : k) .

Then we have:
F [H1 [· · · Hm [@(x, z + )] · · · ]] : k = (F : k)[ let1 k1 = λy.(H1 [y] : k) in
let1 k2 = λy.(H2 [y] : k1 ) in
···
let1 km = λy.(Hm [y] : km−1 ) in
@(x, z + , km ) ]
Recalling that ψ(λy + .D ′ ) = λy + , k.(D ′ : k), we observe that the CPS translation is ready to
perform the corresponding reduction. Then we proceed by case analysis on the shape of D ′
to show that the CPS translation reduces to:
letu (x = ψ(V ))∗ in (F [H1 [· · · Hm [[z + /y + ]D ′ ] · · · ]] : k)
1. D ′ ≡ letu′ (x′ = V ′ )∗ in x′ . Then the CPS translation performs a first reduction by
replacing @(x, z + , km ) with
[z + /y + , km /k](letu′ (x′ = ψ(V ′ ))∗ in @(k, x′ )) .
If there is no enclosing elementary evaluation context, i.e. m = 0, km = k, we are done.
Otherwise, the CPS translation performs an additional reduction along the continuation
km . Following this reduction the let definition of km can be removed applying the second
rule of structural congruence.
20

2. D ′ ≡ letu′ (x′ = V ′ )∗ in @(M ′ , M ′+ ). Then the CPS translation performs a reduction
replacing @(x, z + , km ) with
[z + /y + , km /k](letu′ (x′ = ψ(V ′ ))∗ in (@(M ′ , M ′+ ) : k)) .
3. D ′ ≡ letu′ (x′ = V ′ )∗ in (M1 | M2 ). In this case, the typing requires that there are no
enclosing elementary evaluations contexts, i.e. m = 0, km = k. The CPS translation
performs a reduction replacing @(x, z + , km ) with
[z + /y + , km /k](letu′ (x′ = ψ(V ′ ))∗ in (M1 : k) | (M2 : k)) .

Acknowledgment
The author acknowledges the financial support of the Future and Emerging Technologies (ET) program within
the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number:
243881 (project CerCo).

21

