# Closure Conversion, Flat Environments, and the Complexity of Abstract Machines

Beniamino Accattoli, Cláudio Belo Lourenço, Dan R. Ghica, Giulio Guerrieri, Claudio Sacerdoti Coen

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

To cite this version:

Beniamino Accattoli, Cláudio Belo Lourenço, Dan R. Ghica, Giulio Guerrieri, Claudio Sacerdoti Coen. Closure Conversion, Flat Environments, and the Complexity of Abstract Machines. PPDP2025 - 27th International Symposium on Principles and Practice of Declarative Programming, Sep 2025, Rende, Italy. pp.1 - 15, 10.1145/3756907.3756922. hal-05454748

HAL Id: hal-05454748

https://hal.science/hal-05454748v1

Submitted on 12 Jan 2026

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

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

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

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Closure Conversion, Flat Environments, and the Complexity of Abstract Machines

Beniamino Accattoli

Inria & LIX, École Polytechnique

Palaiseau, France

beniamino.accattoli@inria.fr

Cláudio Belo Lourenço

Huawei Central Software Institute

Edinburgh, United Kingdom

claudio.lourenco@huawei.com

Dan R. Ghica

Huawei Central Software Institute

Edinburgh, United Kingdom

University of Birmingham

Birmingham, United Kingdom

dan.ghica@huawei.com

Giulio Guerrieri

University of Sussex

Brighton, United Kingdom

g.guerrieri@sussex.ac.uk

Claudio Sacerdoti Coen

Università di Bologna

Bologna, Italy

claudio.sacerdoticoen@unibo.it

## Abstract

Closure conversion is a program transformation at work in compilers for functional languages to turn inner functions into global ones, by building *closures* pairing the transformed functions with the *environment* of their free variables. Abstract machines rely on similar and yet different concepts of *closures* and *environments*. We study the relationship between the two approaches. We adopt a simple $\lambda$-calculus with tuples as source language and study abstract machines for both the source language and the target of closure conversion. Moreover, we focus on the simple case of flat closures/environments (no sharing of environments). We provide three contributions. Firstly, a new simple proof technique for the correctness of closure conversion, inspired by abstract machines. Secondly, we show how the closure invariants of the target language allow us to design a new way of handling environments in abstract machines, not suffering the shortcomings of other styles.

Thirdly, we study the machines from the point of view of time complexity. We show that closure conversion decreases various dynamic costs while increasing the size of the initial code. Despite these changes, the overall complexity of the machines before and after closure conversion turns out to be the same.

## CCS Concepts

* Theory of computation → Lambda calculus; Abstract machines; Operational semantics; Invariants; Software and its engineering → Compilers.

## Keywords

Lambda calculus, abstract machine, program transformation

## ACM Reference Format:

Beniamino Accattoli, Cláudio Belo Lourenço, Dan R. Ghica, Giulio Guerrieri, and Claudio Sacerdoti Coen. 2025. Closure Conversion, Flat Environments, and the Complexity of Abstract Machines. In *Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming*

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

This work is licensed under a Creative Commons Attribution 4.0 International License.
PPDP '25, Rende, Italy

© 2025 Copyright held by the owner/author(s).
ACM ISBN 979-8-4007-2085-7/25/09
https://doi.org/10.1145/3756907.3756922

(PPDP '25), September 10–11, 2025, Rende, Italy. ACM, New York, NY, USA, 15 pages. https://doi.org/10.1145/3756907.3756922

## 1 Introduction

A feature of functional languages, as well as of the $\lambda$-calculus on which they are based, is the possibility of defining *inner functions*, that is, functions defined inside the definition of other functions. The tricky point is that inner functions can also use the external variables of their enveloping functions. For instance, the Church numerical $\frac{3}{2} := \lambda x.\lambda y.x(xy)$ contains the inner function $\lambda y.x(x(y))$ that uses the externally defined variable $x$.

The result of functional programs can be a function. In particular, it can be the instantiation of an inner function. For instance, the result of applying $\frac{3}{2}$ above to a value $v$ is the instantiated function $\lambda y.v(v(y))$, as one can easily see by doing one $\beta$-reduction step.

*Closure Conversion.* In practice, however, compiled functional programs do not follow $\beta$-reduction literally, nor do they produce the code of the instantiated function itself, because the potential duplications of the substitution process would be too costly. The idea is to decompose $\beta$-reduction in smaller, micro steps, delaying substitution as much as possible, and computing representations of instantiated functions called *closures*. A closure, roughly, is the pair of the defined inner function (that is, before instantiation) plus the tuple of instantiations for its free variables, called its *environment*.

This is achieved via a program transformation called *closure conversion*, that re-structures the code turning beforehand all inner functions into closures. At compile time, closures pair inner functions with *initial environments* that simply contain the free variables of the functions. Execution shall then dynamically fill up the environments with the actual instantiations.

*Compilation and Abstract Machines.* Abstract machines are often seen as a technique alternative to compilation and related to the interpretation of programming languages. This is because abstract machines tend to be developed for the source language, before the pipeline of transformations and optimizations of the compiler.

A *first aim* of our paper is to take a step toward closing the gap between compilation and abstract machines, by studying how transformations used by compilers—here closure conversion—induce
invariants exploitable for the design of machines working at further stages of the compilation pipeline, while still being abstract.

*Same Terminology, Different Concepts.* Similarly to compilation, abstract machines do not follow $\beta$-reduction literally, nor do they produce the code of instantiated functions. In particular, some abstract machines use data structures called again *closures* and *environments*. These notions, however, are similar and yet *different*.

In closure conversion, an inner function with free variables is transformed at compile time into a closed function paired with the environment of its free variables. The environment is in general *open* (it is closed by some enveloping converted function, yet locally it is open), and shall be filled/closed only during execution, which provides the instantiations. The aim is to hoist the closed function up to global scope while its environment stays at the call site.

In abstract machines, every piece of code receives an environment, not just functions, and environments and closures have a mutually recursive structure. Additionally, environments are built dynamically, during execution, not in advance, and they are always closed: the pair of a piece of code and its environment is called a *closure* because they read back (or decode) to a closed $\lambda$-term. Moreover, there is no hoisting of code.

A second aim of this paper is to establish and clarify the relationship between these two approaches. To disambiguate, we keep *closures* for the pairs (*closed function, possibly open environment*) of closure conversion and use *m-closures* for the pairs (*code, closed environment*) used in abstract machines; we further disambiguate calling *bags* the environments of closures, while the environments of *m-closures* keep their usual names. With respect to this terminology, we study *closure conversion for m-closures*. One of the outcomes of closure conversion turns out to be the elimination of *m-closures*.

*Complexity of Abstract Machines.* Finally, a last influence on our study comes from the recent development by Accattoli and co-authors of both a complexity-based theory of abstract machines [2–4, 6, 9, 12, 13, 20] and time and space reasonable cost models for the $\lambda$-calculus [7, 8, 10]. Such a line of work has developed fine analyses of tools and techniques for abstract machines, studying how different kinds of environments and forms of sharing impact on the cost of execution of abstract machines. The *third aim* of the paper is to understand how tuples and closure conversions affect environments, forms of sharing, and the cost of execution.

To avoid misunderstandings, our aim is not the study of optimized/shared notions of (compiler) closures, their efficient representations, their minimization, or the trade-off between access time and allocation time—in fact, we adopt the basic form of *flat closure conversion* that we apply to *all* functions for *all* their free variables.

*Flat Environments.* Different data structures for (m-)closures and bags/environments and various closure conversion algorithms can be used. The design space, in particular, is due to chains of nested functions—say, *f* is nested inside *g*, in turn, nested inside *h*—where two consecutive nested functions, *f* and *g*, can both use variables, say *x*, of *h*. Therefore, one might want the closures for *f* and *g* to share the environment entry for *x*. Perhaps surprisingly, sharing bags between closures can easily break *safety for space* of closure conversion, i.e. might not preserve the space required by the source program, if parts of shared environments survive the lifespan of

<figure><img src="image_4.png" /><figcaption>**Figure 1: $\lambda$-Calculi and abstract machines in the paper.**</figcaption></figure>

the associated closures. The simplest approach is using *flat bags* (and flat closure conversion), where no sharing between bags is used; with flat bags, there are two distinct but identical entries for *x* in the bags of *f* and *g*. Flat bags are safe for space [31, 35, 36].

Machine environments can also either be shared or flat (i.e. with no sharing between environments). The distinction, however, is not often made since it does not show up in the abstract specification of the machine, but only when one concretely implements it or studies the complexity of the overhead of the machine (since the two techniques have different costs). For a meaningful comparison with flat closure conversion, for source programs we adopt an abstract machine meant to be implemented using flat environments.

Our aim is to understand how closure conversion compares *asymptotically* with m-closures of abstract machines, in particular with respect to one of the key parameters for time analyses, the size of the initial term. Flat environments are chosen for their simplicity and their safeness for space. More elaborated forms are future work.

*Our Setting.* We decompose closure conversion in two phases, first going from a source calculus $\lambda_{\text{sou}}$ to an intermediate one $\lambda_{\text{int}}$, and then to a target calculus $\lambda_{\text{tar}}$. We provide each of the three calculi with its own abstract machine. Our setting is summed up in Fig. 1, where TAM stands for *tupled abstract machine*.

Our source $\lambda$-calculus $\lambda_{\text{sou}}$ is the simplest possible setting accommodating closure conversion, that is, Plotkin's effect-free call-by-value $\lambda$-calculus extended with tuples, because tuples are needed to define the conversion. Our setting is untyped, because it is how abstract machines are usually studied, and for the sake of minimality.

The first transformation $\_ : \lambda_{\text{sou}} \rightarrow \lambda_{\text{int}}$, dubbed *wrapping*, replaces abstractions $\lambda\tilde{x}.t$ (where $\tilde{x}$ is a sequence of variables) with the dedicated construct of *abstract closures* $\lambda\tilde{x}.t := [[\lambda\tilde{y}.\lambda\tilde{x}.t|\tilde{y}]]$ where $\tilde{y}$ is the sequence of free variables of $\lambda\tilde{x}.t$, and $|\tilde{y}$ is the tuple of these same variables, forming the *initial bag* of the closure.

Roughly, the second transformation $\lambda_{\text{int}} \rightarrow \lambda_{\text{tar}}$, deemed *name elimination*, turns the abstraction $\lambda\tilde{y}$ of many variables into the abstraction of a single variable representing the bag/environment. It is similar to a translation from named variables to de Bruijn indices. In fact, name elimination is only outlined in the paper, the details are given in [5], because they are mostly routine.

The target calculus $\lambda_{\text{tar}}$ is not the low-level target language of a compiler. It is indeed still high-level, because we study only flat closure conversion, not the whole compilation pipeline. We do not model the hoisting of closed functions up to global scope; it is an easy aspect of closure conversion and is usually avoided in its study.

We give three contributions, shaping the paper into three parts.

*Contribution 1: A Simple Proof of Correctness.* The correctness of closure conversion is often showed by endowing both the source and the target calculus of the transformation with big-step operational semantics and establishing a logical relation between the two
[16, 28, 31, 37]. The reason is that adopting a small-step semantics does not seem to work: closure conversion does not commute with meta-level substitution (that is, the substitution of converted terms is not the conversion of the substituted terms), and thus it does not map $\beta$-steps from the source to the target calculus.

Bowman and Ahmed [18] are to our knowledge the only ones adopting a small-step semantics. They neatly get around the non-commutation issue by noticing that the substitution of converted terms is $\eta$-equivalent to the conversion of the substituted terms. Our proof technique looks at the same issue in a different way, inspired by correctness proofs for abstract machines and independently of $\eta$-equivalence (which we do not consider for our calculi, for the sake of minimality). It might be of interest for languages where $\eta$-equivalence is not sound (e.g. because of observable effects, as in OCaml, or when $\eta$-equivalence does not preserve typability, like in languages with mutability and the value restriction), since in these cases Bowman and Ahmed's proof might not scale up.

**Contribution 2: New Kinds of Machine Environments.** According to Fernández and Siafakas [23], there are two kinds of abstract machines, those using many (shared or flat) *local environments*, which are defined by mutual induction with m-closures, and those using a single (necessarily flat) *global environment* or *heap* and no m-closures. Each kind has pros and cons, there is no absolute better style of machine environments; see also Accattoli and Barras [4].

For our machine for the source calculus $\lambda_{\text{sou}}$, the Source TAM, we adopt flat local environments and m-closures, so as to allow us to compare closures (with flat bags) and m-closures. The contribution here is that the invariants enforced by flat closure conversion (more precisely, by wrapping) enable a new management of environments, what we dub *stackable environments* and plug into the Int TAM, our machine for the intermediate calculus $\lambda_{\text{int}}$. Stackable environments have the pros of both global and local environments, and none of their cons, as explained in Sect. 8. They are called *stackable* because the current one can be put on hold—on the stack—when entering a closed function with its new environment, and re-activated when the evaluation of the function is over. But be careful: their stackability is not necessarily an advantage, it is just the way they work; the advantage is the lack of the cons of local and global environments.

Moving to the target calculus $\lambda_{\text{tar}}$ enables a further tweak of environments, adopted by the Target TAM: environments—which usually are *maps* associating variables to values—become *tuples* of values, with no association to variables. This is enabled by *name elimination*, which turns variables into indices referring to the tuple, in a way reminiscent of de Bruijn indices.

**Contribution 3: Time Complexity.** We study how tuples and flat closure conversion impact the forms of sharing and the time complexity of the machines. Our analyses produce four insights:

(1) *Tuples raise the overhead:* we give a theoretical analysis of the cost of adding tuples to the pure $\lambda$-calculus, which, to our knowledge, does not appear anywhere in the literature. We show why tuples require their own form of sharing and that the *creation of tuples* at runtime is unavoidable. This is done by adapting *size exploding families* from the study of reasonable time cost models for the $\lambda$-calculus [1]. Moreover, tuples raise the dependency on the size $|t|$ of the initial code t

$$ \begin{array}{l@{\quad}l@{\quad}l@{\quad}l} \text{TERMS} & t, u, s, r & ::= & x \mid \lambda x.t \mid tu & \multicolumn{1}{c}{(\lambda x.t)v \mapsto \beta_v t \{x \leftarrow v\}} \\ \text{VALUES} & v, v' & ::= & \lambda x.t & t \mapsto \beta_v u \\ \text{Ev. CTXS} & C, C' & ::= & \langle \cdot \rangle \mid tC \mid Cv & \frac{C\langle t \rangle \mapsto \beta_v C\langle u \rangle}{C\langle t \rangle \mapsto \beta_v u} \end{array} $$

<caption>**Figure 2: The untyped pure call-by-value calculus $\lambda_{\text{cbv}}$**</caption>

of the overhead of the machine. Namely, let the height $\text{hg}(t)$ be the maximum number of bound variables of $t$ in the scope of which a sub-term of $t$ is contained: the dependency for flat environments raises from $O(\text{hg}(t))$ to $O(|t| \cdot \text{hg}(t))$.

(2) *Name elimination brings a logarithmic speed-up:* with variable names, flat environments have at best $O(\log(\text{hg}(t)))$ access time, while de Bruijn indices (or our name elimination) enable $O(1)$ access time—this is true both before and after closure conversion. Before conversion, however, the improvement does not lower the overall asymptotic overhead of the machine with respect to the size of the initial term, which is dominated by the other flat environment operations. After closure conversion, instead, it does lower the overall dependency of the machine from $O(|t^{cc}| \cdot \text{hg}(t^{cc}))$ to $O(|t^{cc}|)$, where $t^{cc}$ is $t$ after closure conversion.

(3) *Amortized constant cost of transitions:* in any abstract machine, independently of their implementation, the number of transitions of an execution and the cost of some single transitions depend on the size of the initial term. This is related to the higher-order nature of $\lambda$-calculi. Closure conversion impacts on the cost of single transitions (but not on their number): their amortized cost becomes constant. The insight is that the non-constant cost of transitions in ordinary abstract machines is related to inner functions.

(4) *Dynamically faster, statically bigger, overall the same:* the previous two points show that closure conversion decreases the dependency of machines on the size of the initial term during execution. The dynamic improvement however is counter-balanced by the fact that $|t^{cc}|$ is possibly bigger than $|t|$, namely $|t^{cc}| \in O(|t| \cdot \text{hg}(t))$. Therefore, the overall complexity is $O(|t| \cdot \text{hg}(t))$ also after closure conversion.

*OCaml Code and Proofs.* As additional material on GitHub [33], we provide an OCaml implementation of the Target TAM, the machine for closure converted terms, described in [5, Appendix K]. All proofs are in [5], the long version of this paper.

## 2 Preliminaries: $\lambda_{\text{cbv}}$, a Call-by-Value $\lambda$-Calculus

In Fig. 2 we present $\lambda_{\text{cbv}}$, a variant of Plotkin's call-by-value $\lambda$-calculus [32] with its $\beta$-reduction by value $\rightarrow \beta_v$, adopting two specific choices. Firstly, the only values are $\lambda$-abstractions. Excluding variables from values differs from [32] but is common in the machine-oriented literature. It does not change the result of evaluation while inducing a faster substitution process, see [14].

Secondly, we adopt a small-step operational semantics, defined via evaluation contexts. Evaluation contexts $C$ are special terms with exactly one occurrence of the *hole* constant $\langle \cdot \rangle$. We write $C\langle t \rangle$ for the term obtained from the evaluation context $C$ by replacing its hole with the term $t$ (possibly capturing some free variables of $t$).

The small-step rule of $\beta_v$-reduction is weak, that is, it does not evaluate abstraction bodies (indeed, the production $\lambda x.C$ is absent
<figure><img src="image_5.png" /><figcaption>**Figure 3: The source calculus $\lambda_{\text{sou}}$ extending $\lambda_{\text{cbv}}$ with tuples.**</figcaption></figure>

in the definition of evaluation context C in Fig. 2), as it is common in functional programming languages, and deterministic, namely proceeding from right to left (as forced by the production $Cv$)$^1$.

We identify terms up to $\alpha$-renaming; $t\{x\leftarrow u\}$ stands for metalevel capture-avoiding substitution of $u$ for the free occurrences of $x$ in $t$.

The lemma below rests on the closed hypothesis and will be used as a design check for the calculi in the next sections. It is an untyped instantiation of Wright and Felleisen's uniform evaluation property [41]. The term "harmony" is borrowed from [11].

**LEMMA 2.1 ($\lambda_{\text{cbv}}$ HARMONY).** If $t \in \lambda_{\text{cbv}}$ is closed, then either $t$ is a value or $t \to \beta_o$ $u$ for some closed $u \in \lambda_{\text{cbv}}$.

**Notations.** We set some notations for both calculi and machines. Let $\to$ be a reduction relation. An evaluation sequence $e: t \to^* u$ is a possibly empty finite sequence of $\to$-steps from $t$ to $u$, the length of which is noted $|e|$ (we also write $e: t \to^k u$ if $|e| = k$). If moreover $\to_a \subseteq \to$, then $|e|_a$ is the number of $a$-steps in $e$.

### 3 Part 1: The Source Calculus $\lambda_{\text{sou}}$

In this section, we extend $\lambda_{\text{cbv}}$ with tuples, which are needed to define closure conversion, obtaining $\lambda_{\text{sou}}$, our source calculus.

**Terms.** The source calculus $\lambda_{\text{sou}}$ defined in Fig. 3 adopts n-ary tuples $\vec{t} = (t_1, \dots, t_n)$, together with projections $\pi_i$ on the $i^{th}$ element$^2$. Abstractions are now on sequences of variables $\tilde{x} = x_1, \dots, x_n$. With a slight abuse, we also compact $(\tilde{t}_1, \dots, \tilde{t}_n)$ into $(\tilde{t})$, and write $(\tilde{t}, u, \tilde{s})$ (note that replacing sequences with tuples changes the meaning: $(\tilde{t}, u, \tilde{s})$ and $(\tilde{t}, u, \tilde{s})$ are different terms, and we shall need both notations). Both tuples and sequences of variables can be empty, that is, $\lambda.t$ and $\|\|$ are terms of $\lambda_{\text{sou}}$. Values now are abstractions and tuples of values—tuples of arbitrary terms are not values in general.

**Notations and Conventions about Tuples and Sequences.** We assume that in every sequence $\tilde{x}$ all elements are distinct and, for brevity, we abuse notations and consider sequences of variables also as the sets of their elements, writing $x_i \in \tilde{x}$, or $fv(t) = \tilde{x}$, or $\tilde{x} \cup \tilde{y}$. We set $\|\vec{t}\| := n$ if $\vec{t} = (t_1, \dots, t_n)$ and call it the length of the tuple $\vec{t}$ (so, $\|\|\| = 0$), and similarly for $\|\tilde{x}\|$. Moreover, if $\tilde{x} = x_1, \dots, x_n$ and $\vec{v} = (v_1, \dots, v_n)$ we then set $t\{\tilde{x} \leftarrow \vec{v}\} := t\{x_1 \leftarrow v_1, \dots, x_n \leftarrow v_n\}$ (the simultaneous substitution). We write $\tilde{x}^{\#\tilde{y}}$ when $\tilde{x}$ and $\tilde{y}$ have no element in common, and $fv(t) \subseteq \tilde{x}^{\#\tilde{y}}$ when moreover $fv(t) \subseteq (\tilde{x} \cup \tilde{y})$.

**Small-Step Operational Semantics.** The $\beta_o$-rule can fire only if the argument is a tuple of values of the right length, and similarly for the $\pi$-rule. For instance, $(\lambda x.x)(\lambda y.yy) \leftrightarrow \beta_o \lambda y.yy$,

<figure><img src="image_6.png" /><figcaption>**Figure 4: The intermediate calculus $\lambda_{\text{int}}$**</figcaption></figure>

because one needs a unary tuple around the argument, that is, $(\lambda x.x)(\|\lambda.y.yy\|) \to \beta_o \lambda.y.yy$. Note that evaluation contexts now enter projections and tuples, proceeding right-to-left. As it shall be the case for all calculi in this paper, the operational semantics $\to_{\text{sou}}$ of $\lambda_{\text{sou}}$ is deterministic: if $t \to_{\text{sou}} u$ and $t \to_{\text{sou}} s$ then $u = s$ and $t$ is not a value. The proof is a routine induction (see [5, Appendix A]).

**Clashes.** In an untyped setting, there might be terms with clashes, that is, irreducible badly formed configurations such as $\pi_i(\lambda x.t)$. To exclude clashes without having to have types, we adopt a notion of clash-freeness, which would be ensured by any type system.

**Definition 3.1 (Clashes, clash-free terms).** A term $t$ is a clash if it has shape $C\langle u \rangle$ where $u$ has one of the following forms:

* Clashing projection: $u = \pi_i v$ and if $v = \vec{v}$ then $\|\vec{v}\| < i$;

* Clashing abstraction: $u = (\lambda \tilde{x}.s)v$ and if $v = \vec{v}$ then $\|\tilde{x}\| \neq \|\vec{v}\|$;

* Clashing tuple: $u = \vec{r}s$.

A term $t$ is clash-free when, co-inductively, $t$ is not a clash and if $t \to_{\text{sou}} u$ then $u$ is clash-free.

Note that clashes are normal forms. All the calculi and machines of the paper shall come with their notion of clash and clash-freeness, which shall be taken into account in statements and proofs but the definitions of which shall be omitted (they are in [5]).

**LEMMA 3.2 ($\lambda_{\text{sou}}$ HARMONY).** If $t \in \lambda_{\text{sou}}$ is closed and clash-free, then either $t$ is a value or $t \to_{\text{sou}} u$ for some closed and clash-free $u$.

### 4 Part 1: the Intermediate Calculus $\lambda_{\text{int}}$ and the Wrapping Transformation

In this section, we define the intermediate calculus $\lambda_{\text{int}}$ and the wrapping translation from $\lambda_{\text{sou}}$ to $\lambda_{\text{int}}$. We discuss why the natural first attempt to show the correctness of the translation does not work, and solve the issue via a reverse translation from $\lambda_{\text{int}}$ to $\lambda_{\text{sou}}$.

**Terms of $\lambda_{\text{int}}$.** In $\lambda_{\text{int}}$, defined in Fig. 4, abstractions $\lambda \tilde{x}.t$ are replaced by closures $[\lambda \tilde{y}.\lambda \tilde{x}.t|b]$, which are compactly noted $[\tilde{y}; \tilde{x}.t|b]$. The bag $b$ of a closure can be of two forms $\vec{z}$ and $\vec{v}$, giving variable closures $[\tilde{y}; \tilde{x}.t|\vec{z}]$ and evaluated closures $[\tilde{y}; \tilde{x}.t|\vec{v}]$, which are both values. In a closure $[\tilde{y}; \tilde{x}.t|b]$, $\tilde{y}$ and $\tilde{x}$ verify $\tilde{y}^{\#\tilde{x}}$ (i.e. no elements in common), and scope over the body $t$ of the closure; $\tilde{y}$ and $\tilde{x}$ do not scope over $b$. The idea is that $fv(\lambda \tilde{x}.t) \subseteq \tilde{y}$, so that $\lambda \tilde{y}.\lambda \tilde{x}.t$ is closed. The elements of $b$ are meant to replace the variables $\tilde{y}$ in $t$.

The rationale behind $\lambda_{\text{int}}$ is understood by looking at the translation from $\lambda_{\text{sou}}$ to $\lambda_{\text{int}}$ in Fig. 5. Basically, every abstraction is closed and paired with the bag of its free variables. Evaluated closures $[\tilde{y}; \tilde{x}.t|\vec{v}]$ are not in the image of the translation, unless

<footnote>$^1$The right-to-left order (adopted also in [24, 26]) induces a more natural presentation of the machines, but all our results could be restated using the left-to-right order.</footnote>

<footnote>$^2$We do not define projections as tuple-unpacking abstractions because it would turn $\pi$-steps into $\beta$-steps and so blur the cost analysis (that counts $\beta$ but not $\pi$-steps).</footnote>
<figure><img src="image_7.png" /><figcaption>**Figure 5: The translations** : $\lambda_{\text{int}} \to \lambda_{\text{sou}}$ (wrapping) and $[\cdot] : \lambda_{\text{int}} \to \lambda_{\text{sou}}$ (unwrapping).</figcaption></figure>

$f v(\lambda \tilde{x}. t) = \emptyset$, which gives the closure $[; \tilde{x}. t | \emptyset]$ that is both a variable and an evaluated closure. Evaluated closures are generated by the reduction rules, discussed after defining well-formedness.

**Definition 4.1.** A closure $[[\tilde{y}; \tilde{x}. t | b]]$ is well-formed if $f v(t) \subseteq \tilde{y}^* \tilde{x}$, $\|b\| = \|\tilde{y}\|$ and if $b$ is a variable bag then $b = (\tilde{y})$. Terms $t \in \lambda_{\text{int}}$ and evaluation contexts $C \in \lambda_{\text{int}}$ are well-formed if all their closures are well-formed, and *prime* if moreover they are variable closures.

**Operational Semantics.** The intermediate variant $\to_i \beta_v$ of the $\beta_v$-rule involves a well-formed evaluated closure $[[\tilde{y}; \tilde{x}. t | \tilde{v}_1]]$ and an argument $\tilde{v}_2$ of the same length as $\tilde{x}$, and amounts to substitute the bag $\tilde{v}_1$ on $\tilde{y}$ and the argument $\tilde{v}_2$ on $\tilde{x}$. Substitution $t\{\tilde{y}; \tilde{x} \to \tilde{v}_1; \tilde{v}_2\}$ is defined as expected (see [5, Appendix B]) by performing $\{\tilde{y} \to \tilde{v}_1\}$ and $\{\tilde{x} \to \tilde{v}_2\}$ simultaneously and requires that $f v(t) \subseteq \tilde{y}^* \tilde{x}$. Well-formed terms are stable by substitution, when defined, and the reduct of $\to_i \beta_v$ is a (well-formed) term of $\lambda_{\text{int}}$ because (by well-formedness) closures close their bodies, so the closing substitution generated by the step turns variable bags into value bags. Tuple projection is as in $\lambda_{\text{sou}}$. Note that evaluation contexts do not enter closures. See [5, Appendix B] for the definition of clash(-freeness) for $\lambda_{\text{int}}$. A term $t \in \lambda_{\text{int}}$ is *good* if it is well-formed and clash-free.

The intermediate calculus $\lambda_{\text{int}}$ is deterministic (if $t \to_{\text{int}} u$ and $t \to_{\text{int}} s$ then $u = s$ and $t$ is not a value) and harmonic.

**LEMMA 4.2 (HARMONY OF $\lambda_{\text{int}}$).** Let $t \in \lambda_{\text{int}}$ be closed and good. Then either $t$ is a value or $t \to_{\text{int}} u$ for some closed good $u \in \lambda_{\text{int}}$.

**Translation From Source to Intermediate, or Wrapping.** The wrapping translation $\underline{\cdot}$ from $\lambda_{\text{sou}}$ to $\lambda_{\text{int}}$ takes a (possibly open) term $t \in \lambda_{\text{sou}}$ and returns a term $\underline{t} \in \lambda_{\text{int}}$, and it is defined in Fig. 5. As already mentioned, it turns abstractions into closures by closing them and pairing them with the bag of their free variables. It is extended to evaluation contexts $C$ as expected, setting $\langle \cdot \rangle := \langle \cdot \rangle$.

**LEMMA 4.3 (PROPERTIES OF THE TRANSLATION $\lambda_{\text{sou}} \to \lambda_{\text{int}}$).**

(1) Values: if $v \in \lambda_{\text{sou}}$ then $\underline{v}$ is a value of $\lambda_{\text{int}}$.

(2) Terms: if $t \in \lambda_{\text{sou}}$ then $\underline{t} \in \lambda_{\text{int}}$ is well-formed and prime.

(3) Contexts: if $C \in \lambda_{\text{sou}}$ then $\underline{C}$ is an evaluation context of $\lambda_{\text{int}}$.

**Problem: Wrapping and Substitution Do not Commute.** As source values and contexts are translated to their intermediate analogous, one may think that the translation preserves reduction steps: if $t \to_{\text{sou}} u$ then $\underline{t} \to_{\text{int}} u$. But this is false, because the translation does not commute with substitution, as also discussed in [18, 38]. Indeed, in general $\underline{t}\{x \to \underline{v}\} \neq \underline{t}\{x \to \underline{v}\}$: take $t := \lambda y.yx$ and a closed value $v$, we get the terms below, where $[[x; y.yx | \underline{\{v\}}]] \neq [[; y.yv | \underline{\{v\}}]]$.

$$ \begin{aligned} \underline{t}\{x \to \underline{v}\} &= [[x; y.yx | \underline{\{x\}}]]\{x \to \underline{v}\} = [[x; y.yx | \underline{\{v\}}]] \\ \underline{t}\{x \to \underline{v}\} &= \lambda y.yv = [[; y.yv | \underline{\{v\}}]] \end{aligned} $$

The point being that $t\{x \to \underline{v}\}$ is closed and so its wrapping is different from first wrapping $t$, which is instead *open*, and then closing the wrapped term $t$ using $\{x \to \underline{v}\}$. Not only $t\{x \to \underline{v}\} \neq t\{x \to \underline{v}\}$, they are not even related by $\to_{\text{int}}$, or by the *equational theory* generated by $\to_{\text{int}}$ (but they can be shown to be contextually equivalent).

The issue is that the translation targets prime terms (Lemma 4.3.2) but $\to_{\text{int}}$ creates evaluated closures (which are not in the image of translation), i.e., the *reduct of a prime term* (of $\lambda_{\text{int}}$) may not be prime. Take $t := \lambda y.yx$ again: $(\lambda x.t)(\underline{\{v\}}) \to_{\text{sou}} t\{x \to \underline{v}\} = \lambda y.yv$ and $(\lambda x.t)(\underline{\{v\}}) = [[; x, [[x; y.yx | \underline{\{x\}}]]\{\underline{\{v\}}\}]]$ is prime, but $(\lambda x.t)(\underline{\{v\}}) \to_{\text{int}}$ reduces to the non-prime $[[x; y.yx | \underline{\{v\}}]] = \underline{t}\{x \to \underline{v}\} \neq \underline{t}\{x \to \underline{v}\}$.

**Reverse Translation.** The literature usually overcomes this problem by switching to a different approach, adopting a big-step semantics and a logical relation proof technique. One of our contributions is to show a direct solution, as done also by Bowman and Ahmed [18], but in a different way. The idea comes from the correctness of abstract machines, which is proved by projecting the machine on the calculus, rather than the calculus on the machine. Therefore, we define a reverse *unwrapping* translation from $\lambda_{\text{int}}$ to $\lambda_{\text{sou}}$ and show that it smoothly preserves reduction steps.

The *unwrapping translation* $\underline{[t]}$ of a well formed term $t \in \lambda_{\text{int}}$ to $\lambda_{\text{sou}}$ is defined in Fig. 5. It amounts to substitute the bag $b$ for the sequence $\tilde{y}$ of variables of a closure $[[\tilde{y}; \tilde{x}. t | b]]$. In contrast with wrapping, now unwrapping and substitution commute.

**PROPOSITION 4.4 (COMMUTATION OF SUBSTITUTION AND THE REVERSE TRANSLATION).** If $t, \tilde{v}_1, \tilde{v}_2 \in \lambda_{\text{int}}$ and $f v(t) \subseteq \tilde{x}^* \tilde{y}$, then $\underline{[t\{\tilde{x}; \tilde{y} \to \tilde{v}_1; \tilde{v}_2\}]} = \underline{[t\{\tilde{x} \to \underline{\tilde{v}_1}\}]}\{\underline{\{\tilde{y} \to \underline{\tilde{v}_2}\}}\}$.

**Strong Bisimulation.** From the commutation property (Prop. 4.4), it easily follows that the reverse translation projects and reflects rewrite steps and—if terms are closed—also normal forms. As a consequence, it is a termination-preserving strong bisimulation, possibly the strongest form of *correctness* for a program transformation.

**THEOREM 4.5 (SOURCE-INTERMEDIATE TERMINATION-PRESERVING STRONG BISIMULATION).** Let $t \in \lambda_{\text{int}}$ be closed and well-formed.

(1) Projection: for $a \in \{\beta_v, \pi\}$, if $t \to_{ia} u$ then $\underline{[t]} \to_a \underline{[u]}$.

(2) Halt: $t$ is $\to_{\text{int}}$ normal if and only if $\underline{[t]}$ is $\to_{\text{sou}}$ normal.

(3) Reflection: for $a \in \{\beta_v, \pi\}$, if $\underline{[t]} \to_a u$ then there exists $s \in \lambda_{\text{int}}$ such that $t \to_{ia} s$ and $\underline{[s]} = u$.

(4) Inverse: if $u$ is a *source term* then $\underline{[u]} = u$.

Projection can be extended to sequences of steps. The reflection and inverse properties ensure that reflections of consecutive steps from the source can be composed, bypassing the problem with the wrapping translation, see the corollary below. Its proof only depends on the abstract properties of our notion of bisimulation, thus similar corollaries hold for all bisimulations in this paper.

**COROLLARY 4.6 (PRESERVATION OF REDUCTION STEPS).** If $t \to_{\text{sou}}^k u$ then there exists $s \in \lambda_{\text{int}}$ such that $\underline{t} \to_{\text{int}}^k s$ and $\underline{[s]} = u$.

**PROOF.** By induction on $k$. If $k = 0$ then $t = u$; taking $s := \underline{t}$, the inverse property gives $\underline{[s]} = \underline{[\underline{t}]} = t = u$. For $k > 0$, one has
<figure><img src="image_8.png" /><figcaption>Figure 6: The target calculus $\lambda_{\text{tar}}$, and the translations $\lambda_{\text{int}} \to \lambda_{\text{tar}}$ (name elimination) and $\lambda_{\text{tar}} \to \lambda_{\text{int}}$ (naming).</figcaption></figure>

$t \to_{\text{sou}}^{k-1} u' \to_{\text{sou}} u$. By $i.h., \underline{t} \to_{\text{int}}^{k-1} s'$ with $[s'] = u'$, so $[s'] \to_{\text{sou}} u$; by reflection $s' \to_{\text{int}} s$ for some $s$ such that $[s] = u$. $\square$

About the proof of the various points of Theorem 4.5, the closed hypothesis is used for the left-to-right direction of the halt property, which in turn is used to prove the reflection property. Projection is used instead in the right-to-left direction of the halt property. The inverse property is straightforward.

# 5 Part 1: Outline of the Target Calculus $\lambda_{\text{tar}}$ and of Name Elimination

In this section, we quickly outline the target calculus $\lambda_{\text{tar}}$ and the translation from $\lambda_{\text{int}}$ to $\lambda_{\text{tar}}$, dubbed name elimination, which, when composed with the wrapping translation of Section 4, provides the closure conversion transformation. The unsurprising details (definitions, statements, and proofs) are given in [5, Appendix C]. The ideas behind $\lambda_{\text{tar}}$ and name elimination, defined in Fig. 6, are:

*   **Variable binders:** replacing the sequences $\tilde{y}$ and $\tilde{x}$ of abstracted variables in closures $[[\tilde{y}; \tilde{x}.t|b]]$ with the special variables w and s (short for wrapped and source), standing for the tuples $\vec{v}_1$ and $\vec{v}_2$ meant to be substituted on $\tilde{y}$ and $\tilde{x}$;

*   **Variable occurrences:** replacing every occurrence of a variable $y_i$ or $x_j$ in $t$ with the projected variables $\pi_i w$ or $\pi_j s$, which are two special compound terms as w and s cannot appear without being paired with a projection.

We use $p$ (for projected variable) to refer to either $\pi_i w$ or $\pi_j s$. The transformation is similar to switching to de Brujin indices, except that—because of the already wrapped setting—the index simply refers to the composite binder of the closure, rather than to the nested binders above the variable occurrence. It also slightly differs from standard closure conversion: the latter would eliminate the $\tilde{y}$ names but usually not the $\tilde{x}$ ones. We eliminate both, as the total elimination of names shall induce a logarithmic speed-up for the abstract machine associated with $\lambda_{\text{tar}}$, see Sect. 12.

The terminology name elimination refers to the fact that, after this transformation, a term uses only two variables, w and s. As all

closures would then have shape $[[w; s.t|b]]$, we simplify the notation and just write $[[t|b]]$, with the implicit assumption that every closure now binds w and s in $t$. To define a reverse translation from $\lambda_{\text{tar}}$ to $\lambda_{\text{int}}$ dubbed naming in Fig. 6, closures $[[t|b]]_{n,m}$ are annotated with two natural numbers $n, m \in \mathbb{N}$, which record the length of the replaced sequences of variables $\tilde{y}$ and $\tilde{x}$. To simplify the notation, however, we shall omit these annotations when not relevant. The body of a closure $[[t|b]]$ is $t$, and—as in $\lambda_{\text{int}}$—closures are either variable closures, if $b = \tilde{p}$, or evaluated closures, if $b = \vec{v}$. A term $t \in \lambda_{\text{tar}}$ is closed if $\pi_i w$ and $\pi_i s$ do not occur out of closure bodies.

Name elimination is parametric in two lists $\tilde{y}$ and $\tilde{x}$ of abstracted variables, which intuitively are those of the closest enclosing closure being translated. In particular the two parametric lists change when the translation crosses the boundary of a closure in the $[[\tilde{z}; \tilde{w}.t|b]]^{\tilde{y}, \tilde{x}}$ clause in Fig. 6. On closed terms, the translation is meant to be applied with empty parameter lists (as $t^{\epsilon, \epsilon}$).

Reduction $\to_{\text{tar}} := \to_{t\beta_v} \cup \to_{t\pi}$ is defined in [5, Appendix C].

**Results.** We prove that name elimination, its reverse naming translation (from $\lambda_{\text{tar}}$ to $\lambda_{\text{int}}$), and the composed naming-unwrapping reverse translation (from $\lambda_{\text{tar}}$ to $\lambda_{\text{sou}}$) are termination-preserving strong bisimulations as in Theorem 4.5. The technical development is rather smooth and follows the structure of Section 4 without the subtleties related to the commutation with substitution.

More precisely, in [5, Appendix C], we show that the name elimination translation is a termination-preserving strong bisimulation between $\lambda_{\text{int}}$ and $\lambda_{\text{tar}}$. The two obtained strong bisimulation theorems—namely Theorem 4.5 and the latter concerning name elimination—do not compose, because the first one uses the reverse translation from $\lambda_{\text{int}}$ to $\lambda_{\text{sou}}$, while the second one uses the direct translation from $\lambda_{\text{int}}$ to $\lambda_{\text{tar}}$. To solve the issue, we use the reverse translation from $\lambda_{\text{tar}}$ to $\lambda_{\text{int}}$ dubbed naming in Fig. 6.

Unsurprisingly, naming is a termination-preserved strong bisimulation from the target calculus $\lambda_{\text{tar}}$ to the intermediate one $\lambda_{\text{int}}$.

**THEOREM 5.1 (TARGET-INTERMEDIATE TERMINATION-PRESERVING STRONG BISIMULATION).** Let $t \in \lambda_{\text{tar}}$ be closed.

(1) Projection: $\text{for } a \in \{\beta_v, \pi\}, \text{ if } t \to_{ta} u \text{ then } t^{\epsilon, \epsilon} \to_{ia} u^{\epsilon, \epsilon}$.

(2) Halt: $t$ is $\to_{\text{tar}}$ normal (resp. a value, resp. a clash) if and only if $t^{\epsilon, \epsilon}$ is $\to_{\text{tar}}$ normal (resp. a value, resp. a clash).

(3) Reflection: $\text{for } a \in \{\beta_v, \pi\}, \text{ if } t^{\epsilon, \epsilon} \to_{ia} u \text{ then there exists } s \in \lambda_{\text{tar}} \text{ such that } t \to_{ta} s \text{ and } s^{\epsilon, \epsilon} = u$.

(4) Inverse: $\text{let } u \in \lambda_{\text{int}}, \text{ if } \text{fv}(u) \subseteq \tilde{y}^{\#\tilde{x}} \text{ then } u^{\tilde{y}, \tilde{x}} \text{ is } \alpha$.

The following theorem states that the reverse transformation $[t^{\epsilon, \epsilon}]$ of closure conversion (obtained by composing naming and unwrapping) is a termination-preserving strong bisimulation. It is our final correctness result for closure conversion. The proof is obtained by simply composing the two bisimulations results for unwrapping (Theorem 4.5) and naming (Theorem 5.1).

**THEOREM 5.2 (TARGET-SOURCE TERMINATION-PRESERVING STRONG BISIMULATION).** Let $t \in \lambda_{\text{tar}}$ be closed.

(1) Projection: $\text{for } a \in \{\beta_v, \pi\}, \text{ if } t \to_{ta} u \text{ then } t^{\epsilon, \epsilon} \to_{ia} u^{\epsilon, \epsilon}$.

(2) Halt: $t$ is $\to_{\text{tar}}$ normal if and only if $[t^{\epsilon, \epsilon}]$ is $\to_{\text{sou}}$ normal.
(3) Reflection: for $a \in \{\beta_v, \pi\}$, if $[t_{\epsilon, \epsilon}] \to_a u$ then there exists $s \in \lambda_{\text{tar}}$ such that $t \to_{\text{ta}} s$ and $[s_{\epsilon, \epsilon}] = u$.

(4) Inverse: if $u \in \lambda_{\text{sou}}$ then $[\underline{u}_{\epsilon, \epsilon}] = u$.

# 6 Part 2 Preliminaries: Abstract Machines

This section starts the second part of the paper. Here, we introduce the terminology and the form of implementation theorem that we adopt for our abstract machines, along the lines of Accattoli and co-authors [2, 6, 13], here adapted to handle clashes.

**Abstract Machines Glossary.** An abstract machine for a strategy (i.e. a deterministic reduction) $\to_{\text{str}}$ of a calculus $\lambda_{\text{cal}}$ is a quadruple $M = (\text{States}, \sim, \cdot, \circ)$ where $(\text{States}, \sim)$ is a deterministic labeled transition system with transitions $\sim$ partitioned into principal transitions $\sim_{\text{pr}}$, corresponding to the steps of the strategy and labeled with the labels of the rewrite rules in $\lambda_{\text{cal}}$ (here variants of $\beta_v$ and $\pi$ steps), and overhead transitions $\sim_{\text{oh}}$, that take care of the various tasks of the machine (searching, substituting, and $\alpha$-renaming), together with two functions:

* Initialization $^{\circ}: \lambda_{\text{cal}} \to \text{States}$ turns $\lambda_{\text{cal}}$-terms into states;

* Read-back $^{\circ}: \text{States} \to \lambda_{\text{cal}}$ turns states into $\lambda_{\text{cal}}$-terms and satisfies the constraint $t^{\circ} = t$ for every $\lambda_{\text{cal}}$-term $t$.

A state $q \in \text{States}$ is composed by the active term $t$, and some data structures. A state $q$ is initial for $t$ if $t^{\circ} = q$. A state is final if no transitions apply; final states are partitioned into successful and clash states. A run $r$ is a possibly empty sequence of transitions. For runs, we use notations such as $|r|$ as for evaluation sequences (Sect. 2). An initial run (from $t$) is a run from an initial state $t^{\circ}$. A state $q$ is reachable if it is the target state of an initial run.

Abstract machines manipulate pre-terms, that is, terms without implicit $\alpha$-renaming, even if for simplicity we keep calling them terms. In that setting, we write $t^{\alpha}$ in a state $q$ for a fresh renaming of $t$, i.e. $t^{\alpha}$ is $\alpha$-equivalent to $t$ but all of its bound variables are fresh (with respect to those in $t$ and in the other components of $q$).

**Implementation Theorem, Abstractly.** We now define when a machine implements the strategy $\to_{\text{str}}$ of a calculus $\lambda_{\text{cal}}$, abstracting and generalizing the setting of the previous sections.

**Definition 6.1 (Machine implementation).** A machine $M = (\text{States}, \sim, \cdot, \circ)$ implements the strategy $\to_{\text{str}}$ of a calculus $\lambda_{\text{cal}}$ when given a $t \in \lambda_{\text{cal}}$ the following holds:

(1) *Runs to evaluations:* for any M-run $r : t^{\circ} \to^* q$ there exists a $\to_{\text{str}}$-evaluation $e : t \to^*_{\text{str}} q$. Additionally, if $q$ is a successful state then $q$ is a clash-free $\to_{\text{str}}$-normal form.

(2) *Evaluations to runs:* for every $\to_{\text{str}}$-evaluation $e : t \to^*_{\text{str}} u$ there exists a M-run $r : t^{\circ} \to^* q$ such that $q = u$. Additionally, if $u$ is a clash-free $\to_{\text{str}}$-normal form then there exists a successful state $q'$ such that $q \sim^*_{\text{oh}} q'$.

(3) *Principal matching:* in both previous points the number $|e|_l$ of steps with label $l$ in the evaluation $e$ is exactly the number $|r|_l$ of principal $l$ transitions in $r$, i.e. $|e|_l = |r|_l$.

Next, we give sufficient conditions that a machine and a (deterministic) strategy have to satisfy in order for the former to implement the latter, what we call an implementation system.

<table><caption>**Figure 7: The local abstract machine (LAM) for $\lambda_{\text{cbv}}$**.</caption><thead><tr><th colspan="2">M-CLOSURES</th><th colspan="2">LOCAL ENVVS</th><th colspan="2">STACKS</th></tr><tr><th colspan="2">c ::= (t, E)</th><th colspan="2">E ::= ε | [x&larr;c] : E'</th><th colspan="2">S ::= ε | ●c : S | ◦c : S</th></tr><tr><th>M-CLOS.</th><th>STACK</th><th>TRANS.</th><th>M-CLOS.</th><th>STACK</th><th></th></tr></thead><tbody><tr><td>t u</td><td>E</td><td>S</td><td>~<sub>sea<sub>1</sub></sub></td><td>u</td><td>E</td></tr><tr><td>λx.t</td><td>E</td><td>○c : S</td><td>~<sub>sea<sub>2</sub></sub></td><td>c</td><td>○(t, E) : S</td></tr><tr><td>λx.t</td><td>E</td><td>●c : S</td><td>~<sub>β<sub>v</sub></sub></td><td>t | [x&larr;c] : E</td><td>●(λx.t, E) : S</td></tr><tr><td>x</td><td>E</td><td>S</td><td>~<sub>sub</sub></td><td>E(x)</td><td>S</td></tr></tbody></table>

**Definition 6.2 (Implementation system).** A machine $M = (\text{States}, \sim, \cdot, \circ)$ and a strategy $\to_{\text{str}}$ form an implementation system if:

(1) *Overhead transparency:* $q \sim_{oh} q'$ implies $q = q'$;

(2) *Principal projection:* $q \sim_{pr} q'$ implies $q \to_{\text{str}} q'$ and the two have the same label;

(3) *Overhead termination:* $\sim_{oh}$ terminates;

(4) *Halt:* $M$ successful states read back to clash-free $\to_{\text{str}}$-normal forms, and clash states to clashes of $\lambda_{\text{cal}}$.

Via a simple lemma for the evaluation to runs part (in [5, Appendix D]), we obtain the following abstract implementation theorem.

**THEOREM 6.3 (SUFFICIENT CONDITION FOR IMPLEMENTATIONS).** Let $M$ be a machine and $\to_{\text{str}}$ be a strategy forming an implementation system. Then, $M$ implements $\to_{\text{str}}$ (in the sense of Definition 6.1).

**Local Environments.** We overview one the two main forms of environments for abstract machines, the local one (as opposed to global), for the archetypal call-by-value calculus $\lambda_{\text{cbv}}$ of Sect. 2, to compare it later with the Source TAM for $\lambda_{\text{sou}}$. The terminology local/global is due to [23], and the two techniques are analyzed e.g. (for call-by-name and call-by-need) in [4] but they are folklore.

The local abstract machine (LAM), a machine with local environments for $\lambda_{\text{cbv}}$, is defined in Fig. 7. It is a right-to-left variant of the CEK machine [22]. It uses a stack to search for $\beta_v$-redexes, filling it with entries that encode an evaluation context of $\lambda_{\text{cbv}}$. The substitutions triggered by the encountered $\beta_v$-redexes are delayed and stored in environments. There is one principal transition $\sim_{\beta_v}$, of label $\beta_v$, and three overhead transitions $\sim_{sea_1}$, $\sim_{sea_2}$, and $\sim_{sub}$ realizing the search for $\beta_v$-redexes and substitution. Contrary to the global approach, the LAM has many environments $E$, paired with terms so as to form m-closures $c$. In fact, a local environment $E$ is itself a list of pairs of variables and m-closures: m-closures and environments are defined by mutual induction. A state is a triple $(t, E, S)$ where $(t, E)$ is the m-closure of an active term $t$ and a local environment $E$, and $S$ is a stack. Initial states have shape $(t, \epsilon, \epsilon)$.

M-Closures are called in this way because when evaluating a closed term an invariant ensures that $fv(t) \subseteq \text{dom}(E)$ for any m-closure $(t, E)$ in a reachable state (including the active one), where the domain $\text{dom}(E)$ of an environment $E$ is the set of variables on which it has a substitution. The use of m-closures allows one to avoid $\alpha$-renaming (and copying code) in transition $\sim_{sub}$, at the price of using many environments, thus using space anyway. The duplication of $E$ in transition $\sim_{sea_1}$ is where different implementation approaches (shared vs flat) play a main role. With shared environments (whose simplest implementation is as linked lists), the duplication only duplicates the pointer to the environment, not the whole environment. With flat environments (whose simplest
implementation is as arrays), duplication is an actual duplication of the array; we shall further discuss the duplication of flat environments when discussing the complexity of abstract machines.

# 7 Part 2: the Source TAM for $\lambda_{\text{sou}}$

Here we present a machine with local environments, the *source tupled abstract machine* (Source TAM) for the source calculus $\lambda_{\text{sou}}$. We adopt local rather than global environments to have m-closures, to then show that wrapping removes their need, in the next section.

The Source TAM is defined in Fig. 8. M-Closures carry a flag $\bullet \in \{\circ, \bullet\}$, where $\circ$ stands for non-(completely)-evaluated and $\bullet$ for evaluated. In $\lambda_{\text{sou}}$, values have a tree structure, the leaves of which are abstractions. The evaluated m-closures $\bullet c$ of the Source TAM have a similar tree structure, plus local environments. A state is a couple $(\bullet c | S)$, where $\bullet c$ is a m-closure and $S$ is a stack. The active m-closure is also flagged, naturally inducing a partition of transitions in two blocks. Stack entries are flagged m-closures, $\pi_i$ and partially evaluated tuples $((\vec{t}, \downarrow, \vec{\bullet c})|E)$ ($\vec{t}$ are non-evaluated terms).

The initialization of $t$ is the initial state $t^0 := (\circ(t, \epsilon) | \epsilon)$. Successful states are $(\bullet c | \epsilon)$, i.e., an evaluated m-closure and an empty stack. Clash and clash-free states are defined in [5, Appendix E].

*Transitions.* The union of all the transitions of the Source TAM is noted $\sim^{\text{STAM}}$. The principal transitions are $\sim^{\bullet\beta_v}$ and $\sim^{\bullet\pi}$, of label $\beta_v$ and $\pi$, all the other transitions are overhead ones. If $\vec{x} = x_1, \dots, x_n$ and $\vec{\bullet c} = (\bullet c_1, \dots, \bullet c_n)$, we set $[\vec{x} \leftarrow \vec{\bullet c}] := [x_1 \leftarrow \bullet c_1] \dots [x_n \leftarrow \bullet c_n]$; this notation is used in transition $\sim^{\bullet\beta_v}$. In presence of tuples, there are additional overhead transitions. If the active m-closure is:

* $\circ(\pi_i t, E)$ then $\sim^{\circ\text{sea}_2}$ triggers the evaluation of $t$ and the projection $\pi_i$ goes on the stack (to trigger transition $\sim^{\circ\bullet\pi}$);

* $\circ(\lambda\vec{x}.t, E)$ then $\sim^{\circ\text{sea}_5}$ flips the flag to $\bullet$ (weak evaluation);

* $\circ(\emptyset, E)$ then $\sim^{\circ\text{sea}_4}$ changes the flag to $\bullet$, discarding $E$;

* $\circ(\langle\cdot, t_n\rangle, E)$ then $\sim^{\circ\text{sea}_3}$ evaluates its elements right-to-left, adding a partially evaluated tuple to the stack $((\downarrow, \cdot, \downarrow)|E)$.

* $\bullet c$ then the behavior depends on the first element of the stack. If it is a partially evaluated tuple $((\downarrow, \cdot, t, \downarrow, \cdot, \downarrow)|E)$ then $\sim^{\bullet\text{sea}_6}$ swaps $\bullet c$ and the next element $t$ in the tuple (duplicating $E$), similarly to $\sim^{\bullet\text{sea}_1}$. If the tuple on the stack is $((\downarrow, \cdot, \downarrow)|E)$ then $\sim^{\bullet\text{sea}_3}$ plugs $\bullet c$ on $\downarrow$ forming a new evaluated m-closure.

The name of transitions $\sim^{\bullet\text{sea}_1}$ and $\sim^{\bullet\text{sea}_3}$ stresses that they do the dual job of $\sim^{\circ\text{sea}_1}$ and $\sim^{\circ\text{sea}_3}$—such a duality shall be exploited in the complexity analysis of Sect. 11. Transition $\sim^{\circ\text{sea}_6}$ has no dual (it is not named $\sim^{\circ\bullet\text{sea}_2}$ because it is not the dual of $\sim^{\circ\text{sea}_2}$).

*Invariant and Read Back.* Here is an invariant of the Source TAM.

**LEMMA 7.1 (M-CLOSURE INVARIANT).** Let $q$ be a Source TAM reachable state and $\bullet c = \bullet(\cdot, t, E)$ be a m-closure or $((\cdot, \cdot, t, \cdot, \cdot, \downarrow, \vec{\bullet c})|E)$ be a stack entry in $q$. Then $fv(t) \subseteq \text{dom}(E)$.

The read-back of the Source TAM to $\lambda_{\text{sou}}$ is defined in Fig. 8. M-Closures and states read back to terms, stacks read back to evaluation contexts. In the read back of partially evaluated m-closures $((\vec{t}, \downarrow, \vec{\bullet c})|E)$ on the stack, $E$ spreads on the non-evaluated terms $\vec{t}$ (the m-closures in $\vec{\bullet c}$ have their own environments on their leaves).

**LEMMA 7.2 (READ-BACK PROPERTIES).**

(1) $\bullet c$ is a value of $\lambda_{\text{sou}}$ for every $\bullet c$ of the Source TAM.

(2) $\underline{S}$ is an evaluation context of $\lambda_{\text{sou}}$ for any Source TAM stack $S$.

*Implementation Theorem.* According to the recipe in Sect. 6, we now prove the properties inducing the implementation theorem. The read-back to evaluation contexts (Lemma 7.2) is used for principal projection. The m-closure invariant (Lemma 7.1) is used in the proof of the halt property, to prove that the machine is never stuck on the left-hand side of a $\sim^{\circ\text{sub}}$ transition (see [5, Appendix E]). Overhead termination is proved via a measure, developed in Sect. 11, which gives a bound on the number of overhead transitions.

**THEOREM 7.3.** *The Source TAM and $\lambda_{\text{sou}}$ form an implementation system (as in Def. 6.2), hence the Source TAM implements $\rightarrow_{\text{sou}}$.*

# 8 Part 2: the Int TAM for $\lambda_{\text{int}}$

Here we present the *intermediate tupled abstract machine* (Int TAM) for the intermediate calculus $\lambda_{\text{int}}$. Its feature is a new way of handling environments, resting on the strong properties of $\lambda_{\text{int}}$.

The Int TAM is defined in Fig. 9. The flags will be explained after an overview of the new aspects of the machine. Mostly, the Int TAM behaves as the Source TAM by just having removed the structure of m-closures. The principal transitions are $\sim^{\circ\bullet\beta_v}$ and $\sim^{\circ\bullet\pi}$, of label $\beta_v$ and $\pi$, all the other transitions are overhead. There are two new aspects: transition $\sim^{\circ\text{subc}}$ that evaluates variable bags and the use of *stackable environments* rather than *local* environments and m-closures. The machine is akin to those with global environments, except that no $\alpha$-renaming is needed, as in the local approach.

*Evaluating Bags.* In the Int TAM, abstractions $\lambda\vec{x}.t$ are replaced by non-evaluated prime closures $\circ[\vec{y}; \vec{x}.t|\langle\vec{y}\rangle]$. The new transition $\sim^{\circ\text{subc}}$ (replacing $\sim^{\circ\text{sea}_5}$) substitutes on all variables in $\vec{y}$ in one shot, producing the evaluated closure $\circ[\langle\vec{y}; \vec{x}.t|E(\vec{y})\rangle]$ where $E(\vec{y}) = (E(y_1), \dots, E(y_n))$ if $\vec{y} = y_1, \dots, y_n$, and $E$ is the (global) environment.

*Stackable Environments.* Transitions $\sim^{\circ\bullet\beta_v}$ and the new $\sim^{\circ\bullet\text{sea}_7}$ encapsulate a second new aspect, *stackable environments*. Indeed:

* **Closure bodies and environments:** when the machine encounters the analogous of a $\rightarrow_i \beta_v$-redex $[\vec{y}; \vec{x}.t|\vec{v}_1] \vec{v}_2$, the new entries $[\vec{y} \leftarrow \vec{v}_1]$ $[\vec{x} \leftarrow \vec{v}_2]$ of the environment created by transition $\sim^{\circ\bullet\beta_v}$ in the machine are all that is needed to evaluate $t$, because the free variables of $t$ are all among $\vec{y}$ and $\vec{x}$. Thus, the environment $E$ that is active before firing the redex is useless to evaluate $t$, and can be removed after transition $\sim^{\circ\bullet\beta_v}$.

* **Stackability:** $E$ is not garbage collected but pushed on the new activation stack, along with the ordinary stack $S$ (now called *constructor stack*) which holds non-evaluated terms with variables in $\text{dom}(E)$. This is still done by transition $\sim^{\circ\bullet\beta_v}$.

* **Popping:** when the body $t$ of the closure has been evaluated, the focus is on a value $\bullet v$ and the constructor stack is empty. The activation stack has the pair $(S, E)$ that was active before firing the $\beta_v$-redex. The machine throws away the current environment $E' := [\vec{y} \leftarrow \vec{v}_1][\vec{x} \leftarrow \vec{v}_2]$, since $\vec{y}$ and $\vec{x}$ have no occurrences out of $t$, and reactivates the pair $(S, E)$, to keep evaluating terms in $S$. This is done by the new transition $\sim^{\circ\bullet\text{sea}_7}$.

*Flags.* The Int TAM evaluates (well-formed) terms of $\lambda_{\text{int}}$ decorated (only on top) with a flag $\bullet \in \{\circ, \bullet\}: ot$ denotes that $t$ has not been evaluated yet, while $\bullet t$ denotes that $t$ has been evaluated. The results of evaluation are values, thus the $\bullet$ flag shall be associated to
<figure><img src="image_9.png" /><figcaption>Figure 8: The source tupled abstract machine (Source TAM).</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>Figure 9: The intermediate tupled abstract machine (Int TAM).</figcaption></figure>

values only, and an invariant shall ensure that every evaluated value
●v in a reachable state is closed. In ○t, t has no flags, and non-flagged
sub-terms are implicitly considered as flagged with ◦. Every evalu-
ated value carries a ● flag, so in ●v there are in general other ● flags
(when it is a tuple or the bag of the closure). Moreover, evaluated clo-
sures shall have shape ●[**(y; x̃.o†t|●v**]**, that is, they have an additional
(redundant) ◦ flag on their body (it shall be used in section Sect. 12
for the complexity analysis). The machine is started on *prime* terms
of λ<sub>int</sub> (because wrapped terms of λ<sub>sou</sub> are prime, Lemma 4.3), thus
all closures in an initial state have shape [**(y; x̃.t|**(y)**]. In fact, all
non-evaluated closures ◦[**(y; x̃.t|b**] in reachable states shall always
be prime (that is, such that b = *(y*))): we prove this invariant and
we avoid assuming the general shape of non-evaluated closures,
which would require additional and never used transitions.

The initialization $t^\circ$ of $t \in \lambda_{\text{int}}$ is given by the initial state $(ot | \epsilon | \epsilon | \epsilon)$ where $t$ is closed and prime. Successful states have shape $(\bullet v | \epsilon | E | \epsilon)$. Clash states are defined in [5, Appendix F].

Invariants and Read Back. Here are the invariants of the Int TAM.

LEMMA 8.1 (INVARIANTS). Let $q = (\bullet t | S | E | A)$ be a Int TAM reachable state.

(1) Well-formedness: all closures in $q$ are well-formed.

(2) Closed values: every value ●v in q is closed.

(3) Closure: $fv(t) \cup fv(S) \subseteq \text{dom}(E)$ and $fv(S') \subseteq \text{dom}(E')$ for every entry $(S', E')$ of the activation stack A.

The read back _ is defined in Fig. 9. Flagged terms ⚫t and states
q read back to terms of λ<sub>int</sub>, the constructor and activation stacks
S and A read back to evaluation contexts of λ<sub>int</sub>. The read back
of A and q is based on a notion of meta-level environment-induced
(simultaneous) substitution σ<sub>E</sub>, defined in Fig. 9 and applied to terms
(as read back of flagged terms) and evaluation contexts (as read
back of stacks); meta-level substitutions are extended to evaluation
contexts as expected, the definition is in [5, Appendix F].

The implementation theorem is proved following the schema
used for the Source TAM, see [5, Appendix F]. Overhead trans-
parency for the additional transition ↠●sea₇ relies on the closed
values invariant (Lemma 8.1).
<figure><img src="image_11.png" /></figure>

<figure><img src="image_12.png" /><figcaption>**Figure 10: The target tupled abstract machine (Target TAM):** changes with respect to the Int TAM.</figcaption></figure>

**LEMMA 8.2 (READ BACK PROPERTIES).**

(1) Values: $\bullet v$ is a value of $\lambda_{int}$ for every $\bullet v$ of the Int TAM.

(2) Evaluation contexts: $S$ and $A$ are evaluation contexts of $\lambda_{int}$ for every Int TAM constructor and activation stacks $S$ and $A$.

**THEOREM 8.3.** *The Int TAM and $\lambda_{int}$ form an implementation system on prime terms (as in Def. 6.2), thus the Int TAM implements $\rightarrow_{int}$ on prime terms.*

## 9 Part 2: the Target TAM for $\lambda_{tar}$

Here we present the target *tupled abstract machine* (Target TAM) for the target calculus $\lambda_{int}$, a minor variant of the Int TAM. Beyond the elimination of variable names, its key feature is the use of *tupled environment*, that is, a pair of tuples as data structures for environments, instead of a list of explicit substitution entries $[x \leftarrow v]$.

The Target TAM is defined in Fig. 10, by giving the only ingredients of the Int TAM that are redefined for the Target TAM, leaving everything else unchanged but for the fact that, when considering the omitted transitions of the Int TAM as transitions of the Target TAM, the symbol $E$ for environment refers to the new notion of environment adopted here (the omitted transitions do not touch the environment). Here the closures $[[t|b]]_{n,m}$ of $\lambda_{tar}$ are written $[[t|b]]$ (and are then decorated with flags as for the Int TAM) because $n$ and $m$ play a role only for the reverse translation from $\lambda_{tar}$ to $\lambda_{int}$ studied in [5, Appendix C], while here they are irrelevant.

The elimination of names enables the use of a *tupled (stackable environment)*: the environment is now a pair of tuples $\overrightarrow{\bullet v_w}, \bullet v_s$, where $\overrightarrow{\bullet v_w}$ provides values for the wrapped projected variables $\pi_i w$, and $\bullet v_s$ for the source ones $\pi_i s$, with no need to associate the values of these tuples to variable names via entries of the form $[x \leftarrow v]$ (as it was the case for the Int TAM). The change is relevant, as the data structure for environments changes from a *map* to a *tuple*, removing the need (and the cost) of creating a *map* in transition $\rightsquigarrow \bullet \beta_v$ and inducing a logarithmic speed-up, as we shall see.

The look up into tupled environments is defined in Fig. 10 and is the only new notion needed in the new transitions. The implementation theorem is proved following the same schema used for the Source TAM and the Int TAM, the details are in [5, Appendix G].

**THEOREM 9.1.** *The Target TAM and $\lambda_{tar}$ form an implementation system on prime terms (as in Def. 6.2), thus the Target TAM implements $\rightarrow_{tar}$ on prime terms.*

*Actual Implementation of the Target TAM.* We provide an OCaml implementation of the Target TAM on GitHub [33], described in

[5, Appendix K]. The textual interface asks for a term of the source calculus $\lambda_{sou}$, which is translated to the target calculus $\lambda_{tar}$ by applying first wrapping and then name elimination, thus passing through the intermediate calculus $\lambda_{int}$, as described above. The obtained $\lambda_{tar}$-term is then reduced by the Target TAM until a normal form is reached, if any, and the final $\lambda_{tar}$-term is extracted. The machine state is printed after every step, in ASCII art.

The implementation is not particularly optimized and it does not have a graphical user interface. It is designed to stay as close as possible to the definitions given in the paper, and to provide evidence supporting the assumptions of the cost analysis of Sect. 12. In particular, we use OCaml arrays for tuples, variables in abstractions, and bags in closures, for achieving $O(1)$ access times.

## 10 Part 3 Preliminaries: Sharing, Size Explosion, and the Complexity of Abstract Machines

This section starts the third part of the paper, about the time complexity analysis of abstract machines. Here, we quickly overview the size explosion problem of the $\lambda$-calculus as the theoretical motivation for the use of sharing in implementations, as well as the structure of the study of the overhead of abstract machines.

*Size Explosion.* A well-known issue of the $\lambda$-calculus is the existence of families of terms whose size grows exponentially with the number of $\beta$-steps. They are usually built exploiting some variant of the duplicator $\delta := \lambda x.xx$. We give an example in $\lambda_{cbv}$. Define:

$$ \begin{array}{c} \text{VARIANT OF } \delta \\ \pi := \lambda x.\lambda y.\overline{xyx} \end{array} \quad \begin{array}{c} \text{SIZE EXPLOD. FAMILY} \\ t_0 := I \quad t_{n+1} := \pi t_n \end{array} \quad \begin{array}{c} \text{EXPLODED RESULTS} \\ u_0 := I \quad u_{n+1} := \lambda y.yu_n u_n \end{array} $$

**PROPOSITION 10.1 (SIZE EXPLOSION IN $\lambda_{cbv}$).** Let $n \in \mathbb{N}$. Then $t_n \rightarrow^{n} \beta_v u_n$, moreover $|t_n| = O(n)$, $|u_n| = \Omega(2^n)$, and $u_n$ is a value.

The proof is in [5, Appendix H]. Size explosion has been extensively analyzed in the study of reasonable cost models—see [1] for an introduction—because it suggests that the number $n$ of $\rightarrow \beta_v$ steps is not a reasonable time measure for the execution of $\lambda$-terms: for size exploding families, indeed, it does not even account for the time to write down the normal form, which is of size $\Omega(2^n)$.

It is tempting to circumvent the problem by tweaking the calculus, with types, by changing the evaluation strategy, using CPS, and so on. None of these tweaks works, size explosion can always be adapted: it is an inherent feature of higher-order computations [1].

*Sharing for Functions.* A solution nonetheless exists: it amounts to share sub-terms to avoid their blind duplication during evaluation. For size explosion in $\lambda_{cbv}$, it is enough to add a simple form of *sub-term sharing* by delaying meta-level substitution and avoiding substituting under abstractions. For instance, evaluating the size exploding term $t_n$ above in a variant of $\lambda_{cbv}$ where sub-term sharing is implemented via explicit substitutions, gives the following normal form, of size *linear* (rather than exponential) in $n$:

$$ \lambda y_1.y_1 x_1 x_1 [x_1 \leftarrow \lambda y_2.y_2 x_2 x_2] \dots [x_{n-1} \leftarrow \lambda y_n.y_n x_n x_n] [x_n \leftarrow I]. $$

The explosion re-appears if one unfolds that normal form to an ordinary $\lambda$-term, but it is now encapsulated in the unfolding.

Abstract machines of the previous sections have environments to implement sub-term sharing and avoid the size explosion due to $\beta_v$, giving hope for a time complexity lower than exponential.
*Parameters for the Time Complexity Analysis of Abstract Machines.* Given a strategy $\rightarrow_{str}$ of a calculus $\lambda_{cal}$ and an abstract machine M implementing $\rightarrow_{str}$ (see Definition 6.1), the time complexity of M is obtained by estimating the cost—when concretely implemented on random access machines (RAMs)—of a run $r_e : t_0^o \sim^{*} q$ implementing an arbitrary evaluation sequence $e : t_0 \rightarrow_{str} t_n$ (thus having $q = t_n$) as a function of two parameters:

(1) *Code size:* the size $|t_0|$ of the initial term $t_0$;

(2) *Number of $\rightarrow_{str}$-steps/$\beta$-steps:* the number $n$ of $\rightarrow_{str}$-steps in $e$. If $\lambda_{cal}$ has other rules other than $\beta/\beta_v$, the parameter is often just the number of $\beta/\beta_v$ steps, which is usually considered the relevant time cost model.

*Recipe for Time Complexity.* The way the time complexity of an abstract machine is established tends to follow the same schema:

(1) *Number of overhead transitions:* bounding the number of overhead transitions as a function of $|t_0|$ and $n$ (which by the principal matching property of implementations—see Definition 6.1—is enough to bound the length of $r_e$);

(2) *Cost of single transitions:* bounding the cost of single transitions, which is typically constant or depends only on $|t_0|$;

(3) *Total cost:* inferring the total cost of a run $r$ by multiplying the number of steps of each kind of transition for their cost, and summing all the obtained costs.

The key tool for such an analysis is the *sub-term property*, an *invariant* of abstract machines stating that some of the terms in a reachable state are sub-terms of the initial term. This allows one to develop bounds with respect to the size $|t_0|$ of the initial term $t_0$.

*Time Complexity of the LAM.* The LAM verifies a sub-term invariant, and its time complexity follows a well-known schema in the literature, closely inspected by Accattoli and Barras [4] for call-by-name and call-by-need, and that smoothly adapts to CbV. Consider an evaluation $e: t_0 \rightarrow_{\beta_v}^n t_n$ in $\lambda_{cbv}$. About the first point of the recipe, the bound on overhead transitions is $O((n+1) \cdot |t_0|)$, that is, bilinear. Additionally, if one takes *complete* evaluations, that is, for which $t_n = v$ is a value, then the bound lowers to $O(n)$. Such an independence from the initial term is due to the fact that whether a term is a value can be checked in $O(1)$ in $\lambda_{cbv}$, by simply checking whether the top-most constructor is an abstraction.

For the second point of the recipe, the cost of single transitions of the LAM depends on the data structures used for local environments, as discussed by Accattoli and Barras [4]. With flat environments, the cost of manipulating them is $O(|t_0|)$ (because of the duplication of $E$ in $\sim_{sea_1}$), giving a total cost of $O(n \cdot |t_0|)$ for complete runs. With shared environments, the best structures manipulate them in $O(\log |t_0|)$, giving a total cost of $O(n \cdot \log |t_0|)$ for complete runs. Thus, shared local environments are faster, but they are optimized for time and inefficient with respect to space, as they prevent some garbage collection to take place. Here, we take as reference *flat* local environment, which induce the same overall $O(n \cdot |t_0|)$ overhead as global environments and enable a better management of space (not discussed here, see [10] instead).

*Notions of Flatness for Local Environment.* Let us be precise on a subtle point about local environments and their flatness. Local environments are defined by mutual recursion with m-closures,

and various notions of sharing and flatness are possible, as one can share environments, or m-closures, both, or none of them. Sharing both is essentially the same as sharing only environments.

Sharing m-closures rather than environments is what we above called *flat environments*. For instance, if $E = [x_1 \leftarrow \bullet c_1] : [x_2 \leftarrow \bullet c_2] : \epsilon$ then $\bullet c_1$ and $\bullet c_2$ are shared so that the concrete representation of $E$ is $E = [x_1 \leftarrow p_1] : [x_2 \leftarrow p_2] : \epsilon$ where $p_1$ and $p_2$ are pointers to $\bullet c_1$ and $\bullet c_2$. Copying $E$ then means copying $[x_1 \leftarrow p_1] : [x_2 \leftarrow p_2] : \epsilon$, without recursively copying the structure of $\bullet c_1$ and $\bullet c_2$.

The *super flat environments* obtained by removing sharing for both environments and m-closures are studied in [10], where it is shown that the overhead of abstract machines becomes *exponential*. This is the reason why we do not consider them here.

*No Sharing for Stackable Environments.* An interesting aspect of the new stackable environments is that they need no sharing. Indeed, the Int TAM and the Target TAM never duplicate their stackable environments. In particular, when they discard the current environment $E$ in transition $\sim^{\bullet sea_7}$, it can be collected.

*De Bruijn Indices Do Not Change the Overhead.* It is well-known that, representing flat environments as arrays and variables with de Bruijn indices, one can look-up environments in $O(1)$ rather than in $O(\log |t_0|)$, which is the best that one can do with (some ordered domain of) names. However, the $O(|t_0|)$ cost of copying flat environments in transition $\sim^{\bullet sea_1}$ dominates, so that turning to de Bruijn indices does not change the overall $O(n \cdot |t_0|)$ overhead.

*Size Exploding Tuples.* In $\lambda_{sou}$, there is a new form of size explosion, due to tuples, requiring another form of sharing. To our knowledge, the view provided here is novel. Set $I := \lambda z.z$ and:

$$ \begin{array}{c|c|c} \text{VARIANT OF } \delta & \text{SIZE EXPLOD. FAMILY} & \text{EXPLODED RESULTS} \\ \tau := \lambda x.(x, x) & s_0 := \text{I} & r_0 := \text{I} \\ & s_{n+1} := \tau(\lfloor s_n \rfloor) & r_{n+1} := \lfloor r_n, r_n \rfloor \end{array} $$

**PROPOSITION 10.2 (SIZE EXPLOSION OF TUPLES).** Let $n \in \mathbb{N}$. Then $s_n \rightarrow_{\beta_v}^n r_n$, moreover $|s_n| = O(n)$, $|r_n| = \Omega(2^n)$, and $r_n$ is a value.

*Sharing for Tuples.* To avoid the size explosion of tuples, another form of sharing is used. The idea is the same as for functions: forms of size explosion are circumvented by forms of sharing designed to limit the substitution process. The key point is that tuples should never be copied, only *pointers* to them should be copied, thus representing $r_n$ above using *linear* (rather than exponential) space in $n$, as follows (where the $p_i$ are *pointers* and $[p_i \leftarrow v]$ are *heap entries*):

$$ (\lfloor p_1, p_1 \rfloor)[p_1 \leftarrow (\lfloor p_2, p_2 \rfloor)] \dots [p_n \leftarrow (\lfloor p_n, p_n \rfloor)] [p_n \leftarrow \text{I}] $$

The abstract machines of the previous sections have environments for sub-term sharing (needed for $\beta_v$) but they do *not explicitly* handle tuple sharing. The reason is practical: explicitly handling tuple sharing would require a treatment of *pointers* and a *heap* (i.e., a further global environment) and more technicalities. Our machines, however, are meant to be concretely implemented with tuple sharing, as in our OCaml implementation of the Target TAM [33].

# 11 Part 3: Complexity of the Source TAM, or, Tuples Raise the Overhead

Here, we develop the time complexity analysis of the Source TAM, stressing the novelty of tuples (see [5, Appendix I] for proofs).

The Source TAM verifies the following *sub-term invariant*.
<figure><img src="image_13.png" /><figcaption>**Figure 11: Size** $|\cdot|$ of $\lambda_{\text{SOU}}$ terms and overhead measure $|\cdot|_{\text{oh}}$.</figcaption></figure>

**LEMMA 11.1 (SUB-TERM INVARIANT).** Let $q$ be a Source TAM reach-
able state from the initial state $t^o$.

(1) $u$ is a sub-term of $t$ for every m-closure of shape $\circ(u, E)$ or $((\cdot, u, \cdot, \downarrow, \vec{\circ c}), E)$ in $q$.

(2) $\lambda\bar{x}.u$ is a sub-term of $t$ for every m-closure $\bullet(\lambda\bar{x}.u, E)$ in $q$.

Tuples are Not Sub-Terms. Point 2 only concerns evaluated m-
closures containing abstractions, and not evaluated tuples. Consider
$t := (\lambda x.\lambda y.((x, y))((I)(\delta)) \to \beta_v) (\lambda y.((I, y))((\delta)) \to \beta_v) ((I, \delta))$ in $\lambda_{\text{SOU}}$
and note that $((I, \delta)$ is not a sub-term of $t$. The run of the Source
TAM on $t$ produces a m-closure $((\bullet I, \bullet \delta), E)$ for some $E$. The leaves
of the tree-structure of an evaluated tuple are abstractions (I and
$\delta$ in the example), which are initial sub-terms, but they might be
arranged in ways that were not present in the initial term.

A consequence of this fact is that when the Source TAM starts evaluating a non-empty tuple `((., t_n))` with transition $\sim^{\circ sea_3}$, by adding `((., l))` to the stack, it has to allocate a new tuple on the heap for `((., l))` (which has a cost, discussed below). This never happens in absence of tuples, that is, in the LAM of Fig. 7. More precisely, the LAM does not copy any code, but it has to allocate new pointers to local environments, when they are extended by $\sim \beta_v$.

Step 1 of the Recipe: Number of Transitions and Overhead Measure.
For establishing a bound on overhead transitions, we first factor
some of them ($\sim^{\circ sea_{1,3}}$) out by simply noticing that they are enabled
and thus bound by some others ($\sim^{\circ sea_{1,3}}$). Actually, the same is
true also for the principal transition $\sim^{\bullet \pi}$, bounded by $\sim^{\circ sea_2}$. We
set $\sim^{a,b} := \sim_a \cup \sim_b$ and $|r|_{a,b} := |r|_a + |r|_b$ for every run $r$.

LEMMA 11.2 (TRANSITION MATCH). Let $r$ be a Source TAM run.
Then $|r|_{\pi, \bullet sea_{1,3}} \le |r|_{\bullet sea_{1,2,3}}$.

For the other transitions, we use a measure $|\cdot|_{oh}$, defined in Fig. 11
together with the size $|t|$ of $\lambda_{\text{SOU}}$ terms, which we use to derive a
bilinear bound on overhead/projection transitions (Prop. 11.4).

LEMMA 11.3 (OVERHEAD MEASURE PROPERTIES). Let $t^o \stackrel{\sim}{\rightarrow}^{\star}_{\text{STAM}} q$ a Source TAM run and $q \stackrel{\sim}{\rightarrow}^{a} q'$.

(1) if $a = \bullet \beta_v$ then $|q'|_{oh} \le |q|_{oh} + |t|$;

(2) if $a \in \{\circ \text{sub}, \circ \text{sea}_{1-5}, \bullet \text{sea}_6\}$ then $|q'|_{oh} < |q|_{oh}$;

(3) if $a \in \{\bullet \text{sea}_{1,3}, \bullet \pi\}$ then $|q'|_{oh} = |q|_{oh}$.

PROPOSITION 11.4 (BILINEAR NUMBER OF TRANSITIONS). Let $t \in \lambda_{\text{SOU}}$ be closed. If $r: t^o \rightsquigarrow^*_{\text{STAM}} q$ then $|r| \in \mathcal{O}((|r|\beta_o+1) \cdot |t|)$.

Tuples Raise the Overhead. Prop. 11.4 shows that projection tran-
sitions are also bi-linear. In Section 10, we mentioned that, without
tuples, the bound improves to $O(|r|\beta_v)$ if one considers complete
runs (that is, runs ending on values). With tuples, there is no such
improvement. Indeed, even just checking that the initial term is ac-
tually a value $v$ takes time $O(|v|)$ with tuples: if $v$ is a tree of tuples,

the Source TAM has to visit the tree and check that all the leaves
are abstractions; in absence of tuples the check instead costs $O(1)$.

**Step 2 of the Recipe: Cost of Single Transitions.** To obtain fine bounds with respect to the initial term, we introduce the notions of width and height of a term $t$, both bounded by the size $|t|$ of $t$.

**Definition 11.5 (Width, height).** The width $wd(t) \in \mathbb{N}$ of $t \in \lambda_{\text{SOU}}$ is the maximum length of a tuple or of a sequence of variables in $t$. The height $hg(t) \in \mathbb{N}$ of $t \in \lambda_{\text{SOU}}$ is the maximum number of bound variables of $t$ in the scope of which a sub-term of $t$ is contained.

As discussed after Lemma 11.1, $\sim^{\circ sea_3}$ has to allocate a new
tuple, thus its cost seems to depend on $wd(t)$, and similarly for $\sim^{\bullet \beta_v}$.
However, the price related to tuples can be considered as absorbed
by the cost of search (by changing the multiplicative constant),
since the new tuple of $\sim^{\circ sea_3}$ is then traversed, if the run is long
enough, and the one of $\sim^{\bullet \beta_v}$ was traversed before the transition.
Therefore, if we consider complete runs (i.e. ending on final states),
$\sim^{\circ sea_3}$ and $\sim^{\bullet \beta_v}$ have amortized cost independent of $wd(t)$.

Transitions $\bullet sea_1, \bullet sea_3$, and $\bullet sea_6$ duplicate $E$, the length of which is bounded by $hg(t)$. With flat environments, this costs $O(hg(t))$. Transition $\sim^{\circ sub}$ has to look-up the environment, the cost of which is $O(hg(t))$. De Brujin indices or an ordered domain of names might improve the cost of look-up, but at no overall advantage, because of the dominating cost of duplicating environments for $\bullet sea_1, \bullet sea_3$, and $\bullet sea_6$. All other transitions have constant cost, assuming that accessing the $i$-th component of a tuple (needed for $\sim^{\bullet \pi}$) takes constant time. The next proposition sums it up.

PROPOSITION 11.6 (COST OF SINGLE TRANSITIONS). Let $r$: $t^o \stackrel{\sim}{\rightarrow}^{\star}_{\text{STAM}} q$ be a complete Source TAM run. A transition $\sim^a$ of $r$ costs $O(hg(t))$ if $a \in \{\bullet sea_1, \bullet sea_3, \bullet sea_6, \circ \text{sub}\}$, and $O(1)$ otherwise.

Step 3 of the Recipe: Total Complexity. By simply multiplying
the number of single transitions (Proposition 11.4) for their cost
(Proposition 11.6), we obtain the complexity of the Source TAM.

THEOREM 11.7. Let $t \in \lambda_{\text{SOU}}$ be closed and $r: t^o \rightsquigarrow^*_{\text{STAM}} q$ be a complete Source TAM run. Then, $r$ can be implemented on RAMs in time $O((|r|\beta_o + 1) \cdot |t| \cdot hg(t))$.

If one flattens $hg(t)$ as $|t|$, the complexity of the Source TAM is $O((|r|\beta_o + 1) \cdot |t|^2)$, that is, quadratic in $|t|$, while in absence of tuples—that is, for the LAM—it is linear in $|t|$.

12 Part 3: Complexity of the Target TAM, or,
Closure Conversion Preserves the Overhead

In this section, we adapt the time complexity analysis of the Source TAM to an analysis of the Target TAM (skipping the less efficient Int TAM), and then connect source and target by considering the impact of closure conversion on the given analysis.

The Target TAM has a sub-term invariant, expressed compactly
thanks to our flags. In particular the part about abstractions of
the sub-term invariant for the Source TAM (Lemma 11.1) is here
captured by having flagged the body of unevaluated closures with $\circ$.

LEMMA 12.1 (SUB-TERM INVARIANT). Let $q$ be a Target TAM reach-
able state from the initial state $t^o$. Then $u$ is a sub-term of $t$ for every
non-evaluated term $\circ u$ in $q$.
**Step 1: Number of (Overhead) Transitions.** The bound on the number of (overhead) transitions is obtained following the same reasoning used for the Source TAM. The new transition $\rightsquigarrow_{\bullet sea_7}$ is part of the transitions that are factored out, since each $\rightsquigarrow_{\bullet sea_7}$ transition is enabled by a $\rightsquigarrow_{\bullet \beta_v}$ transition, which adds an entry to the activation stack. We also use an overhead measure (in [5, Appendix J]) which is a direct adaptation to the Target TAM of the one given for the Source TAM. Note indeed that the measure ignores environments, which are the main difference between the two machines.

**PROPOSITION 12.2 (BILINEAR NUMBER OF TRANSITIONS).** Let $t \in \lambda_{\text{tar}}$ be closed. If $r: t^o \rightsquigarrow_{\text{TTAM}}^* q$ then $|r| \in O((|r|\beta_v + 1) \cdot |t|)$.

**Step 2: Cost of Single Transitions.** For all transitions of the Target TAM but $\rightsquigarrow_{osub_v}$, $\rightsquigarrow_{osub_c}$, and $\rightsquigarrow_{\bullet sea_7}$ the cost is the same. For $\rightsquigarrow_{osub_v}$, the cost is now $O(1)$ since tupled environments have $O(1)$ access time via indices (in the Int TAM its cost is instead $O(\text{hg}(t))$).

For the new transition $\rightsquigarrow_{osub_c}$, $O(\text{wd}(t))$ look-ups in the environment are needed. Because of tupled environments, each look-up costs $O(1)$. Thus, the cost seems to depend on $\text{wd}(t)$, but—reasoning as for $\rightsquigarrow_{\bullet \beta_v}$ and $\rightsquigarrow_{\bullet sea_3}$ in Section 11—one can amortize it with the cost of search in complete runs. That is, we shall consider $\rightsquigarrow_{osub_c}$ to have constant cost. The new transition $\rightsquigarrow_{\bullet sea_7}$ has constant cost as well. Summing up, we get one of the insights mentioned in the introduction: the amortized cost of all single transitions is $O(1)$.

**PROPOSITION 12.3 (COST OF SINGLE TRANSITIONS).** Let $r: t^o \rightsquigarrow_{\text{TTAM}}^* q$ be a complete Target TAM run. Every transition of $r$ costs $O(1)$.

**Step 3: Total Complexity.** Multiplying the number of single transitions (Prop. 12.2) for their cost (Prop. 12.3), we obtain the time complexity of the Target TAM, which seem better than for the Source TAM. After the theorem we discuss why it is not necessarily so.

**THEOREM 12.4.** Let $t \in \lambda_{\text{tar}}$ be closed and $r: t^o \rightsquigarrow_{\text{TTAM}}^* q$ be a complete Target TAM run. Then, $r$ can be implemented on RAMs in time $O((|r|\beta_v + 1) \cdot |t|)$.

**Factoring in the Size Growth of Wrapping.** To complete the analysis, consider that the term $t \in \lambda_{\text{tar}}$ on which the Target TAM is run is meant to be the closure conversion (that is, wrapping + name elimination) of a term $u \in \lambda_{\text{sou}}$. While name elimination does not affect the size of terms, wrapping does (proof in [5, Appendix J]).

**LEMMA 12.5 (WRAPPING SIZE GROWTH BOUND).**

(1) If $t \in \lambda_{\text{sou}}$ then $|t| \in O(\text{hg}(t) \cdot |t|)$.

(2) There are families of terms $\{t_n\}_{n \in \mathbb{N}}$ for which $\text{hg}(t_n) = \Theta(|t_n|)$, so that $|t_n| \in \Theta(|t_n|^2)$.

**PROOF.** Point 1: the size increment in $|t|$ is due to the bags introduced by wrapping abstractions, and it is proportional to the number of free variables in the body of the abstraction, bounded by $\text{hg}(t)$; so $|t| \in O(\text{hg}(t) \cdot |t|)$. Point 2: take $t_n := \lambda x_1.. \lambda x_n x_1 x_2... x_n \neq \lambda x_1,.., x_n x_1 x_2... x_n$ (note $n$ abstractions in $t_n$, not just 1). $\square$

We can now instantiate the bounds for running the Target TAM on the closure conversion of a $\lambda_{\text{sou}}$ term, obtained by substituting the bounds in Lemma 12.5.2 in Theorem 12.4. We end up obtaining the same complexity as for the Source TAM (Theorem 11.7), despite the bound here being the outcome of a different reasoning.

**THEOREM 12.6.** Let $t \in \lambda_{\text{sou}}$ be closed and $r: (\underline{t}^{\epsilon, \epsilon})^o \rightsquigarrow_{\text{TTAM}}^* q$ be a complete Target TAM run. Then, $r$ can be implemented on RAMs in time $O((|r|\beta_v + 1) \cdot |t| \cdot \text{hg}(t))$.

# 13 Related Work and Conclusions

*Related work.* The seminal work of Minamide et al. [28] uses existential types to type closure conversion, and other works study the effect of closure conversion on types, as well as conversion towards typed target languages [16, 18, 29]. This line of work explores the use of types in compilation which can span the entire compiler stack, from $\lambda$-calculus to (typed) assembly [30].

Appel and co-authors have studied closure conversion, its efficient variants, and its space safety [17, 31, 35, 36]. Unlike them, we address a direct style $\lambda$-calculus, without relying on a CPS. We are however inspired by [31] in studying flat environments, also known as *flat closures*. Optimizations of flat closures are studied in [25].

Closure conversion of only some abstractions, and of only some of their free variables is studied by Wand and Steckler [39]. Closure conversion has also been studied in relation to graphical languages [34], non-strict languages [37], formalizations [19, 40], extended to mutable state by Mates et al. [27] and to a type-preserving transformation for dependent types by Bowman and Ahmed [18].

Many of the cited works study various aspects of the efficiency of closure conversion. As said in the introduction, our concerns here are orthogonal, as we are rather interested in the asymptotic overhead of the machines with respect to flat closure conversion.

Sullivan et al. [38] study a call-by-push-value $\lambda$-calculus where converted and non-converted functions live together, considering also an abstract machine. They do not study the complexity of the machine, nor the new notions of environments studied here.

For abstract machines, we follow Accattoli and co-authors, see for instance [2, 6, 13]. Another framework is [21].

Work orthogonal to our concerns is the *derivation* of abstract machines using closure conversion as a step in the process, along with CPS transformation and defunctionalization [15].

**Conclusions.** We study the relationship between closure conversion and abstract machines in probably the simplest possible setting, an extension with tuples of Plotkin's untyped call-by-value $\lambda$-calculus, and with respect to the simple notion of flat environments. Our starting point is to decompose closure conversion in two sub-transformations, dubbed *wrapping* and *name elimination*, turning the source calculus into a target calculus, via an intermediate one.

Each calculus is then paired with a variant of the *tupled abstract machine* (TAM). The Source TAM has machine-closures and local environments, while the Int TAM and the Target TAM have forms of converted closures. Moreover, they exploit the invariants enforced by the transformations, adopting new, better behaved forms of environments, namely *stackable* and *tupled environments*.

We give proof of correctness—under the form of termination-preserving strong bisimulations—for wrapping and name elimination, as well as implementation theorems for every machine with respect to its associated calculus. In particular, the proof technique for the correctness of closure conversion is new and simple.

Lastly, we study the time complexity of the abstract machines, showing that flat closure conversion reshuffles the costs, lowering
the dependency on the initial term, while at the same time increas-
ing the size of the initial term, ending up with the same complexity.

Various directions for future work are possible, e.g. extending the
source calculus with recursive let and pattern matching; or refining
the abstract machines by making explicit the sharing for tuples.

References

[1] Beniamino Accattoli. 2019. A Fresh Look at the lambda-Calculus (Invited Talk). In *Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)*. 1:1-1:20. doi:10.4230/LIPIcs.FSCD.2019.1

[2] Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. 2014. Dis-
tilling abstract machines. In *Proceedings of the 19th ACM SIGPLAN interna-
tional conference on Functional programming, Gothenburg, Sweden, September
1-3, 2014*, Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 363-376.
doi:10.1145/2628136.2628154

[3] Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. 2015. A Strong Distillery. In *Programming Languages and Systems - 13th Asian Symposium, APLAS 2015*, Pohang, South Korea, November 30 - December 2, 2015, *Proceedings (Lecture Notes in Computer Science, Vol. 9458)*. Xinyu Feng and Sungwoo Park (Eds.). Springer, 231-250. doi:10.1007/978-3-319-26529-2_13

[4] Beniamino Accattoli and Bruno Barras. 2017. Environments and the complexity of abstract machines. In *Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming (PPDP 2017)*. 4-16. http://doi.acm.org/10.1145/3131851.3131855

[5] Beniamino Accattoli, Cláudio Belo Lourenço, Dan Ghica, Giulio Guerrieri, and Claudio Sacerdoti Coen. 2025. Closure Conversion, Flat Environments, and the Complexity of Abstract Machines (Long Version). arXiv:2507.15843 [cs.PL] https://arxiv.org/abs/2507.15843

[6] Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, and Claudio Sacerdoti Coen. 2019. Crumbling Abstract Machines. In *Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019*, Porto, Portugal, October 7-9, 2019, *Ekaterina Komendantskaya* (Ed.). ACM, 4:1-4:15. doi:10.1145/3354166.3354169

[7] Beniamino Accattoli, Andrea Condoluci, and Claudio Sacerdoti Coen. 2021. Strong Call-by-Value is Reasonable, Implosively. In *36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021*, Rome, Italy, June 29 - July 2, 2021. IEEE, 1-14. doi:10.1109/LICS52264.2021.9470630

[8] Beniamino Accattoli and Ugo Dal Lago. 2016. (Leftmost-Outermost) Beta-Reduction is Invariant. Indeed, Logical Methods in Computer Science 12, 1 (2016). doi:10.2168/LMCS-12(1:4)2016

[9] Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. 2021. The (In)Efficiency of Interaction. *Proc. ACM Program. Lang.* 5, POPL (2021), 1-33. doi:10.1145/3434332

[10] Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. 2022. Reasonable Space for the λ-Calculus, Logarithmically. In *LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022*, Christel Baier and Dana Fisman (Eds.). ACM, 47:1-47:13. doi:10.1145/3531130.3533362

[11] Beniamino Accattoli and Giulio Guerrieri. 2016. Open Call-by-Value. In *Programming Languages and Systems - 14th Asian Symposium, APLAS 2016*, Hanoi, Vietnam, November 21-23, 2016, *Proceedings (Lecture Notes in Computer Science, Vol. 10017)*, Atsushi Igarashi (Ed.). 206-226. doi:10.1007/978-3-319-47958-3_12

[12] Beniamino Accattoli and Giulio Guerrieri. 2017. Implementing Open Call-by-Value. In *Proceedings of the 7th IPM International Conference on Fundamentals of Software Engineering (FSEN 2017)*, Tehran, Iran, April 26-28, 2017, Revised Selected Papers. 1-19. doi:10.1007/978-3-319-68972-2_1

[13] Beniamino Accattoli and Giulio Guerrieri. 2019. Abstract machines for Open Call-by-Value. *Sci. Comput. Program.* 184 (2019). doi:10.1016/j.scico.2019.03.002

[14] Beniamino Accattoli and Claudio Sacerdoti Coen. 2017. On the value of variables. *Inf. Comput.* 255 (2017), 224-242. doi:10.1016/j.ic.2017.01.003

[15] Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. 2003. A functional correspondence between evaluators and abstract machines. In *Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 27-29 August 2003, Uppsala, Sweden*. ACM, 8-19. doi:10.1145/888251.888254

[16] Amal Ahmed and Matthias Blume. 2008. Typed closure conversion preserves observational equivalence. In *Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008*, Victoria, BC, Canada, September 20-28, 2008, James Hook and Peter Thiemann (Eds.). ACM, 157-168. doi:10.1145/1411204.1411227

[17] Andrew W. Appel and Trevor Jim. 1989. Continuation-Passing, Closure-Passing Style. In *Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989*. ACM Press, 293-302. doi:10.1145/75277.75303

[18] William J. Bowman and Amal Ahmed. 2018. Typed closure conversion for the calculus of constructions. In *Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018*, Philadelphia, PA, USA, June 18-22, 2018, Jeffrey S. Foster and Dan Grossman (Eds.). ACM, 797-811. doi:10.1145/3192366.3192372

[19] Adam Chlipalı. 2010. A verified compiler for an impure functional language. In *Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010*, Madrid, Spain, January 17-23, 2010, Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 93-106. doi:10.1145/1706299.1706312

[20] Andrea Condoluci, Beniamino Accattoli, and Claudio Sacerdoti Coen. 2019. Sharing Equality is Linear. In *Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019)*. 9:1-9:14. doi:10.1145/3354166.3354174

[21] Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. *Semantics Engineering with PLT Redex*. MIT Press. https://mitpress.mit.edu/9780260267256/semantics-engineering-with-plt-redex/

[22] Matthias Felleisen and Daniel P. Friedman. 1987. Control operators, the SECD-machine, and the λ-calculus. In *Formal Description of Programming Concepts - III: Proceedings of the IFIP TC 2/WG 2.2 Working Conference on Formal Description of Programming Concepts - III, Ebberup, Denmark, 25-28 August 1986*, Martin Wirsing (Ed.). North-Holland, 193-222.

[23] Maribel Fernández and Nikolaia Siafakas. 2008. New Developments in Environment Machines. In *Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming*, WRS@RTA 2008, Hagenberg, Austria, July 14, 2008 (Electronic Notes in Theoretical Computer Science, Vol. 237), Aart Middeldorp (Ed.). Elsevier, 57-73. doi:10.1016/J.ENTCS.2009.03.035

[24] Benjamin Grégoire and Xavier Leroy. 2002. A compiled implementation of strong reduction. In *Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02)*, Pittsburgh, Pennsylvania, USA, October 4-6, 2002, Mitchell Wand and Simon L. Peyton Jones (Eds.). ACM, 235-246. doi:10.1145/581478.581501

[25] Andrew W. Keep, Alex Hearn, and R. Kent Dybvig. 2012. Optimizing closures in O(0) time. In *Proceedings of the 2012 Annual Workshop on Scheme and Functional Programming, Scheme 2012*, Copenhagen, Denmark, September 9-15, 2012, Olivier Danvy (Ed.). ACM, 30-35. doi:10.1145/2661103.2661106

[26] Xavier Leroy. 1990. *The ZINC experiment: an economical implementation of the ML language*. Technical report 117. INRIA. http://gallium.inria.fr/~xleroy/publi/ZINC.pdf

[27] Phillip Mates, Jamie Perconti, and Amal Ahmed. 2019. Under Control: Computationally Correct Closure Conversion with Mutable State. In *Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019*, Porto, Portugal, October 7-9, 2019, *Ekaterina Komendantskaya* (Ed.). ACM, 16:1-16:15. doi:10.1145/3354166.3354181

[28] Yasuhiko Minamide, J. Gregory Morrisett, and Robert Harper. 1996. Typed Closure Conversion. In *Conference Record of POPL '96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996*, Hans-Juergen Boehm and Guy L. Steele Jr. (Eds.). ACM Press, 271-283. doi:10.1145/237721.237791

[29] J. Gregory Morrisett and Robert Harper. 1997. Typed Closure Conversion for Recursively-Defined Functions. In *Second Workshop on Higher-Order Operational Techniques in Semantics, HOOTS 1997*, Stanford, CA, USA, December 8-12, 1997 (Electronic Notes in Theoretical Computer Science, Vol. 10), Andrew D. Gordon, Andrew M. Pitts, and Carolyn L. Talcott (Eds.). Elsevier, 230-241. doi:10.1016/S1571-0661(05)80702-9

[30] J. Gregory Morrisett, David Walker, Karl Crary, and Neal Glew. 1999. From system F to typed assembly language. *ACM Trans. Program. Lang. Syst.* 21, 3 (1999), 527-568. doi:10.1145/319301.319345

[31] Zoe Paraskevopoulou and Andrew W. Appel. 2019. Closure conversion is safe for space. *Proc. ACM Program. Lang.* 3, ICFP (2019), 83:1-83:29. doi:10.1145/3341687

[32] Gordon D. Plotkin. 1975. Call-by-Name, Call-by-Value and the lambda-Calculus. *Theor. Comput. Sci.* 1, 2 (1975), 125-159. doi:10.1016/0304-3975(75)90017-1

[33] Claudio Sacerdoti Coen. 2025. Artifact for the Closure Conversion and Abstract Machines paper. https://github.com/sacerdot/closure-conversion-machine/releases/tag/PPDP25.

[34] Ralf Schweimeier and Alan Jeffrey. 1999. A Categorical and Graphical Treatment of Closure Conversion. In *Fifteenth Conference on Mathematical Foundations of Programming Semantics*, MFPS 1999, Tulane University, New Orleans, LA, USA, April 28 - May 1, 1999 (Electronic Notes in Theoretical Computer Science, Vol. 20), Stephen D. Brookes, Achim Jung, Michael W. Mislove, and Andre Scedrov (Eds.). Elsevier, 481-511. doi:10.1016/S1571-0661(04)80090-2

[35] Zhong Shao and Andrew W. Appel. 1994. Space-Efficient Closure Representations. In *Proceedings of the 1994 ACM Conference on LISP and Functional Programming*, Orlando, Florida, USA, 27-29 June 1994, Robert R. Kessler (Ed.). ACM, 150-161. doi:10.1145/182409.156783

[36] Zhong Shao and Andrew W. Appel. 2000. Efficient and safe-for-space closure conversion. *ACM Trans. Program. Lang. Syst.* 22, 1 (2000), 129-161. doi:10.1145/345099.345125
[37] Zachary J. Sullivan, Paul Downen, and Zena M. Ariola. 2021. Strictly capturing non-strict closures. In *Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation*, PEPM@POPL 2021, Virtual Event, Denmark, January 18-19, 2021, Sam Lindley and Torben Æ. Mogensen (Eds.). ACM, 74-89. doi:10.1145/3441296.3441398

[38] Zachary J. Sullivan, Paul Downen, and Zena M. Ariola. 2023. Closure Conversion in Little Pieces. In *International Symposium on Principles and Practice of Declarative Programming*, PPDP 2023, Lisboa, Portugal, October 22-23, 2023, Santiago Escobar and Vasco T. Vasconcelos (Eds.). ACM, 10:1-10:13. doi:10.1145/3610612.3610622

[39] Mitchell Wand and Paul Steckler. 1994. Selective and Lightweight Closure Conversion. In *Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, Portland, Oregon, USA, January 17-21,

1994, Hans-Juergen Boehm, Bernard Lang, and Daniel M. Yellin (Eds.). ACM Press, 435-445. doi:10.1145/174675.178044

[40] Yuting Wang and Gopalan Nadathur. 2016. A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs. In *Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (Lecture Notes in Computer Science, Vol. 9632)*, Peter Thiemann (Ed.). Springer, 752-779. doi:10.1007/978-3-662-49498-1_29

[41] Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. *Inf. Comput.* 115, 1 (1994), 38-94. doi:10.1006/INCO.1994.1093