higher-order functions, tail calls, conditionals, side effects,
exceptions, first-class continuations, and even garbage collection. Thus, we are able to refashion semantic techniques
used to model language features into abstract interpretation techniques for reasoning about the behavior of those
very same features.
Background and notation: We present a brief introduction to reduction semantics and abstract machines. For
background and a more extensive introduction to the concepts, terminology, and notation employed in this paper,
we refer the reader to Semantics Engineering with PLT Redex.
2. fRom semantiCs to maChines anD maChines
In this section, we demonstrate our systematic approach
to analysis by stepping through a derivation from the
high-level semantics of a prototypical higher-order programming language to a low-level abstract machine, and
from the abstract machine to a sound and computable
analytic model that predicts intensional properties of
that machine. As a prototypical language, we choose the
19 a core computational model
for both functional and object-oriented languages. We
choose to model program behavior with a simple operational model given in the form of a reduction semantics. Despite this simplicity, reduction semantics scale
to full-fledged programming languages,
22 although the
choice is somewhat arbitrary since it is known how to
construct abstract machines from a number of semantic paradigms.
5 In subsequent sections, we demonstrate
the approach handles richer language features such as
control, state, and garbage collection, and we have successfully employed the same method to statically reason
about language features such as laziness, exceptions, and
stack-inspection, and programming languages such as
2. 1. Reduction semantics
To begin, consider the following language of expressions:
e ∈ Exp = x | (ee) | (λ x . e)
x ∈ Var an infinite set of identiers.
The syntax of expressions includes variables, applications,
and functions. Values v, for the purposes of this language,
include only function terms, (λ x.e). We say x is the formal
parameter of the function (λ x.e), and e is its body. A program
is a closed expression, i.e., an expression in which every vari-
able occurs within some function that binds that variable as
its formal parameter. Call-by-value reduction is character-
ized by the relation v:
((λx.e)v) v [v/x]e,
which states that a function applied to a value reduces to
the body of the function with every occurrence of the formal
parameter replaced by the value. The expression on the left-hand side is a known as a redex and the right-hand side is its
Reduction can occur within a context of an evaluation
context, defined by the following grammar:
E = [ ] | (Ee) | (vE).
An evaluation context can be thought of as an expression with
a single “hole” in it, which is where a redex may be reduced.
It is straightforward to observe that for all programs, either
the program is a value, or it decomposes uniquely into an
evaluation context and redex, written E[( (λx.e)v)]. Thus the
grammar as given specifies a deterministic reduction strategy, which is formalized as a standard reduction relation on
E[e] av E[e¢], if e v e¢.
The evaluation of a program is defined by a partial function
relating programs to values (p. 67 of Felleisen et al.
eval(e) = v if e →v v, for some v,
where →v denotes the reflexive, transitive closure of the
standard reduction relation.
2. 2. CeK machine
The CEK machine (Interpreter III of Reynolds20) (p. 100
of Felleisen et al.
7) is a state transition system that efficiently performs evaluation of a program. There are two
key ideas in its construction, which can be carried out systematically.
2 The first is that substitution, which is not a
viable implementation strategy, is instead represented in a
delayed, explicit manner as an environment structure. So a
substitution [v/x]e is represented by e and an environment
that maps x to v. Since e and v may have previous substitutions applied, this will likewise be represented with environments. So in general, if r is the environment of e and
r′ is the environment of v, then we represent [v/x]e by e in
the environment r extended with a mapping of x to (v, r′),
written r[x a (v, r′)]. The pairing of a value and an environment is known as a closure.
The second key idea is that evaluation contexts are constructed inside-out and represent continuations: