A Case for First-Class Environments
JINHAO TAN, The University of Hong Kong, China
BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, China
Formalizations of programming languages typically adopt the substitution model from the lambda calculus.
However, substitution creates notorious complications for reasoning and implementation. Furthermore, it is
disconnected from practical implementations, which normally adopt environments and closures.
In this paper we advocate for formalizing programming languages using a novel style of small-step
environment-based semantics, which avoids substitution and is closer to implementations. We present acall-by-value statically typed calculus, called λE , using our small-step environment semantics. With our alternative environment semantics programming language constructs for first-class environments arise naturally,
without creating significant additional complexity. Therefore, λE also adopts first-class environments, adding
expressive power that is not available in conventional lambda calculi. λE is a conservative extension of thecall-by-value Simply Typed Lambda Calculus (STLC), and employs de Bruijn indices for its formalization,
which fit naturally with the environment-based semantics. Reasoning about λE is simple, and in many cases
simpler than reasoning about the traditional STLC. We show an abstract machine that implements the semantics of λE , and has an easy correctness proof. We also extend λE with references. We show that λE canmodel a simple form of first-class modules, and suggest using first-class environments as an alternative toobjects for modelling capabilities. All technical results are formalized in the Coq proof assistant. In summary,our work shows that the small-step environment semantics that we adopt has three main and orthogonal
benefits: 1) it simplifies the notorious binding problem in formalizations and proof assistants; 2) it is closer toimplementations; and 3) additional expressive power is obtained from first-class environments almost for free.
CCS Concepts: • Software and its engineering → Formal language definitions.
Additional Key Words and Phrases: First-class Environments, Semantics, Mechanical Formalization
ACM Reference Format:
Jinhao Tan and Bruno C. d. S. Oliveira. 2024. A Case for First-Class Environments. Proc. ACM Program. Lang.
8, OOPSLA2, Article 360 (October 2024), 30 pages. https://doi.org/10.1145/3689800

1Introduction

Formalizations of programming languages have historically been heavily influenced by the foundational concepts of the lambda calculus [Church 1941]. The substitution model, a key element of thelambda calculus, provides a powerful yet elegant mechanism for expressing computation throughthe process of replacing variables with their corresponding values. This model has been widelyadopted in the design and formalization of modern programming languages.
Despite its elegance and widespread adoption, the substitution model is not without drawbacks.
One of the most notable complications, arising from the use of substitution, is the challenge it poses
for reasoning and implementation. In particular, the process of substituting variables can lead toissues such as variable capture, where the meaning of a program may be inadvertently alteredduring substitution. The challenges posed by the substitution model often create complications
Authors’ Contact Information: Jinhao Tan, The University of Hong Kong, Hong Kong, China, jhtan@cs.hku.hk; Bruno C. d.
S. Oliveira, The University of Hong Kong, Hong Kong, China, bruno@cs.hku.hk.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2024 Copyright held by the owner/author(s).
ACM 2475-1421/2024/10-ART360
https://doi.org/10.1145/3689800

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:2Jinhao Tan and Bruno C. d. S. Oliveira

when attempting to reason about proofs. In particular, working with proof assistants can be notoriously difficult due to the intricacies associated with formalizing binding and substitution [Abelet al. 2019; Aydemir et al. 2005; Charguéraud 2012]. Additionally, the necessity of performing substitutions throughout the entire program can result in significant computational overhead, making
it less efficient for practical applications. Consequently, practical implementations of programming
languages often diverge from the pure substitution model by adopting techniques such as environments and closures. By employing these concepts, programming languages can be efficiently
implemented, and the execution model remains faithful to the conceptual underpinnings of thelambda calculus. However, this creates a gap between substitution-based formalizations and theirefficiently implementable execution models. This gap has been noted by several researchers [Abadiet al. 1991; Amin and Rompf 2017; Biernacka and Danvy 2007; Curien 1991; Curien et al. 1996],
who have argued for alternatives to the substitution model.
In this paper, we advocate for an alternative way in formalizing programming languages byutilizing a novel small-step environment-based semantics. This alternative semantics offers threesignificant advantages over the traditional substitution model: 1) it simplifies the notorious binding
problem in formalizations and proof assistants; 2) it is closer to implementations, by directly
adopting closures and environments; and 3) it enables a natural and simple extension with firstclass environments, adding significant additional expressive power, almost for free. We shouldnote that previous research, for instance on calculi with explicit substitutions [Abadi et al. 1991;
Curien et al. 1996], has already put a lot of emphasis on point (2) and on having calculi closer toimplementations. However explicit substitutions still have a complex metatheory, and they only
provide a form of second-class environments. Thus, they do not enable advantages (1) and (3). Our
work aims at having the three advantages together.
We present a call-by-value statically typed calculus, called λE , with our new environment
semantics. λE uses de Bruijn indices, which fit naturally with the environment-based semantics.
Due to the use of environments, substitution is not needed. In turn, this simplifies the use of deBruijn indices, and shifting/unshifting operations are not needed as well. Thus, we avoid wellknown complications arising from the use of those operations on de Bruijn indices. This simplified
formulation of de Bruijn indices is particularly beneficial when working with proof assistants, as itallows for a more efficient and manageable approach to formalizing programming languages.
We formalize a substantial number of results in the Coq proof assistant for λE . These results
include: syntactic type soundness; semantic type soundness and normalization; correspondence
between small and big-step semantics; simulation and conservativity results for the (traditional)
call-by-value Simply Typed Lambda Calculus (STLC); the design and correctness of an abstract
machine; and others. We also extend λE with references. In all of these results, we only had to reason
about substitutions when showing the conservativity to the STLC. This is, of course unavoidable,
since the standard formulation of the STLC involves substitution. Overall we never felt that issues
with binding were in our way in our Coq formalization. Throughout the paper we will document
places in our proofs, where we believe that the environment-based approach made a significant
difference to an approach based on substitution.
When using a small-step environment semantics to model a calculus with static (or lexical)
scoping, a mechanism for evaluating an expression under a given local environment (which may bedifferent from the global environment) is necessary. In λE , such a mechanism is realised by boxes:
e1 ▷ e2 . When e1 is a (value) environment, then boxes provide exactly a mechanism to evaluate e2
under a given local environment (e1 ). Boxes play a key role in beta reduction in λE . However, byallowing e1 to be an arbitrary expression that evaluates to an environment, and with some otherconstructs provided by λE , we enable programmer-controlled environments to be set up and used to
run some computations. The following program (with some syntactic sugar) is allowed in λE :Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

360:3

var x = 1; (?, {y = 2}) ▷ y + x

In this program, we have a variable x initialized with 1. Then we use a box to run a computation
under a local environment that contains the current (global) environment (with x = 1), and a local
binding y = 2. Thus we can run y + x to compute 3. In the expression above, in addition to boxes,
we use environment merging/concatenation (,) and a reification operator ?. The reification operator
simply returns the global environment. If we had written insteadvar x = 1; {y = 2} ▷ y + x

the program would not type-check, because the local environment in the box does not containa binding x. In other words, the expression to be evaluated in a box can only access the local
environment provided by the box, but not the global environment. Therefore, boxes provide aform of sandboxing where computations can be run in an isolated and controlled environment.
Sandboxing is not available in standard lambda calculi, which typically only allow constructs that
extend the global environment.
Programming language constructs for first-class environments arise naturally from boxes and theenvironment-based small-step semantics that we propose, without creating significant additional
complexity. Thus, in λE , environments are first-class citizens within the language. In other words,
environments can be passed as arguments, returned from functions, or assigned to variables, justas any other values. First-class environments and sandboxing in λE are achieved while retaining
the simplicity of reasoning and binding. This is in contrast with previous work on first-class environments [Nishizaki 1994; Sato et al. 2001, 2002], where issues with binding introduce significant
complexity. First-class environments are useful to enhance both the expressive power and practicality of the language, empowering developers to fully harness the potential of an environment-based
semantics in their programs. The increased expressive power can facilitate the development ofsophisticated and modular programs, as developers can now leverage environments to encapsulate
and manage variable bindings more effectively. To illustrate the expressive power of λE , we showthat λE can model a simple form of first-class modules, and suggest using first-class environments
as an alternative to objects for modelling capabilities [Miller 2006; Miller et al. 2000]. In essence,since we can use first-class environments to model a form of (sandboxed) modules, we can use
these modules as capabilities that can be passed to clients of the modules.
Overall, there is a synergy of factors that make calculi with a small-step environment-based
semantics and first-class environments appealing. Nevertheless we acknowledge that the study
in this paper is limited, and that with more advanced programming language features additional
complications may arise from binding. Section 6 discusses some expected challenges and limitations,as well as possible variants in the design. The contributions of this paper are:
• The λE calculus, which is a call-by-value statically typed calculus with first-class environments.
λE adopts an environment-based semantics and supports lookup by de Bruijn indices or labels.
We illustrate its applicability to encodings of first-class modules and capabilities.
• A small-step style of environment semantics with easy metatheory. The λE calculus isshown to have desirable properties including determinism, type soundness, and normalization.
The proofs in the metatheory are simple and do not involve reasoning about substitutions.
• Operational correspondence between the λE calculus and other models. The results include
equivalence between small-step and big-step semantics, completeness and conservativity withrespect to the lambda calculus, and correctness of compilation to an abstract machine.
• An extension of λE with references: We also investigate a type sound and deterministic
extension of the λE calculus with mutable references.
• Coq formalization: We have formalized all the calculi and proofs in this paper in the Coq
theorem prover and they are available in the companion artifact [Tan and Oliveira 2024].

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:42

Jinhao Tan and Bruno C. d. S. Oliveira

Overview

This section provides an overview of our work. We start with some relevant background, and thenpresent the key ideas in our work.
2.1

Background: Substitution-based Semantics

The lambda calculus [Church 1941] is an abstract mathematical model of computation, which can be
regarded as the theoretical foundation of functional programming. Beta reduction, which reduces
function applications, is the core rule that performs computation. In the typical presentation of theoperational semantics for the lambda calculus [Barendregt 1985], a substitution-based semantics is
usually employed. Function application reduces by substituting the right-hand component in the
body of the function definition, which is formally expressed as the following rule:Beta(λx. e1 ) e2 ,→ e1 [e2 /x]
While the substitution model is, by far, the most widely adopted model for formalizing lambda
calculi, it does have some important drawbacks, which we discuss next.
Reasoning about binding and substitutions is tricky. Defining a correct capture-avoiding substitution is quite tricky, as the representation of variable names, freshness, and α-conversion need to beconsidered carefully. The Barendregt convention is often adopted in pencil-and-paper proofs, where
all bound variables are assumed to be distinct and their names should be different from any freevariables. Nevertheless, nowadays proofs about programming languages tend to be mechanizedusing proof assistants to enhance the rigor of the work. Therefore, a rigorous representation of variables, such as de Bruijn indices [De Bruijn 1972] (or others, such as locally nameless [Charguéraud
2012]) should be applied in mechanized proofs.
Reasoning about substitutions with de Bruijn indices is, however, tedious. Several lemmas need
to be established to characterize the interaction between shifting and substitution [Aydemir et al.
2005]. The manipulation of terms becomes fragile and error-prone. For example, incrementing
the mismatched index can easily disrupt the binding connection and cause issues in the encoding.
Proving normalization with a logical relation for the substitution-based lambda calculus requires
even stronger reasoning about substitutions, since we need to define simultaneous substitutions
for dealing with open terms. As a consequence, the proof relies on many properties about context
extensions, renaming, and composition of single and simultaneous substitution [Abel et al. 2019].
For example, the proof of normalization using de Bruijn indices in Abel et al.’s formalization consistsof a large amount of lemmas stating properties about composition, decomposition, and associativityof substitutions, which requires development of a sophisticated theory of substitutions.
Gap to implementations. In most practical implementations of programming languages, beta
reduction is not implemented with substitution, since substitution is algorithmically inefficient.
The essential problem with substitutions is that it requires traversing terms to replace the variables
by their corresponding values or expressions. Since applications are pervasive, this means thatsome expressions need to be traversed multiple times to replace different variables, which is very
costly. Since implementations, such as abstract machines, avoid substitutions, this complicatesestablishing the connection between substitution-based calculi and those implementations.
2.2

Background: Environment-based Semantics

In practical implementations, an explicit representation of environments is used, to avoid traversing
or modifying expressions. The substitution for a variable is deferred in the sense that the associatedvalue is looked up only if a variable needs to be evaluated. As a result, many abstract machines,
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

360:5

such as Krivine’s machine [Crégut 1990], the CEK machine [Felleisen and Friedman 1987], and theSECD machine [Landin 1964], can be implemented efficiently with environments. In such a setting,de Bruijn indices can be adapted easily by abstract machines and work quite well.
While much less common in formalizations of lambda calculi, there are some alternative presentations of the lambda calculus that employ an environment-based semantics, instead of substitution.
Typically, the environment-based evaluation of lambda calculus is presented with a big-step semantics [Kahn 1987]. The evaluation judgment E ⊢ e ⇒ v means that, with the global environment E,
expression e evaluates to the value v. Function closures [Landin 1964] naturally appear as part of
the formalization in such a formulation. A function closure is basically a pair (λx. e)[E] containing
a function and an environment E associating values to the free variables of the function.
Curien [1991] went one step further to internalize environments and closures into a closure
calculus λρ using de Bruijn indices. The λρ calculus can be seen as a lightweight form of explicit
substitutions [Abadi et al. 1991], since reduction under lambdas is not allowed in closure calculi. A
follow-up untyped calculus λb
ρ extends λρ with one-step reductions [Biernacka and Danvy 2007]. In
this way, small-step semantics and weak reduction strategies can be expressed in λb
ρ. Closure calculi
do not employ a global environment as in the conventional representation of big-step semantics.
Instead, an environment is propagated to each component of an expression. Thus, in the λb
ρ calculus
with the call-by-value strategy, the application ((λ.e)[s]) v is beta-reduced to e[v · s], in whichv · s is the environment by appending s with v. In this way, a general notion of closures e[s] isintroduced to the syntax of closure calculi, where s denotes the environment for computing e.
Lambda calculi based on an environment semantics solve the problems in Section 2.1:
• Simplified binding. Calculi based on environments do not need substitution. Thus they can
avoid the issues related to substitution. In particular, with an environment-based semantics deBruijn indices work quite well. The cumbersome aspects of working with de Bruijn indices,which are related to substitutions, can be avoided.
• The gap to implementations is smaller. If a lambda calculus is based on an environment
semantics, then it has a smaller gap to implementations, such as abstract machines. Since implementations also use an environment-based approach, then reasoning about the relationshipbetween the lambda calculus and the abstract machine is simpler.
We should note that while simplified binding is indeed a benefit of an environment-based
semantics and closure calculi, previous work [Biernacka and Danvy 2007; Curien 1991] has focusedon the second point. As far as we know, the benefits of using closure calculi for mechanicalformalizations have not been discussed previously in the literature. Moreover, in general, thebenefits for simplifying reasoning about binding have received little attention. In our work we wish
to emphasize and highlight those benefits, while providing improvements with our novel form ofsmall-step semantics and the addition of first-class environments.
2.3 First-class Environments
We can generalize the notion of environments and closures from closure calculi, so that environments are first-class expressions. With first-class environments, we can treat an environment as
any other value. In other words, variables can be assigned to an environment, and we can pass anenvironment as an argument to a function and/or return it as a result. In closure calculi and explicit
substitutions, we have a notion of environments, but we cannot express the previous operations.
We can use environments in certain places in expressions (e.g., assigning an environment to an
expression, or creating a closure), but we cannot treat them as other first-class values. In contrast,
several entities (e.g., environments, closures, STLC expressions) fall on the same level in calculi
with first-class environments. Following this idea, several statically typed calculi with first-classenvironments have been proposed [Nishizaki 1994; Sato et al. 2001; Tan and Oliveira 2023].
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:6Jinhao Tan and Bruno C. d. S. Oliveira

Unlike closure calculi, where binding is simple, existing calculi with first-class environments
have to deal with problems that complicate the binding story again. For example, the λ→env calculus
proposed by Nishizaki and the λε calculus proposed by Sato et al. are both based on explicit
substitutions [Abadi et al. 1991]. Moreover, both of them use a named presentation for variables andemploy record-like environments {e1 /x1 , . . . , en /xn }, and they have an expression e1 Je2 K which
denotes the evaluation of an expression e2 in an environment e1 . As a result, (λx. e1 ) e2 is reducedto {e1 /x} Je2 K, where {e1 /x} is the environment for evaluating e2 . Consider the following example:(λz. ((λy. λx. y) z JxK 10)) {e1 /x1 , . . . , en /xn },→ {{e1 /x1 , . . . , en /xn }/z}J(λy. λx. y) z JxK 10K,→ {{e1 /x1 , . . . , en /xn }/z}J({z JxK/y} Jλx. yK) 10K

Since environments are first-class, they can be passed to a function. The initial expression above
is an application of a function with an environment. Inside the function body, there is anotherapplication, which is expected to return the first argument. Now we evaluate this expression. The
first step is performing beta reduction, so that variable z is associated with an environment. The
second step is a beta reduction inside the function body, which produces {z JxK/y} Jλx. yK. Now weneed to consider how to deal with the evaluation of λx. y in the environment {z JxK/y}. One way is
to push the environment into the lambda abstraction, which gives λx. ({z JxK/y} JyK). However, inorder to ensure α-equivalence, we need to make sure that x is not free in z JxK first. This introduces
the question: how can we determine the free variables of z JxK? We know that z is associated with
{e1 /x1 , . . . , en /xn }, but this information cannot be passed to the evaluation of {z JxK/y} Jλx. yK.
The λ→
env calculus forbids substitution under lambdas to avoid the issue above. In general, theproblem of defining free variables for an expression is not considered in the λ→env calculus. As a result,the issues caused by α-equivalence and variable renaming are not investigated. In such a setting,the property of conservativity over the lambda calculus is not satisfied in λ→env . In other words,
λ→env cannot encode all the behaviour of the lambda calculus. The λε calculus allows substitution
under lambdas but it requires significant machinery. We know from the example above that z does
not have enough information about free variables from its syntactic representation. To solve thisproblem, the definition of freeness in λε resorts to the information from types: x is free in e1 Je2 K if
x is free in both e1 and e2 , and x does not exist in the set of names collected from the type of e1 .
For example, if the type of z is an environment type {xA , yB }, then x is not free in z JxK, since x is“bound” by the type of z even though z is just a variable. On the other hand, x is free in z JxK if z
has type {uA , yB } which does not contain x.
In this setting, the definition of freeness is entwined with environment types in λε. The correctness of reduction rules requires carefully considering the interaction between variables, environments and types. Moreover, we need devices and constraints, such as positions and occurrences,that identify the scope of variables within the context of first-class environments. Consequently,
the reasoning involved about binding is complex, and it is not clear whether such a formulation
can be easily adapted to theorem provers. Although lambda abstractions allow local renaming oflambda-bound variables to fresh names, α-conversion is not permitted on variables bound by theenvironment as they resemble labels. Otherwise the freeness would be broken. For example, y isfree in {1/x} JxK, but it is not free in {1/y} JyK which is α-converted from {1/x} JxK.
The Ei calculus [Tan and Oliveira 2023] is another typed calculus with first-class environments.
In Ei , variables are encoded as label names. The name bound by the abstraction {e}• needs tomatch the label name from the argument. For example, {e}• : {x : Int} → Int only accepts anargument labelled with x such as {x = 1}. Thus, α-conversion is not allowed on variables bound by
an abstraction, since {e}• : {y : Int} → Int cannot accept {x = 1}. To model conventional lambda
abstractions, a special kind of abstractions {e}◦ : {x : A} → B is proposed where x is only used
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

360:7

internally in the function body. Thus, {e}◦ : {x : Int} → Int can accept 1 as an argument. However,the connection between such abstractions and standard lambda abstractions is not clearly defined.
Complications of first-class environments. In addition to the complications introduced by binding,none of the calculi with first-class environments comes with a corresponding abstract machine.
The complexities of binding may partly explain this, as the abstract machine needs to deal withsuch complexities itself. For closure calculi an environment-based semantics has very appealing
properties. However, these good properties seem to be lost in calculi with first-class environments.
This seems unfortunate, as first-class environments introduce useful expressive power, and theadded expressiveness, together with the other nicer attributes of closure calculi would make apowerful argument for the use of calculi with first-class environments.
2.4

Key Ideas

In this paper, we propose a typed, call-by-value calculus, called λE , with first-class environments.
λE recovers the simplicity of binding found in closure calculi. Moreover, we provide an abstract
machine that implements λE and is shown to correctly model the semantics of λE . We show that
λE has numerous desirable properties, such as being conservative over the call-by-value lambda
calculus, and being normalizing. Next we introduce the key ideas of λE .
Lookups by de Bruijn indices. As mentioned above, the named representation can be burdensome
and inefficient, especially in the context of first-class environments. To address this problem, like inclosure calculi, de Bruijn indices (denoted by n) are employed for variables in the λE calculus. Hence,α-equivalence coincides with syntactic equality. Thus, standard lambda abstractions are definablein λE . For example, the named lambda abstraction λf : Int → Int. λx : Int. f x is represented as
λInt → Int. λInt. 1 0Moreover, α-equivalence is also respected for those variables that are bound by the environment.
In the λE calculus, e1 ▷ e2 , where ▷ is called a box, denotes the evaluation of e2 in the environment
e1 . The variables in e2 can be a de Bruijn index bound by e1 . For example, in the expression(· · · # succ(1) # 42 # true) ▷ 1
the environment consists of some expressions composed by the merge operator (#), which serves
the purpose of environment concatenation here. In the environment, the rightmost expression
is indexed by 0, and the index increments from right to left. Thus, index 1 refers to 42 in theenvironment. Note that counting of indices in environments coincides with counting in typing
contexts. This is achieved by the unification of typing contexts and types. In contrast, α-equivalence
is not respected under an environment type in λε [Sato et al. 2001].
Lookups by labels. λE also provides label-based lookups. The addition of label-based lookup isimportant for fully enabling the expressive power of first-class environments, and some of theirapplications. Label-based lookups would not be needed if our goal would be merely to encode thelambda calculus or a closure calculus (see also Section 6.2). A label, unlike a name or a de Bruijn
index, does not admit α-conversion. Labels fetch values from records. For example,
λ{l : Int → Int}. λInt. l 0
is a well-typed abstraction, where type Int → Int is looked up by l. This is also true for looking up
a value in an environment, such as (· · · # succ(1) # {l = 42} # true) ▷ l. In λE , ambiguous lookups bylabels are forbidden: ambiguous lookups are type errors. For example,(· · · # succ(1) # {l = 42} # {l = true}) ▷ l
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:8Jinhao Tan and Bruno C. d. S. Oliveira

is not allowed since the lookup would result in either 42 or true. However, the environment itself iswell-typed even though l appears twice. This treatment of environments is similar to how Haskell,and other languages, deal with ambiguous occurrences of names imported from multiple modules.
Moreover, in λE we have a query construct ? to reify the environment, and e.n and e.l forindex-based and label-based lookups for an expression respectively. In this way, a de Bruijn index
n is desugared as ?.n, and a label l is desugared as ?.l.
In our design, we desire both de Bruijn indices and labels at the same time. This is because they
have different roles in calculi. De Bruijn indices are important since they enable α-equivalence
easily by syntactic equality. This is especially true in the context of first-class environments, sinceprevious calculi with first-class environments employ only a named representation for variables,
resulting that binding and α-equivalence are difficult to deal with. However, we also want labels
for practical modelling of declarations and modules. Take the following as an example:
module A
var x = 1
var y = x + x
open A in y

Such a definition of module is common in programming languages. Note that for the variables indeclarations inside a module, the names matter (i.e., we cannot simply rename variables and retain
the meaning of the modules). For instance, renaming y to z can break the code, because clientsof the module assume that a field has a certain name. In other words, the names of variables arevisible outside the scope where they are being defined.
This is unlike variables in lambda abstractions where λx. x is the same as λy. y, as names
in declarations do not admit α-conversion. For this reason, most previous work on first-classenvironments needs to have quite a complicated story for binding, because in some cases/uses (e.g.,creating a calculus that is conservative w.r.t. lambda calculus) we want α-equivalence, but in someothers (e.g., modelling environments or modules) we do not. Keeping both de Bruijn indices andlabels leads to a clear formalization without losing expressiveness in λE .
A small-step style for environment-based semantics. λE employs a call-by-value style of environment semantics. In the lexical environment for a function closure, each expression is a value. The
reduction relation v ⊢ e1 ,→ e2 is read as: with the global environment v, expression e1 reduces to
e2 in one step. An expression e1 ▷ e2 with the box construct is evaluated using the call-by-value
strategy. The environment e1 , which possibly contains open expressions, evaluates to a value
environment v1 within the global environment first, and then e2 evaluates under v1 . For example,{l1 = 42} ⊢ {l2 = l1 } ▷ l2 ,→∗ {l2 = 42} ▷ l2 ,→∗ 42
This setting gives rise to simple reasoning about the evaluation of boxes, especially in the case ofnested evaluations. Every e1 ▷e2 needs to evaluate to a value, simplifying evaluation, and eliminating
the need for determining free variables. For example, suppose that the initial environment is empty(ε), and v is {l1 = 3} # {l2 = 4} that has type {l1 : Int} & {l2 : Int}, i.e., an intersection type of two
single-field record types. We have the following evaluation:ε ⊢ (λ{l1 : Int} & {l2 : Int}. ((λInt. λInt. 1) (0 ▷ l1 ) 10)) v,→∗ (ε # v) ▷ (λInt. λInt. 1) (0 ▷ l1 ) 10,→∗ (ε # v) ▷ ⟨ε # v, λInt. λInt. 1⟩ (0 ▷ l1 ) 10,→∗ (ε # v) ▷ ⟨ε # v, λInt. λInt. 1⟩ 3 10,→∗ (ε # v) ▷ (ε # v # 3 # 10 ▷ 1),→∗ 3

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

360:9This is similar to the problematic example shown in Section 2.3. In the example above, a function
is applied with environment v, and 0 ▷ l1 in the function body expects to fetch the value of l1
from v. First, the argument v is added into the initial environment, and the function body is goingto evaluate in the updated environment. Next, λInt. λInt. 1 evaluates to a function closure withenvironment ε # v. Then 0 ▷ l1 evaluates directly to 3 in environment ε # v without entering thefunction closure. As a result, the unevaluated 0 ▷ l1 is never added into the lexical environment of
the function closure.
Easy proofs of metatheory and operational correspondence. In previous calculi with first-classenvironments, the absence of a global environment, together with the named representation, makes
the evaluation of e1 Je2 K (similar to e1 ▷ e2 in our setting) rather complex and error-prone. On thecontrary, we have a simple design for bindings and evaluation of boxes, which results in simple
proofs of type safety and termination for λE . In particular, the proof of termination is easier than→in λ→
env and λε. We do not need to translate the calculus to another calculus (like in λenv ), or definesome advanced concepts to record the flow of environments (like in λε). The proof of termination
is even easier than in substitution-based lambda calculi. No reasoning of substitutions is needed
given that the global environment in λE contains enough information. Furthermore, the use of deBruijn indices also paves the way to connect λE with other conventional computational models
using de Bruijn indices, which is not done for Ei .
2.5

Applications of the λE Calculus

First-class environments provide interesting expressiveness over conventional lambda calculi.
Several authors, have already argued for the ability of first-class environments to model a formof first-class modules and/or declarations [Gelernter et al. 1987; Jagannathan 1994; Queinnec andRoure 1996]. We revisit this ability in λE . Furthermore, we argue that first-class environments
provide an alternative to model capabilities [Miller 2006; Miller et al. 2000], which are commonlymodelled via objects. We propose using first-class environments instead, as an alternative to objects
to model capabilities.
First-class modules. Cardelli [1997] proposed a simply-typed calculus with high-level abstractions
for modules and interfaces, where a module consists of abstract interfaces and a list of function
declarations that may require the interfaces. Here we adopt a similar form of first-class modules
where imports from other modules are done by module parameters. In our design modules are
sandboxed: the only functionality that a module can use must either be defined in the module itself,or it must come from the module parameters. In other words, modules cannot access the global
environment. In this way, users are able to determine the authority of a module by examining thecapabilities supplied as arguments [Melicher et al. 2017]. Such setting, makes it convenient to track
and control module access. To illustrate how first-class modules can be modelled with first-classenvironments using λE , consider two libraries represented as modules:
module IOUtils whereprint : String → Void = ...
...
module ListUtils(print : String → Void) where
sort : [Int] → [Int] = ...
printLst : [Int] → Void = ...
IOUtils is a module that consists of several IO-related operations such as a print function. Module
ListUtils requires an external print function. Moreover, it contains a sort function that sorts alist of integers and printLst that calls the imported function print for printing a list. A user canalso create a program as follows:
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:10

Jinhao Tan and Bruno C. d. S. Oliveira

module Main(sort : [Int] → [Int], printLst : [Int] → Void) whereprintSorted : [Int] → Void = printLst . sort
main : Void = printSorted([2, 1, 3])Here, Main requires functions sort and printLst. In the module, printSorted uses these two functionalities to print a sorted list, and main applies printSorted with [2, 1, 3]. The sorted list
[1, 2, 3] should be printed after the execution of main.
Sandboxed modules in λE . IOUtils and ListUtils above are modelled as first-class entities in λE :{IOUtils : {print : String → Void} & ...}
{IOUtils = ε ▷ {print = ...} # ...}
{ListUtils : {print : String → Void} →{sort : [Int] → [Int]} & {printLst : [Int] → Void}}{ListUtils = ε ▷ λ{print: String → Void}.
({sort = ...} # {printLst = ...}) }The merge operator is used to compose declarations of functions in a module. A module is not
fully implemented if a module requires external functions. For instance ListUtils is not fully
implemented. Nevertheless, functions defined in such a module can rely on the abstract interfaces(i.e., arguments passed to the module). In this case, a lambda abstraction boxed with empty environment ε is used for modelling such a module, where the imported interfaces are encoded as
input types. Thus, to use the module we must apply it with some concrete implementations of therequired functions. Note also that in the encoding above, the local environment is ε (the empty
environment) so that functions inside a module can only rely on what it imports. In other words,
the module is sandboxed and can only use bindings that are explicitly required by the module.
Therefore, functions inside ListUtils cannot get access to resources from the global environment.
The user-defined module can be modelled in a similar manner:{Main : {sort : [Int] → [Int]} & {printLst : [Int] → Void} →{printSorted : [Int] → Void} & {main : Void}}{Main = ε ▷ λ{sort : [Int] → [Int]} & {printLst : [Int] → Void}.
({printSorted = printLst . sort} # {main = printSorted([2, 1, 3])}) }The merge operator in λE is dependent. Thus printSorted can be referred by main. Now we canimplement the ListUtils module and then pass the implementation of sort and printLst to Main:({ListUtilsImp = ListUtils({print = IOUtils.print})} # {Main = Main}) ▷Main({sort = ListUtilsImp.sort} # {printLst = ListUtilsImp.printLst})

The expression above can be compiled in an environment containing IOUtils, ListUtils and Main.
Note that at the end of the first line there is a box operator ▷. This example illustrates how one canmanipulate environments. Module ListUtilsImp is implemented by accepting the print function
from IOUtils, and Main is imported to the environment for the box. In this way, we obtain anenvironment {ListUtilsImp = ...} # {Main = ...}, from which we can make module Main be
concretized with sort and printLst coming from ListUtilsImp. The advantage of module systems
is that a user-defined program is decoupled from concrete implementations of libraries. Hence,
users are supposed not to know the concrete implementation of modules. For example, sort could
be reimplemented later using a more efficient algorithm, and printLst can be updated to print alist in a prettier format. Thus we could have a different implementation of ListUtils, to obtainthese alternative functions.
Capabilities as first-class environments. Object-capability programming [Miller 2006; Miller et al.
2000] is a programming paradigm that provides a mechanism for controlling access to resources.
Several capability languages have been developed, such as Joe-E [Mettler et al. 2010], Caja [Miller
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

360:11

et al. 2008], ADsafe [Crockford 2008], and Wyvern [Melicher et al. 2017]. With these languages,
one can grant limited privileges to untrusted code by selectively passing it relevant capabilities.
To ensure security, some form of explicit authorization mechanism is needed to be applied in theimplementation of capability languages. In a capability-safe setting, we must ensure that capabilities
can only be provided explicitly via some parameters, instead of being implicitly accessed via the
global environment. Sandboxed modules, which can only use bindings that are explicitly passed asarguments, are thus useful for modelling capabilities.
In general, with the box construct, only a specific set of APIs is exposed to users as mediatedaccess to certain capabilities is performed. Alternatively access to the APIs can be restricted. In λE ,we can use first-class environments/modules to model capabilities, and the box construct to model
mediated access to capabilities. For example, it is possible that a program is created as follows:
module Untrusted(sort : [Int] → [Int], print : String → Void) where
sorted : [Int] = sort([2, 1, 3])
main : Void = print("hacked")

This module imports a sort and a print function. Suppose that this is a module from an untrusted
party. Hence, we want to restrict this module so that it is not implemented with the real printfunction and thus “hacked” will not be printed. In λE , we can use first-class environments and thebox construct to achieve the goal:({printReal = IOUtils.print} #{ListUtilsImp = ListUtils({print = printReal})} #{Untrusted = Untrusted} #{printImp = error "cannot access this function"}) ▷Untrusted({sort = ListUtilsImp.sort} # {print = printImp})

Here, printReal is the real implementation of the print function. We can use it to implement
ListUtilsImp to obtain the implementation of a sort function. On the other hand, printImp is amock implementation of the print function. Note that boxes can only access the local environment.
This means that boxes provide mediated access to the environment, as well as, fine-grained controlof capabilities. Moreover, Untrusted is not able to use the real print capability implicitly, since the“print” capability accessed by Untrusted is printImp which is passed as an argument by the user.
Now the execution of the expression above will output an error message instead of “hacked”.
3

The λE Calculus: Syntax, Typing and Semantics

In this section, we will introduce the λE calculus, which is a calculus with first-class environments.
The design of first-class environments in λE is partly inspired by Tan and Oliveira [2023]. In particular we borrow the following ideas: typing contexts are modelled as types; runtime environments
as values; and compositions of environments as merges. However, our approach to binding is basedon de Bruijn indices, making modelling standard lambda abstractions simple and straightforward.
3.1

SyntaxThe syntax of the λE calculus is shown in Figure 1. We use colors to highlight the constructs,
and corresponding rules, that are related to first-class environments. Blue is used to highlight theconstructs related to standard environment lookup. Red is used to highlight constructs that can beused to create labelled expressions and lookup by label. We also use green, to highlight boxes which,in a calculus with first-class environments, can have a very general form. Though λE supports
first-class environments, we can restrict the expressiveness of λE such that first-class environments
are disabled, while retaining the notion of closures. To do so we remove or change the colored
constructs, to obtain a closure calculus. We show how this alternative design works in Section 6.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:12Jinhao Tan and Bruno C. d. S. Oliveira

TypesA, B, Γ F Int | ε | A & B | A → B | {l : A}

Expressions
ValuesFramesSyntactic Sugare F ? | e.n | i | ε | λA. e | e1 ▷ e2 | ⟨v, λA. e⟩ | e1 e2 | e1 # e2 | {l = e} | e.lv F i | ε | ⟨v, λA. e⟩ | v1 # v2 | {l = v}

F F [ ].n | [ ] # e | [ ] e | [ ] ▷ e | v [ ] | {l = [ ]} | [ ].ln ≜ ?.nl ≜ ?.lFig. 1. λE syntax

Types and contexts. Meta-variables A, B, Γ range over types and typing contexts. Note that in
our calculus there is no distinction between contexts and types. Contexts are just types and any
type can act as a context. Types/contexts include base types (Int), a unit type used to denote
empty environments (ε), a limited form of intersection types (A & B), arrow types (A → B), andsingle-field record types ({l : A}). A multi-field record type {l1 : A1 , . . . , ln : An } can be obtainedby intersecting several single-field records: {l1 : A1 } & · · · & {ln : An } [Reynolds 1997].
Expressions. Meta-variables e range over expressions. Expressions include several standard
constructs: integers (i), the unit expression (ε), applications (e1 e2 ), merges (e1 # e2 ) and lambda
abstractions (λA. e). Merges are left associative. Thus, e1 # e2 # e3 is interpreted as (e1 # e2 ) # e3 . Notethat de Bruijn notation is applied in our calculus, and the variable bound by a lambda abstraction isnameless. In addition, we have boxes (e1 ▷ e2 ) for running computations under a given environment,
and closures (⟨v, λA. e⟩) that record the lexical environment of a function. The query construct (?)
reifies the current environment, and the projection (e.n) construct returns the n-th element of an
expression. In this way, a variable, denoted by a de Bruijn index n, can be regarded as ?.n, which is
a compound expression with a query and a projection. Single-field records are denoted by {l = e}.
A multi-field record {l1 = e1 , . . . , ln = en } can be represented as a merge of single-field records{l1 = e1 } # · · · # {ln = en }. Finally, besides being able to lookup an environment by a de Bruijn
index, it is also possible to have labelled entries in the environment and lookup by label. Using theselection construct (e.l), the field labelled by l from a multi-field record can be fetched. Similarly tolookup by de Bruijn indices, we can also have syntactic sugar for looking up a labelled entry in theenvironment by its label l.
Values and frames. Meta-variables v range over values. A value is either an integer (i), the unit
expression (ε), a closure (⟨v, λA. e⟩) where the lexical environment is also a value, a merge (v1 # v2 )of two values, or a record whose field is also a value ({l = v}). Frames (F) specify evaluation contexts
for applications, merges, boxes, projections, records, and selections. Note that frames do not include
evaluation on the right-hand side of a merge or a box.
3.2

Type System

Figure 2 shows the type system. The typing rules for integers, the unit expression, applications andlambda abstractions are standard. Rule Typ-lam is the typing rule for lambda abstractions. Since deBruijn notation is used in our calculus, the variable bound by the current λ is represented as 0. In
rule Typ-lam, the type of 0, which is the input type A, is appended to the context Γ by intersecting Γand A, such that it is the rightmost type in the context. This matches the conventional right-to-leftcounting of λ binders. The query construct ? can synthesize the context (rule Typ-ctx). Since a
context is simply a type in our setting, the type of ? is the current context. Rule Typ-proj is thetyping rule for projections. The type of a query e.n is the n-th element of the type of e that is
obtained by the lookup function:
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

360:13

l:A∈B(Containment)

ctm-rcdl : A ∈ {l : A}

ctm-andl

ctm-andrl:A∈Bl ∉ label(C)l : A ∈ B&C

l:A∈Cl ∉ label(B)l : A ∈ B&CΓ ⊢e:A(Typing)
Typ-proj
Typ-ctx

Γ ⊢e:BΓ ⊢?:Γ
Typ-topΓ ⊢ε:εTyp-litlookup(B, n) = AΓ ⊢ e.n : AΓ ⊢ i : Int

Typ-boxTyp-merge

Γ ⊢ e1 : Γ1
Γ1 ⊢ e2 : AΓ ⊢ e1 ▷ e2 : AΓ ⊢ e1 : A
Γ & A ⊢ e2 : BΓ ⊢ e1 # e2 : A & B

Typ-app

Typ-lamΓ ⊢ e1 : A → BΓ ⊢ e2 : AΓ ⊢ e1 e2 : B

Γ &A ⊢ e : BΓ ⊢ λA. e : A → B

Typ-closTyp-rcd

Typ-selε ⊢ v : Γ1
Γ1 & A ⊢ e : BΓ ⊢ ⟨v, λA. e⟩ : A → BΓ ⊢e:AΓ ⊢ {l = e} : {l : A}Γ ⊢e:Bl:A∈B
Γ ⊢ e.l : A

Fig. 2. Type System.

lookup(A & B, 0) = B
lookup(A & B, n + 1) = lookup(A, n)Consequently, the type of variable n (encoded as ?.n) is the n-th element in the typing context.
Rule Typ-merge is the typing rule for merges. The right branch e2 may depend on the left branch
e1 in merge e1 # e2 , since the context for typing e2 is the type Γ & A, which is the intersection of thetyping context for e1 # e2 and the type of e1 . Rule Typ-box is the rule for boxes. In order to typechecka box e1 ▷ e2 , we first check that e1 is well-typed under the global context and then e2 is checked
under the type of e1 . Rule Typ-clos is the rule for closures. For a closure ⟨v, λA. e⟩, the body e ischecked under the type of the lexical environment v and the input type A. Since v is a value that isclosed, the typing context for it can be ε in the rule. Rule Typ-sel is the rule for selection. The typeof e.l is A if the type of e contains the entry l : A. In order to ensure determinism, when there are
multiple entries for l in B, the selection fails according to the containment judgment l : A ∈ B.
3.3

Dynamic Semantics

Figure 3 shows the small-step call-by-value operational semantics for λE . The reduction has theform of v ⊢ e1 ,→ e2 . The value v denotes the runtime environment. We define multi-step reduction,→∗ as the reflexive and transitive closure of ,→. Rule Step-ctx reduces a query ? to the current
runtime environment. To evaluate a projection e.n, expression e is evaluated to a value v first, after
which rule Step-proj is triggered. The n-th element of v is fetched by lookupv:
lookupv(v1 # v2 , 0) = v2
lookupv(v1 # v2 , n + 1) = lookupv(v1 , n)A merge e1 # e2 is evaluated from left to right. After e1 is evaluated to a value v1 , v1 is added to theruntime environment by rule Step-merger, and e2 can refer to both v and v1 . An application e1 e2Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:14

Jinhao Tan and Bruno C. d. S. Oliveira

v.l ⇝ v ′(Selection)
sel-rec{l = v}.l ⇝ v

sel-mrgl

sel-mrgr

v1 .l ⇝ v
(v1 # v2 ).l ⇝ v

v2 .l ⇝ v
(v1 # v2 ).l ⇝ v

v ⊢ e ,→ e ′(Small-step Operational Semantics)
Step-evalv ⊢ e ,→ e ′v ⊢ F[e] ,→ F[e ′ ]Step-mergerv # v1 ⊢ e2 ,→ e2′v ⊢ v1 # e2 ,→ v1 # e2′

Step-ctx

Step-projv ⊢ ? ,→ v

v ⊢ v1 .n ,→ lookupv(v1 , n)

Step-box

v1 ⊢ e ,→ e ′v ⊢ v1 ▷ e ,→ v1 ▷ e ′Step-boxvv ⊢ v1 ▷ v2 ,→ v2
Step-sel

Step-closure

Step-betav ⊢ λA. e ,→ ⟨v, λA. e⟩v ⊢ ⟨v1 , λA. e⟩ v2 ,→ (v1 # v2 ) ▷ e

v1 .l ⇝ v2v ⊢ v1 .l ,→ v2

Fig. 3. Dynamic Semantics.

is also evaluated from left to right. We have closures, instead of lambda abstractions, as values in our
calculus. Hence, e1 in the application evaluates to a closure ⟨v1 , λA. e⟩. Moreover, beta reduction issubstitution-free: argument v2 is not substituted into the function body. Instead, rule Step-beta
adds v2 into the runtime environment by merging v1 , the lexical environment for the closure, with
v2 . In our small-step reduction, this action is represented as a single step, and the result of beta
reduction is (v1 # v2 ) ▷ e, i.e., e boxed with v1 # v2 . After that, the function body e can be evaluatedfurther under environment v1 # v2 . To evaluate a box e1 ▷ e2 , we first evaluate e1 to a value v1 ,and then e2 is reduced under environment v1 by rule Step-box. Once the evaluation of e2 is done,
rule Step-boxv extracts the value from the box. For a selection e.l, e is evaluated to a value v andthen v.l ⇝ v ′ is called by rule Step-sel to get the value labelled by l.
4

Reasoning with Environment-Based Semantics

In this section, we show that λE has numerous interesting properties. More importantly, reasoning
about these properties is simple, and we argue that is often easier than formulations based ona standard lambda calculus with substitution-based beta-reduction. In particular, because there
is no substitution in the calculus, the use of de Bruijn indices is very natural and no reasoning
about shifting/unshifting is ever needed. Moreover, the formalization style is very friendly tomechanized theorem provers where binding is a well-known source of complexity [Aydemir et al.
2005; Charguéraud 2012]. In our Coq formalization binding was never a problem.
4.1

Determinism and Syntactic Type Soundness

The operational semantics of λE is deterministic and type-sound. The statement of these theorems
follows the form by Tan and Oliveira. In contrast to substitution-based reduction, a value v is
responsible for tracking how the runtime environment is updated during reduction. As a result,
the theorem would not be strong enough if we set v to the empty environment ε. Hence, anarbitrary environment needs to be considered in the theorems, and we need to ensure that theenvironment involved is well-typed. Note that we do not need to define a typing judgment forenvironments, since environments and expressions share the same set of typing rules as they are
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

360:15

unified. Importantly, note that the substitution lemma, which is used in traditional type soundness
proofs [Wright and Felleisen 1994], is not needed, since we do not use substitution in the semantics.
We first show that our type system prevents ambiguous selections. A repeated label is allowed toappear in a multi-field record. For example, let e be {l1 = 1} # {l2 = true} # {l2 = 2} and it has type{l1 : Int} & {l2 : Bool} & {l2 : Int}. Invoking selection of l1 for e gives 1 safely. However, if the label is
l2 , then e.l2 would evaluate to either true or 2, resulting in ambiguity. The containment judgmentl : A ∈ B in the type system rules out the ambiguous selections statically. Hence, e.l2 is forbidden.
Formally, we have the following lemma stating that well-typed selection is deterministic:
Lemma 4.1 (Determinism of Selection). If Γ ⊢ v.l : A and v.l ⇝ v1 and v.l ⇝ v2 , then v1 = v2 .
With the help of determinism of selection, we have determinism of reduction.
Theorem 4.2 (Generalized Determinism). If ε ⊢ v : Γ and Γ ⊢ e : A and v ⊢ e ,→ e1 andv ⊢ e ,→ e2 , then e1 = e2 .
By instantiating v and Γ with ε, we obtain the standard determinism theorem as a corollary.
Corollary 4.3 (Determinism). If ε ⊢ e : A and ε ⊢ e ,→ e1 and ε ⊢ e ,→ e2 , then e1 = e2 .
Next we introduce the progress and preservation theorems for type-soundness. We first prove
progress and preservation for the lookup function and label selection.
Lemma 4.4 (Progress of Lookup). If ε ⊢ v : A and lookup(A, n) = B, then there exists v ′ s.t.
lookupv(v, n) = v ′ .
Lemma 4.5 (Preservation of Lookup). If ε ⊢ v : A and lookup(A, n) = B and lookupv(v, n) =v ′ , then ε ⊢ v ′ : B.
Lemma 4.6 (Progress of selection). If ε ⊢ v : A and l : B ∈ A, then there exists v ′ s.t. v.l ⇝ v ′ .
Lemma 4.7 (Preservation of selection). If ε ⊢ v : A and l : B ∈ A and v.l ⇝ v ′ , thenε ⊢ v ′ : B.
With the lemmas above, we know that if the environment v is well-typed, then any value produced
during the evaluation of e that refers to v (by lookup or by label selection) should progress andpreserve types. Consequently, we have the following generalized theorems.
Theorem 4.8 (Generalized Progress). If ε ⊢ v : Γ and Γ ⊢ e : A, then either e is a value or
there exists e ′ s.t. v ⊢ e ,→ e ′ .
Theorem 4.9 (Generalized Preservation). If ε ⊢ v : Γ and Γ ⊢ e : A and v ⊢ e ,→ e ′ , thenΓ ⊢ e ′ : A.
Standard progress and preservation theorems are now corollaries as follows.
Corollary 4.10 (Progress). If ε ⊢ e : A, then either e is a value or there exists e ′ s.t. ε ⊢ e ,→ e ′ .
Corollary 4.11 (Preservation). If ε ⊢ e : A and ε ⊢ e ,→ e ′ , then ε ⊢ e ′ : A.
4.2

Semantic Type Soundness and Termination

Termination. We also define semantic typing and prove the termination (or normalization) for
our calculus following Tait’s method [Tait 1967]. Proving the termination of the Simply Typed
Lambda Calculus (STLC) by performing induction on the typing judgment directly does not work,
since we are stuck at the case of application e1 e2 : the induction hypotheses for e1 and e2 are notstrong enough to conclude that e1 e2 terminates. We know that e1 and e2 evaluate to a lambda
abstraction λx : A. e and a value v2 respectively, and the beta reduction gives e[v2 /x]. However,whether the function body e terminates is unknown and the proof cannot proceed.
The standard method to strengthen the theorem is to define a unary logical relation (a.k.a. logicalpredicate) as a proxy to decompose the proof into two steps: we first embed the termination property
into the logical predicate, and then prove that every well-typed expression satisfies the logicalpredicate. We follow this approach to prove the termination of the λE calculus.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:16

Jinhao Tan and Bruno C. d. S. Oliveirav ∈ VJεK ≜ v = εv ∈ VJIntK ≜ ∃i, v = iv ∈ VJA & BK ≜ ∃v1 v2 , v = v1 # v2 ∧ v1 ∈ VJAK ∧ v2 ∈ VJBKv ∈ VJ{l : A}K ≜ ∃v ′ , v = {l = v ′ } ∧ v ′ ∈ VJAKv ∈ VJA → BK ≜ ∃v1 e, v = ⟨v1 , λA. e⟩ ∧ (∀v2 ∈ VJAK, ∃v ′ , ε ⊢ (v1 # v2 ) ▷ e ,→∗ v ′ ∧ v ′ ∈ VJBK)Γ |= e : A ≜ ∀v ∈ VJΓ K, ∃v ′ , v ⊢ e ,→∗ v ′ ∧ v ′ ∈ VJAK

Fig. 4. Semantic Typing.

Semantic typing is recursively defined in Figure 4. We define a logical predicate to include values(v ∈ VJAK) and expressions (Γ |= e : A) that have the expected semantic behaviour. The semantic
type VJAK captures all the values of type A that terminates. To be more specific, VJεK includes theempty environment ε, VJIntK consists of all of the integers; VJA & BK and VJ{l : A}K are comprisedof merge values and record values, respectively. VJA → BK is made up of closures. Moreover, it isrequired that, for any value v2 of semantic type A, the result of the beta reduction, i.e., (v1 # v2 ) ▷ e,can be evaluated to a value v ′ of semantic type B. This condition ensures that the function body,which is exposed after the beta reduction, actually terminates (under the updated environment),
and thus it provides a strong hypothesis for the termination proof. The definition of VJA → BK issimilar to the one in the proof of termination for substitution-based calculi, but a boxed expression,
instead of meta-level substitution e[v2 /x], is applied in the definition.
An expression e has semantic type A in typing context Γ , if e can evaluate to a value of type A inevery environment v of semantic type Γ . We prove that syntactic typing entails semantic typing:
Theorem 4.12 (Semantic Soundness). If Γ ⊢ e : A then Γ |= e : A.
The proof is done by induction on the typing judgment. In each case, we need to show that therule of syntactic typing can be derived for semantic typing. For example, we have the lemmas forquery, box, and lambda abstraction as follows:
Lemma 4.13 (Soundness of qery). Γ |= ? : Γ .
Lemma 4.14 (Soundness of box). If Γ |= e1 : Γ1 and Γ1 |= e2 : A, then Γ |= e1 ▷ e2 : A.
Lemma 4.15 (Soundness of lambda abstraction). If Γ & A |= e : B, then Γ |= λA. e : A → B.
Each lemma has the same “shape” of its corresponding syntactic typing rule. This property also
holds for the other constructs. Next we introduce briefly the proof of Lemma 4.15, which is a hardcase in the termination proof for substitution-based semantics, but is easy in our formulation. To
prove Γ |= λA. e : A → B, suppose that v1 ∈ VJΓ K, then we have v1 ⊢ λA. e ,→∗ ⟨v1 , λA. e⟩. So
we need to show ⟨v1 , λA. e⟩ ∈ VJA → BK by the definition of semantic typing. By the definition
of VJA → BK, we suppose that v2 ∈ VJAK. Now we merge the environment v1 with v2 , and wehave v1 # v2 ∈ VJΓ & AK. By the assumption Γ & A |= e : B, we know that there exists a value
v ′ such that v1 # v2 ⊢ e ,→∗ v ′ and v ′ ∈ VJBK. By the semantics of the box construct, we haveε ⊢ (v1 # v2 ) ▷ e ,→∗ (v1 # v2 ) ▷ v ′ ,→∗ v ′ and the proof is complete.
Now we can obtain the termination result easily because termination is plugged in the definitionof semantic typing. Theorem 4.12 is in a generalized form. By picking Γ to be empty, we get thefollowing termination theorem.
Theorem 4.16 (Termination). If ε ⊢ e : A then there exists a value v s.t. ε ⊢ e ,→∗ v.
Our definition of semantic typing uses the environment-based evaluation v ⊢ e ,→∗ v ′ so that
open terms in e can refer to v. In the proof of termination of STLC, a simultaneous substitution γ,
which is essentially an environment, is introduced for dealing with open terms. However, sinceProc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

360:17v ⊢ e ⇒ e′

(Big-step Operational Semantics)

Bstep-ctx

Bstep-projv ⊢ e ⇒ v1

Bstep-lit

Bstep-closv⊢?⇒vv ⊢ e.n ⇒ lookupv(v1 , n)v⊢i⇒iv ⊢ ⟨v1 , λA. e⟩ ⇒ ⟨v1 , λA. e⟩

Bstep-unit

Bstep-mergev ⊢ e1 ⇒ v1

v # v1 ⊢ e2 ⇒ v 2

Bstep-boxv ⊢ e1 ⇒ v1v ⊢ e1 # e2 ⇒ v1 # v2v⊢ε⇒ε

Bstep-appv ⊢ e1 ⇒ ⟨v1 , λA. e⟩

v ⊢ e2 ⇒ v2v ⊢ e1 e2 ⇒ v′

Bstep-lam

Bstep-recv ⊢ e ⇒ v1v ⊢ λA. e ⇒ ⟨v, λA. e⟩v ⊢ {l = e} ⇒ {l = v1 }v1 ⊢ e2 ⇒ v 2

v ⊢ e1 ▷ e2 ⇒ v2
v1 # v2 ⊢ e ⇒ v ′Bstep-selv ⊢ e ⇒ v1

v1 .l ⇝ v2v ⊢ e.l ⇒ v2

Fig. 5. Big-step operational semantics.

environments are not involved in the substitution-based semantics of STLC, the target expression is
set to be γ(e), the application of γ with e, for generalizing the theorem. As a result, the lambda caseof semantic soundness requires careful reasoning about substitutions. In contrast, reasoning about
environments is much easier in λE and we do not need to handle substitutions at all. In addition, fora substitution-based semantics, γ cannot be any arbitrary substitution. A context relation γ |= Γ isdefined to ensure that γ respects termination: γ should produce expressions that are terminating
for all the variables in Γ . On the other hand, the λE calculus features first-class environments, andthus v ∈ VJΓ K can act as such a context relation because environments are values.
4.3

Big-step Semantics

We also present a big-step operational semantics (shown in Figure 5) for λE , which is in spirit
to the environment-based natural semantics [Kahn 1987]. The big-step semantics specifies theentire transition from an expression to a final value. The rules for values, lambda abstractions, andapplications are mostly standard. Values reduce to themselves and lambda abstractions reduce toclosures. Unlike small-step reduction, rule Bstep-app does not rely on the box construct, since
we do not need to store the intermediate result in the big-step evaluation. Rule Bstep-box is theevaluation rule for boxes, where e1 reduces to a value that acts as an environment for e2 and thene2 reduces to the final value. Note that rule Step-boxv in the small-step semantics is not needed in
the big-step evaluation, since the result of reducing e2 can be obtained directly from the premise ofrule Bstep-box. Also note that n is a syntactic sugar of ?.n. Thus the rule for variables is
Bstep-varv ⊢ n ⇒ lookupv(v, n)
In fact, the semantics in Figure 5 can be seen as a modular extension of the environment-based
big-step semantics of the lambda calculus, except that the environments in the relation are values.
Next we prove that the small- and big-step semantics are equivalent. The proof is simple, since
our small-step semantics is also environment-based. We first show that big-step semantics is soundw.r.t. the small-step semantics:
Lemma 4.17. If v ⊢ e ⇒ v ′ then v ⊢ e ,→∗ v ′ .
The proof is done by induction on the big-step relation. For the case of application, we know thatv ⊢ e1 ,→∗ ⟨v1 , λA. e⟩ and v ⊢ e2 ,→∗ v2 . Thus we have v ⊢ e1 e2 ,→∗ ⟨v1 , λA. e⟩ v2 ,→∗ (v2 #v1 )▷e.
However, we only have v2 # v1 ⊢ e ,→∗ v ′ by the induction hypothesis for e, while our goal is toProc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:18

Jinhao Tan and Bruno C. d. S. Oliveira

prove v ⊢ (v2 # v1 ) ▷ e ,→∗ v ′ . We have the following lemma to fill this gap. That is, the global
environment can be assigned as a local environment and the final result is not affected.
Lemma 4.18. If v ⊢ e ,→∗ v ′ and v ′ is a value, then v1 ⊢ (v ▷ e) ,→∗ v ′ for any v1 .
Moreover, we show that the big-step semantics is complete, which relies on lemma 4.20, statingthat one single step can be encompassed by the big-step semantics.
Lemma 4.19. If v ⊢ e ,→∗ v ′ and v ′ is a value, then v ⊢ e ⇒ v ′ .
Lemma 4.20. If v ⊢ e1 ,→ e2 and v ⊢ e2 ⇒ v ′ , then v ⊢ e1 ⇒ v ′ .
Finally, by combining lemma 4.17 and lemma 4.19, we have the equivalence result as following.
Theorem 4.21 (Eqivalence of Semantics). v ⊢ e ⇒ v ′ if and only if v ⊢ e ,→∗ v ′ .
4.4Conservativity over the Simply Typed Lambda Calculus

For our calculus to serve as a replacement to the Simply Typed Lambda Calculus (STLC), it isdesirable that it is a conservative extension of the STLC. Thus, λE should be able to simulate andexpress different aspects of the semantics of the STLC. We relate our calculus to the STLC here.
Figure 6 shows the definition of the STLC. We use Γλ and Γλ ⊩ e : A to denote the contexts andtyping judgment respectively for the STLC. Binding is also modelled using de Bruijn indices, andthe dynamic semantics is a standard call-by-value small-step reduction. Since the reduction is weak(no reductions happen under abstractions), we can employ a simpler form of substitution for beta
reduction [Forster and Smolka 2017]. The correspondence between STLC contexts and λE types
is defined by the relation Γ ∼ Γλ . Let ⊢λ e and ⊢λ A represent that e and A are expressions andtypes respectively in STLC. The connection with the typing of STLC is easy to establish:
Theorem 4.22 (Completeness w.r.t. Typing). If Γλ ⊩ e : A and Γ ∼ Γλ , then Γ ⊢ e : A.
Theorem 4.23 (Conservativity w.r.t. Typing). If ⊢λ e, ⊢λ A, Γ ∼ Γλ , and Γ ⊢ e : A, thenΓλ ⊩ e : A.
Now we connect our semantics with the semantics of STLC. Since lambda abstractions are values
in STLC, but not in λE , we need first to relate values in STLC and values in λE . Inspired by theunfolding operation in the work by Forster et al. [2020], we define a substitution function S(v, e, k)that substitutes free variables in a λE expression e by their values in the environment v at depth k,
and returns an STLC expression after the substitution. In this way, a closure in λE is transformed
to a corresponding closed lambda abstraction. Note that this substitution function is not the sameas the one in the reduction rule of STLC. The substitution in the beta reduction is an operation on
STLC expressions and does not involve environments.
Definition 4.24 (Substitution). The substitution function S(v, e, k) is recursively defined as:
S(v, i, k) = i
S(v, n, k) = n

if n < kS(v, n, k) = i if n ⩾ k and lookupv(v, n − k) = i
S(v, n, k) = λA.S(v ′ , e, 1)

if n ⩾ k and lookupv(v, n − k) = ⟨v ′ , λA. e⟩S(v, λA. e, k) = λA.S(v, e, k + 1)
S(v, e1 e2 , k) = S(v, e1 , k) S(v, e2 , k)With the help of the substitution function, now we can define value correspondence, as shown in
Figure 6. Any integer corresponds to itself. An STLC lambda abstraction λA. e corresponds to a λE
closure ⟨v, λA. e ′ ⟩ such that substituting e ′ with environment v at depth 1 gives the function bodye. We prove that the dynamic semantics of λE is complete and conservative w.r.t. the one of STLC.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

360:19A, B F Int | A → B

Types
Terms

e F n | i | e1 e2 | λA. e

Valuesvλ F i | λA. e

Contexts

Γλ F · | Γλ , A(Typing of STLC)Γλ ⊩ e : A
styp-litΓλ ⊩ i : Int

styp-varstyp-appstyp-lamΓλ [n] = AΓλ ⊩ n : AΓλ ⊩ e1 : A → BΓλ ⊩ e2 : AΓλ ⊩ e1 e2 : B

Γλ , A ⊩ e : BΓλ ⊩ λA. e : A → B

e ,→ e ′(Reduction of STLC)
sred-beta(λA. e) v ,→ e[0 7→ v]

sred-appl

sred-appr

e1 ,→ e1′
e1 e2 ,→ e1′ e2

e2 ,→ e2′
v1 e2 ,→ v1 e2′Γ ∼ Γλ(Context Correspondence)
crel-andcrel-topε∼·A ∼ ΓλA & B ∼ Γλ , Bv ∼ vλ(Value Correspondence)
vrel-lamvrel-liti∼i

S(v, e ′ , 1) = e⟨v, λA. e ′ ⟩ ∼ λA. e

Fig. 6. Simply Typed Lambda Calculus and correspondence to λE .

Theorem 4.25 (Completeness w.r.t. Dynamic). If · ⊩ e : A and e ,→∗ vλ . then there exists v s.t.
ε ⊢ e ,→∗ v and v ∼ vλ .
Theorem 4.26 (Conservativity w.r.t. Dynamic). If ⊢λ e, ε ⊢ e : A and ε ⊢ e ,→∗ v, then there
exists vλ s.t. e ,→∗ vλ and v ∼ vλ .
An important point to note is that the conservativity proof to the STLC is the only place inour proofs where we need to reason about substitution. This is, of course unavoidable, since thestandard formulation of the STLC employs substitution in beta-reduction.
4.5

Closure Calculus λb
ρ

We also connect the λE calculus with the CBV version of the closure calculus λb
ρ [Biernacka andDanvy 2007] shown in Figure 7. Since λb
ρ is an untyped calculus, we only show a connection withrespect to the dynamic semantics. In λb
ρ, terms consist of de Bruijn indices, applications and lambda
abstractions. A closure is either a lambda equipped with a substitution, or an application of two
closures. Values include function closures, and substitutions are lists of closures.
Unlike conventional lambda calculi, the reduction in λb
ρ is defined for closures instead of lambda
terms. Applications of closures are evaluated from left to right. Moreover, closures are distributive
over application of lambda terms, and environment duplicates for each term in the application(rule Red-appdist). Note that this is different from how we evaluate boxes in λE . If there is anapplication e1 e2 boxed by an environment v, then v becomes the global environment for evaluating
e1 e2 , and no duplication of environments is performed for evaluating boxed expressions.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:20

Jinhao Tan and Bruno C. d. S. Oliveirae F n | e1 e2 | λ.e

Terms
Substitutionss F ∅|v·s

Closuresc F e[s] | c1 c2

Valuesv F (λ.e)[s]c ,→ c ′b)(Reduction of λ ρRed-var

Red-betan[v1 · · · vn · · · vm ] ,→ vn((λ.e)[s]) v ,→ e[v · s]

Red-appl

Red-appr

c1 ,→ c1′
c1 c2 ,→ c1′ c2

c2 ,→ c2′
v1 c2 ,→ v1 c2′

Red-appdist(e1 e2 )[s] ,→ (e1 [s]) (e2 [s])Fig. 7. The λb
ρ Calculus

We show that the semantics of the λE calculus can encode the one of λb
ρ by first translating thesubstitutions in λb
ρ to the environments in λE :J∅Ks = εJv · sKs = JsKs # JvKc

Here a list of values is translated to a merge of corresponding values in λE , and the translation ofclosures JcKc is defined as follows:
Jc1 c2 Kc = Jc1 Kc Jc2 Kc

J(λ.e)[s]Kc = ⟨JsKs , λε. e⟩Je[s]Kc = JsKs ▷ e, otherwise

Applications of closures are translated to applications of two expressions. A function closure istranslated to a closure in λE , in which an untyped lambda abstraction in λb
ρ is encoded as a lambda
abstraction with a dummy unit type in λE . For any other closures in λb
ρ, they are encoded as boxes.
With the translation defined, we can prove that the λE is semantically complete and conservative
w.r.t. λb
ρ.
Theorem 4.27 (Completeness). If c ,→∗ v in λb
ρ, then ε ⊢ JcKc ,→∗ JvKc .

Theorem 4.28 (Conservativity). If ε ⊢ JcKc ,→∗ JvKc in λE , then c ,→∗ v.
5Compilation to an Abstract Machine

We compile our calculus to a modern SECD abstract machine [Leroy and Grall 2009]. The syntax
for the abstract machine is:
Instructions

I F Lit(i) | Unit | Clos(C) | Ret | App | Query | Proj(n) | Box(C) | Merge | Trans| Del | Rec(l) | Sel(l)Code

V F i | ε | C[V] | V1 # V2 | {l = V}

StacksS F • | S, V | S, (C, V)

ValuesC F • | I, C

Code is represented as a list of instructions, and instructions are tailored to accommodate theoperations required for implementing the constructs of the λE calculus. The form of values corresponds to the one in the λE calculus where C[V] denotes a function closure in the machine. Like in
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

360:21

JiKe = Lit(i)⟨Lit(i), C; S; V⟩ 7−→ ⟨C; S, i; V⟩⟨Unit, C; S; V⟩ 7−→ ⟨C; S, ε; V⟩⟨Clos(C ′ ), C; S; V⟩ 7−→ ⟨C; S, C ′ [V]; V⟩⟨App, C; S, C ′ [V2 ], V1 ; V⟩ 7−→ ⟨C ′ ; S, (C, V); V2 # V1 ⟩⟨Ret, C; S, (C ′ , V2 ), V1 ; V⟩ 7−→ ⟨C ′ ; S, V1 ; V2 ⟩⟨Query, C; S; V⟩ 7−→ ⟨C; S, V; V⟩⟨Proj(n), C; S, V ′ ; V⟩ 7−→ ⟨C; S, V ′ .n; V⟩⟨Box(C ′ ), C; S, V ′ ; V⟩ 7−→ ⟨C ′ ; S, (C, V); V ′ ⟩⟨Merge, C; S, V1 , V2 ; V⟩ 7−→ ⟨C; S, (V1 # V2 ); V⟩⟨Trans, C; S, V ′ ; V⟩ 7−→ ⟨C; S, V ′ ; V # V ′ ⟩⟨Del, C; S; V # V ′ ⟩ 7−→ ⟨C; S; V⟩⟨Rec(l), C; S, V ′ ; V⟩ 7−→ ⟨C; S, {l = V ′ }; V⟩⟨Sel(l), C; S, V ′ ; V⟩ 7−→ ⟨C; S, V ′ .l; V⟩

JεKe = Unit

J?Ke = QueryJλA. eKe = Clos(JeKe , Ret)Je1 e2 Ke = Je1 Ke , Je2 Ke , App

Je1 # e2 Ke = Je1 Ke , Trans, Je2 Ke , Del, Merge

Je1 ▷ e2 Ke = Je1 Ke , Box(Je2 Ke , Ret)
Je.nKe = JeKe , Proj(n)J{l = e}Ke = JeKe , Rec(l)Je.lKe = JeKe , Sel(l)JiKv = iJεKv = εJ⟨v, λA. e⟩Kv = (JeKe , Ret)[JvKv ]Jv1 # v2 Kv = Jv1 Kv # Jv2 KvJ{l = v}Kv = {l = JvKv }Fig. 8. Transition of the Abstract Machine and Compilation from λE .

the calculus, an environment of the machine is simply a value and we do not need to introduce a
separate definition for environments. A stack consists of values and return frames.
5.1

Transition Relation

The machine state is defined as a triple consisting of code, a stack and an environment. The
transition relation ⟨C; S; V⟩ 7−→ ⟨C ′ ; S ′ ; V ′ ⟩, shown in Figure 8, defines the behaviour of themachine. For example, Clos(C) creates a closure for code C and Ret returns to the calling function,
while App facilitates the execution of a function application. Query reifies the environment bypushing the current environment V to the stack. Proj returns the n-th values V ′ .n of the top
value V ′ of the stack. Rec(l) and Sel(l) return a single-field record and the selection for a label
respectively. Moreover, Merge returns a merge of the top two values of the stack. With Trans andDel, we are able to implement dependent merges. For a dependent merge e1 # e2 , we first computethe code translated from e1 , and this results that a machine value V1 will appear at the top of thestack. Then Trans appends V1 to the environment for computing the code corresponding to e2 .
After that, Del deletes the V1 from the environment for avoiding that V1 affects future computation.
Finally, Merge gives the result by merging V1 and V2 . The instruction that corresponds to the box
construct in λE is Box. Basically, Box(C ′ ) imports an environment for code C ′ . The top value V ′from the stack is assigned as the environment to compute C ′ . After the computation of C ′ , weneed to continue to compute code C with environment V. Thus, a return frame (C, V) is pushed
into the stack in the transition rule for Box.
We define 7−→+ as the transitive closure of 7−→. That is, there is one or more transitions along thecomputation. To establish the connection with the machine, we need to define the compilation from
λE to the abstract machine (Figure 8). The compilation function JeKe compiles each λE expression
to machine code that corresponds to the construct. We also need to connect the values from thesource language to the machine values. JvKv compiles a λE value to a corresponding machine value.
Note that for a closure ⟨v, λA. e⟩ in λE , the environment v is also needed to be compiled.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:22

Jinhao Tan and Bruno C. d. S. Oliveira

A, B, C, Γ ::= . . . | Ref A

Types
Expressions

e ::= . . . | o | ref e | !e | e1 := e2

Valuesv ::= . . . | oLocationsΣ ::= · | Σ, o : A

Storesµ ::= · | µ, o = v

FramesF ::= . . . | ref [ ] | ![ ] | v := [ ] | [ ] := eΣ; Γ ⊢ e : A(Extended Typing)Rtyp-loco:A ∈ ΣRtyp-refΣ; Γ ⊢ e : A

Σ; Γ ⊢ o : Ref A

Σ; Γ ⊢ ref e : Ref A

Rtyp-assign
Σ; Γ ⊢ e1 : Ref A

Rtyp-deref
Σ; Γ ⊢ e : Ref A
Σ; Γ ⊢!e : Av ⊢ µ; e ,→ µ ′ ; e ′Σ; Γ ⊢ e2 : A

Σ; Γ ⊢ e1 := e2 : ε(Extended Small-step Operational Semantics)

Rstep-evalv ⊢ µ; e ,→ µ ′ ; e ′Rstep-refvo ∉ dom(µ)

Rstep-derefo = v1 ∈ µ

v ⊢ µ; F[e] ,→ µ ′ ; F[e ′ ]v ⊢ µ; ref v1 ,→ µ, o = v1 ; ov ⊢ µ; !o ,→ µ; v1

Rstep-assigno ∈ dom(µ)
v ⊢ µ; o := v1 ,→ µ[o 7→ v1 ]; εv ⊢ µ; e ⇒ µ ′ ; e ′Brstep-locv ⊢ µ; o ⇒ µ; o(Extended Big-step Operational Semantics)
Brstep-refv ⊢ µ; e ⇒ µ ′ ; v1o ∉ dom(µ ′ )Brstep-derefv ⊢ µ; e ⇒ µ ′ ; o′v ⊢ µ; ref e ⇒ µ , o = v1 ; oBrstep-assignv ⊢ µ; e1 ⇒ µ1 ; ov ⊢ µ1 ; e 2 ⇒ µ2 ; v 1

o = v1 ∈ µ ′v ⊢ µ; !e ⇒ µ ′ ; v1o ∈ dom(µ2 )v ⊢ µ; e1 := e2 ⇒ µ2 [o 7→ v1 ]; εFig. 9. Extended calculus

We can prove the correctness of the compilation using our big-step semantics. That is, thecompilation preserves program behaviour. If a λE expression e is evaluated to a value v ′ , then themachine reaches a final state, in which the corresponding machine code JeKe is consumed and thecorresponding machine value Jv ′ Kv is left on top of the stack.

Theorem 5.1 (Semantic Preservation). If v ⊢ e ⇒ v ′ then for any code C and stack S,⟨(JeKe , C); S; JvKv ⟩ 7−→+ ⟨C; (S, Jv ′ Kv ); JvKv ⟩.
6

Discussion, Variants and Extensions

We have only studied simply typed calculi. With more advanced calculi and type systems there canbe additional complications. Nonetheless, many programming language features are still quite easy
to add to calculi employing our proposed environment-based semantics. To illustrate this point we
extended λE with references. We also discuss some challenges that we foresee with more advanced
type systems, and some alternative designs may help with some challenges.
6.1

Extension with References

To investigate the addition of features to λE , we create an extension with references. The syntax
and rules for references in the extended calculus are shown in Figure 9.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

Instructions

360:23

I F . . . | Loc(o) | Ref | Deref | Assign

ValuesV F ... | oStoresH F • | H, o = V⟨Loc(o), C; S; V; H⟩ 7−→ ⟨C; S, o; V; H⟩⟨Ref, C; S, V ′ ; V; H⟩ 7−→ ⟨C; S, o; V; H, o = V ′ ⟩′⟨Deref, C; S, o; V; H⟩ 7−→ ⟨C; S, V ; V; H⟩

if o ∉ dom(H)if o = V ′ ∈ H⟨Assign, C; S, o, V ′ ; V; H⟩ 7−→ ⟨C; S, ε; V; H[o 7→ V ′ ]⟩ if o ∈ dom(H)Fig. 10. Extended abstract machine

Syntax. Types are extended with reference types (Ref A), and expressions are extended with
dereferences (!e), assignments (e1 := e2 ), references (ref e) and locations (o). Moreover, the calculus
is equipped with location typing contexts (Σ) that track the bound locations with their types, andstores (µ) for tracking locations with their stored values during the reduction.
Typing and dynamic semantics. The typing relation is enriched as judgment Σ; Γ ⊢ e : A,
where the rules propagate the location typing context Σ. The rules related to references utilize
the information from Σ and they are standard. In the presence of references, we need to define
the well-formedness of stores. A store µ is well-formed with the typing location Σ if they sharethe same domains, and for each location in the store, the bounded value has the corresponding
bounded type. Formally,Σ ⊢ µ ≜ dom(Σ) = dom(µ) ∧ ∀o ∈ µ, Σ; ε ⊢ µ(o) : Σ(o)The small-step reduction is extended with stores as v ⊢ µ; e ,→ µ ′ ; e ′ , which states that inenvironment v, e with store µ reduces to e ′ with the updated store µ ′ . The semantics for referencerelated constructs is also standard. We also define a big-step semantics v ⊢ µ; e ⇒ µ ′ ; e ′ , which isproved to be equivalent to the small-step semantics.
Determinism and type-soundness. We prove that the extended calculus is deterministic:
Theorem 6.1 (Determinism). If Σ; Γ ⊢ e : A, Σ; ε ⊢ v : Γ , Σ ⊢ µ, v ⊢ µ; e ,→ µ1 ; e1 , andv ⊢ µ; e ,→ µ2 ; e2 , then e1 = e2 and µ1 = µ2 .
Furthermore, the progress and preservation of the extended calculus are shown below:
Theorem 6.2 (Progress). If Σ; Γ ⊢ e : A, Σ; ε ⊢ v : Γ , and Σ ⊢ µ, then either e is a value or there
exist e ′ and µ ′ s.t. v ⊢ µ; e ,→ µ ′ ; e ′ .
Theorem 6.3 (Preservation). If Σ; Γ ⊢ e : A, Σ; ε ⊢ v : Γ , Σ ⊢ µ, and v ⊢ µ; e ,→ µ ′ ; e ′ , thenthere exists Σ ′ s.t. Σ ′ ; Γ ⊢ e ′ : A, Σ ′ ⊢ µ ′ and Σ ′ ⊇ Σ.
Compilation to an abstract machine. We also extend the abstract machine so that it has extra
instructions for dealing with references (Figure 10). Moreover, the transition relation becomes⟨C; S; V; H⟩ 7−→ ⟨C ′ ; S ′ ; V ′ ; H ′ ⟩ which includes machine stores. To define the compilation, we
have an extra function J·Kh that translates stores µ in the calculus to the machine stores. We provethat the compilation is correct using the big-step semantics.
Theorem 6.4 (Semantic Preservation). If v ⊢ µ; e ⇒ µ ′ ; v ′ , then ⟨(JeKe , C); S; JvKv ; JµKh ⟩ 7−→+⟨C; (S, Jv ′ Kv ); JvKv ; Jµ ′ Kh ⟩ for any C and S.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:24

6.2

Jinhao Tan and Bruno C. d. S. Oliveira

An Alternative Design: No First-class Environments

In the design of λE we opted to include constructs for first-class environments, since they do not
introduce significant complexity. However, we can easily remove first-class environments, while
preserving our environment-based semantics and making the calculus closer to the lambda calculus.
Firstly, we can remove the constructs (and associated rules) highlighted with red for lookups bylabel. Those constructs are not needed for modelling a conventional lambda calculus. Secondly,
we can simplify the box construct highlighted with green, such that the environment in the box isalways a value:ε ⊢ v : Γ1
Γ1 ⊢ e : A
Typ-boxΓ ⊢v▷e:A
In this way, we can remove [ ] ▷ e from frames since the environment does not need to be evaluatedin the box. Finally, we can remove the blue constructs for queries and index lookups. Instead, we
define directly de Bruijn indexes n, whose static and dynamic behaviour are the same as ?.n:
Typ-var

Step-varΓ ⊢ n : lookup(Γ , n)v ⊢ n ,→ lookupv(v, n)After these steps, and removing corresponding rules, we have a simple calculus with closures. The
simplified calculus may be interesting for language designers, who are not interested in having
first-class environments. Furthermore, in some settings, first-class environments themselves may
introduce complexity, which would not appear without first-class environments. In this case aclosure calculus may be simpler to design and formalize.
6.3

More Powerful Calculi and Type Systems

We foresee some challenges when extending our ideas to more powerful calculi. For example, in
System F, substitution is performed on types. In the type system, substitution on types is needed forthe output type of type applications:Γ ⊢ e : ∀X. B
Typ-tappΓ ⊢ e A : B[A/X]
and substitution of types in terms e[A/X] is applied on beta-reduction of type applications:step-tapp(ΛX. e) A ,→ e[A/X]
in the dynamic semantics. We expect to be able to extend the idea of environment-based reduction
and delaying substitutions to the dynamic semantics: pushing A into the environment rather thansubstituting A for the type variables in e. That is, firstly ΛX. e would reduce to a closure ⟨v, ΛX. e⟩,and then ⟨v, ΛX. e⟩A is beta-reduced to (v # X = A) ▷ e (for readability, here we use a named
presentation for variables in the environment).
It is less clear how to deal with the type-level substitution in the typing rule for type applications.
If we are to follow the spirit of an environment-based semantics, then we ought to replace thetype level substitution with a closure. This hints for a reformulation of the type syntax to include
closures. However, how to redesign the type syntax of System F and its type system with thisclosure formulation is non-obvious. Another alternative is to keep the substitution at the type level,and still benefit from the environment-semantics for terms. However, some complications would be
introduced in this setting. For example, the reasoning would require a form of type correspondence
that connects types with respect to their environments, since substitution is performed in thetyping rule but type references are not resolved in the reduction rule. We expect that the work by
Amin and Rompf [2017] will be helpful to pursue this direction, since they present a definitional(big-step style) interpreter for System F<: , which does not employ substitution. Nevertheless, it isclear that extending the environment semantics to System F requires further study.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

360:25

While many programming languages and calculi rely only on weak forms of reduction, suchas call-by-value reduction, some calculi also employ full reduction. For example, dependent types
are a powerful tool adopted by proof assistants such as Coq. Typically, in a dependently typed
language, determining the equality of types is necessary and is captured as the conversion rule.
The definitional equality of two dependent types is implemented by evaluating the terms on which
the types rely to normal form and subsequently comparing these normalized terms. For example,
to check Vec (1 + 1) is equal to Vec 2 we need to reduce 1 + 1 to 2. Dealing with equality
requires reducing sub-terms at any position including those inside lambdas. However we have notstudied full reduction in our work. For future work, we want to explore the design of environmentbased semantics with full reduction for first-class environments, while expecting to simplify thecomplicated reasoning of (explicit) substitutions in previous work [Nishizaki 1994; Sato et al. 2001].

7

Related WorkFirst-class environments. First-class environments were first introduced by Gelernter et al. [1987]
in the research literature. They proposed a programming language called Symmetric Lisp thatenriches Lisp with first-class environments that can be manipulated at runtime by users. Following
the work by Gelernter et al., there have been several attempts to incorporate first-class environments
into dialects of Lisp. For example, Queinnec and Roure [1996] presented a form of first-classenvironments as an approach to share data objects for the Scheme programming language.
There is also some work on statically typed calculi with first-class environments. Nishizaki [1994]
proposed λ→env with reification and reflection on environments. In our work, the two corresponding
operators are the query and box constructs in λE . λ→env is a non-deterministic calculus defined fromthe weak reduction of the λσ calculus [Curien et al. 1996]. λ→env is proved to have confluence andnormalization. Normalization is proved indirectly by translating the calculus to another calculus
with records. The issue of defining the set of free variables is not covered in λ→env .
Sato et al. [2001] identified the importance of a correct definition of free variables in the presenceof first-class environments. They proposed the λε calculus and addressed the issue of variables
and bindings. The λε calculus is conservative over the lambda calculus with full reduction. Bothλ→env and λε use a named representation for variables, while de Bruijn indices are applied in λE .
However, record-like environments and label-based lookups are still possible in λE . The proof of
normalization in λ→env and λε requires careful reasoning about names and (explicit) substitutions.
For example, the proof in λε requires some sophisticated techniques, such as decoration trees, fortracking the movements of the environments. As discussed by Sato et al., subtle counter-examples
occur if the reduction rule for nested evaluation is not defined properly. In contrast, normalization
is easy to prove with the environment-based semantics in λE . Dezani-Ciancaglini et al. [2008] also
proposed a typed calculus with first-class environments, which we call λc . The calculus focuses onmodelling context-dependent behaviour of objects and employs call-by-value reduction. However,termination and the correspondence to the lambda calculus are unknown.
None of the work above is mechanically formalized in theorem provers. The Ei calculus proposedby Tan and Oliveira is a calculus with environment-based semantics. Similarly to λε and λ→env ,first-class environments are represented as records. Conventional variables and lambda abstractions,however, cannot be expressed in Ei . Thus conservativity over the lambda calculus is unknown, andtermination is not investigated. Fetching values from (global or local) contexts is done by the query
construct and label projections. However, the access of a value from the environment is indirect:
an annotated multi-field record needs to be cast to a single-field record before the lookup by label.
In contrast, the selection in λE is direct since no casting is triggered.

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:26First-class Environments
Reification of Environments
Conservativity over lambda calculus
Termination
Reduction Strategy
Big-step Semantics
Compilation to an Abstract Machine
Extended with References
Mechanized Proofs

Jinhao Tan and Bruno C. d. S. Oliveira

λb
ρ
2007
×
×
✓
Weak

λ→
λε
env
1994 2001
✓
✓
✓
×
×
✓
✓
✓
Weak Full

λc
2008
✓
×

Ei
2023
✓
✓

CBV

CBV

✓
×

✓

✓
×

×

×

λE
present work
✓
✓
✓
✓
CBV
✓
✓
✓
✓

Table 1. A comparison between closure calculi and calculi with first-class environments. A × symbol
denotes a negative result (the property or feature does not hold). A ✓ denotes a positive result. Whitespace denotes that the property/feature has not been studied or it is unknown.

Closure calculi. The calculus of closures λρ [Curien 1991] is a calculus that aims to maintainfaithfulness to the substitution-based lambda calculus, while better reflecting the computational
aspects of abstract machines. Explicit substitutions [Abadi et al. 1991] extend the idea of the closure
calculus where reduction under lambdas is allowed in general. As a result, if de Bruijn notation isused for encoding variables, shifting needs to be defined and an amount of reasoning of shifting
is involved in the proof of metatheory. In contrast, λρ targets weak lambda calculus and there is
no reduction under lambdas. Hence there is no need to be concerned about name clashes, andα-conversion does not need to be performed at any point. Thus de Bruijn indices fit very wellwith λρ. Our calculus λE generalizes this idea with first-class environments. For example, while all
substitutions are at the top level in λρ, nested environments, such as (e1 ▷ e2 ) ▷ e3 , are allowed in
λE . Moreover, a global environment is also applied for evaluating environments with open terms.
The λb
ρ calculus [Biernacka and Danvy 2007] is a minimal extension of λρ, where one-step
reductions can be expressed. In this way, call-by-name and call-by-value strategies are investigatedin λb
ρ. Following the refocusing method [Danvy and Nielsen 2004], several environment machines
can be derived for corresponding reduction strategies. In our work, the calculus is compiled toan abstract machine using a big-step semantics. Jay [2019] also proposes a closure calculus in aformulation different from Curien. The calculus requires no metatheory for substitution and canbe translated to a calculus of combinators. However, the connection with the lambda calculus orabstract machines is unknown. Table 1 provides an overview of the key results in various closure
calculi and calculi with first-class environments.
Type Soundness for Definitional Interpreters. Siek [2013] proposed a simple type soundness proof
for the STLC, based on a (big-step style) definitional interpreter, inspired by an approach toprove type soundness by Ernst et al. [2006]. Amin and Rompf [2017] extended Siek’s approach to
System F<: and variants of the Dependent Object Calculus (DOT) [Rompf and Amin 2016]. In theirapproach, definitional interpreters, which are big-step and substitution-free, are parametrized bya step-counter and errors are dealt with monads. The use of the latter two techniques addresses
well-known limitations of a big-step style for type soundness proofs. In particular in terms of
distinguishing errors from non-termination. Furthermore, the use of step-counters avoids the needfor coinduction, and the proofs can remain inductive. They showed that their approach extends tocommon features, such as references or exceptions. The environment semantics that we employ issmall-step (although we also present a big-step version), so the complications due to the big-stepstyle do not arise in our setting. Thus we do not need to employ step-counters or monads, which
add some additional complexity to proofs and reasoning. Furthermore, we present a calculus with
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

360:27

first-class environments, and we study a broader set of results besides type soundness proofs. Unlike
us, their work covers more advanced type systems. As mentioned in Section 6 we believe that theirwork will be helpful when extending our results to polymorphism.
Binding in mechanized proofs. While paper proofs often overlook the complexities of binders,mechanical proofs that involve binders tend to be more intricate. To measure the progress of
mechanizing proofs, the POPLmark challenge [Aydemir et al. 2005] and POPLMark Reloaded [Abelet al. 2019] have introduced a collection of benchmarks about the metatheory of programming
languages. Many tools have been developed to simplify the process of defining infrastructureand enhance proof automation. For example, Autosubst [Schäfer et al. 2015; Stark et al. 2019] isa Coq library that provides automation for de Bruijn syntax and substitution based on the λσ
calculus [Abadi et al. 1991]. Besides de Bruijn indices, there are other binding representations. The
locally nameless representation [Charguéraud 2012] uses de Bruijn indices to represent boundvariables but applies names to represent free variables. With this approach, the use of shifting andthe need to rename variables can be eliminated. However, this approach requires handling two typesof variables (bound variables and free variables) and managing a separate substitution operation for
each. Moreover, one needs to deal with other concepts, such as variable opening/closing, locallyclosed terms, and universal quantification, when using locally nameless representation. Higher
order abstract syntax (HOAS) [Pfenning and Elliott 1988] is a technique that relies on binders in themeta-language to model binders in the object language. HOAS provides a high level of abstraction
to encapsulate the complexities of reasoning about binders. However, its usability depends on thechosen proof assistant. Abella [Baelde et al. 2014] and Beluga [Pientka and Cave 2015] are two proof
assistants supporting HOAS. Nevertheless, they are based on two rather different background logics.
The nominal approach [Pitts 2003] handles named variables explicitly and offers well-behaved
principles for inductive reasoning for abstract syntax. This method allows for the creation of
mechanized proofs that closely resemble traditional paper proofs. However, the nominal approachrequires the development of an extensive framework and it is currently supported by Nominal
Isabelle [Urban 2008], which relies on a great deal of infrastructure only available in Isabelle. In
our work we suggest that, by adopting an environment-based approach in formalizations, many
common issues with binding and substitution can essentially be avoided. However, more study isneeded to cover more advanced type systems with an environment-based semantics.
8

Conclusion

This paper presents a case for the formalization of programming languages by adopting anenvironment-based semantics. An environment-based semantics provides substantial advantages
over the traditional substitution model. The proposed call-by-value statically typed calculus, λE ,aligns closely with practical execution models and simplifies reasoning, thereby facilitating more
efficient and manageable formalizations with proof assistants. By elevating environments to firstclass citizens within the language, λE enables powerful and flexible abstractions, promoting thedevelopment of sophisticated and modular programs. Furthermore, λE has several desirable properties, such as determinism, type soundness, and normalization, while also establishing operationalcorrespondence with other models. The extension of λE with references and the Coq formalizationof all calculi and proofs further underscores the potential of environment-based semantics as a
viable alternative to the substitution model in programming languages.
Acknowledgments
We are grateful to the anonymous reviewers for their valuable comments. This work has beensponsored by Hong Kong Research Grant Council project number 17209821.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:28

Jinhao Tan and Bruno C. d. S. Oliveira

Data-Availability Statement
The mechanical formalization in Coq is available on Zenodo [Tan and Oliveira 2024].
References
Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. 1991. Explicit Substitutions. J. Funct. Program. 1, 4
(1991), 375–416. https://doi.org/10.1017/S0956796800000186
Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, and Kathrin Stark.
2019. POPLMark reloaded: Mechanizing proofs by logical relations. Journal of Functional Programming 29 (2019), e19.
Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In Proceedings of the 44th ACM
SIGPLAN Symposium on Principles of Programming Languages (POPL ’17). Association for Computing Machinery, 666–679.
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios
Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. 2005. Mechanized Metatheory for the Masses:
The PoplMark Challenge. In Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford,
UK, August 22-25, 2005, Proceedings (Lecture Notes in Computer Science, Vol. 3603), Joe Hurd and Thomas F. Melham (Eds.).
Springer, 50–65. https://doi.org/10.1007/11541868_4
David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. 2014.
Abella: A System for Reasoning about Relational Specifications. J. Formaliz. Reason. 7, 2 (2014), 1–89.
Hendrik Pieter Barendregt. 1985. The lambda calculus - its syntax and semantics. Studies in logic and the foundations ofmathematics, Vol. 103. North-Holland.
Malgorzata Biernacka and Olivier Danvy. 2007. A concrete framework for environment machines. ACM Trans. Comput. Log.
9, 1 (2007), 6. https://doi.org/10.1145/1297658.1297664
Luca Cardelli. 1997. Program Fragments, Linking, and Modularization. In Conference Record of POPL’97: The 24th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France,
15-17 January 1997, Peter Lee, Fritz Henglein, and Neil D. Jones (Eds.). ACM Press, 266–277. https://doi.org/10.1145/
263699.263735
Arthur Charguéraud. 2012. The locally nameless representation. Journal of automated reasoning 49 (2012), 363–408.
Alonzo Church. 1941. The calculi of lambda-conversion. Princeton University Press.
Pierre Crégut. 1990. An Abstract Machine for Lambda-Terms Normalization. In Proceedings of the 1990 ACM Conferenceon LISP and Functional Programming, LFP 1990, Nice, France, 27-29 June 1990, Gilles Kahn (Ed.). ACM, 333–340. https://doi.org/10.1145/91556.91681
Douglas Crockford. 2008. ADsafe. http://www.adsafe.org
Pierre-Louis Curien. 1991. An abstract framework for environment machines. Theoretical Computer Science 82, 2 (1991),
389–402.
Pierre-Louis Curien, Thérèse Hardin, and Jean-Jacques Lévy. 1996. Confluence Properties of Weak and Strong Calculi of
Explicit Substitutions. J. ACM 43, 2 (1996), 362–397. https://doi.org/10.1145/226643.226675
Olivier Danvy and Lasse R Nielsen. 2004. Refocusing in reduction semantics. BRICS Report Series 11, 26 (2004).
Nicolaas Govert De Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In Indagationes mathematicae (proceedings), Vol. 75. Elsevier,381–392.
Mariangiola Dezani-Ciancaglini, Paola Giannini, and Oscar Nierstrasz. 2008. A Calculus of Evolving Objects. Sci. Ann.
Comput. Sci. 18 (2008), 63–98. http://www.info.uaic.ro/bin/Annals/Article?v=XVIII&a=3
Erik Ernst, Klaus Ostermann, and William R. Cook. 2006. A virtual class calculus. In Conference Record of the 33rd ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’06). Association for Computing Machinery,
270–282.
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 Descriptionof Programming Concepts - III, Ebberup, Denmark, 25-28 August 1986, Martin Wirsing (Ed.). North-Holland, 193–222.
Yannick Forster, Fabian Kunze, and Marc Roth. 2020. The weak call-by-value λ-calculus is reasonable for both time andspace. Proc. ACM Program. Lang. 4, POPL (2020), 27:1–27:23. https://doi.org/10.1145/3371095
Yannick Forster and Gert Smolka. 2017. Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. In
Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings(Lecture Notes in Computer Science, Vol. 10499), Mauricio Ayala-Rincón and César A. Muñoz (Eds.). Springer, 189–206.
https://doi.org/10.1007/978-3-319-66107-0_13
David Gelernter, Suresh Jagannathan, and Thomas London. 1987. Environments as First Class Objects. In Conference Recordof the Fourteenth Annual ACM Symposium on Principles of Programming Languages, Munich, Germany, January 21-23,
1987. ACM Press, 98–110. https://doi.org/10.1145/41625.41634

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

A Case for First-Class Environments

360:29Suresh Jagannathan. 1994. Dynamic Modules in Higher-Order Languages. In Proceedings of the IEEE Computer Society 1994
International Conference on Computer Languages, May 16-19, 1994, Toulouse, France, Henri E. Bal (Ed.). IEEE Computer
Society, 74–87. https://doi.org/10.1109/ICCL.1994.288391
Barry Jay. 2019. A simpler lambda calculus. In Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and
Program Manipulation, PEPM@POPL 2019, Cascais, Portugal, January 14-15, 2019, Manuel V. Hermenegildo and Atsushi
Igarashi (Eds.). ACM, 1–9. https://doi.org/10.1145/3294032.3294085
Gilles Kahn. 1987. Natural semantics. In Annual symposium on theoretical aspects of computer science. Springer, 22–39.
P. J. Landin. 1964. The Mechanical Evaluation of Expressions. Comput. J. 6, 4 (1964), 308–320. https://doi.org/10.1093/
COMJNL/6.4.308
Xavier Leroy and Hervé Grall. 2009. Coinductive big-step operational semantics. Inf. Comput. 207, 2 (2009), 284–304.
https://doi.org/10.1016/J.IC.2007.12.004
Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich. 2017. A Capability-Based Module System for
Authority Control. In ECOOP (LIPIcs, Vol. 74). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 20:1–20:27.
Adrian Mettler, David A. Wagner, and Tyler Close. 2010. Joe-E: A Security-Oriented Subset of Java. In Proceedings of the
Network and Distributed System Security Symposium, NDSS 2010, San Diego, California, USA, 28th February - 3rd March
2010. The Internet Society. https://www.ndss-symposium.org/ndss2010/joe-e-security-oriented-subset-javaMark Miller. 2006. Robust composition: Towards a unified approach to access control and concurrency control. Johns Hopkins
University.
Mark S. Miller, Chip Morningstar, and Bill Frantz. 2000. Capability-Based Financial Instruments. In Financial Cryptography,
4th International Conference, FC 2000 Anguilla, British West Indies, February 20-24, 2000, Proceedings (Lecture Notes in
Computer Science, Vol. 1962), Yair Frankel (Ed.). Springer, 349–378. https://doi.org/10.1007/3-540-45472-1_24
Mark S Miller, Mike Samuel, Ben Laurie, Ihab Awad, and Mike Stay. 2008. Safe active content in sanitized JavaScript. Google,Inc., Tech. Rep (2008).
Shin-ya Nishizaki. 1994. Simply Typed Lambda Calculus with First-Class Environments. Publications of the Research Institutefor Mathematical Sciences 30, 6 (1994), 1055–1121.
Frank Pfenning and Conal Elliott. 1988. Higher-Order Abstract Syntax. In Proceedings of the ACM SIGPLAN’88 Conference on
Programming Language Design and Implementation (PLDI), Atlanta, Georgia, USA, June 22-24, 1988, Richard L. Wexelblat(Ed.). ACM, 199–208. https://doi.org/10.1145/53990.54010
Brigitte Pientka and Andrew Cave. 2015. Inductive Beluga: Programming Proofs. In CADE (Lecture Notes in Computer
Science, Vol. 9195). Springer, 272–281.
Andrew M. Pitts. 2003. Nominal logic, a first order theory of names and binding. Inf. Comput. 186, 2 (2003), 165–193.
Christian Queinnec and David De Roure. 1996. Sharing Code through First-class Environments. In Proceedings of the 1996
ACM SIGPLAN International Conference on Functional Programming, ICFP 1996, Philadelphia, Pennsylvania, USA, May
24-26, 1996, Robert Harper and Richard L. Wexelblat (Eds.). ACM, 251–261. https://doi.org/10.1145/232627.232653
John C Reynolds. 1997. Design of the programming language Forsythe. In ALGOL-like languages. Birkhauser Boston Inc.,
173–233.
Tiark Rompf and Nada Amin. 2016. Type soundness for dependent object types (DOT). In Proceedings of the 2016 ACM
SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (Amsterdam,
Netherlands) (OOPSLA 2016). 624–641.
Masahiko Sato, Takafumi Sakurai, and Rod M. Burstall. 2001. Explicit Environments. Fundam. Informaticae 45, 1-2 (2001),
79–115. http://content.iospress.com/articles/fundamenta-informaticae/fi45-1-2-05
Masahiko Sato, Takafumi Sakurai, and Yukiyoshi Kameyama. 2002. A Simply Typed Context Calculus with First-class
Environments. J. Funct. Log. Program. 2002 (2002). http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/2002/S0201/JFLP-A02-04.pdf
Steven Schäfer, Tobias Tebbi, and Gert Smolka. 2015. Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions.
In Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings(Lecture Notes in Computer Science, Vol. 9236), Christian Urban and Xingyuan Zhang (Eds.). Springer, 359–374. https://doi.org/10.1007/978-3-319-22102-1_24
Jeremy Siek. 2013. Type safety in three easy lemmas. http://siek.blogspot.com/2013/05/type-safety-in-three-easylemmas.html
Kathrin Stark, Steven Schäfer, and Jonas Kaiser. 2019. Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector
substitutions. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP
2019, Cascais, Portugal, January 14-15, 2019, Assia Mahboubi and Magnus O. Myreen (Eds.). ACM, 166–180. https://doi.org/10.1145/3293880.3294101
William W. Tait. 1967. Intensional Interpretations of Functionals of Finite Type I. J. Symb. Log. 32, 2 (1967), 198–212.
https://doi.org/10.2307/2271658

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.

360:30

Jinhao Tan and Bruno C. d. S. Oliveira

Jinhao Tan and Bruno C. d. S. Oliveira. 2023. Dependent Merges and First-Class Environments. In 37th European Conference
on Object-Oriented Programming (ECOOP 2023) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 263), Karim
Ali and Guido Salvaneschi (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 34:1–34:32.
https://doi.org/10.4230/LIPIcs.ECOOP.2023.34
Jinhao Tan and Bruno C. d. S. Oliveira. 2024. A Case for First-Class Environments (Artifact). https://doi.org/10.5281/zenodo.
13370814
Christian Urban. 2008. Nominal Techniques in Isabelle/HOL. J. Autom. Reason. 40, 4 (2008), 327–356.
A.K. Wright and M. Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation 115, 1 (1994),
38–94.

Received 2024-04-06; accepted 2024-08-18

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 360. Publication date: October 2024.