arXiv:1110.2350v2 [] 16 Jan 2013

Certifying and reasoning about
cost annotations of functional programs ∗
Roberto M. Amadio(1)

Yann Régis-Gianas(2)

(1)

(2)

Université Paris Diderot (UMR-CNRS 7126)
Université Paris Diderot (UMR-CNRS 7126) and INRIA (Team πr2 )

April 11, 2018

Abstract
We present a so-called labelling method to insert cost annotations in a higher-order
functional program, to certify their correctness with respect to a standard, typable compilation chain to assembly code including safe memory management, and to reason about
them in a higher-order Hoare logic.

1

Introduction

In previous work [2, 3], we have discussed the problem of building a C compiler which can
lift in a provably correct way pieces of information on the execution cost of the object code
to cost annotations on the source code. To this end, we have introduced a so called labelling
approach and presented its application to a prototype compiler written in OCaml from a large
fragment of the C language to the assembly languages of Mips and 8051, a 32 bits and 8 bits
processor, respectively.
In the following, we are interested in extending the approach to (higher-order) functional
languages. On this issue, a common belief is well summarized by the following epigram by
A. Perlis [22]: A Lisp programmer knows the value of everything, but the cost of nothing.
However, we shall show that, with some ingenuity, the methodology developed for the C
language can be lifted to functional languages.

1.1

A standard compilation chain

Specifically, we shall focus on a rather standard compilation chain from a call-by-value λcalculus to a register transfer level (RTL) language. Similar compilation chains have been
explored from a formal viewpoint by Morrisett et al. [21] (with an emphasis on typing but
with no simulation proofs) and by Chlipala [9] (for type-free languages but with machine
certified simulation proofs).
∗
An extended abstract with the same title without proofs and not accounting for the typing of the compilation chain and the memory management of the compiled code has appeared in [4]. Also the present version
introduces a prototype implementation available in [24]. The authors were supported by the Information and
Communication Technologies (ICT) Programme as Project FP7-ICT-2009-C-243881 CerCo.

1

λM o

I

λI ℓ

Ccps

Cvn

/ λℓ

er

L

λ

k

cps

Ccps

-

λℓcps,vn
-



R

er



/ λcps k

Ccc

/ λℓ
cc,vn

Ccc



er
Cvn
R

λcps,vn

Ch

/ λℓ
h,vn

Ch



er

/ λcc,vn

er

/ λh,vn

Table 1: The compilation chain with its labelling and instrumentation.
The compilation chain is described in the lower part of Table 1. Starting from a standard
call-by-value λ-calculus with pairs, one performs first a CPS translation, then a transformation
that gives names to values, followed by a closure conversion, and a hoisting transformation.
All languages considered are subsets of the initial one though their evaluation mechanism is
refined along the way. In particular, one moves from an ordinary substitution to a specialized
one where variables can only be replaced by other variables. One advantage of this approach,
as already noted for instance by Fradet and Le Métayer [14], is to have a homogeneous
notation that makes correctness proofs simpler.
Notable differences with respect to Chlipala’s compilation chain [9] is a different choice of
the intermediate languages and the fact that we rely on a small-step operational semantics. We
also diverge from Chlipala [9] in that our proofs, following the usual mathematical tradition,
are written to explain to a human why a certain formula is valid rather than to provide a
machine with a compact witness of the validity of the formula.
The final language of this compilation chain can be directly mapped to a RTL language:
functions correspond to assembly level routines and the functions’ bodies correspond to sequences of assignments on pseudo-registers ended by a tail recursive call.

1.2

The labelling approach to cost certification

While the extensional properties of the compilation chain have been well studied, we are not
aware of previous work focusing on more intensional properties relating to the way the compilation preserves the complexity of the programs. Specifically, in the following we will apply
to this compilation chain the ‘labelling approach’ to building certified cost annotations. In a
nutshell the approach consists in identifying, by means of labels, points in the source program
whose cost is constant and then determining the value of the constants by propagating the
labels along the compilation chain and analysing small pieces of object code with respect to
a target architecture.
Technically the approach is decomposed in several steps. First, for each language considered in the compilation chain, we define an extended labelled language and an extended
operational semantics (upper part of Table 1). The labels are used to mark certain points
of the control. The semantics makes sure that, whenever we cross a labelled control point, a
labelled and observable transition is produced.
Second, for each labelled language there is an obvious function er erasing all labels and
producing a program in the corresponding unlabelled language. The compilation functions
are extended from the unlabelled to the labelled language so that they commute with the
respective erasure functions. Moreover, the simulation properties of the compilation functions
are lifted from the unlabelled to the labelled languages and transition systems.
Third, assume a labelling L of the source language is a right inverse of the respective
2

erasure function. The evaluation of a labelled source program produces both a value and
a sequence of labels, written Λ, which intuitively stands for the sequence of labels crossed
during the program’s execution. The central question we are interested in is whether there is
a way of labelling the source programs so that the sequence Λ is a sound and possibly precise
representation of the execution cost of the program.
To answer this question, we observe that the object code is some kind of RTL code and
that its control flow can be easily represented as a control flow graph. The fact that we have
to prove the soundness of the compilation function means that we have plenty of information
on the way the control flows in the compiled code, in particular as far as procedure calls
and returns are concerned. These pieces of information allow to build a rather accurate
representation of the control flow of the compiled code at run time.
The idea is then to perform some simple checks on the control flow graph. The main check
consists in verifying that all ‘loops’ go through a labelled node. If this is the case then we
can associate a ‘cost’ with every label which over-approximates the actual cost of running a
sequence of instructions. An optional check amounts to verify that all paths starting from a
label have the same abstract cost. If this check is successful then we can conclude that the
cost annotations are ‘precise’ in an abstract sense (and possibly concrete too, depending on
the processor considered).
In our previous work [2, 3], we have showed that it is possible to produce a sound and
precise (in an abstract sense) labelling for a large class of C programs with respect to a moderately optimising compiler. In the following we show that a similar result can be obtained for
a higher-order functional language with respect to the standard compilation chain described
above. Specifically we show that there is a simple labelling of the source program that guarantees that the labelling of the generated object code is sound and precise. The labelling of
the source program can be informally described as follows: it associates a distinct label with
every abstraction and with every application which is not ‘immediately surrounded’ by an
abstraction.
In this paper our analysis will stop at the level of an abstract RTL language, however our
previously quoted work [2, 3] shows that the approach extends to the back-end of a typical
moderately optimising compiler including, e.g., dead-code elimination and register allocation.
Concerning the source language, preliminary experiments suggest that the approach scales
to a larger functional language such as the one considered in Chlipala’s Coq development [9]
including fixpoints, sums, exceptions, and side effects. Let us also mention that our approach
has been implemented for a simpler compilation chain that bypasses the CPS translation. In
this case, the function calls are not necessarily tail-recursive and the compiler generates a
Cminor program which, roughly speaking, is a type-free, stack aware fragment of C defined in
the Compcert project [17].

1.3

Reasoning about the certified cost annotations

If the check described above succeeds every label has a cost which in general can be taken as
an element of a ‘cost’ monoid. Then an instrumentation of the source labelled language is a
monadic transformation I (left upper part of Table 1) in the sense of Gurr’s PhD thesis [15]
that replaces labels with the associated elements of the cost monoid. Following this monadic
transformation we are back into the source language (possibly enriched with a ‘cost monoid’
such as integers with addition). As a result, the source program is instrumented so as to
monitor its execution cost with respect to the associated object code. In the end, general
3

logics developed to reason about functional programs such as the higher-order Hoare logic codeveloped by one of the authors [25] can be employed to reason about the concrete complexity
of source programs by proving properties on their instrumented versions (see Table 11 for an
example of a source program with complexity assertions).

1.4

Accounting for the cost of memory management

In a realistic implementation of a functional programming language, the runtime environment
usually includes a garbage collector. In spite of considerable progress in real-time garbage
collectors (see, e.g., the work of Bacon et al. [6]), it seems to us that this approach does
not offer yet a viable path to a certified and usable WCET prediction of the running time
of functional programs. Instead, the approach we shall adopt, following the seminal work of
Tofte et al. [27], is to enrich the last calculus of the compilation chain described in Table 1, (1)
with a notion of memory region, (2) with operations to allocate and dispose memory regions,
and (3) with a type and effect system that guarantees the safety of the dispose operation. This
allows to further extend to the right with one more commuting square the compilation chain
mentioned above and then to include the cost of safe memory management in our analysis.
Actually, because effects are intertwined with types, what we shall actually do, following the
work of Morrisett et al. [21], is to extend a typed version of the compilation chain.

1.5

Related work

There is a long tradition starting from the work of Wegbreit [30] which reduces the complexity
analysis of first-order functional programs to the solution of finite difference equations. Much
less is known about higher-order functional programs. Most previous work on building cost
annotations for higher-order functional programs we are aware of does not take formally into
account the compilation process. For instance, in an early work D. Sands [26] proposes an
instrumentation of call-by-value λ-calculus in order to describe its execution cost. However
the notion of cost adopted is essentially the number of function calls in the source code. In a
standard implementation such as the one considered in this work, different function calls may
have different costs and moreover there are ‘hidden’ function calls which are not immediately
apparent in the source code.
A more recent work by Bonenfant et al. [7] addresses the problem of determining the worst
case execution time of a specialised functional language called Hume. The compilation chain
considered consists in first compiling Hume to the code of an intermediate abstract machine,
then to C, and finally to generate the assembly code of the Resenas M32C/85 processor using
standard C compilers. Then for each instruction of the abstract machine, one computes an
upper bound on the worst-case execution time (WCET) of the instruction relying on a wellknown aiT tool [5] that uses abstract interpretation to determine the WCET of sequences of
binary instructions.
While we share common motivations with this work, we differ significantly in the technical
approach. First, the Hume approach follows a tradition of compiling functional programs to
the instructions of an abstract machine which is then implemented in a C like language. In
contrast, we have considered a compilation chain that brings a functional program directly
to RTL form. Then the back-end of a C like compiler is used to generate binary instructions.
Second, the cited work [7] does not address at all the proof of correctness of the cost annotations; this is left for future work. Third, the problem of producing synthetic cost statements

4

starting from the cost estimations of the abstract instructions of the Hume machine is not
considered. Fourth, the cost of dynamic memory management, which is crucial in higher-order
functional programs, is not addressed at all. Fifth, the granularity of the cost annotations is
fixed in Hume [7] (the instructions of the Hume abstract machine) while it can vary in our
approach.
We also share with the Hume approach one limitation. The precision of our analyses
depends on the possibility of having accurate predictions of the execution time of relatively
short sequences of binary code on a given processor. Unfortunately, as of today, user interfaces
for WCET systems such as the aiT tool mentioned above or Chronos [19] do not support
modular reasoning on execution times and therefore experimental work focuses on processors
with simple and predictable architectures. In a related direction, another potential loss of
precision comes from the introduction of aggressive optimisations in the back-end of the
compiler such as loop transformations. An ongoing work by Tranquilli [28] addresses this
issue by introducing a refinement of the labelling approach.

1.6

Paper organisation

In the following, section 2 describes the certification of the cost-annotations, section 3 a
method to reason about the cost annotations, section 4 the typing of the compilation chain,
and section 5 an extension of the compilation chain to account for safe memory deallocation.
Proofs are available in the appendix A.

2

The compilation chain: commutation and simulation

We describe the intermediate languages and the compilation functions from an ordinary λcalculus to a hoisted, value named λ-calculus. For each step we check that: (i) the compilation
function commutes with the function that erases labels and (ii) the object code simulates the
source code.

2.1

Conventions

The reader is assumed to be acquainted with the type-free and typed λ-calculus, its evaluation
strategies, and its continuation passing style translations [29]. In the following calculi, all
terms are manipulated up to α-renaming of bound names. We denote with ≡ syntactic
identity up to α-renaming. Whenever 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. With this assumption, we can omit obvious side conditions on binders
and free variables. Similar conventions are applied when reasoning about 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 .
Let C, C1 , C2 , . . . be one hole contexts and T a term. Then C[T ] is the term resulting
from the replacement in the context C of the hole by the term T and C1 [C2 ] is the one hole
context resulting from the replacement in the context C1 of the hole by the context C2 .
For each calculus, we assume a syntactic category id of identifiers with generic elements
x, y, . . . and a syntactic category ℓ of labels with generic elements ℓ, ℓ1 , . . . For each calculus,
we specify the syntactic categories and the reduction rules. For the sake of clarity, the metavariables of these syntactic categories are sometimes shared between several calculus: the
5

context is always sufficiently precise to determine to which syntax definitions we refer. We
α
let α range over labels and the empty word ǫ. We write M −
→ N if M rewrites to N with a
ǫ
∗
transition labelled by α. We abbreviate M −
→ N with M → N . We write → for the reflexive
α
∗
∗ α ∗
and transitive closure of →. We also define M ⇒ N as M → N if α = ǫ and as M →−
→→ N
otherwise.
α1
αn
Given a term M in one of the labelled languages we write M ⇓Λ N if M −→
· · · −−→
N,
Λ = α1 · · · αn , and N cannot reduce (in general this does not imply that N is a value). We
write M ⇓Λ for ∃ N M ⇓Λ N . Also, if the term M is unlabelled, Λ is always the empty word
and we abbreviate M ⇓ǫ N with M ⇓ N .
We shall write X + (resp. X ∗ ) for a non-empty (possibly empty) finite sequence X1 , . . . , Xn
of symbols. By extension, λx+ .M stands for λx1 . . . xn .M , [V + /x+ ]M stands for
[V1 /x1 , . . . , Vn /xn ]M , and let (x = V )+ in M stands for let x1 = V1 in · · · let xn = Vn in M .

2.2

The source language

Table 2 introduces a type-free, left-to-right call-by-value λ-calculus. The calculus includes letdefinitions and polyadic abstraction and tupling with the related application and projection
operators. Any term M can be pre-labelled by writing ℓ > M or post-labelled by writing
M > ℓ. In the pre-labelling, the label ℓ is emitted immediately while in the post-labelling it
is emitted after M has reduced to a value. It is tempting to reduce the post-labelling to the
pre-labelling by writing M > ℓ as @(λx.ℓ > x, M ), however the second notation introduces
an additional abstraction and a related reduction step which is not actually present in the
original code. Roughly speaking, every λ-abstraction is a potential starting point for a loop in
the control-flow graph. Thus, we will need the body of every λ-abstraction to be pre-labelled
so as to maintain the invariant that all loops go through a labelled node in the control-flow
graph. As the CPS translation introduces new λ-abstractions that are not present in the
source code but correspond to the image of some applications, we will also need to post-label
these particular applications so that the freshly introduced λ-abstraction can be assigned a
label.
Table 2 also introduces an erasure function er from the λℓ -calculus to the λ-calculus. This
function simply traverses the term and erases all pre and post labellings. Similar definitions
arise in the following calculi of the compilation chain and are omitted.

2.3

Compilation to CPS form

Table 3 introduces a fragment of the λℓ -calculus described in Table 2 and a related CPS
translation. To avoid all ambiguity, let us assume that (V1 , . . . , Vn ) | K is translated according
to the case for values, but note that if we follow the general case for tuples we obtain the
same result. We recall that in a CPS translation each function takes its evaluation context
as a fresh additional parameter (see, e.g., the work of Wand [29], for an elaboration of this
idea). The results of the evaluation of subterms (of tuples and of applications) are also
named using fresh parameters x0 , . . . , xn . The initial evaluation context is defined relatively
to a fresh variable named ’halt ’. Then the evaluation context is always trivial. Notice that
the reduction rules are essentially those of the λℓ -calculus modulo the fact that we drop the
rule to reduce V > ℓ since post-labelling does not occur in CPS terms and the fact that we
optimize the rule for the projection to guarantee that CPS terms are closed under reduction.
For instance, the term let x = π1 (V1 , V2 ) in M reduces directly to [V1 /x]M rather than going
6

Syntax
V
M
E

::= id | λid + .M | (V ∗ )
::= V | @(M, M + ) | let id = M in M | (M ∗ ) | πi (M ) | ℓ > M | M > ℓ
::= [ ] | @(V ∗ , E, M ∗ ) | let id = E in M | (V ∗ , E, M ∗ ) | πi (E) | E > ℓ

(values)
(terms)
(eval. cxts.)

Reduction Rules
E[@(λx1 . . . xn .M, V1 , . . . , Vn )]
E[let x = V in M ]
E[πi (V1 , . . . , Vn )]

→
→
→

E[ℓ > M ]

→
−

ℓ

E[M ]

E[V > ℓ]

ℓ

E[V ]

→
−

E[[V1 /x1 , . . . , Vn /xn ]M ]
E[[V /x]M ]
E[Vi ]
1≤i≤n

Label erasure (selected equations)
er (ℓ > M ) = er (M > ℓ) = er (M )

Table 2: An ordinary call-by-value λ-calculus: λℓ
through the intermediate term let x = V1 in M which does not belong to the CPS terms.
We study next the properties enjoyed by the CPS translation. In general, the commutation of the compilation function with the erasure function only holds up to call-by-value
η-conversion, namely λx.@(V, x) =η V if x ∈
/ fv(V ). This is due to the fact that post-labelling
introduces an η-expansion of the continuation if and only if the continuation is a variable. To
cope with this problem, we introduce next the notion of well-labelled term. We will see later
(section 3.1) that terms generated by the initial labelling are well-labelled.
Definition 1 (well-labelling) We define two predicates Wi , i = 0, 1 on the terms of the
λℓ -calculus as the least sets such that W1 is contained in W0 and the following conditions
hold:
x ∈ W1

M ∈ W0
M > ℓ ∈ W0

M ∈ Wi i ∈ {0, 1}
ℓ > M ∈ Wi
Mi ∈ W0 i = 1, . . . , n
@(M1 , . . . , Mn ) ∈ W1

M ∈ W1
λx+ .M ∈ W1

N ∈ W0 , M ∈ Wi i ∈ {0, 1}
let x = N in M ∈ Wi

Mi ∈ W0 i = 1, . . . , n
(M1 , . . . , Mn ) ∈ W1

M ∈ W0
.
πi (M ) ∈ W1

The intuition is that we want to avoid the situation where a post-labelling receives as
continuation the continuation variable generated by the translation of a λ-abstraction. To
that end, we make sure that post-labelling is only applied to terms M ∈ W0 , that is, terms
that are not the immediate body of a λ-abstraction (which are in W1 ).
Example 2 (labelling and commutation) Let M ≡ λx.(@(x, x) > ℓ). Then M ∈
/ W0
because the rule for abstraction requires @(x, x) > ℓ ∈ W1 while we can only show @(x, x) >
ℓ ∈ W0 . Notice that we have:
er(Ccps (M )) ≡ @(halt , λx, k.@(x, x, λx.@(k, x)))
Ccps (er (M )) ≡ @(halt , λx, k.@(x, x, k)) .
7

So, for M , the commutation of the CPS translation and the erasure function only holds up
to η.
Proposition 3 (CPS commutation) Let M ∈ W0 be a term of the λℓ -calculus (Table 2).
Then: er (Ccps (M )) ≡ Ccps (er (M )).
The proof of the CPS simulation is non-trivial but rather standard since Plotkin’s seminal
work [23]. The general idea is that the CPS translation pre-computes many ‘administrative’
reductions so that the translation of a term, say E[@(λx.M, V )] is a term of the shape
@(ψ(λx.M ), ψ(V ), KE ) for a suitable continuation KE depending on the evaluation context E.
α

Proposition 4 (CPS simulation) Let M be a term of the λℓ -calculus. If M −
→ N then
α
Ccps (M ) ⇒ Ccps (N ).
We illustrate this result on the following example.
Example 5 (CPS) Let M ≡ @(λx.@(x, @(x, x)), I), where I ≡ λx.x. Then
Ccps (M ) ≡ @(λx, k.@(x, x, λy.@(x, y, k)), I ′ , H)
where: I ′ ≡ λx, k.@(k, x) and H ≡ λx.@(halt , x). The term M is simulated by Ccps (M ) as
follows:
M
→
@(I, @(I, I))
→
@(I, I)
→
I
′
′
′
+
′
′
+
Ccps (M ) → @(I , I , λy.@(I , y, H)) →
@(I , I , H) →
@(halt , I ′ ) .

2.4

Transformation in value named CPS form

Table 4 introduces a value named λ-calculus in CPS form: λℓcps,vn . In the ordinary λ-calculus,
the application of a λ-abstraction to an argument (which is a value) may duplicate the argument as in: @(λx.M, V ) → [V /x]M . In the value named λ-calculus, all values are named and
when we apply the name of a λ-abstraction to the name of a value we create a new copy of the
body of the function and replace its formal parameter name with the name of the argument
as in:
let y = V in let f = λx.M in @(f, y) → let y = V in let f = λx.M in [y/x]M .
We also remark that in the value named λ-calculus the evaluation contexts are a sequence
of let definitions associating values to names. Thus, apart for the fact that the values are
not necessarily closed, the evaluation contexts are similar to the environments of abstract
machines for functional languages (see, e.g., [13]).
Table 5 defines the compilation into value named form along with a readback translation.
(Only the case for the local binding of values is interesting.) The latter is useful to state the
∗
simulation property. Indeed, it is not true that if M → M ′ in λℓcps then Cvn (M ) → Cvn (M ′ ) in
λℓcps,vn . For instance, consider M ≡ (λx.xx)I where I ≡ (λy.y). Then M → II but Cvn (M )
does not reduce to Cvn (II) but rather to a term where the ‘sharing’ of the duplicated value
I is explicitly represented.

8

Syntax CPS terms
V
M
K

::= id | λid + .M | (V ∗ )
::= @(V, V + ) | let id = πi (V ) in M | ℓ > M
::= id | λid.M

(values)
(CPS terms)
(continuations)

Reduction rules
@(λx1 . . . xn .M, V1 , . . . , Vn )
let x = πi (V1 , . . . , Vn ) in M

→
→

ℓ>M

→
−

ℓ

[V1 /x1 , . . . , Vn /xn ]M
[Vi /x]M 1 ≤ i ≤ n
M

CPS translation
ψ(x)
ψ(λx+ .M )
ψ((V1 , . . . , Vn ))

=
=
=

x
λx+ , k.(M | k)
(ψ(V1 ), . . . , ψ(Vn ))

V |k
V | (λx.M )
@(M0 , . . . , Mn ) | K
let x = M1 in M2 | K
(M1 , . . . , Mn ) | K
πi (M ) | K
(ℓ > M ) | K
(M > ℓ) | K

=
=
=
=
=
=
=
=

@(k, ψ(V ))
[ψ(V )/x]M
M0 | λx0 . . . . (Mn | λxn .@(x0 , . . . , xn , K))
M1 | λx.(M2 | K)
M1 | λx1 . . . . (Mn | λxn .(x1 , . . . , xn ) | K )
M | λx.let y = πi (x) in y | K
ℓ > (M | K)
M | (λx.ℓ > (x | K))

Ccps (M )

=

M | λx.@(halt, x),

halt fresh variable

Table 3: CPS λ-calculus (λℓcps ) and CPS translation
Example 6 (value named form) Suppose
N ≡ @(λx, k.@(x, x, λy.@(x, y, k)), I ′ , H))
where: I ′ ≡ λx, k.@(k, x) and H ≡ λx.@(halt , x). (This is the term resulting from the CPS
translation in example 5.) The corresponding term in value named form is:
let z1 = λx, k.(let z11 = λy.@(x, y, k) in @(x, x, z11 )) in
let z2 = I ′ in
let z3 = H in
@(z1 , z2 , z3 ) .
Proposition 7 (VN commutation) Let M be a λ-term in CPS form. Then:
(1) R(Cvn (M )) ≡ M .
(2) er (Cvn (M )) ≡ Cvn (er (M )).
Proposition 8 (VN simulation) Let N be a λ-term in CPS value named form. If R(N ) ≡
α
α
M and M −
→ M ′ then there exists N ′ such that N −
→ N ′ and R(N ′ ) ≡ M ′ .

9

Syntax
V
C
M
E

::= λid + .M | (id ∗ )
::= V | πi (id)
::= @(id, id + ) | let id = C in M | ℓ > M
::= [ ] | let id = V in E

(values)
(let-bindable terms)
(CPS terms)
(evaluation contexts)

Reduction Rules
E[@(x, z1 , . . . , zn )]
E[let z = πi (x) in M ]

→
→

E[ℓ > M ]

→
−

E[[z1 /y1 , . . . , zn /yn ]M ]
E[[yi /z]M ]]

if E(x) = λy1 . . . yn .M
if E(x) = (y1 , . . . , yn ), 1 ≤ i ≤ n

ℓ

E[M ]

if E = E ′ [let x = V in [ ]]
 V
′
E (x)
if E = E ′ [let y = V in [ ]], x 6= y
where: E(x) =

undefined otherwise

Table 4: A value named CPS λ-calculus: λℓcps,vn

2.5

Closure conversion

The next step is called closure conversion. It consists in providing each functional value with
an additional parameter that accounts for the names free in the body of the function and in
representing functions using closures. Our closure conversion implements a closure using a
pair whose first component is the code of the translated function and whose second component
is a tuple of the values of the free variables.
It will be convenient to write “let (y1 , . . . , yn ) = x in M ” for “let y1 = π1 (x) in · · · let yn =
πn (x) in M ” and “let x1 = C1 . . . xn = Cn in M ” for “let x1 = C1 in . . . let xn = Cn in M ”.
The transformation is described in Table 6. The output of the transformation is such that
all functional values are closed. In our opinion, this is the only compilation step where the
proofs are rather straightforward.
Example 9 (closure conversion) Let M ≡ Cvn (Ccps (λx.y)), namely
M ≡ let z1 = λx, k.@(k, y) in @(halt , z1 ) .
Then Ccc (M ) is the following term:
let c = λe, x, k.(let (y) = e, (c, e) = k in @(c, e, y)) in
let e = (y), z1 = (c, e), (c, e) = halt in
@(c, e, z1 ) .
Proposition 10 (CC commutation) Let M be a CPS term in value named form. Then
er (Ccc (M )) ≡ Ccc (er (M )).
α

Proposition 11 (CC simulation) Let M be a CPS term in value named form. If M −
→ M′
α
then Ccc (M ) ⇒ Ccc (M ′ ).

10

Transformation in value named form (from λℓcps to λℓcps,vn )
Cvn (@(x0 , . . . , xn ))
Cvn (@(x∗ , V, V ∗ ))
Cvn (let x = πi (y) in M )
Cvn (let x = πi (V ) in M )
Cvn (ℓ > M )

=
=
=
=
=

@(x0 , . . . , xn )
Evn (V, y)[Cvn (@(x∗ , y, V ∗ ))] V 6= id, y fresh
let x = πi (y) in Cvn (M )
Evn (V, y)[let x = πi (y) in Cvn (M )] V 6= id, y fresh
ℓ > Cvn (M )

Evn (λx+ .M, y)
Evn ((x∗ ), y)
Evn ((x∗ , V, V ∗ ), y)

=
=
=

let y = λx+ .Cvn (M ) in [ ]
let y = (x∗ ) in [ ]
Evn (V, z)[Evn ((x∗ , z, V ∗ ), y)]

V 6= id, z fresh

Readback translation (from λℓcps,vn to λℓcps )
R(λx+ .M )
R(x∗ )
R(@(x, x1 , . . . , xn ))
R(let x = πi (y) in M )
R(let x = V in M )
R(ℓ > M )

=
=
=
=
=
=

λx+ .R(M )
(x∗ )
@(x, x1 , . . . , xn )
let x = πi (y) in R(M )
[R(V )/x]R(M )
ℓ > R(M )

Table 5: Transformations in value named CPS form and readback

2.6

Hoisting

The last compilation step consists in moving all functions definitions at top level. In Table 7,
we formalise this compilation step as the iteration of a set of program transformations that
commute with the erasure function and the reduction relation. Denote with λz + .T a function
that does not contain function definitions. The transformations consist in hoisting (moving
up) the definition of a function λz + .T with respect to either a definition of a pair or a projection, or another including function, or a labelling. Note that the hoisting transformations
do not preserve the property that all functions are closed. Therefore the hoisting transformations are defined on the terms of the λℓcps,vn -calculus. As a first step, we analyse the hoisting
transformations.
Proposition 12 (on hoisting transformations) The iteration of the hoisting transformation on a term in λℓcc,vn (all function are closed) terminates and produces a term satisfying
the syntactic restrictions specified in Table 7.
Next we check that the hoisting transformations commute with the erasure function.
Proposition 13 (hoisting commutation) Let M be a term of the λℓcps,vn -calculus.
(1) If M ❀ N then er(M ) ❀ er (N ) or er (M ) ≡ er (N ).
(2) If M 6❀ · then er (M ) 6❀ ·.
(3) er (Ch (M )) ≡ Ch (er (M )).
The proof of the simulation property requires some work because to close the diagram we
need to collapse repeated definitions, which may occur, as illustrated in the example below.
Example 14 (hoisting transformations and transitions) Let
M ≡ let x1 = λy1 .N in @(x1 , z)
11

Syntactic restrictions on λℓcps,vn after closure conversion
All functional values are closed.
Closure Conversion
Ccc (@(x, y + ))

= let (c, e) = x in @(c, e, y + )

Ccc (let x = C in M )

let c = λe, x+ .let (z1 , . . . , zk ) = e in Ccc (N ) in
let e = (z1 , . . . , zk ) in
=
let x = (c, e) in
Ccc (M )
(if C = λx+ .N, fv(C) = {z1 , . . . , zk })

Ccc (let x = C in M )

= let x = C in Ccc (M )

Ccc (ℓ > M )

= ℓ > Ccc (M )

(if C not a function)

Table 6: Closure conversion on value named CPS terms
where N ≡ let x2 = λy2 .T2 in T1 and y1 ∈
/ fv(λy2 .T2 ). Then we either reduce and then hoist:
M

→ let x1 = λy1 .N in [z/y1 ]N
≡ let x1 = λy1 .N in let x2 = λy2 .T2 in [z/y1 ]T1
❀ let x2 = λy2 .T2 in let x1 = λy1 .T1 in let x2 = λy2 .T2 in [z/y1 ]T1 6❀

or hoist and then reduce:
M

❀ let x2 = λy2 .T2 in let x1 = λy1 .T1 in @(x1 , z)
→ let x2 = λy2 .T2 in let x1 = λy1 .T1 in [z/y1 ]T1

6❀

In the first case, we end up duplicating the definition of x2 .
We proceed as follows. First we introduce a relation Sh that collapses repeated definitions
and show that it is a simulation. Second, we show that the hoisting transformations induce a
ℓ
ℓ
‘simulation up to Sh ’. Namely if M −
→ M ′ and M ❀ N then there is a N ′ such that N −
→ N′
and M ′ (❀∗ ◦Sh ) N ′ . Third, we iterate the previous property to derive the following one.
Proposition 15 (hoisting simulation) There is a simulation relation Th on the terms of
the λℓcps,vn -calculus such that for all terms M of the λℓcc,vn -calculus we have M Th Ch (M ).

2.7

Composed commutation and simulation properties

Let C be the composition of the compilation steps we have considered:
C = Ch ◦ Ccc ◦ Cvn ◦ Ccps .
We also define a relation RC between terms in λℓ and terms in λℓh as:
M RC P if ∃ N Ccps (M ) ≡ R(N ) and Ccc (N ) Th P .
Notice that for all M , M RC C(M ).
Theorem 16 (commutation and simulation) Let M ∈ W0 be a term of the λℓ -calculus.
Then:
(1) er (C(M )) ≡ C(er (M )).
α
α
(2) If M RC N and M −
→ M ′ then N ⇒ N ′ and M ′ RC N ′ .
12

Syntax for λℓh
Syntactic restrictions on λℓcps,vn after hoisting
All function definitions are at top level.
C
T
P

::= (id ∗ ) | πi (id )
::= @(id, id + ) | let id = C in T | ℓ > T
::= T | let id = λid + .T in P

(restricted let-bindable terms)
(restricted terms)
(programs)

Specification of the hoisting transformation
Ch (M ) = N if M ❀ · · · ❀ N 6❀,
D

::=
(h1 )

(h2 )

(h3 )

where:

+

[ ] | let id = C in D | let id = λid .D in M | ℓ > D

(hoisting contexts)

D[let x = C in let y = λz + .T in M ] ❀
D[let y = λz + .T in let x = C in M ]

if x ∈
/ fv(λz + .T )

D[let x = (λw+ .let y = λz + .T in M ) in N ] ❀
D[let y = λz + .T in let x = λw+ .M in N ]

if {w+ } ∩ fv(λz + .T ) = ∅

D[ℓ > let y = λz + .T in M ] ❀
D[let y = λz + .T in ℓ > M ]

Table 7: Hoisting transformation

3

Reasoning about the cost annotations

We describe an initial labelling of the source code leading to a sound and precise labelling
of the object code and an instrumentation of the labelled source program which produces a
source program monitoring its own execution cost. Then, we explain how to obtain static
guarantees on this execution cost by means of a Hoare logic for purely functional programs.

3.1

Initial labelling

We define a labelling function L of the source code (terms of the λ-calculus) which guarantees
that the associated RTL code satisfies the conditions necessary for associating a cost with
each label. We set L(M ) = L0 (M ), where the functions Li are specified in Table 8. When
the index i in Li is equal to 1, it attests that M is an immediate body of a λ-abstraction. In
that case, even if M is an application, it is not post-labelled. Otherwise, when i is equal to 0,
the term M is not an immediate body of a λ-abstraction, and, thus is post-labelled if it is an
application.
Example 17 (labelling application) Let M ≡ λx.@(x, @(x, x)). Then L(M ) ≡ λx.ℓ0 >
@(x, @(x, x) > ℓ1 ). Notice that only the inner application is post-labelled.
Proposition 18 (labelling properties) Let M be a term of the λ-calculus.
(1) The function L is a labelling and produces well-labelled terms, namely:
er (Li (M )) ≡ M and Li (M ) ∈ Wi for i = 0, 1.
(2) We have: C(M ) ≡ er(C(L(M ))).
13

L(M )

=

L0 (M )

Li (x)
Li (λx+ .M )
Li ((M1 , . . . , Mn ))
Li (πj (M ))

=
=
=
=

Li (@(M, N + ))

=

Li (let x = M in N )

=

x
λx+ .ℓ > L1 (M ) ℓ fresh
(L0 (M1 ), . . . , L0 (Mn ))
π
j (L0 (M ))
@(L0 (M ), (L0 (N ))+ ) > ℓ
@(L0 (M ), (L0 (N ))+ )
let x = L0 (M ) in Li (N )

where:

i = 0, ℓ fresh
i=1

Table 8: A sound and precise labelling of the source code
(3) Labels occur exactly once in the body of each function definition and nowhere else, namely,
C(L(M )) is a term P specified by the following grammar:
P
Tlab
T
C

::= T | let id = λid + .Tlab in P
::= ℓ > T | let id = C in Tlab
::= @(id , id + ) | let id = C in T
::= (id ∗ ) | πi (id )

Point (2) of the proposition above depends on the commutation property of the compilation function (theorem 16(1)). The point (3) entails that a RTL program generated by the
compilation function is composed of a set of routines and that each routine is composed of a
sequence of assignments on pseudo-registers and a terminal call to another routine. Points (2)
and (3) entail that the only difference between the compiled code and the compiled labelled
code is that in the latter, upon entering a routine, a label uniquely associated with the routine
is emitted.
Now suppose we can compute the cost of running once each routine, where the cost is
an element of a suitable commutative monoid M with binary operation ⊕ and identity 0
(the reader may just think of the natural numbers). Then we can define a function costof
which associates with every label the cost of running once the related routine; the function
costof is extended to words of labels in the standard way. A run of a terminating program
M corresponds to a finite sequence of routine calls which in turn correspond to the finite
sequence of labels that we can observe when running the labelled program. We summarise
this argument in the following proviso (a modelling hypothesis rather than a mathematical
proposition).
Proviso 19 For any term M of the source language, if C(L(M )) ⇓Λ then costof(Λ) is the
cost of running M .
We stress that the model at the level of the RTL programs is not precise enough to obtain
useful predictions on the execution cost in terms, say, of CPU cycles. However, the compilation
chain of this paper can be composed with the back-end of a moderately optimising C compiler
described in our previous work [2, 3]. For RTL programs such as those characterized by the
grammar above, the back end produces binary code which satisfies the checks for soundness
and precision that we outlined in the introduction. This remains true even if the source
language is enriched with other constructions such as branching and loops as long as the
labelling function is extended to handle these cases.
14

ψ(x)
ψ(λx+ .M )
ψ(V1 , . . . , Vn )

=
=
=

x
λx+ .I(M )
(ψ(V1 ), . . . , ψ(Vn ))

I(V )
I(@(M0 , . . . , Mn ))

=
=

I((M1 , . . . , Mn ))

=

I(πi (M ))
I(let x = M1 in M2 )

=
=

I(ℓ > M )
I(M > ℓ)

=
=

(0, ψ(V ))
let (m0 , x0 ) = I(M0 ) · · · (mn , xn ) = I(Mn ),
(mn+1 , xn+1 ) = @(x0 , . . . , xn ) in
(m0 ⊕ m1 ⊕ · · · ⊕ mn+1 , xn+1 )
let (m1 , x1 ) = I(M1 ) · · · (mn , xn ) = I(Mn ) in
(m1 ⊕ · · · ⊕ mn , (x1 , . . . , xn )) ((M1 , . . . , Mn ) not a value)
let (m, x) = I(M ) in (m, πi (x))
let (m1 , x) = I(M1 ) in (m2 , x2 ) = I(M2 ) in
(m1 ⊕ m2 , x2 )
let (m, x) = I(M ) in (mℓ ⊕ m, x)
let (m, x) = I(M ) in (m ⊕ mℓ , x)

Table 9: Instrumentation of labelled λ-calculus.

3.2

Instrumentation

As already mentioned, given a cost monoid M, we assume the analysis of the RTL code
associates with each label ℓ in the term an element mℓ = costof(ℓ) of the cost monoid.
Table 9 describes a monadic transformation, extensively analysed in Gurr’s PhD thesis [15],
which instruments a program (in our case λℓ ) with the cost of executing its instructions. We
are then back to a standard λ-calculus (without labels) which includes a basic data type to
represent the cost monoid.
We assume that the reduction rules of the source language (λ) are extended to account
for a call-by-value evaluation of the monoidal expressions, where each element of the monoid
is regarded as a value. Then instrumentation and labelling are connected as follows.
Proposition 20 (instrumentation vs. labelling) Let M be a term of the source labelled
language λℓ . If I(M ) ⇓ (m, V ) where V is a value then M ⇓Λ U , costof(Λ) = m, and
I(U ) = (0, V ).
The following result summarizes the labelling approach to certified cost annotations.
Theorem 21 (certified cost) Let M be a term of the source language λ. If π1 (I(L(M ))) ⇓
m then the cost of running C(M ) is m.
Proof. We take the following steps:
π1 (I(L(M ))) ⇓ m
implies L(M ) ⇓Λ and costof(Λ) = m
(by proposition 20 above)
implies C(L(M )) ⇓Λ and costof(Λ) = m (by the simulation theorem 16(2)).
By proposition 18 and the following proviso 19, we conclude that m is the cost of running the
compiled code C(M ).
✷

3.3

Higher-order Hoare Logic

Many proof systems can be used to obtain static guarantees on the evaluation of a purely
functional program. In our setting, such systems can also be used to obtain static guarantees
on the execution cost of a functional program by reasoning about its instrumentation.
15

Syntax
F

::=

θ
V
M

::=
::=
::=

True | False | x | F ∧ F | F = F | (F, F )
| π1 | π2 | λ(x : θ).F | F F | F ⇒ F | ∀(x : θ).F
prop | ι | θ × θ | θ → θ
id | λ(id : A)+ /F : (id : A)/F.M | (V ∗ )
V | @(M, M + ) | let id : A/F = M in M | (M ∗ ) | πi (M )

(formulae)
(types)
(values)
(terms)

Logical reflection of types
⌈ι⌉
⌈A1 × . . . × An ⌉
⌈A1 → A2 ⌉

=
=
=

ι
⌈A1 ⌉ × . . . ⌈An ⌉
(⌈A1 ⌉ → prop) × (⌈A1 ⌉ × ⌈A2 ⌉ → prop)

Logical reflection of values
⌈id⌉
⌈(V1 , . . . , Vn )⌉
⌈λ(x1 : A1 )/F1 : (x2 : A2 )/F2 . M ⌉

=
=
=

id
(⌈V1 ⌉, . . . , ⌈Vn ⌉)
(F1 , F2 )

Table 10: The surface language.
We illustrate this point using a Hoare logic dedicated to call-by-value purely functional
programs [25]. Given a well-typed program annotated by logic assertions, this system computes a set of proof obligations, whose validity ensures the correctness of the logic assertions
with respect to the evaluation of the functional program.
Logic assertions are written in a typed higher-order logic whose syntax is given in Table 10.
From now on, we assume that our source language is also typed. The metavariable A ranges
over simple types, whose syntax is A ::= ι | A × A | A → A where ι are the basic types
including a data type cm for the values of the cost monoid. The metavariable θ ranges over
logical types. prop is the type of propositions. Notice that the inhabitants of arrow types
on the logical side are purely logical (and terminating) functions, while on the programming
language’s side they are computational (and potentially non-terminating) functions. Types
are lifted to the logical level through a logical reflection ⌈•⌉ defined in Table 10.
We write “let x : A/F = M in M ” to annotate a let definition by a postcondition F of
type ⌈A⌉ → prop. We write “λ(x1 : A1 )/F1 : (x2 : A2 )/F2 . M ” to ascribe to a λ-abstraction
a precondition F1 of type ⌈A1 ⌉ → prop and a postcondition F2 of type ⌈A1 ⌉ × ⌈A2 ⌉ → prop.
Computational values are lifted to the logical level using the reflection function defined in
Table 10. The key idea of this definition is to reflect a computational function as a pair
of predicates consisting of its precondition and its postcondition. Given a computational
function f , a formula can refer to the precondition (resp. the postcondition) of f using the
predicate pre f (resp. post f ). Thus, pre (resp. post) is a synonymous for π1 (resp. π2 ).
To improve the usability of our tool, we define in Table 10 a surface language by extending
λ with several practical facilities. First, terms are explicitly typed. Therefore, the labelling L
must be extended to convey type annotations in an explicitly typed version of λℓ (the typing
system of λℓ is quite standard and will be presented formally in the following section 4). The
instrumentation I defined in Table 9 is extended to types by replacing each type annotation A
by its monadic interpretation I(A) defined by I(A) = cm × A, ι = ι, A1 × A2 = (A1 × A2 )
and A1 → A2 = A1 → I(A2 ).
Second, since the instrumented version of a source program would be cumbersome to

16

reason about because of the explicit threading of the cost value, we keep the program in its
initial form while allowing logic assertions to implicitly refer to the instrumented version of
the program. Thus, in the surface language, in the term “let x : A/F = M in M ”, F has
type ⌈I(A)⌉ → prop, that is to say a predicate over pairs of which the first component is the
execution cost.
Third, we allow labels to be written in source terms as a practical way of giving names
to the labels introduced by the labelling L. By these means, the constant cost assigned to a
label ℓ can be symbolically used in specifications by writing costof(ℓ).
Finally, as a convenience, we write “x : A/F ” for “x : A/λ(cost : cm, x : ⌈I(A)⌉).F ”.
This improves the conciseness of specifications by automatically allowing reference to the
cost variable in logic assertions without having to introduce it explicitly.

3.4

Prototype implementation

We implemented a prototype compiler [24] in OCaml (∼ 3.5Kloc). In addition to the distributed source code, a web application enables basic experiments without any installation
process.
This compiler accepts a program P written in the surface language extended with fixpoints
and algebraic datatypes. We found no technical difficulty in handling these extensions and
this is the reason why they are excluded from the core language in the presented formal
development. Specifications are written in the Coq proof assistant [11]. A logic keyword is
used to include logical definitions written in Coq to the source program.
Type checking is performed on P and, upon success, it produces a type annotated program Pt . Then, the labelled program Pℓ = L(Pt ) is generated. Following the same treatment
of branching as in our previous work on imperative programs [2, 3], the labelling introduces
a label at the beginning of each pattern matching branch.
By erasure of specifications and type annotations, we obtain a program Pλ of λ (Table 2).
Using the compilation chain presented earlier, Pλ is compiled into a program Ph of λh,vn
(Table 7) . The annotating compiler uses the cost model that counts for each label ℓ the
number of primitive operations that belong to execution paths starting from ℓ (and ending
in another label or in an instruction without successor).
Finally, the instrumented version of Pℓ as well as the actual cost of each label is given
as input to a verification condition generator to produce a set of proof obligations implying
the validity of the user-written specifications. These proof obligations are either proved
automatically using first-order theorem provers or manually in Coq.

3.5

Examples

In this section, we present two examples that are idiomatic of functional programming: an
inductive function and a higher-order function. These examples were checked using our
prototype implementation. More involved examples are distributed with the software. These
examples include several standard functions on lists (fold, map, . . . ), combinators written in
continuation-passing style, and functions over binary search trees.
An inductive function Table 11 contains an example of a simple inductive function: the
standard concatenation of two lists. In the code, one can distinguish three kinds of toplevel

17

definitions: the type definitions prefixed by the type keyword, the definitions at the logical
level surrounded by logic { . . . }, and the program definitions introduced by the let keyword.
On lines 1 and 2, the type definitions introduce a type list for lists of natural numbers as
well as a type bool for booleans. Between lines 3 and 9, at the logical level, a Coq inductive
function defines the length of lists so that we can use this measure in the cost annotation of
concat. Notice that the type definitions are automatically lifted at the Coq level, provided
that they respect the strict positivity criterion imposed by Coq to ensure well-foundedness of
inductive definitions.
The concatenation function takes two lists l1 and l2 as input, and it is defined, as usual,
by induction on l1. In order to write a precise cost annotation, each part of the function body is labelled so that every piece of code is dominated by a label: ℓmatch dominates “match l1 with Nil ⇒ • | Cons(x, xs) ⇒ •”, ℓnil dominates “Nil”, ℓcons dominates
“Cons(x, •)”, and ℓrec dominates “concat(xs, l2)”. Looking at the compiled code in Table 12,
it is easy to check that the covering of the code by the labels is preserved through the compilation process. One can also check that the computed costs are correct with respect to a
cost model that simply counts the number of instructions, i.e., costof(ℓnil ) = 2, costof(ℓrec )
= 6, costof(ℓcons ) = 5 and costof(ℓmatch ) = 1. Here we are simply assuming one unit of time
per low-level instruction, but a more refined analysis is possible by propagating the binary
instructions till the binary code (cf. [2, 3]).
Finally, the specification says that the cost of executing concat (l1, l2) is proportional
to the size of l1. Recall that the ‘cost’ and ‘result’ variables are implicitly bound in the
post-condition. Notice that the specification is very specific on the concrete time constants
that are involved in that linear function. Following the proof system of the higher-order
Hoare logic [25], the verification condition generator produces 37 proof obligations out of this
annotated code. All of them are automatically discharged by Coq (using, in particular, the
linear arithmetic decision procedure omega).
A higher-order function Let us consider a higher-order function pexists that looks for
an integer x in a list l such that x validates a predicate p. In addition to the functional
specification, we want to prove that the cost of this function is linear in the length n of the
list l. The corresponding program written in the surface language can be found in Table 13.
A prelude declares the type and logical definitions used by the specifications. On lines 1
and 2, two type definitions introduce data constructors for lists and booleans. Between lines
4 and 5, a Coq definition introduces a predicate bound over the reflection of computational
functions from nat to nat × bool that ensures that the cost of a computational function p is
uniformly bounded by a constant k.
On line 9, the precondition of function pexists requires the function p to be total. Between
lines 10 and 11, the postcondition first states a functional specification for pexists: the boolean
result witnesses the existence of an element x of the input list l that is related to BT rue by
the postcondition of p. The second part of the postcondition characterizes the cost of pexists
in case of a negative result: assuming that the cost of p is bounded by a constant k, the cost of
pexists is proportional to k · n. Notice that there is no need to add a label in front of BT rue
in the first branch of the inner pattern-matching since the specification only characterizes the
cost of an unsuccessful search.
The verification condition generator produces 53 proof obligations out of this annotated
program; 46 of these proof obligations are automatically discharged and 7 of them are man-

18

01
02
03
04
05
06
07
08
09
10
11
12
13
14
15
16
17
18
19

type list = Nil | Cons (nat, list)
type bool = BTrue | BFalse
logic {
Fixpoint length (l : list) : nat : =
match l with
| Nil ⇒ 0
| Cons (x, xs) ⇒ 1 + length (xs)
end.
}
let rec concat (l1 : list, l2 : list) : list {
cost = costof(ℓmatch ) + costof(ℓnil )
+ (costof(ℓrec ) + costof(ℓmatch ) + costof(ℓcons )) × length (l1)
}
=
ℓmatch >
match l1 with
| Nil → ℓnil > l2
| Cons (x, xs) → ℓcons > Cons (x, concat (xs, l2) > ℓrec )
end


costof(ℓnil )



costof(ℓrec )
with
costof(ℓcons )



costof(ℓmatch )

=
=
=
=

2
6
5
1

Table 11: A function that concatenates two lists, and its cost annotation.

01 routine x19 (c20 , x7 )
02 ℓrec :
03 k2 ← proj 1 c20 ;
04 x ← proj 2 c20 ;
05 x14 ← make int 1 ;
06 x15 ← make tuple (x14 , x, x7 ) ;
07 x22 ← proj 0 k2 ;
08 call x22 (k2 , x15 )
09 routine x16 (c17 , l1, l2, k2 )
10 ℓmatch :
11 switch l1
12 0 : ℓnil :
13
x18 ← proj 0 k2 ;
14
call x18 (k2 , l2)
15 1 : ℓcons :
16
xs ← proj 2 l1 ;
17
x ← proj 1 l1 ;
18
x13 ← make tuple (x19 , k2 , x) ;
19
x21 ← proj 0 c17 ;
20
call x21 (c17 , xs, l2, x13 )

Table 12: The compiled code of concat.

19

01
02
03
04
05
06
07
08
09
10
11
12
13
14
15
16

type list = Nil | Cons (nat, list)
type bool = BTrue | BFalse
logic {
Definition bound (p : nat −→ (nat ∗ bool)) (k : nat) : Prop : =
∀ x m : nat, ∀ r : bool, post p x (m, r) ⇒ m ≤ k.
Definition k0 : = costof(ℓm ) + costof(ℓnil ).
Definition k1 : = costof(ℓm ) + costof(ℓp ) + costof(ℓc ) + costof(ℓf ) + costof(ℓr ).
}
let rec pexists (p : nat → bool, l : list) { ∀ x, pre p x } : bool {
((result = BTrue) ⇔ (∃ x c : nat, mem x l ∧ post p x (c, BTrue))) ∧
(∀ k : nat, bound p k ∧ (result = BFalse) ⇒ cost ≤ k0 + (k + k1) × length (l))
} = ℓm > match l with
| Nil → ℓnil > BFalse
| Cons (x, xs) → ℓc > match p (x) > ℓp with
| BTrue → BTrue
| BFalse → ℓf > (pexists (p, xs) > ℓr )

Table 13: A higher-order function and its specification.
ually proved in Coq.

4

Typing the compilation chain

We describe a (simple) typing of the compilation chain. Specifically, each λ-calculus of the
compilation chain is equipped with a type system which enjoys subject reduction: if a term
has a type then all terms to which it reduces have the same type. Then the compilation
functions are extended to types and are shown to be type preserving: if a term has a type
then its compilation has the corresponding compiled type.
Besides providing insight into the compilation chain, typing is used in two ways. First, the
tool for reasoning about cost annotations presented in section 3 takes as input a typed λ-term
and second, and more importantly, in section 5, we rely on an enrichment of a type system
which is expressive enough to type a compiled code with explicit memory deallocations.
The two main steps in typing the compilation chain are well studied, see, e.g., the work
of Morrisett et al. [21], and concern the CPS and the closure conversion steps. In the former,
the basic idea is to type the continuation/the evaluation context of a term of type A with its
negated type (A → R), where R is traditionally taken as the type of ‘results’. In the latter,
one relies on existential types to hide the details of the representation of the ‘environment’ of
a function, i.e. the tuple of variables occurring free in its body.

4.1

Typing conventions

We shall denote with tid the syntactic category of type variables with generic elements t, s, . . .
and with A the syntactic category of types with generic elements A, B, . . . A type context is
denoted with Γ, Γ′ , . . ., and it stands for a finite domain partial function from variables to
types. To explicit a type context, we write x1 : A1 , . . . , xn : An where the variables x1 , . . . , xn
must be all distinct and the order is irrelevant. Also we write x∗ : A∗ for a possibly empty
sequence x1 : A1 , . . . , xn : An , and Γ, x∗ : A∗ for the context resulting from Γ by adding
20

Syntax types
A

::= tid | A+ → A | ×(A∗ )

(types)

Typing rules
x:A∈Γ
Γ⊢x:A

Γ, x : A ⊢ N : B
Γ⊢M :A
Γ ⊢ let x = M in N : B

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

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

Γ ⊢ M ∗ : A∗
Γ ⊢ (M ∗ ) : ×(A∗ )

Γ ⊢ M : ×(A1 , . . . , An ) 1 ≤ i ≤ n
Γ ⊢ πi (M ) : Ai

Γ⊢M :A
Γ⊢ℓ>M :A

Γ⊢M :A
Γ⊢M >ℓ:A

Restricted syntax CPS types, R type of results
A

::= tid | A+ → R | ×(A∗ )

(CPS types)

CPS type compilation
Ccps (t)
Ccps (×(A∗ ))
Ccps (A+ → B)

=t
= ×(Ccps (A)∗ )
= (Ccps (A))+ , ¬Ccps (B) → R
where: ¬A ≡ (A → R)

Table 14: Type system for λℓ and λℓcps
the sequence x∗ : A∗ . Hence the variables in x∗ must not be in the domain of Γ. If A is a
type, we write ftv(A) for the set of type variables occurring free in it and, by extension, if Γ
is a type context ftv(Γ) is the union of the sets ftv(A) where A is a type in the codomain
of Γ. A typing judgement is typically written as Γ ⊢ M : A where M is some term. We
shall write Γ ⊢ M ∗ : A∗ for Γ ⊢ M1 : A1 , . . . ,Γ ⊢ Mn : An . Similar conventions apply
if we replace the symbol ‘∗′ with the symbol ‘+′ except that in this case the sequence is
assumed not-empty. A type transformation, say T , is lifted to type contexts by defining
T (x1 : A1 , . . . xn : An ) = x1 : T (A1 ), . . . , xn : T (An ). Whenever we write:
if Γ ⊢S1 M : A then T (Γ) ⊢S2 T (M ) : T (A)
what we actually mean is that if the judgement in the hypothesis is derivable in a certain
‘type system S1 ’ then the transformed judgement in derivable in the ‘type system S2 ’.

4.2

The type system of the source language

Table 14 describes the typing rules for the source language defined in Table 2. These rules are
standard except those for the labellings, and, as announced, they are preserved by reduction.
Proposition 22 (subject reduction) If M is a term of the λℓ calculus, Γ ⊢ M : A and
M → N then Γ ⊢ N : A.
21

The typing rules described in Table 14 apply to the CPS λ-calculus too. Table 14 describes
the restricted syntax of the CPS types and the CPS type translation. Then the CPS term
translation defined in Table 3 preserves typing in the following sense.
Proposition 23 (type CPS) If Γ ⊢ M : A then Ccps (Γ), halt : ¬Ccps (A) ⊢ Ccps (M ) : R.

4.3

Type system for the value named calculi

Table 15 describes the typing rules for the value named calculi. For the sake of brevity, we
shall omit the type of a term since this type is always the type of results R and write Γ ⊢vn M
rather than Γ ⊢vn M : R. The first 6 typing rules are just a specialization of the corresponding
rules in Table 14. The last two rules allow for the introduction and elimination of existential
types; we shall see shortly how they are utilised in typing closure conversion.
In the proposed formalisation, we rely on the tuple constructor to introduce an existential
type and the first projection to eliminate it. This has the advantage of leaving unchanged
the syntax and the operational semantics of the value named λ-calculus. An alternative
presentation consists in introducing specific operators to introduce and eliminate existential
types which are often denoted with pack and unpack, respectively. The reader who is familiar
with this notation may just read (x) as pack(x) and π1 (x) as unpack(x) when x has an
existential type. With this convention, the rewriting rule which allows to unpack a packed
value is just a special case of the rule for projection.
As in the previous system, typing is preserved by reduction.
Proposition 24 (subject reduction, value named) If M is a term of the λℓcps,vn -calculus,
Γ ⊢vn M and M → N then Γ ⊢vn N .
The transformation into value named CPS form specified in Table 5 affects the terms but
not the types.
Proposition 25 (type value named) If M is a term of the λℓcps -calculus and Γ ⊢ M : R
then Γ ⊢vn Cvn (M ).
On the other hand, to type the closure conversion we rely on existential types to abstract/hide the type of the environment as specified in Table 15. Then the term translation
of the function definition and application given in Table 6 has to be slightly modified to account for the introduction and elimination of existential types. The revised definition is as
follows:
let x = π1 (x) in
(← existential elimination)
let (c, e) = x in @(c, e, y + )

Ccc (@(x, y + ))

=

Ccc (let x = C in M )

let c = λe, x+ .let (z1 , . . . , zk ) = e in Ccc (N ) in
let e = (z1 , . . . , zk ) in
= let x = (c, e) in
let x = (x) in
(← existential introduction)
Ccc (M )
(if C = λx+ .N, fv(C) = {z1 , . . . , zk })

This modified closure conversion does not affect the commutation and simulation properties stated in propositions 10 and 11 and moreover it preserves typing as follows.

22

Syntax types
A

::= tid | (A+ → R) | ×(A∗ ) | ∃tid .A
Typing rules

+

+

vn

x : A+ → R, y + : A+ ∈ Γ
Γ ⊢vn @(x, y + )

Γ, x : A ⊢ M
Γ ⊢vn λx+ .M : A+ → R

y : ×(A1 , . . . , An ) ∈ Γ 1 ≤ i ≤ n
Γ, x : Ai ⊢vn M
vn
Γ ⊢ let x = πi (y) in M

x∗ : A∗ ∈ Γ
Γ ⊢ (x∗ ) : ×(A∗ )
vn

Γ ⊢vn V : A Γ, x : A ⊢vn M
Γ ⊢vn let x = V in M

Γ ⊢vn M
Γ ⊢vn ℓ > M

x : [B/t]A ∈ Γ
Γ ⊢vn (x) : ∃t.A

y : ∃t.A ∈ Γ Γ, x : A ⊢vn M t ∈
/ ftv(Γ)
Γ ⊢vn let x = π1 (y) in M

Closure conversion type compilation
Ccc (t)
Ccc (×(A∗ ))
Ccc (A+ → R)
Ccc (∃t.A)

=t
= ×(Ccc (A)∗ )
= ∃t. × ((t, Ccc (A)+ → R), t)
= ∃t.Ccc (A)

Table 15: Type system for the value named calculi and closure conversion
Proposition 26 (type closure conversion) If M is a term in λℓcps,vn and Γ ⊢vn M then
Ccc (Γ) ⊢vn Ccc (M ).
Similarly to the transformation in value named form, the hoisting transformations affect
the terms but not the types.
Proposition 27 (type hoisting) If M is a term in λℓcps,vn , Γ ⊢vn M , and M ❀ N then
Γ ⊢vn N .

4.4

Typing the compiled code

We can now extend the compilation function to types by defining:
C(A) = Ccc (Ccps (A))
and by composing the previous results we derive the following type preservation property of
the compilation function.
Theorem 28 (type preserving compilation) If M is a term of the λℓ -calculus and Γ ⊢
M : A then
C(Γ), halt : ∃t. × (t, C(A) → R, t) ⊢vn C(M ) .
Remark 29 The ‘halt’ variable introduced by the CPS translation can occur only in a subterm
of the shape @(halt , x) in the intermediate code prior to closure conversion. Then in the
closure conversion translation, it suffices that Ccc (@(halt , x)) = @(halt , x) and give to ‘halt ′ a
functional rather than an existential type. With this proviso, theorem 28 above can be restated
as follows:
23

If M is a term of the λℓ -calculus and Γ ⊢ M : A then C(Γ), halt : ¬C(A) ⊢vn C(M ).
Example 30 (typing the compiled code) We consider again the compilation of the term
λx.y (cf. example 9) which can be typed, e.g., as follows:
y : t1 ⊢ λx.y : (t2 → t1 ) .
Its CPS translation is then typed as:
y : t1 , halt : ¬Ccps (t2 → t1 ) ⊢ @(halt , λx, k.@(k, y)) : R .
The value named translation does not affect the types:
y : t1 , halt : ¬Ccps (t2 → t1 ) ⊢vn let z1 = λx, k.@(k, y) in @(halt , z1 ) .
After closure conversion we obtain the following term M :
let c = λe, x, k.let y = π1 (e), k = π1 (k), c = π1 (k), e = π2 (k) in @(c, e, y) in
let e = (y), z1 = (c, e), z1 = (z1 ), halt = π1 (halt ), c = π1 (halt ), e = π2 (halt ) in
@(c, e, z1 )
which is typed as follows:
y : t1 , halt : ∃t. × (t, C(t2 → t1 ) → R, t) ⊢vn M .
In this case no further hoisting transformation applies. If we adopt the optimised compilation
strategy sketched in remark 29 then after closure conversion we obtain the following term M ′ :
let c = λe, x, k.let y = π1 (e), k = π1 (k), c = π1 (k), e = π2 (k) in @(c, e, y) in
let e = (y), z1 = (c, e), z1 = (z1 ), in
@(halt , z1 )
which is typed as follows:
y : t1 , halt : C(t2 → t1 ) → R ⊢vn M ′ .

5

Memory management

We describe an enrichment of the λℓh,vn -calculus called λℓ,r
h,vn -calculus which explicitly handles
allocation and deallocation of memory regions. At our level of abstraction, the memory
regions are just names r, r ′ , . . . of a countable set. Intuitively, the ‘live’ locations of a memory
are partitioned into regions. The three new operations the enriched calculus may perform
are: (1) allocate a new region, (2) allocate a value (in our case a non-empty tuple) in a region,
and (3) dispose a region. The additional operation of reading a value from a region is implicit
in the projection operation which is already available in the non-enriched calculus λℓh,vn . In
order to gain some expressivity we shall also allow a function to be parametric in a collection
of region names which are provided as arguments at the moment of the function call.
From our point of view, the important property of this approach to memory management is
both its cost predictability and the possibility of formalising and certifying it using techniques
similar to those presented in section 2. Indeed the operations (1-3) inject short sequences of
24

instructions in the compiled code that can be executed in constant time as stressed by Tofte
and Talpin [27] (more on this at the end of section 5.2).
Because of the operation (3) described above (dispose), the following memory errors may
arise at run-time: (i) write a value in a disposed region, (ii) access (project) a value in a disposed region, and (iii) dispose an already disposed region. To avoid these errors, we formulate
a type and effect system in the sense of Lucassen and Gifford [18] that over-approximates the
visible set of regions and guarantees safe memory disposal, following Tofte and Talpin [27].
This allows to further extend to the right with one more commuting square a typed version
of the compilation chain described in Table 1 and then to include the cost of safe memory
management in our analysis.

5.1

Region conventions

We introduce a syntactic category of regions rid with generic elements r, r ′ , . . . and a syntactic
category of effects e with generic elements e, e′ , . . . An effect is a finite set of region variables.
We keep denoting types with A, B, . . . However types may depend on both regions and effects.
Regions can be bound when occurring either in types or in terms. In the first case, the binder
is a universal quantifier ∀r.A, while in the second it is either a new region allocation operator
let all(r) in T or a region λ-abstraction. On the other hand, we stress that the disposal operator
dis(r) in T is not a binder. Because of the universal quantification and the λ-abstraction both
the untyped and the typed region enriched calculi include a notion of region substitution.
Note that such a substitution operates on the effects contained in the types too and that, as
a result, it may reduce the cardinality of the set of regions which composes an effect. The
change of cardinality however, can only arise in the untyped calculus. In the typed calculus,
all the region substitutions are guaranteed to be injective. We denote with frv(A) the set
of regions occurring free in the type A, and frv(Γ) denotes the obvious extension to type
contexts.

5.2

A region enriched calculus

A formalisation of the operations and the related memory errors is given through the region
enriched calculus presented in Tables 16 and 17. Notice that an empty tuple is stored in a
local variable rather than in a region and that a similar stategy would be adopted for basic
data values such as booleans or integers. The usual formalisation of the operational semantics
relies on a rather concrete representation of a heap as a (finite domain) function mapping
regions to stores which are (finite domain) functions from locations to values satisfying some
coherence conditions (see, e.g. [27, 1, 8]). In the following, we will take a slightly more
abstract approach by representing the heap implicitly as a heap context H. The latter is
simply a list of region allocations, value allocations at a region, and region disposals.
It turns out that it is possible to formulate the coherence conditions on the memory
directly on this list so that we do not have to commit to a concrete representation of the heap
as the one sketched above. A first consequence of this design choice, is that we can dispense
with the introduction of additional syntactic entities like that of ‘location’ or ‘address’ and
consequently avoid the non-deterministic rules that choose fresh regions or locations (as in,
say, the π-calculus, α-renaming will take care of that). A second consequence is that the
proof of the simulation property of the standard calculus by the region-enriched calculus is
rather direct.

25

Coherent heap context relative to live regions

Coh([ ], L)

Coh(H, L) r ∈ L
Coh(let x = (y + )at(r) in H, L)

Coh(H, L)
Coh(let x = () in H, L)
Coh(H, L ∪ {r})
Coh(let all(r) in H, L)

Coh(H, L\{r}) r ∈ L
Coh(dis(r) in H, L)

Region not-disposed in a heap context
NDis(r, [ ])

NDis(r, H)
NDis(r, let x = () in H)

(r = r ′ ) or (r 6= r ′ and NDis(r, H))
NDis(r, let all(r ′ ) in H)

NDis(r, H)
NDis(r, let x = (y + )at(r ′ ) in H)
r 6= r ′ NDis(r, H)
NDis(r, dis(r ′ ) in H)

Table 16: Coherence predicate on heap contexts
Continuing the comparison with formalisations found in the literature, we notice that the
fact that region disposal is decoupled from allocation avoids the introduction of a special
‘disposed’ or ‘free’ region which is sometimes used in the operational semantics to represent
the situation where a region becomes inaccessible (see, e.g., [27, 1]). What we do instead is
to keep track of the disposal operation in the heap context.
Finally, let us notice that we certainly take advantage of the fact that our formalisation
of region management targets an intermediate RTL language where the execution order and
the operations of writing and reading a value from memory are completely explicit. The
formalisation of region management at the level of the source language, e.g., the λ-calculus,
appears a bit more involved because one has to enrich the language with operations that really
refer to the way the language is compiled. For instance, one has to distinguish between the
act of storing a value in memory and the act of referring to it without exploring its internal
structure.
Table 16 specifies the coherence predicate Coh(H, L) of the heap context H relatively to
a set of ‘live’ regions L. Briefly, a heap context is coherent if whenever the context contains
an allocation for a tuple in a region, or a disposal of a region, the region in question is alive.
This is defined by induction on the structure of the heap context H.
The reduction rules in Table 17 are a refinement of those of the value named λ-calculus
described in Table 4. The main novelties are that a transition can be fired only if the heap
context is coherent relatively to an empty set of regions in the sense described above and
moreover that a tuple can be projected only if it is allocated in a region which has not been
disposed. To formalise this last property we have refined the definition of the function E(x)
which looks for the value bound to a variable in an evaluation context. The refined function,
upon success, returns both the value and the part of the heap context, say H, which has been
explored. Then the predicate NDis(r, H) defined in Table 16 checks that the region r where
the tuple is allocated is not disposed by H. Again, this predicate is defined by induction on
the structure of the heap context H.
We remark the following decomposition property of region-enriched programs.
Proposition 31 (decomposition) A program P in the region enriched λ-calculus can be
uniquely decomposed as F [H[∆]] where F is a function context, H a heap context, and ∆ is
either an application of the shape @(x, r ∗ , y + ) or a projection of the shape let x = πi (y) in T ,
26

Syntax
rid
C
T
P
F
H
E

::= r | r ′ | · · ·
::= () | (id + )at(rid ) | πi (id)
::= @(id, rid ∗ , id + ) | let id = C in T | ℓ > T |
let all(rid ) in T | dis(rid) in T
::= T | let id = λrid ∗ , id + .T in P
::= [ ] | let id = λrid ∗ , id + .T in F
::= [ ] | let id = () in H | let id = (id + )at(rid ) in H |
let all(rid ) in H | dis(rid) in H
::= F [H]

(region identifiers)
(restricted let-bindable terms)
(restricted terms)
(programs)
(function contexts)
(heap contexts)
(evaluation contexts)

Reduction rules
′
E[@(x, r1′ , . . . , rm
, z1 , . . . , zn )]

′
→ E[[r1′ /r1 , . . . , rm
/rm , z1 /y1 , . . . , zn /yn ]T ]
if π1 (E(x)) ≡ λr1 , . . . , rm , y1 , . . . , yn .T, E ≡ F [H], Coh(H, ∅)

E[let z = πi (x) in T ] → E[[yi /z]T ]]
if E(x) = ((y1 , . . . , yn )at(r), H ′ ), 1 ≤ i ≤ n, E ≡ F [H], Coh(H, ∅), NDis(r, H ′ )
ℓ

E[ℓ > T ] −
→ E[T ]


if E ≡ F [H], Coh(H, ∅)

if E = E ′ [let x = V in [ ]]
 (V, [ ])
′′
(V, E [El ]) otherwise if E = E ′ [El], E ′ (x) = (V, E ′′ )
E(x) =

undefined
otherwise




where: 


 V ::= () | (id ∗ )at(rid) | λrid ∗ , id + .T
El ::= let id = V in [ ] | let all(rid) in [ ] | dis(rid ) in [ ]

Table 17: The region-enriched calculus: λℓ,r
h,vn

27










or a labelling of the shape ℓ > T .
We define an obvious erasure function on the region-enriched types, values, and terms that
just erases all the region related pieces of information (please refer to the formal definition in
Table 19 of the appendix for details).
Because of the possible memory errors described above, a region enriched program does
not necessarily simulate its region erasure.
Example 32 (memory errors) Consider the following program P in λℓh,vn (not necessarily
the result of a compilation):
P ≡ F [@(pair , v1 , v2 )]
F ≡ let prj1 = λx.let y = π1 (x) in @(halt , y) in
let pair = λx1 , x2 .let y = (x1 , x2 ) in @(prj1 , y) in [ ] .
One strategy to manage memory regions in P is to allocate a region upon entering the pair
function and to dispose it just before calling the prj1 function as in the following program P1
in λℓ,r
h,vn .
P1 ≡ F1 [@(pair , v1 , v2 )]
F1 ≡ let prj1 = λx.let z = π1 (x) in @(halt , z) in
let pair = λx1 , x2 .let all(r) in let y = (x1 , x2 )at(r) in dis(r) in @(prj1 , y) in [ ] .
Unfortunately this strategy leads to a memory error as:
∗

P1 → F1 [H1 [let z = π1 (y) in @(halt , z)]]
H1 ≡ let all(r) in let y = (v1 , v2 )at(r) in dis(r) in [ ]
Formally, F1 [H1 ](y) = ((v1 , v2 )at(r), H2 ), H2 = dis(r) in [ ], and the predicate NDis(r, H2 )
does not hold. In plain words, the problem with this strategy is that it disposes the region r
before the value (v1 , v2 ) allocated into it is projected. A better strategy is to pass the region
created in the function pair to the function prj1 and let this function dispose the region once
the value (v1 , v2 ) has been projected. This strategy is described by the following program P2 in
λℓ,r
h,vn .
P2 ≡ F2 [@(pair , v1 , v2 )]
F2 ≡ let prj1 = λr, x.let z = π1 (x) in dis(r) in @(halt , z) in
let pair = λx1 , x2 .let all(r) in let y = (x1 , x2 )at(r) in @(prj1 , r, y) in [ ] .
This time the reduction leads to a normal termination:
∗

P2 → F2 [H2 [@(halt , v1 )]]
H2 ≡ let all(r) in let y = (v1 , v2 )at(r) in dis(r) in [ ] .
We conclude this section with an overview of a rather standard implementation scheme
of region based memory management (see, e.g., [20] for more details). Initially, the available
memory is partitioned in pages which constitute a free list. A region is a pointer to a ‘region
descriptor’ that contains a pointer to the beginning and the end of a list of pages and a
counter which gives the amount of memory available in the last page of the list. A value (a
non-empty tuple in our case) is just a pointer to a memory address and an access to a value is
28

direct. Storing a value in a region means storing the value in the last page of the list related
to the region and updating the region descriptor. If the space available is not sufficient, then
one or more pages are taken from the free list and appended to the end of the region list and
again the region descriptor is updated. This operation can be executed in constant time as
long as the size of the values to be allocated can be determined at compile time (which is
obviously true in our case). Deallocating a region means concatenating the list related to the
region to the free list. We refrain from going into the details of the implementation scheme
mentioned above which really belong to the backend of the compiler. Indeed, the scheme is
rather independent from the source language (for instance, Christiansen et al. [10] rely on it
to implement an object-oriented language) while depending for its efficiency on the memory
organisation of the processor and possibly the operating system.

5.3

A type and effect system

In order to have the simulation property, we require that the region-enriched program is
typable with respect to an enhanced type and effect system described in Table 18 whose
purpose is precisely to avoid memory errors at run time. The system defines judgment (i)
Γ ⊢rg T : e read “restricted term T has effect e under Γ” ; (ii) Γ ⊢rg C : A read “restricted
let-bindable term C has type A under Γ” and (iii) Γ ⊢rg P : e read “program P has effect
e under Γ”. The formalisation follows the work of Aiken et al. [1] in that allocation and
disposal of a region are decoupled (see also Henglein et al. [16] for a survey and Boudol [8]
for a discussion). Then a region can be disposed only if the following computation neither
accesses nor disposes it. Note that in typing values we omit the effect (which is always empty)
and in typing terms we omit the type (which is always the type of results R). The typing
rules are designed to maintain several invariants. First, if a program P has effect e then
the set of regions e over-approximates the visible regions that the program P may dispose
or access for allocating or reading a value. Second, all the region names have been allocated
(and possibly disposed afterwards). Third, distinct region names in the program correspond
at run time to different regions, i.e., all region substitutions are injective. With respect to
the system described in Table 15, we notice that we distinguish the rules for typing an empty
and a non-empty tuple as the former has no effect on the heap. For similar reasons, we split
the rule for typing a value definition in three depending on whether the value is an empty
tuple, a function, or a non-empty tuple (possibly of existential type). Only in the last case an
effect on the heap is recorded. As already mentioned, empty tuples do not affect the heap and
function definitions eventually become sequences of assembly language instructions which are
stored in a statically allocated and read-only zone of memory separated by the data memory.
Example 33 (types and effects) Going back to example 32, let us assume the types ti : vi ,
∅

i = 1, 2 and halt : t1 −
→ R. Then the reader may check that the program P2 is typable (has an
effect) assuming the following types for the functions:
{r}

∅

pair : t1 , t2 −
→R

prj1 : ∀r. × (t1 , t2 )at(r) −−→ R

On the other hand, any attempt at typing P1 fails trivially because the type of the function prj1
{r}

must be of the shape ×(t1 , . . .)at(r) −−→ R and it cannot match the type of the pair allocated
by the function pair in a new region. If we fix this problem by abstracting the function prj1
{r}

w.r.t. a region so that it has the type ∀r. × (t1 , . . .)at(r) −−→ R we stumble on the main
29

Types and effects syntax
::= {rid , . . . , rid }
e
::= tid | ∀rid ∗ .A+ −
→ R | ×() | ×(A+ )at(rid ) | (∃tid .A)at(rid )

e
A

(effects)
(types)

Typing rules
+

+

rg

Γ, y : A ⊢ T : e
{r } ∩ frv(Γ) = ∅ frv(λr ∗ , y + .T ) = ∅
e
Γ ⊢rg λr ∗ , y + .T : ∀r ∗ .A+ −
→R
∗

Γ⊢

rg

e

B ≡ ∀r1∗ .A+ −
→ R x : B ∈ Γ y + : [r ∗ /r1∗ ]A+ ∈ Γ
r ∗ distinct frv(B) = ∅
Γ ⊢rg @(x, r ∗ , y + ) : [r ∗ /r1∗ ]e
y : ×(A1 , . . . , An )at(r) ∈ Γ
1 ≤ i ≤ n Γ, x : Ai ⊢rg T : e
Γ ⊢rg let x = πi (y) in T : e ∪ {r}

x+ : A+ ∈ Γ
(x )at(r) : ×(A+ )at(r)
+

x : [B/t]A ∈ Γ
Γ ⊢rg (x)at(r) : (∃t.A)at(r)

y : (∃t.A)at(r) ∈ Γ Γ, x : A ⊢rg T : e t ∈
/ ftv(Γ)
Γ ⊢rg let x = π1 (y) in T : e ∪ {r}
Γ ⊢rg () : A
Γ, x : A ⊢rg T : e
Γ ⊢rg let x = () in T : e

Γ ⊢rg () : ×()

Γ ⊢rg

Γ ⊢rg λr ∗ , y + .T : A
Γ, x : A ⊢rg P : e
let x = λr ∗ , y + .T in P : e

Γ ⊢rg

Γ ⊢rg (y + )at(r) : A
Γ, x : A ⊢rg T : e
let x = (y + )at(r) in T : e ∪ {r}

Γ ⊢rg T : e ∪ {r} r ∈
/ frv(Γ), e
Γ ⊢rg let all(r) in T : e

Γ ⊢rg T : e r ∈
/e
Γ ⊢ dis(r) in T : e ∪ {r}

Γ ⊢rg T : e
Γ ⊢rg ℓ > T : e

Γ ⊢rg P : e e ⊆ e′
Γ ⊢rg P : e′

rg

Table 18: Type and effect system for the region-enriched calculus

30

problem, namely the function pair disposes a region which is used in the continuation; this is
forbidden by the typing rule for region disposal.
Example 34 (injective region substitutions) The soundness and relative simplicity of
the type and effect system bear on the fact that region substitutions are injective. Technically
this property is enforced by the rules for typing an application and an abstraction. In an
application, say @(x, r ∗ , y + ), the region variables r ∗ are distinct and the type of x is region
closed. In an abstraction, say λr ∗ , x+ .T , the function is region closed. It is instructive to see
what can go wrong if we drop these conditions. Consider a function x of the following shape
with its possible (region closed) type:
{r1 ,r2 }

x = λr1 , r2 , y.dis(r1 ) in let z = (y)at(r2 ) in T : ∀r1 , r2 . × () −−−−→ R .
An application @(x, r, r, y) where we pass twice the same region name r will produce a memory
error since we dispose r before writing into it. A similar phenomenon arises with a function
of the following shape and related (region open!) type:
{r1 ,r2 }

x = λr1 , y.dis(r1 ) in let z = (y)at(r2 ) in T : ∀r1 . × () −−−−→ R .
Then an application @(x, r2 , y) where we pass a region name which is free in the type of the
function will also produce a memory error. As a final example, consider a function
x = λr1 , y.let z = () in @(y, r1 , r2 , z)
with a free region variable r2 . Note that r1 , r2 may not appear in the type of the function x
because, e.g., y makes no use of them. Then if we apply x as in @(x, r2 , y) we end up with
an application @(y, r2 , r2 , z) which is not typable because it violates the condition that all the
region variables passed as arguments are distinct.

5.4

Properties of the type and effect system

We notice that the region erasing function preserves typing.
Proposition 35 (region erasure) If Γ ⊢rg P : e then rer (Γ) ⊢vn rer (P ).
In the other direction, it is always possible to insert region annotations in a typable
program of λℓh,vn so as to produce a typable region-enriched program. A simple but not very
interesting way to do this is to allocate one region at the very beginning of the computation
which is never disposed and which is shared by all functions.
Proposition 36 (region enrichment) Let Γ0 be a type context such that if x : A ∈ Γ0 then
A is not a type of the shape ×(B + ) or ∃t.B. If Γ0 ⊢vn P then it is always possible to find a
region enriched typable program P ′ such rer (P ′ ) ≡ P .
Fortunately, more interesting strategies are available; we refer to Aiken et al. [1] for
their description and for an encouraging experimental evaluation and to Henglein et al. [16]
for a survey of region inference techniques. For our purposes, it is enough to know that it is
always possible to define a compilation function Crg from the typed λℓh,vn -calculus to the typed
λℓ,r
h,vn -calculus which is a right inverse of the region erasing function, i.e., rer (Crg (P )) ≡ P ,
31

and which commutes with the label erasure functions, i.e., er(Crg (P )) ≡ Crg (er (P )). Also,
following remark 29, we notice that the typing context of the compiled code satisfies the
conditions in proposition 36 provided that if Γ is the typing context of the source code and
x : A ∈ Γ then the type A is not of the shape ×(B + ).
Next we remark that the type system entails the coherence of the heap context of a
program; this leads to the following progress property.
Proposition 37 (progress) Let P be a typable program in the region enriched calculus such
that frv(P ) = ∅. Then P decomposes as F [H[∆]] (proposition 31) and either (i) P reduces or
(ii) ∆ has the shape @(x, r ∗ , y + ) or let y = πi (x) in T , where x ∈ fv(P ).
Of course, we must also prove that the region enriched types are preserved by reduction.
Proposition 38 (subject reduction, types and effects) If Γ ⊢rg P : e and P → P ′ then
Γ ⊢rg P ′ : e.
Finally, we can show that a well-typed region enriched program does indeed simulate its
region erasure.
α

Theorem 39 (region simulation) If Γ ⊢rg P : e, frv(P ) = ∅, and rer (P ) −
→ Q then
α
′
′
P −
→ P and rer (P ) ≡ Q.

6

Conclusion

We have shown that our approach, that we call the ‘labelling’ approach, can be used to obtain
certified execution costs on functional programs following a standard compilation chain which
composes well with the back-end of a moderately optimising C compiler. The technique
allows to compute the cost of the compiled code while reasoning abstractly at the level of the
source language and it accounts precisely for the cost of memory management for a particular
memory management strategy that uses regions. To provide technical evidence for this claim
has required to have an in-depth and sometimes novel look at the formal properties of the
compilation chain; notable examples are the commutation property of the CPS transformation
and the simulation property for the hoisting and the region aware transformations.
Acknowledgements The authors would like to thank the anonymous reviewers for their
valuable comments and suggestions that significantly helped to improve this paper, as well
as Anindya Banerjee and Olivier Danvy for their efficient work in the edition process.

References
[1] A. Aiken, M. Fähndrich, R. Levien. Better static memory management: improving region-based analysis of higherorder languages. In Proc. ACM-PLDI, pp 174-185, 1995.
[2] R.M. Amadio, N. Ayache, Y. Régis-Gianas, R. Saillard. Certifying cost annotations in compilers. Université Paris
Diderot, Research Report, http://hal.archives-ouvertes.fr/hal-00524715/fr/, 2010.
[3] N. Ayache, R.M. Amadio, Y. Régis-Gianas. Certifying and reasoning on cost annotations in C programs. In Proc.
Formal Methods for Industrial Critical Systems (FMICS), Springer-Verlag 7437:32–46, 2012.
[4] R.M. Amadio, Y. Régis-Gianas. Certifying and reasoning on cost annotations of functional programs. In Proc.
FOPARA, Springer LNCS 7177:72–88, 2012.

32

[5] AbsInt Angewandte Informatik. http://www.absint.com/.
[6] D. Bacon, P. Cheng, V. Rajan. A real-time garbage collector with low overhead and consistent utilization. In Proc.
ACM-POPL, pp 285-298, 2003.
[7] A. Bonenfant, C. Ferdinand, K. Hammond, R. Heckmann. Worst-case execution times for a purely functional
language. In Proc. IFL, Springer LNCS 4449:235-252, 2006.
[8] G. Boudol. Typing safe deallocation. In Proc. ESOP, Springer LNCS 4960:116-130, 2008.
[9] A. Chlipala. A verified compiler for an impure functional language. In Proc. ACM-POPL:93-106, 2010.
[10] M. Christiansen, F. Henglein, H. Niss, P. Velshow. Safe region-based memory management for objects. TOPPS
Report D-397 Department of Computer Science, University of Copenhagen (DIKU), October 1998.
[11] The Coq Development
http://coq.inria.fr.

Team.

The Coq proof assistant.

INRIA-Rocquencourt,

December

2001.

[12] K. Crary, D. Walker, G. Morrisett. Typed memory management in a calculus of capabilities. In Proc. ACM-POPL,
pp 262-275, 1999.
[13] P.-L. Curien. An abstract framework for environment machines. Theoret. Comput. Sci., 82(2):389-402, 1991.
[14] P. Fradet, D. Le Métayer. Compilation of functional languages by program transformation. ACM Transactions on
Programming Languages and Systems, 13(1):21–51, 1991.
[15] D. Gurr. Semantic frameworks for complexity. PhD thesis, University of Edinburgh, 1991.
[16] F. Henglein, H. Makholm, H. Niss. Effect types and region-based memory management. In Advanced topics in
types and programming languages, B. Pierce (ed.), MIT Press, 2005.
[17] X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, 2009.
[18] J. Lucassen, D. Gifford. Polymorphic effect systems. In Proc. ACM-POPL, pp 47-57, 1988.
[19] X. Li, L. Yun, T. Mitra, A. Roychoudhury. Chronos: A timing analyzer for embedded software. Sci. Comput.
Program. 69(1-3): 56–67, 2007.
[20] H. Makholm. A language-independent framework for region inference. PhD thesis, University of Copenhagen, 2003.
[21] J. Morrisett, D. Walker, K. Crary, N. Glew. From system F to typed assembly language. ACM Trans. Program.
Lang. Syst. 21(3): 527-568, 1999.
[22] A. Perlis. Epigrams on programming. SIGPLAN Notices Vol. 17(9):7-13, 1982.
[23] G. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2):125-159, 1975.
[24] Y. Régis-Gianas. An annotating compiler for MiniML. http://www.pps.univ-paris-diderot.fr/~ yrg/fun-cca.
[25] Y. Régis-Gianas, F. Pottier. A Hoare logic for call-by-value functional programs. In Proc. Mathematics of Program
Construction, pp 305-335, 2008.
[26] D. Sands. Complexity analysis for a lazy higher-order language. In Proc. ESOP, Springer LNCS 432:361-376, 1990.
[27] M. Tofte, J.-P. Talpin. Region-based memory management. Information and Computation. 132(2):109-176, 1997.
[28] P. Tranquilli. Indexed labelling for loop iteration dependent costs. Deliverable 5.1, Project CerCo, FP7-ICT-2009C-243881, 2012.
[29] M. Wand. Continuation-based program transformation strategies. Journal of ACM, 27(1):164–180, 1980.
[30] B. Wegbreit. Mechanical Program Analysis. Commun. ACM, 18(9):528–539, 1975.

A

Proofs

We outline the proofs of the results we have stated.
33

Proof of proposition 3 [CPS commutation]
The proof takes the following steps:
1. We remark that if V is a value in λℓ and K a continuation in λℓcps then so are er (V )
and er (K). The proof is a direct induction on the structure of V and K, respectively.
2. For all values V and terms M of the λℓ -calculus, we check that:
er ([V /x]M ) ≡ [er (V )/x]er (M ) .
The proof proceeds by induction on the structure of M .
3. We notice that λx.(x | K) ≡ K holds, for all continuations K such that K is an
abstraction.
4. For all terms M and continuations K such that either M ∈ W0 and K is an abstraction
or M ∈ W1 the following holds:
er (M | K) ≡ er (M ) | er (K) .
We proceed by induction on M .
x We expand the definition of x | K depending on whether K is a variable or a function
and we rely on step 2.
λx+ .M We have λx+ .M ∈ W1 and M ∈ W1 . We analyse λx+ .M | K depending on
whether K is a variable or a function and we apply the inductive hypothesis on
M and step 2. Notice that it is essential that M ∈ W1 to apply the inductive
hypothesis.
@(M0 , . . . , Mn ) We know M0 , . . . , Mn ∈ W0 . We apply the inductive hypothesis on
Mn , . . . , M0 to conclude that:
er (@(M0 , . . . , Mn )) | er (K)
≡ er (M0 ) | λx0 . . . . er(Mn ) | λxn .@(x0 , . . . , xn , er (K))
≡ er (M0 ) | λx0 . . . . er(Mn | λxn .@(x0 , . . . , xn , K))
≡ ···
≡ er (M0 | λx0 . . . . Mn | λxn .@(x0 , . . . , xn , K))
≡ er (@(M0 , . . . , MN ) | K) .
ℓ > M We know that if ℓ > M ∈ Wi then M ∈ Wi and we apply the inductive
hypothesis on M .
M > ℓ By definition, we must have M > ℓ ∈ W0 . Hence K is a function and M ∈ W0 .
Then we apply the inductive hypothesis on M and step 3.
(M1 , . . . , Mn ) We know that Mi ∈ W0 for i = 1, . . . , n. First we notice that:
er (λxn .(x1 , . . . , xn ) | K) ≡ λxn .(x1 , . . . , xn ) | er (K) .

34

Then we apply the inductive hypothesis on Mn , . . . , M0 to conclude that:
er ((M1 , . . . , Mn )) | er (K)
≡ er (M1 ) | λx1 . . . er(Mn ) | λxn .(x1 , . . . , xn ) | er (K)
≡ er (M1 ) | λx1 . . . er(Mn ) | er (λxn .(x1 , . . . , xn ) | K)
≡ er (M1 ) | λx1 . . . er(Mn | λxn .(x1 , . . . , xn ) | K)
≡ ···
≡ er (M1 | λx1 . . . Mn | λxn .(x1 , . . . , xn ) | K)
≡ er ((M1 , . . . , Mn ) | K) .
πi (M ) We know M ∈ W0 . We observe that er (y | K) ≡ y | er (K). Then we apply the
inductive hypothesis on M to conclude that:
er (πi (M )) | er (K)
≡ πi (er (M )) | er (K)
≡ er (M ) | λx.let y = πi (x) in y | er (K)
≡ er (M ) | er (λx.let y = πi (x) in y | K)
≡ er (M | λx.let y = πi (x) in y | K)
≡ er (πi (M ) | K) .
let x = N in M If let x = N in M ∈ Wi then we know N ∈ W0 and M ∈ Wi . We apply
the inductive hypothesis on N and M to conclude that:
er (let x = N in M | K)
≡ er (N | λx.(M | K))
≡ er (N ) | λx.er (M | K)
≡ er (N ) | λx.er (M ) | er (K)
≡ er (let x = N in M ) | er (K) .
5. Then we prove the assertion for M ∈ W0 as follows:
er (Ccps (M )) ≡ er (M | λx.@(halt , x)) (by definition)
≡ er (M ) | λx.@(halt , x) (by point 4)
≡ Ccps (er (M ))
(by definition).
✷

Proof of proposition 4 [CPS simulation]
The proof takes the following steps.
1. We show that for all values V , terms M , and continuations K 6= x:
[V /x]M | [ψ(V )/x]K ≡ [ψ(V )/x](M | K) .
We proceed by induction on M .
M is a variable. By case analysis: M ≡ x or M ≡ y 6= x.

35

λz + .M By case analysis on K which is either a variable or a function. We develop the
second case with K ≡ λy.N . We observe:
[V /x](λz + .M ) | [ψ(V )/x]K
≡ [λz + , k.([V /x]M | k)/y][ψ(V )/x]N
≡ [λz + , k.[ψ(V )/x](M | k)/y][ψ(V )/x]N
≡ [ψ(V )/x][λz + , k.(M | k)/y]N
≡ [ψ(V )/x]((λz + .M ) | K) .
@(M0 , . . . , Mn ) We apply the inductive hypothesis on M0 , . . . , Mn as follows:
[ψ(V )/x](@(M0 , . . . , Mn ) | K)
≡ [ψ(V )/x](M0 | λx0 . . . Mn | λxn .@(x0 , . . . , xn , K))
···
≡ [V /x]M0 | λx0 . . . [ψ(V )/x](Mn | λxn .@(x0 , . . . , xn , K))
≡ [V /x]M0 | λx0 . . . [V /x]Mn | λxn .@(x0 , . . . , xn , [ψ(V )/x]K)
≡ [V /x]@(M0 , . . . , Mn ) | [ψ(V )/x]K .
Note that in this case the substitution [ψ(V )/x] may operate on the continuation. The remaining cases (pairing, projection, let, pre and post labelling) follow
a similar pattern and are omitted.
2. The evaluation contexts for the λℓ -calculus described in Table 2 can also be specified
‘bottom up’ as follows:
E ::= [ ] | E[@(V ∗ , [ ], M ∗ )] | E[let id = [ ] in M ] | E[(V ∗ , [ ], M ∗ )] |
E[πi ([ ])] | E[[ ] > ℓ] .
Following this specification, we associate a continuation KE with an evaluation context
as follows:
K[ ]
= λx.@(halt , x)
KE[@(V ∗ ,[ ],M ∗ )] = λx.M ∗ | λy ∗ .@(ψ(V )∗ , x, y ∗ , KE )
KE[let x=[ ] in N ] = λx.N | KE
KE[(V ∗ ,[ ],M ∗ )]
= λx.M ∗ | λy ∗ .(ψ(V )∗ , x, y ∗ ) | KE
KE[πi ([ ])
= λx.let y = πi (x) in y | KE
KE[[ ]>ℓ]
= λx.ℓ > x | KE
where M ∗ | λx∗ .N stands for M0 | λx0 . . . Mn | λxn .N with n ≥ 0.
3. For all terms M and evaluation contexts E, E ′ we prove by induction on the evaluation
context E that the following holds:
E[M ] | KE ′ ≡ M | KE ′ [E] .
For instance, we detail the case where the context has the shape E[@(V ∗ , [ ], M ∗ )].
E[@(V ∗ , [M ], M ∗ )] | KE ′
≡ @(V ∗ , [M ], M ∗ ) | KE ′ [E]
(by inductive hypothesis)
∗
∗
∗
∗
≡ M | λx.M | λx .@(ψ(V ) , x, x , KE ′ [E])
≡ M | KE ′ [E[@(V ∗ ,[ ],M ∗ )]] .
36

4. For all terms M , continuations K, K ′ , and variable x ∈
/ fv(M ) we prove by induction
on M and case analysis that the following holds:

→ M | K′
if K abstraction, M value, K ′ = x
[K/x](M | K ′ )
′
≡ (M | [K/x]K ) otherwise.
5. Finally, we prove the assertion by proceeding by case analysis on the reduction rule.
• E[@(λx+ .M, V + )] → E[[V + /x+ ]M ]. We have:
E[@(λx+ .M, V + )] | K[ ]
≡ @(λx+ .M, V + ) | KE
≡ @(λx+ , k.M | k, ψ(V )+ , KE )
→ [KE /k, ψ(V )+ /x+ ](M | k)
≡ [KE /k]([V + /x+ ]M | k)
∗
→ [V + /x+ ]M | KE
≡ E[[V + /x+ ]M ] | K[ ] .
• E[let x = V in M ] → E[[V /x]M ]. We have:
E[let x = V in M ] | K[ ]
≡ let x = V in M | KE
≡ V | λx.(M | KE )
≡ [ψ(V )/x](M | KE )
≡ [V /x]M | KE
≡ E[[V /x]M ] | K[ ] .
• E[πi (V )] → E[Vi ], where V ≡ (V1 , . . . , Vn ) and 1 ≤ i ≤ n. We have:
E[πi (V )] | K[ ]
≡ πi (V ) | KE
≡ V | λx.let y = πi (x) in y | KE
≡ let y = πi (ψ(V1 ), . . . , ψ(Vn )) in y | KE
→ [ψ(Vi )/y](y | KE )
≡ Vi | KE
≡ E[Vi ] | K[ ] .
ℓ

• E[ℓ > M ] −
→ E[M ]. We have:
E[ℓ > M ] | K[ ]
≡ ℓ > M | KE
≡ ℓ > (M | KE )
ℓ

− (M | KE )
→
≡ E[M ] | K[ ] .

37

ℓ

• E[V > ℓ] −
→ E[V ]. We have:
E[V > ℓ] | K[ ]
≡ V > ℓ | KE
≡ V | λx.ℓ > x | KE
≡ ℓ > (V | KE )
ℓ

− V | KE
→
≡ E[V ] | K[ ] .
✷

Proof of proposition 7 [VN commutation]
(1) We show that for every P which is either a term or a value of the λℓcps -calculus the
following properties hold:
A If P is a term then R(Cvn (P )) ≡ P .
B If P is a value then for any term N , R(Evn (P, x)[N ]) ≡ [P/x]R(N ).
We prove the two properties at once by induction on the structure of P .
@(x, x+ ) We are in case A and by definition we have:
R(Cvn (@(x, x+ ))) ≡ R(@(x, x+ )) ≡ @(x, x+ ) .
@(x∗ , V, V ∗ ), V 6= id Again in case A. We have:
R(Cvn (@(x∗ , V, V ∗ )))
≡ R(Evn (V, y)[Cvn (@(x∗ , y, V ∗ ))])
≡ [V /y]R(Cvn (@(x∗ , y, V ∗ )))
(by ind. hyp. on B)
≡ [V /y]@(x∗ , y, V ∗ )
(by ind. hyp. on A)
≡ @(x∗ , V, V ∗ ) .
let x = πi (z) in M Again in case A. We have:
R(Cvn (let x = πi (z) in M ))
≡ R(let x = πi (z) in Cvn (M ))
≡ let x = πi (z) in R(Cvn (M ))
≡ let x = πi (z) in M
(by ind. hyp. on A) .
let x = πi (V ) in M, V 6= id Again in case A. We have:
R(Cvn (let x = πi (V ) in M ))
≡ R(Evn (V, y)[let x = πi (y) in Cvn (M )])
≡ [V /y]R(let x = πi (y) in Cvn (M ))
(by ind. hyp. on B)
≡ [V /y]let x = πi (y) in R(Cvn (M ))
≡ [V /y]let x = πi (y) in M
(by ind. hyp. on A)
≡ let x = πi (V ) in M .
38

ℓ > M Last case for A. We have:
R(Cvn (ℓ > M ))
≡ R(ℓ > Cvn (M ))
≡ ℓ > R(Cvn (M ))
≡ℓ>M
(by ind. hyp. on A) .
λy + .M We now turn to case B. We have:
R(Evn (λy + .M, x)[N ])
≡ R(let x = λy + .Cvn (M ) in N )
≡ [R(λy + .Cvn (M ))/x]R(N )
≡ [λy + .R(Cvn (M ))/x]R(N )
≡ [λy + .M/x]R(N )
(by ind. hyp. on A) .
(y ∗ ) Again in case B. We have:
R(Evn ((y ∗ ), x)[N ])
≡ R(let x = (y ∗ ) in N )
≡ [(y ∗ )/x]R(N ) .
(y ∗ , V, V ∗ ), V 6= id Last case for B. We have:
R(Evn ((y ∗ , V, V ∗ ), x)[N ])
≡ R(Evn (V, z)[Evn ((y ∗ , z, V ∗ ), x)[N ]])
≡ [V /z]R(Evn ((y ∗ , z, V ∗ ), x)[N ])
(by ind. hyp. on B)
≡ [V /z]([(y ∗ , z, V ∗ )/x]R(N ))
(by ind. hyp. on B)
≡ [(y ∗ , V, V ∗ )/x]R(N ) .
(2) The proof is similar to the previous one. We show that for every P which is either a term
or a value of the λℓcps -calculus the following properties hold:
A If P is a term then er (Cvn (P )) ≡ Cvn (er (P )).
B If P is a value then for any term N , er (Evn (P, x)[N ]) ≡ Evn (er (P ), x)[er (N )].
We prove the two properties at once by induction on the structure of P .
@(x, x+ ) We are in case A and by definition we have:
er (Cvn (@(x, x+ ))) ≡ er (@(x, x+ )) ≡ @(x, x+ ) ≡ Cvn (er (@(x, x+ ))) .
@(x∗ , V, V ∗ ), V 6= id Again in case A. We have:
er (Cvn (@(x∗ , V, V ∗ )))
≡ er (Evn (V, y)[Cvn (@(x∗ , y, V ∗ ))])
≡ Evn (er (V ), y)[er (Cvn (@(x∗ , y, V ∗ )))] (by ind. hyp. on B)
≡ Evn (er (V ), y)[Cvn (er (@(x∗ , y, V ∗ )))] (by ind. hyp. on A)
≡ Cvn (er (@(x∗ , V, V ∗ ))) .
39

let x = πi (z) in M Again in case A. We have:
er (Cvn (let x = πi (z) in M ))
≡ er (let x = πi (z) in Cvn (M ))
≡ let x = πi (z) in er(Cvn (M ))
≡ let x = πi (z) in Cvn (er (M ))
(by ind. hyp. on A)
≡ Cvn (er (let x = πi (z) in M )) .
let x = πi (V ) in M, V 6= id Again in case A. We have:
er(Cvn (let x = πi (V ) in M ))
≡ er (Evn (V, z)[let x = πi (z) in Cvn (M )])
≡ Evn (er (V ), z)[let x = πi (z) in er (Cvn (M ))] (by ind. hyp. on B)
≡ Evn (er (V ), z)[let x = πi (z) in Cvn (er (M ))] (by ind. hyp. on A)
≡ Cvn (er (let x = πi (V ) in M )) .
ℓ > M Last case for A. We have:
er (Cvn (ℓ > M ))
≡ er (ℓ > Cvn (M ))
≡ er (Cvn (M ))
≡ Cvn (er (M ))
(by ind. hyp. on A)
≡ Cvn (er (ℓ > M )) .
λy + .M We now turn to case B. We have:
er (Evn (λy + .M, x)[N ])
≡ er (let x = λy + .Cvn (M ) in N )
≡ let x = λy + .er (Cvn (M )) in er (N )
≡ let x = λy + .Cvn (er (M )) in er (N ) (by ind. hyp. on A)
≡ Evn (er (λy + .M ), x)[er (N )] .
(y ∗ ) Again in case B. We have:
er (Evn ((y ∗ ), x)[N ])
≡ er (let x = (y ∗ ) in N )
≡ let x = (y ∗ ) in er (N )
≡ Evn (er ((y ∗ )), x)[er (N )] .
(y ∗ , V, V ∗ ), V 6= id Last case for B. We have:
er (Evn ((y ∗ , V, V ∗ ), x)[N ])
≡ er (Evn (V, z)[Evn ((y ∗ , z, V ∗ ), x)[N ]])
≡ Evn (er (V ), x)[er (Evn ((y ∗ , z, V ∗ ), x)[N ])]
(by ind. hyp. on B)
≡ Evn (er (V ), x)[Evn (er ((y ∗ , z, V ∗ )), x)[er (N )]] (by ind. hyp. on B)
≡ Evn (er ((y ∗ , V, V ∗ )), x)[er (N )] .
✷
40

Proof of proposition 8 [VN simulation]
First we fix some notation. We associate a substitution σE with an evaluation context E of
the λℓcps,vn -calculus as follows:
σ[ ] = Id

σlet

x=V in E

= [R(V )/x] ◦ σE .

Then we prove the property by case analysis.
• If R(N ) ≡ @(λy + .M, V + ) → [V + /y + ]M then N ≡ E[@(x, x+ )], σE (x) ≡ λy + .M , and
σE (x+ ) ≡ V + .
Moreover, E ≡ E1 [let x = λy + .M ′ in E2 ] and σE1 (λy + .M ′ ) ≡ λy + .M .
Therefore, N → E[[x+ /y + ]M ′ ] ≡ N ′ and we check that R(N ′ ) ≡ σE ([x+ /y + ]M ′ ) ≡
[V + /y + ]M .
• If R(N ) ≡ let x = πi ((V1 , . . . , Vn )) in M → [Vi /x]M then N ≡ E[let x = πi (y) in N ′′ ],
σE (y) ≡ (V1 , . . . , Vn ), and σE (N ′′ ) ≡ M .
Moreover, E ≡ E1 [let y = (z1 , . . . , zn ) in E2 ] and σE1 (z1 , . . . , zn ) ≡ (V1 , . . . , Vn ).
Therefore, N → E[[zi /x]N ′′ ] ≡ N ′ and we check that R(N ′ ) ≡ σE ([zi /x]N ′′ ) ≡
[Vi /x]M .
ℓ

• If R(N ) ≡ ℓ > M −
→ M then N ≡ E[ℓ > N ′′ ] and σE (N ′′ ) ≡ M . We conclude by
ℓ

observing that N −
→ E[N ′′ ].

✷

Proof of proposition 10 [CC commutation]
This is a simple induction on the structure of the term M .
@(x, y + ) We have:
er (Ccc (@(x, y + )))
≡ er (let (c, e) = x in @(c, e, y + ))
≡ let (c, e) = x in @(c, e, y + )
≡ Ccc (@(x, y + ))
≡ er (Ccc (@(x, y + ))) .
let x = C in M , C not a function We have:
er(Ccc (let x = C in M ))
≡ er (let x = C in Ccc (M ))
≡ let x = C in er (Ccc (M ))
≡ let x = C in Ccc (er (M ))
(by ind. hyp.)
≡ Ccc (er (let x = C in M )) .

41

let x = λx+ .N in M, fv(λx+ .N ) = {z1 , . . . , zk } We have:
er (Ccc (let x = λx+ .N in M ))
≡ er ( let c = λe, x+ .let (z1 , . . . , zk ) = e in Ccc (N ) in
let e = (z1 , . . . , zk ), x = (c, e) in Ccc (M ) )
≡ let c = λe, x+ .let (z1 , . . . , zk ) = e in er(Ccc (N )) in
let e = (z1 , . . . , zk ), x = (c, e) in er (Ccc (M ))
≡ let c = λe, x+ .let (z1 , . . . , zk ) = e in Ccc (er (N )) in
let e = (z1 , . . . , zk ), x = (c, e) in Ccc (er (M ))
(by ind. hyp.)
≡ Ccc (er (let x = λx+ .N in M )) .
ℓ > M We have:
er(Ccc (ℓ > M ))
≡ er(ℓ > Ccc (M ))
≡ er(Ccc (M ))
≡ Ccc (er (M ))
(by ind. hyp.)
≡ Ccc (er (ℓ > M )) .
✷

Proof of proposition 11 [CC simulation]
As a first step we check that the closure conversion function commutes with name substitution:
Ccc ([x/y]M ) ≡ [x/y]Ccc (M ) .
This is a direct induction on the structure of the term M . Then we extend the closure
conversion function to contexts as follows:
Ccc ([ ])
=[]
∗
Ccc (let x = (y ) in E)
= let x = (y ∗ ) in Ccc (E)
+
Ccc (let x = λx .M in E) = let c = λe, x+ .let (z1 , . . . , zk ) = e in Ccc (M ) in
let e = (z1 , . . . , zk ), x = (c, e) in Ccc (E)
where: fv(λx+ .M ) = {z1 , . . . , zk } .
We note that for any evaluation context E, Ccc (E) is again an evaluation context, and moreover for any term M we have:
Ccc (E[M ]) ≡ Ccc (E)[Ccc (M )] .
Finally we prove the simulation property by case analysis of the reduction rule being applied.
• Suppose M ≡ E[@(x, y + )] → E[[y + /x+ ]M ] where E(x) = λx+ .M and fv(λx+ .M ) =
{z1 , . . . , zk }. Then:
Ccc (E[@(x, y + )]) ≡ Ccc (E)[let (c, e) = x in @(c, e, y + )]
with Ccc (E)(x) = (c, e), Ccc (E)(c) = λe, x+ .let (z1 , . . . , zk ) = e in Ccc (M ) and Ccc (E)(e) =
(z1 , . . . , zk ). Therefore:
Ccc (E)[let (c′ , e′ ) = x in @(c′ , e′ , y + )]
∗
→ Ccc (E)[let (z1 , . . . , zk ) = e in [y + /x+ ]Ccc (M )]
∗
→ Ccc (E)[[y + /x+ ]Ccc (M )]
≡ Ccc (E)[Ccc ([y + /x+ ]M )]
(by substitution commutation)
≡ Ccc (E[[y + /x+ ]M ]) .
42

• Suppose M ≡ E[let x = πi (y) in M ] → E[[zi /x]M ] where E(y) = (z1 , . . . , zk ), 1 ≤ i ≤ k.
Then:
Ccc (E[let x = πi (y) in M ]) ≡ Ccc (E)[let x = πi (y) in Ccc (M )]
with Ccc (E)(y) = (z1 , . . . , zk ). Therefore:
Ccc (E)[let x = πi (y) in Ccc (M )]
→ Ccc (E)[[zi /x]Ccc (M )]
≡ Ccc (E)[Ccc ([zi /x]M )]
(by substitution commutation)
≡ Ccc (E[[zi /x]M ]) .
ℓ

• Suppose M ≡ E[ℓ > M ] −
→ E[M ]. Then:
Ccc (E[ℓ > M ])
≡ Ccc (E)[Ccc (ℓ > M )]
≡ Ccc (E)[ℓ > Ccc (M )]
ℓ

− Ccc (E)[Ccc (M )]
→
≡ Ccc (E[M ]) .
✷

Proof of proposition 12 [on hoisting transformations]
As a preliminary remark, note that the hoisting contexts D can be defined in an equivalent
way as follows:
D ::= [ ] | D[let x = C in [ ]] | D[let x = λy + .[ ] in M ] | D[ℓ > [ ]]
If D is a hoisting context and x is a variable we define D(x) as follows:

λz + .T
if D = D ′ [let x = λz + .T in [ ]]


 ′
D (x)
o.w. if D = D ′ [let y = C in [ ]], x 6= y
D(x) =
′
D (x)
o.w. if D = D ′ [let y = λy + .[ ] in M ], x ∈
/ {y + }



undefined o.w.

The intuition is that D(x) checks whether D binds x to a simple function λz + .T . If this is
the case it returns the simple function as a result, otherwise the result is undefined.
Let I be the set of terms of the λℓcps,vn such that if M ≡ D[let x = λy + .T in N ] and
z ∈ fv(λy + .T ) then D(z) = λz + .T ′ . Thus a name free in a simple function must be bound to
another simple function. We prove the following properties:
1. The hoisting transformations terminate.
2. The hoisting transformations are confluent (hence the result of the hoisting transformations is unique).
3. If a term M of the λℓcps,vn -calculus contains a function definition then M ≡ D[let x =
λy + .T in N ] for some D, T, N .
4. All terms in λℓcc,vn belong to the set I (trivially).
43

5. The set I is an invariant of the hoisting transformations, i.e., if M ∈ I and M ❀ N
then N ∈ I.
6. If a term satisfying the invariant above is not a program then a hoisting transformation
applies.
(1) To prove the termination of the hoisting transformations we introduce a size function
from terms to positive natural numbers as follows:
|@(x, x+ )|
|let x = λy + .M in N |
|let x = C in N |
|ℓ > N |

=1
= 2 · |M | + |N |
= 2 · |N |
= 2 · |N | .

Then we check that if M ❀ N then |M | > |N |. Note that the hoisting context D induces a
function which is strictly monotone on natural numbers. Thus it is enough to check that the
size of the redex term is larger than the size of the reduced term.
(h1 )

(h2 )

(h3 )

|let x = C in let y = λz + .T in M |
= 2 · (2 · |T | + |M |)
> 2 · |T | + 2 · |M |
= |let y = λz + .T in let x = C in M | .
|let x = λw+ .let y = λz + .T in M in N |
= 2 · (2 · |T | + |M |) + |N |
> 2 · |T | + 2 · |M | + |N |
= |let y = λz + .T in let x = λw+ .M in N | .
|ℓ > let y = λz + .T in M |
= 2 · (2 · |T | + |M |)
> 2 · |T | + 2 · |M |
= |let y = λz + .T in ℓ > M | .

(2) Since the hoisting transformation is terminating, by Newman’s lemma it is enough to
prove local confluence. There are 9 = 3 · 3 cases to consider. In each case one checks that the
two redexes cannot superpose. Moreover, since the hoisting transformations neither duplicate
nor erase terms, one can close the diagrams in one step.
For instance, suppose the term D[let x = λw+ .let y = λz + .T in M in N ] contains a distinct
redex ∆ of the same type (a function definition containing a simple function definition). Then
the root of this redex can be in the subterms M or N or in the context D. Moreover if it is in
D, then either it is disjoint from the first redex or it contains it strictly. Indeed, the second
let of the second redex cannot be the first let of the first redex since the latter is not defining
a simple function.
(3) By induction on M . Let F be an abbreviation for let x = λy + .T in N .
44

@(x, x+ ) The property holds trivially.
let y = C in M Then M must contain a function definition. Then by inductive hypothesis,
M ≡ D ′ [F ]. We conclude by taking D ≡ let y = C in D ′ .
let y = λx+ .M ′ in M If M is a restricted term then we take D ≡ [ ]. Otherwise, M ′ must
contain a function definition and by inductive hypothesis, M ′ ≡ D ′ [F ]. Then we take
D ≡ let y = λx+ .D ′ in M .
ℓ > M Then M contains a function definition and by inductive hypothesis M ≡ D ′ [F ]. We
conclude by taking D ≡ ℓ > D ′ .
(4) In the terms of the λℓcc,vn calculus all functions are closed and therefore the condition is
vacuously satisfied.
(5) We proceed by case analysis on the hoisting transformations.
(6) We proceed by induction on the structure of the term M .
@(x, y + ) This is a program.
let x = C in M ′ There are two cases:
• If M ′ is not a program then by inductive hypothesis a hoisting transformation
applies and the same transformation can be applied to M .
• If M ′ is a program then it has a function definition on top (otherwise M is a
program). Because M belongs to I the side condition of (h1 ) is satisfied.
let x = λy + .M ′ in M ′′ Again there are two cases:
• If M ′ or M ′′ are not programs then by inductive hypothesis a hoisting transformation applies and the same transformation can be applied to M .
• Otherwise, M ′ is a program with a function definition on top (otherwise M is a
program). Because M belongs to I the side condition of (h2 ) is satisfied.
ℓ > M ′ Again there are two cases:
• If M ′ is not a program then by inductive hypothesis a hoisting transformation
applies and the same transformation can be applied to M .
• If M ′ is a program then it has a function definition on top (otherwise M is a
program) and (h3 ) applies to M .
✷

Proof of proposition 13 [hoisting commutation]
As a preliminary step, extend the erasure function to the hoisting contexts in the obvious
way and notice that (i) if D is a hoisting context then er (D) is a hoisting context too, and
(ii) er(D[M ]) ≡ er (D)[er (M )].

45

(1) We proceed by case analysis on the hoisting transformation applied to M . The case
where er (M ) ≡ er (N ) arises in (h3 ):
D[ℓ > let x = λy + .T in M ]
❀
D[let x = λy + .T in ℓ > M ]
er (D[ℓ > let x = λy + .T in M ]) ≡ er (D[let x = λy + .T in ℓ > M ])
(2) We show that er (M ) ❀ entails that M ❀. Since er (M ) has no labels, either (h1 ) or (h2 )
apply. Then M is a term that is derived from er (M ) by inserting (possibly empty) sequences
of pre-labelling before each subterm. We check that either the hoisting transformation applied
to er (M ) can be applied to M too or (h3 ) applies.
(3) If Ch (M ) ≡ N then by definition we have M ❀∗ N 6❀. By (1) er (M ) ❀∗ er (N ), and by
(2) er (N ) 6❀. Hence Ch (er (M )) ≡ er (N ) ≡ er (Ch (M )).
✷

Proof of proposition 15 [hoisting simulation]
Definition 40 A (strong) simulation on the terms of the λℓcps,vn -calculus is a binary relation
α
α
R such that if M R N and M −
→ M ′ then there is N ′ such that N −
→ N ′ and M ′ R N ′ .
Definition 41 A (pre-)congruence on the terms of the λℓcps,vn -calculus is an equivalence relation (a pre-order) which is preserved by the operators of the calculus.
Definition 42 Let ≃ be the smallest congruence on terms of the λℓcps,vn -calculus which is
induced by structural equivalence and the following commutation of let-definitions:
let x1 = V1 in let x2 = V2 in M ≃ let x2 = V2 in let x1 = V1 in M
where: x1 6= x2 , x1 ∈
/ fv(V2 ), x2 ∈
/ fv(V1 ).
The relation ≃ is preserved by name substitution and it is a simulation.
Definition 43 Let  the smallest pre-congruence on terms of the λℓcps,vn -calculus which is
induced by structural equivalence and the following collapse of let-definitions:
let x = V in let x = V in M ≃ let x = V in M
where: x ∈
/ fv(V ).
The relation  is preserved by name substitution and it is a simulation.
Definition 44 Let Sh be the relation ≃ ◦ .
Note that Sh is a simulation too. Then we can state the main lemma.
α

Lemma 45 Let M be a term of the λℓcps,vn -calculus. If M −
→ M ′ and M ❀ N then there is
α
N ′ such that N −
→ N ′ and M ′ (❀∗ ) ◦ Sh N ′ .
Proof. As a preliminary remark we notice that the hoisting transformations are preserved
by name substitution. Namely if M ❀ N then [y + /x+ ]M ❀ [y + /x+ ]N .
There are three reduction rules and three hoisting transformations hence there are 9 cases
to consider and for each case we have to analyse how the two redexes can superpose.
As usual a term can be regarded as a tree and an occurrence in the tree is identified by a
path π which is a sequence of natural numbers.
46

• The reduction rule is
E[@(x, y + )] → E[[y + /z + ]M ]
where E(x) = λz + .M . We suppose that π is the path which corresponds to the letdefinition of the variable x and π ′ is that path that determines the redex of the hoisting
transformation.
(h1 ) There are two critical cases.
1. The let-definition that defines a function of the hoisting transformation coincides with the let-definition of x. In this case M is actually a restricted term
T . The diagram is closed in one step.
2. The path π ′ determines a subterm of M . If we reduce first then we have to
apply the hoisting transformation twice to close the diagram using the fact
that these transformations are preserved by name substitution.
(h2 ) Again there are two critical situations.
1. The top level let-definition of the hoisting transformation coincides with the
let-definition of the variable x in the reduction. This is the case illustrated by
the example 14. If we reduce first then we have to apply the hoisting transformation twice (again using preservation under name substitution). After this
we have to commute the let-definitions and finally collapse two identical ones.
2. The path π ′ determines a subterm of M . If we reduce first then we have to
apply the hoisting transformation twice to close the diagram using the fact
that these transformations are preserved by name substitution.
(h3 ) There are two critical cases.
1. The function let-definition in the hoisting transformation coincides with the
let-definition of the variable x in the reduction. We close the diagram in one
step.
2. The path π ′ determines a subterm of M . If we reduce first then we have to
apply the hoisting transformation twice to close the diagram using the fact
that these transformations are preserved by name substitution.
• The reduction rule is
E[let x = πi (y) in M ] → E[[zi /x]M ]
where E(y) = (z1 , . . . zn ) and 1 ≤ i ≤ n.
(h1 ) There are two critical cases.
1. The first let-definition in the hoisting transformation coincides with the letdefinition of the tuple in the reduction. We close the diagram in one step.
2. The first let-definition in the hoisting transformation coincides with the projection in the reduction. If we reduce first then there is no need to apply a hoisting
transformation to close the diagram because the projection disappears.
(h2 ) The only critical case arises when the redex for the hoisting transformation is
contained in M . We close the diagram in one step using the fact that the transformations are preserved by name substitution.
47

(h3 ) Same argument as in the previous case.
• The reduction rule is

ℓ

E[ℓ > M ] −
→ E[M ]
The hoisting transformations can be either in E or in M . In both cases we close the
diagram in one step.
✷
We conclude by proving by diagram chasing the following proposition. We rely on the
previous lemma and the fact that Sh is a simulation.
Proposition 46 The relation Th = ((❀∗ ) ◦ Sh )∗ is a simulation and for all terms of the
λℓcc,vn -calculus, M Th Ch (M ).

Proof of theorem 16 [commutation and simulation]
By composition of the commutation and simulation properties of the four compilation steps.

Proof of proposition 18 [labelling properties]
(1) Both properties are proven by induction on M . The first is immediate. We spell out the
second.
x Then Li (x) = x ∈ W1 ⊆ W0 .
λx+ .M Then Li (λx+ .M ) = λx+ .ℓ > L1 (M ) and by inductive hypothesis L1 (M ) ∈ W1 .
Hence, ℓ > L1 (M ) ∈ W1 and λx+ .ℓ > L1 (M ) ∈ W1 .
(M1 , . . . , Mn ) Then Li ((M1 , . . . , Mn )) = (L0 (M1 ), . . . , L0 (Mn )) and by inductive hypothesis
L0 (Mj ) ∈ W0 for j = 1, . . . , n.
Hence, (L0 (M1 ), . . . , L0 (Mn )) ∈ W1 ⊆ W0 .
πj (M ) Same argument as for the pairing.
let x = M in N Then Li (let x = M in N ) = let x = L0 (M ) in Li (N ) and by inductive
hypothesis L0 (M ) ∈ W0 and Li (N ) ∈ Wi . Hence let x = L0 (M ) in Li (N ) ∈ Wi .
@(M1 , . . . , Mn ) and i = 0 Then L0 (@(M1 , . . . , Mn )) = @(L0 (M1 ), . . . , L0 (Mn )) > ℓ and by
inductive hypothesis L0 (Mj ) ∈ W0 for j = 1, . . . , n. Hence @(L0 (M1 ), . . . , L0 (Mn )) >
ℓ ∈ W0 .
@(M1 , . . . , Mn ) and i = 1 Same argument as in the previous case to conclude that
@(L0 (M1 ), . . . , L0 (Mn )) ∈ W1 .
(2) By (1) we know that er (L(M )) ≡ M and L(M ) ∈ W0 . Then:
P

≡ C(M )
≡ C(er (L(M )))
≡ er (C(L(M ))) (by theorem 16(1)) .

48

(3) The main point is to show that the CPS compilation of a labelled term is a term where
a pre-labelling appears exactly after each λ-abstraction. The following compilation steps
(value named, closure conversion, hoisting) neither destroy nor introduce new λ-abstractions
while maintaining the invariant that the body of each function definition contains exactly one
pre-labelling.
As a preliminary step, we define a restricted syntax for the λℓcps -calculus where labels
occur exactly after each λ-abstraction.
V
M
K

::= id | λid + .ℓ > M | (V ∗ )
::= @(V, V + ) | let id = πi (V ) in M
::= id | λid .M

(restricted values)
(restricted CPS terms)
(restricted continuations)

Let us call this language λℓcps,r (r for restricted). First we remark that if V is a restricted
value and M is a restricted CPS term then [V /x]M is again a restricted CPS term. Then we
show the following property.
For all terms M of the λ-calculus and all continuations K of the λℓcps,r -calculus
the term Li (M ) | K is again a term of the λℓcps,r -calculus provided that i = 0 if
K is a function and i = 1 if K is a variable.
Notice that the initial continuation K0 = λx.@(halt , x) is a functional continuation in the
restricted calculus and recall that by definition Ccps (L(M )) = L0 (M ) | K0 . We proceed by
induction on M and case analysis assuming that if i = 0 then K = λy.N .
x, i = 0 We have: L0 (x) | K = x | K = [x/y]N .
x, i = 1 We have: Li (x) | k = x | k = @(k, x).
λx+ .M , i = 0 We have:
L0 (λx+ .M ) | K = λx+ .ℓ > L1 (M ) | K = [λx+ , k.ℓ > L1 (M ) | k/y]N
and we apply the inductive hypothesis on L1 (M ) | k and closure under value substitution.
λx+ .M , i = 1 We have:
L1 (λx+ .M ) | k = λx+ .ℓ > L1 (M ) | k = @(k, λx+ , k.ℓ > L1 (M ) | k)
and we apply the inductive hypothesis on L1 (M ) | k.
@(M1 , . . . , Mn ), i = 0 We have:
Li (@(M1 , . . . , Mn )) | K
≡ @(L0 (M1 ), . . . , L0 (Mn )) > ℓ | K
≡ @(L0 (M1 ), . . . , L0 (Mn )) | K ′
≡ L0 (M1 ) | λx1 . . . L0 (Mn ) | λxn .@(x1 , . . . , xn , K ′ )
where K ′ = λy.ℓ > N . Then we apply the inductive hypothesis on Mn , . . . , M1 with
the suitable functional continuations.
49

@(M1 , . . . , Mn ), i = 1 We have:
Li (@(M1 , . . . , Mn )) | K
≡ @(L0 (M1 ), . . . , L0 (Mn )) | K
≡ L0 (M1 ) | λx1 . . . L0 (Mn ) | λxn .@(x1 , . . . , xn , K) .
Again we apply the inductive hypothesis on Mn , . . . , M1 with the suitable functional
continuations.
(M1 , . . . , Mn ) We have:
Li ((M1 , . . . , Mn )) | K
≡ (L0 (M1 ), . . . , L0 (Mn )) | K
≡ L0 (M1 ) | λx1 . . . L0 (Mn ) | λxn .(x1 , . . . , xn ) | K .
We apply the inductive hypothesis on Mn , . . . , M1 with the suitable functional continuations.
πj (M ) We have:
Li (πj (M )) | K
≡ πj (L0 (M )) | K
≡ L0 (M ) | λx.let y = πj (x) in y | K .
We apply the inductive hypothesis on M with a functional continuation.
let x = N in M We have:

Li (let x = N in M ) | K
≡ let x = L0 (N ) in Li (M ) | K
≡ L0 (N ) | λx.Li (M ) | K .

We apply the inductive hypothesis on M and then on N with a functional continuation.
✷

Proof of proposition 20 [instrumentation vs. labelling]
As a preliminary step, we show that for all terms M and values V, V ′ of the λℓ -calculus the
following (mutually dependent) properties hold.
1. [ψ(V )/x]ψ(V ′ ) ≡ ψ([V /x]V ′ ).
2. [ψ(V )/x]I(M ) ≡ I([V /x]M ).
Let S = [V1 /x1 , . . . , Vn /xn ] denote a substitution in the λℓ -calculus. Then let ψ(S) be the
substitution [ψ(V1 )/x1 , . . . , ψ(Vn )/xn ]. We prove the following generalisation of the proposition.
For all terms M and substitutions S, if ψ(S)I(M ) ⇓ (m, V ) then I(SM ) ⇓Λ V ′ ,
costof(Λ) = m and ψ(V ′ ) ≡ V .
We proceed by induction on the length of the derivation of the judgement ψ(S)I(M ) ⇓ (m, V )
and case analysis on M .

50

We consider the case for application which explains the need for the generalisation. Suppose ψ(S)I(@(M0 , M1 , . . . , Mn )) ⇓ (m, V ). By the shape of I(@(M0 , M1 , . . . , Mn )) this entails that ψ(S)I(Mi ) ⇓ (mi , Vi ) for i = 0, . . . , n. By induction hypothesis, I(SMi ) ⇓Λi Vi′ ,
costof(Λi ) = mi , and ψ(Vi′ ) = Vi , for i = 0, . . . , n. We also have @(V0 , V1 , . . . , Vn ) ⇓ (mn+1 , V )
and m = m0 ⊕ · · · ⊕ mn+1 . Since ψ(V0′ ) = V0 , this requires V0′ = λx1 · · · xn .M ′ and
V0 = λx1 · · · xn .I(M ′ ). So we must have [V1 /x1 , . . . , Vn /xn ]I(M ′ ) ⇓ (mn+1 , V ). Again by inductive hypothesis, this entails that I([V1′ /x1 , . . . , Vn′ /xn ]M ′ ) ⇓Λn+1 V ′ , costof(Λn+1 ) = mn+1 ,
and ψ(V ′ ) = V . We conclude that I(S(@(M0 , M1 , . . . , Mn ))) ⇓Λ V ′ with Λ = Λ0 · · · Λn+1 . ✷

Proof of proposition 22 [subject reduction]
The proof of this result is standard, so we just recall the main steps.
1. Prove a weakening lemma: Γ ⊢ M : A implies Γ, x : B ⊢ M : A for x fresh.
2. Prove a substitution lemma: Γ, x : A ⊢ M : B and Γ ⊢ N : A implies Γ ⊢ [N/x]M : B;
by induction on the proof of M .
3. Derive by iteration the following substitution lemma: Γ, x1 : A1 , . . . , xn : An ⊢ M : B
and Γ ⊢ Ni : Ai for i = 1, . . . , n implies Γ ⊢ [N1 /x1 , . . . , Nn /xn ]M : B.
4. With reference to Table 2, notice that in an evaluation context one does not cross
any binder. Then we have that E[M ] ≡ [M/x]E[x] for x fresh variable. Moreover, if
Γ ⊢ E[M ] : A then for some B, Γ ⊢ M : B.
5. Now examine the 5 possibilities for reduction specified in Table 2. They all have the
shape E[∆] → E[∆′ ]. By the previous remark, it suffices to show that if Γ ⊢ ∆ : B
then Γ ⊢ ∆′ : B. Note that the typing rules in Table 14 are driven by the syntax of the
term. Then the property is checked by case analysis while appealing, for the first two
rewriting rules, to the substitution properties mentioned above.

Proof of proposition 23 [type CPS]
First, we prove the following properties at once by induction on the structure of the term
(possibly a value).
1. If Γ ⊢ V : A then Ccps (Γ) ⊢ ψ(V ) : Ccps (A).
2. If Γ ⊢ M : A then Ccps (Γ), k : ¬Ccps (A) ⊢ (M | k) : R.
3. If Γ ⊢ M : A and Ccps (Γ), Γ′ , x : Ccps (A) ⊢ N : R then Ccps (Γ), Γ′ ⊢ (M | (λx.N )) : R.
We illustrate the analysis for the cases of abstraction and application.
Abstraction Suppose Γ ⊢ λx+ .M : A+ → B is derived from Γ, x+ : A+ ⊢ M : B. We prove
the 3 properties above.
(1) By induction hypothesis (property 2), we know:
Ccps (Γ), x+ : Ccps (A)+ , k : ¬Ccps (B) ⊢ (M | k) : R .

51

Then, recalling that:
ψ(λx+ .M ) ≡ λx+ , k.(M | k) and Ccps (A+ → B) = Ccps (A)+ , ¬Ccps (B) → R ,
we derive:
Ccps (Γ) ⊢ ψ(λx+ .M ) : Ccps (A+ → B) .
(2) Recall that (λx+ .M ) | k ≡ @(k, ψ(λx+ .M )). By property 1, we derive:
Ccps (Γ) ⊢ ψ(λx+ .M ) : Ccps (A+ → B)
Then by weakening and substitution we derive
Ccps (Γ), k : ¬Ccps (A+ → B) ⊢ ψ(λx+ .M ) : Ccps (A+ → B)
Finally the application rule gives
Ccps (Γ), k : ¬Ccps (A+ → B) ⊢ ((λx+ .M ) : k) : R .
(3) Suppose additionally that Ccps (Γ), Γ′ , y : Ccps (A+ → B) ⊢ N : R. Recall that
(λx+ .M | λy.N ) ≡ [ψ(λx+ .M )/y]N . By property 1, we know that:
Ccps (Γ) ⊢ ψ(λx+ .M ) : Ccps (A+ → B) .
Then by weakening and substitution we derive that:
Ccps (Γ), Γ′ ⊢ [ψ(λx+ .M )/y]N : R .
Application Suppose Γ ⊢ @(M0 , . . . , Mn ) : B is derived from Γ ⊢ M0 : A, A ≡ A1 , . . . , An →
B, and Γ ⊢ Mi : Ai for i = 1, . . . , n. In this case, we just look at the last two properties
since an application cannot be a value.
(2) Clearly:
Ccps (Γ), Γ′ , xn : Ccps (An ) ⊢ @(x0 , x1 , . . . , xn , k) : R ,
where Γ′ ≡ x0 : Ccps (A), . . . , xn−1 : Ccps (An−1 ), k : ¬Ccps (B). By induction hypothesis (property 3) on Mn , we derive:
Ccps (Γ), Γ′ ⊢ (Mn : λxn .@(x0 , x1 , . . . , xn , k)) : R .
Then by applying the inductive hypothesis (property 3) on Mn−1 , . . . , M0 we obtain:
Ccps (Γ), k : ¬Ccps (B) ⊢ (M0 | λx0 . · · · Mn | λxn .@(x0 , x1 , . . . , xn , k)) : R .
(3) Suppose additionally that Ccps (Γ), Γ′′ , y : Ccps (B) ⊢ N : R. Then we have:
Ccps (Γ), Γ′ , Γ′′ , xn : Ccps (An ) ⊢ @(x0 , x1 , . . . , xn , λy.N ) : R ,
where Γ′ ≡ x0 : Ccps (A), . . . , xn−1 : Ccps (An−1 ). Then proceed as in the previous
case by applying the inductive hypothesis (property 3) on Mn , . . . , M0 .
The proof of the omitted cases follows a similar pattern. Now to derive proposition 23, recall
that Ccps (M ) ≡ M | λx.@(halt , x). Then we obtain the desired statement from the property 3
above observing that if Γ ⊢ M : A and Ccps (Γ), halt : ¬Ccps (A), x : Ccps (A) ⊢ @(halt , x) : R
then Ccps (Γ), halt : ¬Ccps (A) ⊢ Ccps (M ) : R.
52

Proof of proposition 24 [subject reduction, value named]
First, we prove some standard properties for the type system described in Table 15.
Weakening If Γ ⊢vn M then Γ, x : A ⊢vn M with x fresh.
Variable substitution If Γ, x : A ⊢vn M and y : A ∈ Γ then Γ ⊢vn [y/x]M . This property
generalizes to Γ, x+ : A+ ⊢vn M and y + : A+ ∈ Γ implies Γ ⊢vn [y + /x+ ]M .
Type substitution If Γ ⊢vn M then [B/t]Γ ⊢vn M .
Next, suppose Γ ⊢vn M and M → N according to the rules specified in Table 4. This
means M ≡ E[∆] where for some Γ′ , we have Γ, Γ′ ⊢vn ∆ and ∆ is either an application, or
a projection or a labelling. We consider each case in turn.
∆ ≡ @(x, y + ). Then y + : A+ ∈ Γ, Γ′ , Γ′ ≡ Γ1 , x : A+ → R, Γ2 , x is bound to some function
λz + .M ′ , and Γ, Γ1 , z + : A+ ⊢vn M ′ . By weakening, we have Γ, Γ′ , z + : A+ ⊢vn M ′ and
by substitution Γ, Γ′ ⊢vn [y + /z + ]M ′ . Then we derive Γ ⊢vn E[[y + /z + ]M ′ ] as required.
∆ ≡ let x = πi (y) in M ′ . This case splits in two sub-cases: the first for product types and
the second for existential types.
Product Γ′ ≡ Γ1 , y : ×(A1 , . . . , An ), Γ2 , 1 ≤ i ≤ n, Γ, Γ′ , x : Ai ⊢vn M ′ , and for some
z1 , . . . , zn , z1 : A1 , . . . , zn : An ∈ Γ, Γ1 . By substitution, Γ, Γ′ ⊢vn [zi /x]M ′ . Then
we derive Γ ⊢vn E[[zi /x]M ′ ] as required.
Existential i = 1, Γ′ ≡ Γ1 , y : ∃t.A, Γ2 , Γ, Γ′ , x : A ⊢vn M ′ with t ∈
/ ftv(Γ, Γ′ ), and for
some z, B, we have z : [B/t]A ∈ Γ, Γ1 . By type substitution, Γ, Γ′ , x : [B/t]A ⊢vn
M ′ and by substitution, Γ, Γ′ ⊢vn [z/x]M ′ . Then we derive Γ ⊢vn E[[z/x]M ′ ] as
required.
∆ ≡ ℓ > M ′ . Then Γ, Γ′ ⊢vn M ′ and we derive Γ ⊢vn E[M ′ ] as required.

Proof of proposition 25 [type value named]
We prove at once the following two properties:
1. If Γ ⊢ M : R then Γ ⊢vn Cvn (M ).
2. If Γ ⊢ V : A, V 6= id and Γ, y : A ⊢vn N : R then Γ ⊢vn Evn (V, y)[N ].
We proceed by induction on the structure of M and V along the pattern of the definition
of the value named translation in Table 5. We spell out two typical cases.
M ≡ @(x∗ , V, V ∗ ), V 6= id . Suppose Γ ⊢ @(x∗ , V, V ∗ ) : R. This entails Γ ⊢ V : A for some
type A. We also have Γ, y : A ⊢ @(x∗ , y, V ∗ ) : R and by inductive hypothesis (property 1) Γ, y : A ⊢vn Cvn (@(x∗ , y, V ∗ )). Then, we apply the inductive hypothesis on V
(property 2) to derive that: Γ ⊢vn Evn (V, y)[Cvn (@(x∗ , y, V ∗ ))], and this last term equals
Cvn (@(x∗ , V, V ∗ )).

53

V ≡ (x∗ , V ′ , V ∗ ), V ′ 6= id . Suppose Γ, y : A ⊢vn N and Γ ⊢ (x∗ , V ′ , V ∗ ) : A. This entails
Γ ⊢ V ′ : B for some type B and Γ, z : B ⊢ (x∗ , z, V ∗ ) : A. By weakening and inductive
hypothesis (property 2) on (x∗ , z, V ∗ ) we derive Γ, z : B ⊢vn Evn ((x∗ , z, V ∗ ), y)[N ]. Then
by inductive hypothesis on V ′ (again by property 2) we derive:
Γ ⊢vn Evn (V ′ , z)[Evn ((x∗ , z, V ∗ ), y)[N ]] ,
and this last term equals Evn ((x∗ , V ′ , V ∗ ), y)[N ].

Proof of proposition 26 [type closure conversion]
By induction on the typing of Γ ⊢vn M according to the rules specified in Table 15. We detail
the cases of abstraction and application.
Abstraction Suppose Γ ⊢vn let x = λy + .M in N is derived from Γ, y + : A+ ⊢vn M and
Γ, x : A+ → R ⊢vn N . Let us pose {z ∗ } = fv(λy + .M ). Then for some C ∗ we have
z ∗ : C ∗ ∈ Γ. We have to show that:
Ccc (Γ) ⊢vn

let
let
let
let

c = λe, y + .let (z ∗ ) = e in Ccc (M ) in
e = (z ∗ ) in
x′ = (c, e) in
x = (x′ ) in Ccc (N ) .

By inductive hypothesis on M , variable substitution, and weakening we derive: Ccc (Γ), Γ′ ⊢vn
Ccc (M ), with Γ′ ≡ c : ×(C ∗ ), Ccc (A)+ → R, e : ×(C ∗ ).
Also, by inductive hypothesis on N and weakening we derive:
Ccc (Γ), Γ′ , Γ′′ ⊢vn Ccc (N ) ,
with Γ′′ ≡ x′ : [×(C ∗ )/t]B, x : ∃t.B and B ≡ ×((t, Ccc (A)+ → R), t).
Application Suppose Γ ⊢vn @(x, y + ) is derived from x : A+ → R, y + : A+ ∈ Γ. We have to
show:
Ccc (Γ) ⊢vn let x′ = π1 (x) in
let (c, e) = x′ in @(c, e, y + ) .
Since Ccc (A+ → R) ≡ ∃t. × ((t, Ccc (A)+ → R), t), the judgement above is derived from:
Ccc (Γ), x′ : ×((t, Ccc (A)+ → R), t), c : (t, Ccc (A)+ → R), e : t ⊢vn @(c, e, y + ) .

Proof of proposition 27 [type hoisting]
First, we show the following property.
Strengthening If Γ, x : A ⊢vn P and x ∈
/ fv(P ) then Γ ⊢vn P .
Then we proceed by case analysis (3 cases) on the hoisting transformations specified in
Table 7. They all have the shape D[∆] ❀ D[∆′ ], so it suffices to show that if Γ ⊢vn ∆ then
Γ ⊢vn ∆′ . We detail the analysis for the transformation (h2 ). Suppose:
Γ ⊢vn let x = λw+ .let y = λz + .T in M in N,
54

rer (t)
e
rer (A+ −
→ R)
rer (×())
rer (×(A+ )at(r))
rer ((∃t.A)at(r))

=t
= rer (A)+ → R
= ×()
= ×(rer (A)+ )
= ∃t.rer (A)

rer (λr ∗ , x+ .T )
rer (())
rer ((x+ )at(r))

= λx+ .rer (T )
= ()
= (x+ )

rer (let x = V in P )
rer (@(x, r ∗ , y + ))
rer (let x = πi (y) in T )

= let x = rer (V ) in rer (P )
= @(x, y + )
= let x = πi (y) in rer (T )

Table 19: Region erasure for types, values and terms.
with {w+ } ∩ fv(λz + .T ) = ∅, is derived from:
(1) Γ, x : A+ → R ⊢vn N ,
(2) Γ, w+ : A+ , z + : B + ⊢vn T ,
(3) Γ, w+ : A+ , y : B + → R ⊢vn M .
Then we derive:
Γ ⊢vn let y = λz + .T in let x = λw+ .M in N .
as follows:
(1′ ) Γ, x : A+ → R, y : B + → R ⊢vn N
(2′ ) Γ, z + : B + ⊢vn T
(3′ ) Γ, w+ : A+ , y : B + → R ⊢vn M

(by (1) and weakening)
(by (2) and strengthening)
(by (3)) .

Proof theorem 28 [type preserving compilation]
Suppose M term of the λℓ -calculus and Γ ⊢ M : A. Then:
Ccps (Γ), halt : ¬Ccps (A) ⊢ Ccps (M ) : R
(by proposition 23)
Ccps (Γ), halt : ¬Ccps (A) ⊢vn Cvn (Ccps (M ))
(by proposition 25)
vn
C(Γ), halt : ∃t. × ((t, C(A) → R), t) ⊢ Ccc (Cvn (Ccps (M ))) (by proposition 26)
Next recall that the compiled term C(M ) is the result of iterating the hoisting transformations
on the term Ccc (Cvn (Ccps (M ))) a finite number of times. Hence, by proposition 27 we conclude:
C(Γ), halt : ∃t. × ((t, C(A) → R), t) ⊢vn C(M ) .

Proof of proposition 31 [decomposition]
With reference to Table 17, we know that a program P is a list of function definitions, determining the function context F , followed by a term T . The latter is a list of value definitions
and region allocations and disposals, determining the heap context H, and ending either in
an application or a projection or a labelling. This last part of the program corresponds to
the redex ∆.
55

Proof of proposition 35 [region erasure]
First, we notice that the region erasure function is invariant under region substitutions:
rer ([r ′ /r]A) = rer (A). Then we prove at once the following two properties where it is intended that the judgements on the left are derivable in the type and effect system described
in Table 18 and the ones on the right in the type system described in Table 15.
1. If Γ ⊢rg P : e then rer (Γ) ⊢vn rer (P ).
2. If Γ ⊢rg V : A then rer (Γ) ⊢vn rer (V ) : rer (A).
We detail the cases of abstraction and application.
e

→ R is derived from Γ, y + : A+ ⊢rg T : e.
Abstraction Suppose Γ ⊢rg λr ∗ , y + .T : ∀r ∗ .A+ −
+
Then by inductive hypothesis, rer (Γ), y : rer (A)+ ⊢vn rer (T ). And we conclude:
rer (Γ) ⊢vn λy + .T : rer (A)+ → R as required.
e

→ R, y + :
Application Suppose Γ ⊢rg @(x, r + , y + ) is derived from x : B ∈ Γ, B ≡ ∀r1∗ .A+ −
[r ∗ /r1∗ ]A+ ∈ Γ. Then, by the invariance property of the region erasure function noticed
above, x : rer (A)+ → R, y + : rer (A)+ ∈ rer (Γ). So we conclude: rer (Γ) ⊢vn @(x, y + )
as required.

Proof of proposition 36 [region enrichment]
We define a region enrichment function ren from the programs of the λℓh,vn -calculus to those
ℓ
of the λℓ,r
h,vn -calculus. With reference to Table 7, we recall that a program P of the λh,vn is
composed of a list of function definitions and a term. Thus P is decomposed uniquely as F [T ]
where F is a functional context defined as follows

F ::= [ ] | let id = λid + .T in F .
We fix one region variable r and define the region enrichment function relatively to it as
follows:
ren(F [T ])

= ren(F )[let all(r) in ren(T )]

(Programs)

ren([ ])
ren(let x = λy + .T in F )

=[]
= let x = λr, y + .ren(T ) in ren(F )

(Function contexts)

ren(@(x, y + ))
ren(let x = C in T )
ren(ℓ > T )

= @(x, r, y + )
= let x = ren(C) in ren(T )
= ℓ > ren(T )

(Restricted terms)

ren(())
ren((x+ ))
ren(πi (x))

= ()
= (x+ )at(r)
= πi (x)

(Restricted let-bindable terms)

The intuition is that a region r is created initially and never disposed, that all tuples are
allocated in this region, and that at every function call we pass this region as a parameter.
Then all functions when applied will produce (at most) an effect {r}.
Next we extend the region enrichment function to types as follows:
56

ren(t)

=t

ren(A+ → R)
ren(×())
ren(×(A+ ))
ren((∃t.A))

= ∀r.ren(A)+ −−→ R
= ×()
= ×(ren(A)+ )at(r)
= (∃t.ren(A))at(r)

{r}

We notice that function definitions are region closed and so are the functional types in
the image of the function ren. Let us denote with Γ0 a type context such that if x : A ∈ Γ0
then A is not a type of the shape ×(B + ) or ∃t.B. It follows that frv(ren(Γ0 )) = ∅.
We show the following enrichment property:
If Γ0 , Γ ⊢vn T then ren(Γ0 , Γ) ⊢rg ren(T ) : {r}.
We detail three cases.
Tuple construction Suppose Γ0 , Γ ⊢vn let x = (y + ) in T is derived from
Γ0 , Γ ⊢vn (y + ) : A+ and Γ0 , Γ, x : ×(A+ ) ⊢vn T .
Then we derive:
ren(Γ0 , Γ) ⊢rg let x = (y + )at(r) in ren(T ) : {r}
from:
ren(Γ0 , Γ) ⊢rg (y + )at(r) : ×(ren(A)+ )at(r)
and
ren(Γ0 , Γ), x : ×(ren(A)+ )at(r) ⊢rg ren(T ) : {r} (inductive hypothesis).
Projection Suppose Γ0 , Γ ⊢vn let x = πi (y) in T is derived from y : ×(A1 , . . . , An ) ∈ Γ,
1 ≤ i ≤ n, and Γ0 , Γ, x : Ai ⊢vn T . Then:
y : ×(ren(A1 ), . . . , ren(An ))at(r) ∈ ren(Γ) and ren(Γ0 , Γ, x : Ai ) ⊢vn ren(T ) : {r} .
Hence:
ren(Γ0 , Γ) ⊢vn ren(let x = πi (y) in T ) : {r} .
Application Suppose Γ0 , Γ ⊢vn @(x, y + ) is derived from x : A+ → R, y + : A+ ∈ Γ0 , Γ. Then
we derive ren(Γ0 , Γ) ⊢rg @(x, r, y + ) : {r} from:
{r}

x : ∀r.ren(A)+ −−→ R, y + : ren(A)+ ∈ ren(Γ0 , Γ) .
Finally, we derive from the enrichment property above the following two properties which
suffice to derive the statement:
• If Γ0 ⊢vn λx+ .T : A+ → R then ren(Γ0 ) ⊢rg ren(λx+ .T ) : ren(A+ → R).
• If Γ0 ⊢vn T then ren(Γ0 ) ⊢rg let all(r) in ren(T ) : ∅.

57

Proof of proposition 37 [progress]
First we prove by induction on the structure of a heap context the following monotonicity
property of the coherence predicate:
if Coh(H, L) and L ⊆ L′ then Coh(H, L′ ).
Let frv(H) denote the set of region variables free in a heap context. If the program
P ≡ F [H[∆]] is typable then a judgement of the form Γ ⊢rg H[∆] : e is derivable. We show
by induction on the typing of such judgement the following two properties:
1. Coh(H, frv(H)).
2. If r ∈ frv(H) then r ∈ e.
Because we assumed frv(P ) = ∅ we must have frv(H) = ∅ and by the first property we
derive Coh(H, ∅). In other terms, in a typable program without free region variables the heap
context is coherent relatively to the empty set. We look at the shape of ∆.
Labelling If ∆ is a labelling then the program may reduce.
Application If ∆ is an application @(x, r ∗ , y + ) then either the variable x is not bound in
the function context or it is bound to a function value. The fact that the number of
parameters matches the number of arguments is forced (as usual) by typing. Then a
reduction is possible.
Projection The last case is when the redex is a projection let x = πi (y) in T . Similarly to
the previous case, either y is not bound or it is bound to a tuple allocated at a region
r. Then we must be able to type a term of the shape:
Γ, y : (A)at(r) ⊢rg H[let x = πi (y) in T ]

(1)

The fact that the projection is in the right range is forced (as usual) by typing. To fire
the transition we need to check that NDis(r, H) holds. In fact let us argue that if the
predicate does not hold then the judgement (1) above cannot be typed. By inspecting
the definition of NDis(r, H) we see that for the predicate to fail, H must have the
shape H1 [dis(r) in [H2 ]] for a heap context H1 which contains neither allocations nor
disposals on the region r. But then H2 [let x = πi (y) in T ] must produce a visible effect
on r. Indeed the typing system records an effect on r when projecting y and this effect
cannot be hidden by an allocation because the region variable r is free in the context
Γ, y : (A)at(r). Then the typing of dis(r) in [H2 [let x = πi (y) in T ]] fails because the
typing forbids disposing a region which is in the effect of the continuation.

Proof of proposition 38 [subject reduction, types and effects]
First we prove some standard properties (cf. proof of proposition 24) and a specific property
on injective region substitutions.
Weakening If Γ ⊢rg P : e then Γ, x : A ⊢rg P : e with x fresh.
Variable substitution If Γ, x : A ⊢rg P : e and y : A ∈ Γ then Γ ⊢rg [y/x]P : e.
58

Type substitution If Γ ⊢rg P : e then [B/t](Γ) ⊢rg P : e.
Injective region substitution If Γ ⊢rg T : e and σ is a (finite domain) region substitution
which is injective on frv(T ) ∪ e then σΓ ⊢rg σT : σe.
We detail the proof of the last property which proceeds by induction on the typing proof
of Γ ⊢rg T : e.
Application Suppose Γ ⊢rg @(x, r ∗ , y + ) : [r ∗ /r1∗ ]e is derived from x : B, y + : [r ∗ /r1∗ ]A+ ∈ Γ,
e
→ R, frv(B) = ∅, r ∗ distinct variables. Notice that frv(A+ ) ∪ e ⊆ {r1∗ }. It
B ≡ ∀r1 .A+ −
follows that frv(@(x, r ∗ , y + )) ∪ [r ∗ /r1∗ ]e = {r ∗ }. So suppose σ is an injective substitution
on r ∗ so that r ′∗ = (σr)∗ . We remark:
σB
σ[r ∗ /r1∗ ]A+
σ[r ∗ /r1∗ ]e
σ@(x, r ∗ , y + )
σr ∗

≡B
≡ [r ′∗ /r1∗ ]A+
≡ [r ′∗ /r1∗ ]e
≡ @(x, r ′∗ , y + )
distinct

Then we can prove σΓ ⊢rg σ@(x, r ∗ , y + ) : σ([r ∗ /r1∗ ]e) by the typing rule for application.
Unit Suppose Γ ⊢rg let x = () in T : e is derived from Γ, x : ×() ⊢rg T : e and σ is injective
on frv(let x = () in T ) ∪ e. Then σ is injective on frv(T ) ∪ e, by inductive hypothesis
σΓ, x : ×() ⊢rg σT : σe, and we conclude σΓ ⊢rg σ(let x = () in T ) : σe.
Product Suppose
Γ ⊢rg let x = (y + )at(r) in T : e ∪ {r}
is derived from
Γ, x : ×(A+ )at(r) ⊢rg T : e,
y + : A+ ∈ Γ and σ is injective on the set:
frv(let x = (y + )at(r) in T ) ∪ e ∪ {r} = frv(T ) ∪ e ∪ {r} .
Then σ is injective on frv(T ) ∪ e. By inductive hypothesis:
σΓ, x : (×(σA+ ))at(σr) ⊢rg σT : σe .
Moreover y + : (σA)+ ∈ σΓ. So we conclude:
σΓ ⊢rg (let x = (y + )at(σr) in T ) : σe ∪ {σr} .
Existential This case is similar to the previous one. Suppose:
Γ ⊢rg let x = (y)at(r) in T : e ∪ {r}
is derived from:
Γ, x : (∃t.A)at(r) ⊢rg T : e ,
y : [B/t]A ∈ Γ and σ is injective on the set:
frv(let x = (y)at(r) in T ) ∪ e ∪ {r} = frv(T ) ∪ e ∪ {r} .
59

Then σ is injective on frv(T ) ∪ e. By inductive hypothesis:
σΓ, x : (∃t.σA)at(σr) ⊢rg σT : σe .
Moreover y : σ[B/t]A ∈ σΓ. We notice σ[B/t]A ≡ [σB/t]σA and σ(∃t.A) ≡ ∃t.σA.
Then we conclude:
σΓ ⊢rg (let x = (y)at(σr) in T ) : σe ∪ {σr} .
Projection Suppose:
Γ ⊢rg let x = πi (y) in T : e ∪ {r}
is derived from y : ×(A1 , . . . , An )at(r) ∈ Γ, 1 ≤ i ≤ n, Γ, x : Ai ⊢rg T : e, and σ is
injective on frv(let x = πi (y) in T ) ∪ e ∪ {r}. Then σ is injective on frv(T ) ∪ e and by
inductive hypothesis:
σΓ, x : σ(×(A1 , . . . , An )at(r)) ⊢rg σT : σe .
We conclude:
σΓ ⊢rg σ(let x = πi (y) in T ) : σe ∪ {σr} .
The case where y has an existential type is similar.
Disposal Suppose Γ ⊢rg dis(r) in T : e ∪ {r} is derived from Γ ⊢rg T : e, r ∈
/ e, and σ is
injective on frv(dis(r) in T ) ∪ e ∪ {r}. Then σ is injective on frv(T ) ∪ e and by inductive
hypothesis σΓ ⊢rg σT : σe. Also σr ∈
/ σe. We conclude:
σΓ ⊢rg σ(dis(r) in T ) : σe ∪ {σr} .
Allocation Suppose Γ ⊢rg let all(r) in T : e is derived from Γ ⊢rg T : e ∪ {r}, r ∈
/ e ∪ frv(Γ),
and σ is injective on frv(let all(r) in T ) ∪ e. Up to renaming, we can choose r so that
it is not in the domain or image of σ. Then σ is injective on frv(T ) ∪ e ∪ {r} and by
inductive hypothesis σΓ ⊢rg σT : σe ∪ {σr}. Also, by the choice above, σr ∈
/ σe ∪ σΓ.
rg
We conclude σΓ ⊢ σ(let all(r) in T ) : σe.
Labelling Suppose Γ ⊢rg ℓ > T : e is derived from Γ ⊢rg T : e and σ is injective on frv(ℓ >
T )∪{e}. By inductive hypothesis σΓ ⊢rg σT : σe and we conclude σΓ ⊢rg σ(ℓ > T ) : σe.
Subeffect Suppose Γ ⊢rg P : e is derived from Γ ⊢rg P : e′ , e′ ⊆ e, and σ is injective on
frv(P ) ∪ e. By inductive hypothesis σΓ ⊢rg σP : σe′ and we conclude σΓ ⊢rg σP : σe.
If ΓP ⊢rg P : eP then we know that P ≡ F [H[∆]] and the reduced term has the shape
F [H[∆′ ]]. For some Γ we have Γ ⊢rg ∆ : e′ . We show that then Γ ⊢rg ∆′ : e′ and frv(∆′ ) ⊆
frv(∆). Then we claim that the typing proof for the surrounding context F [H] can be ported
to the program F [H[∆′ ]].
We proceed by case analysis on the reduction rule applied and its typing. Notice that
the typing is syntax directed except for the subeffect rule. So for instance, if Γ ⊢rg ∆ : e′
and ∆ is an application then for some e′′ ⊆ e′ we can derive Γ ⊢rg ∆ : e′′ where the last rule
being applied is the one for application. A similar argument holds for the cases where ∆ is a
projection or a labelling.
60

Application Suppose Γ ⊢rg @(x, r ∗ , y + ) : e′′ with e′′ = [r ∗ /r1∗ ]e is derived from x : B, y + :
e
→ R, frv(B) = ∅, r ∗ distinct variables. Since the program
[r ∗ /r1∗ ]A+ ∈ Γ, B ≡ ∀r1 .A+ −
reduces, x must be bound to a region closed function λr1∗ , z + .T in the functional context
F and Γ1 , z + : A+ ⊢rg T : e where Γ1 is a prefix of Γ and {r1∗ } ∩ frv(Γ1 ) = ∅. We notice
that the substitution σ = [r ∗ /r1∗ ] is injective on frv(T ) ∪ e ⊆ {r1∗ }, hence by the injective
substitution property we derive:
Γ1 , z + : (σA)+ ⊢rg σT : σe .
Notice that we must have y + : (σA)+ ∈ Γ1 hence by the variable substitution property
and weakening we derive:
Γ ⊢rg σ[r ∗ /r1∗ , y + /z + ]T : [r ∗ /r1∗ ]e .
We conclude by noticing that:
frv([r ∗ /r1∗ , y + /z + ]T ) ⊆ frv(@(x, r ∗ , y + )) = {r ∗ } .
Projection Suppose Γ ⊢rg let x = πi (y) in T : e ∪ {r} is derived from y : ×(A1 , . . . , An ) ∈ Γ,
1 ≤ i ≤ n Γ, x : Ai ⊢rg T : e. Since the program reduces, y must be bound to a tuple
(z1 , . . . , zn )at(r) in the heap context H and z1 : A1 , . . . , zn : An ∈ Γ. Then by variable
substitution we derive Γ ⊢rg [zi /x]T : e. Also notice that frv([zi /x]T ) = frv(let x =
πi (y) in T ).
The case where y has an existential type is similar except that it relies on type substitution too (cf. proof of proposition 24).
ℓ

Labelling Suppose Γ ⊢rg ℓ > T : e is derived from Γ ⊢rg T : e. Since ∆ ≡ ℓ > T −
→ T , the
conclusion is immediate.

Proof of theorem 39 [region simulation]
First, we observe that the region erasure function commutes with variable substitution:
[x/y]rer (T ) ≡ rer ([x/y]T ) .
By proposition 31, P decomposes as F [H[∆]] where ∆ is either an application, or a projection,
or a labelling. The region erasure function commutes with this decomposition too, so that we
can write rer (P ) as rer (F )[rer (H)[rer (∆)]], where rer (F )[rer (H)] is an evaluation context.
α
If rer (P ) −
→ Q then we proceed by case analysis on the reduction rule being applied. We
detail the case where ∆ is an application @(x, r ∗ , y + ). Then we must have F ≡ F1 [let x =
λr1∗ , z + .T in F2 ] and
rer (P ) ≡ rer (F1 )[let x = λz + .rer (T ) in rer (F2 )[rer (H)[@(x, y + )]]
→ rer (F1 )[let x = λz + .rer (T ) in rer (F2 )[rer (H)[[y + /z + ]rer (T )]] .
Since P is typable, the heap context is coherent and then P can simulate the reduction above
as follows:
P → F [H[[r ∗ /r1∗ , y + /z + ]T ]]
noticing that rer ([r ∗ /r1∗ , y + /z + ]T ) ≡ [y + /z + ]rer (T ) (initial remark and invariance of the
region erasure function under region substitutions).
61

