Set-Based Analysis for Full Scheme and Its Use in Soft-Typing

Cormac Flanagan Matthias Felleisen

Rice COMP TR95-254

October 1995

Department of Computer Science Rice University P.O. Box 1892 Houston, TX 77251-1892

Copyright \begin{matrix}c \\ ◯ \end{matrix}1995 by

Cormac Flanagan and Matthias Felleisen

Set-Based Analysis for Full Scheme and Its Use in Soft-Typing

Cormac Flanagan^{∗} Matthias Felleisen^{∗}

Department of Computer Science, Rice University, Houston, TX 77251-1982

Abstract

Set-Based Analysis is an efficient and accurate program analysis for higher-order languages. It exploits an intuitive notion of approximation that treats program variables as sets of values. We present a new derivation of set-based analysis, based on a reduction semantics, that substantially simplifies previous formulations. Most importantly, the derivation easily extends from a functional core language to include imperative features such as assignments and first-class continuations, and supports the first correctness proof of set-based analysis for these imperative features. The paper includes an implementation of the derived analysis for a Scheme-like language, and describes a soft-typing algorithm that eliminates type-checks based on the information produced by the analysis.

∗Supported in part by NSF grant CCR 91-22518 and a sabbatical at Carnegie Mellon University.

Contents

1 Introduction 1

2 An Idealized Intermediate Language 2 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

3 Set-Based Analysis 5 3.1 Deriving Set Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.2 Soundness of the Set Constraints . . . . . . . . . . . . . . . . . . . . . . . . 9 3.3 From Set Constraints to Set-Based Analysis . . . . . . . . . . . . . . . . . . 13

4 Set-Based Analysis of Assignments 14 4.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 4.2 Set-Based Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

4.2.1 Deriving Set Constraints . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.2.2 Soundness of the Set Constraints . . . . . . . . . . . . . . . . . . . . 15

5 Set-Based Analysis of First-Class Continuations 15 5.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 5.2 Set-Based Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

5.2.1 Deriving Set Constraints . . . . . . . . . . . . . . . . . . . . . . . . . 17 5.2.2 Soundness of the Set Constraints . . . . . . . . . . . . . . . . . . . . 18

6 Application: Soft Typing from Set-Based Analysis 20 6.1 Soft Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 6.2 Non-Checking Primitives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 6.3 The Soft Typing Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

7 Related Work 22

8 Conclusion 24

A Set-Based Analysis Algorithm 25

1 Introduction

Advanced compiler optimizations heavily rely on static information about the values that program variables may assume. Computing such information for higher-order languages such as Scheme [2] and ML [16] is particularly complex, since a static control-flow graph of a program is not readily available at compile time [19, 22]. Heintze [10, 11] pioneered a set-based approach to program analysis that controls this complexity in two ways. First, the approach is based on a single notion of approximation that treats program variables as sets of values. Second, the approach splits the analysis into two phases: a specification phase and a solution phase. During the specification phase, the analysis derives constraints on the sets of values that program variables may assume. These constraints approximate the dataflow relationships of the analyzed program. During the solution phase, the analysis produces sets of values that satisfy these constraints. The result is a valid approximation of the value sets for the program variables.

In contrast to the simplicity of the analysis, Heintze’s derivation of set-based analysis is complex. The derivation of the specification phase involves a number of intermediate steps. Specifically, Heintze uses the “natural” semantics framework to define a set-based “natural” semantics, from which he reads off “safeness” conditions on set environments. He then shows how to derive set constraints from the set-based semantics and proves that a solution of these constraints is a safe set environment. The derivation of the solution phase is also complex. It involves solving constraints on the infinite sets of values that program variables may assume. Heintze represents these infinite sets using a restricted form of set constraints, which can be regarded as regular tree grammars, and his solution phase produces a regular tree grammar representation of the solution of the set constraints.

Not only is Heintze’s derivation complex, it is also limited to the analysis of purely functional languages. Extending it beyond a simple functional core is difficult, mostly due to the use of “natural” semantics, which cannot easily accommodate destructive data structure manipulations and non-local control operators. Although suitable set constraints for these imperative features can be produced in an ad-hoc manner, there is no semantic foundation for these constraints. Thus existing implementations of set-based analysis for languages like Scheme and ML [10, 11, 8, 7], which include assignments and non-local control operators, are not semantically well-founded.

We present a simpler derivation of set-based analysis than Heintze’s. It avoids the complexities and limitations outlined above, and explains the underlying notion of approximation in a clear manner. Our approach is based on a reduction semantics that explicitly models the allocation of objects in a global heap [5].^{1} We avoid Heintze’s intermediate steps by deriving our set constraints and proving their correctness directly from the reduction semantics. Our semantics also records sufficient information to associate each run-time value with the corresponding syntactic value in the source program. We exploit this information to express our set constraints in terms of finite sets of syntactic values in the source program, thus avoiding the need to reason about constraints on infinite sets of values.

Since our heap-based semantics represents values as general “graphs”, it is straightforward to extend both the semantics and the analysis to a language with assignments. Similarly, because the complete control state is available for each step of the evaluation, the extension to a language with non-local control constructs is also straightforward. Our derivation supports the first soundness proof of set-based analysis for a language containing these imperative features.

1Also see [17] for an application of this idea to model and verify garbage collection algorithms.

The presentation of our results proceeds as follows. The second section presents the syntax and semantics of a simple functional language, and the third section describes the setbased analysis of that language. The fourth and fifth sections shows how the analysis extends to assignments and first-class continuations, respectively. The sixth section describes an application of set-based analysis known as soft-typing, and Section 7 discusses related work. The appendix includes a simple implementation of the derived analysis for a Scheme-like language containing both assignments and first-class continuations.

2 An Idealized Intermediate Language

2.1 Syntax

Our motivation in performing program analyses is to produce information for the optimization phases of a compiler. Compilers typically convert source programs into a simple intermediate representation, and then proceed to analyze and optimize the intermediate representation of the program. Therefore, we formulate the analysis for an intermediate representation of an idealized functional language. Specifically, we use the subset of A-normal forms [9] of a λ-calculus-like language with a let construct and conditional expressions:^{2} see Figure 1. The language also includes the primitives cons, car, and cdr for list manipulation, which will serve to illustrate the treatment of primitive operations, and a basic constant nil denoting the empty list.

The key property of terms in A-normal form is that each intermediate value is explicitly named and that the order of execution follows the lexical nesting of let-expressions. The use of A-normal forms thus simplifies the formulation of the semantics and facilitates the compile-time analysis of programs since every intermediate value is named [20].

Values are either simple values or heap-allocated values. Simple values are either variables or locations. Locations do not occur in source programs; they are only created during program evaluation. Heap-allocated values include procedures (λx. M), pairs of values (cons v v) and basic constants. Procedures and let-expressions are binding constructs, and we assume that all binding constructs in a program introduce distinct variables. A variable occurrence is free if it is not bound by an enclosing binding construct, and a term is closed if it contains no free variables. We use Λ_{a}^{0} to denote the set of location-free, closed terms, or programs.

Notation We use the following notations throughout the paper: P_{fin} denotes the finitary power-set constructor; f : A ⟶ B denotes that f is a total function from A to B; and M ∈ P denotes that the term M occurs in the program P.

2Our language follows the Scheme and Lisp tradition of using conditional expressions instead of a patternmatching construct. The use of conditional expressions, predicates and selectors enables more opportunities for functional abstraction than the pattern matching approach, but imposes more work on the analysis phase.

Programs:

M, N ∈ Λ_{a}  ::= v  (Expressions)
| (let (x h) M)
| (let (x (car v)) M)
| (let (x (cdr v)) M)
| (let (x (if v M M)) M)
| (let (x (apply v v)) M)
| (let (x M) M)
v ∈ Sval ::= x | l  (Simple Values)
x ∈ Vars = {x, y, z, …} (Variables)
l ∈ Loc  (Locations)
h ∈ Hval ::= (λx. M) | (cons v v) | c  (Heap Values)
c ∈ Const =  {nil, …}  (Basic Constants)

Figure 1: The A-normalized Intermediate Language

2.2 Semantics

We define the semantics of programs via an abstract machine (see Figure 2) that explicitly models the allocation of objects into a global heap [17, 5]. A heap is a set of bindings from locations to heap values. The set Loc of locations contains an infinite subset Loc_{x} reserved for each variable x. The function new takes a heap and a variable x, and returns a new location from Loc_{x} that is not already allocated in the heap. The operation M[x ← l_{x}] denotes the substitution of the location l_{x} for all occurrences of x within M, and the operation h[x ← l_{x}] is defined analogously.

Each state of the machine consists of a heap and program term, except for the special state error. The machine evaluates programs by stepping through a sequence of states according to a set of transition rules. Each transition rule of the machine defines the semantics of a particular class of expressions. For example, the transition rule (car) evaluates expressions of the form (let (x (car l_{y})) M). If the heap value at location l_{y} is a pair, then the transition rule extracts the first component of that pair, stores that component at a new location l_{x} in the heap, and replaces all occurrences of x within M by l_{x}. Alternatively, if the heap value at location l_{y} is not a pair, then the transition rule (car) raises an error. Each of the remaining transition rules has a similar intuitive explanation.

The definition of these transition rules relies on the notion of an evaluation context. An evaluation context E is a term with a “hole” [ ] in place of the next subterm to be evaluated. For example, in the term (let (x M) N), the next expression to be evaluated lies within M, and thus the definition of evaluation contexts includes the clause (let (x E) M).

The evaluator eval is a function from programs to results. A result is either a basic constant, or one of the tags procedure or cons, indicating that the program returned an abstraction or a pair respectively, or the tag error, indicating that the program raised an error, or ⊥, indicating that the program diverges.

Set-Based Analysis for Full Scheme and Its Use in Soft-Typing 4

Evaluator:

eval : Λ_{a}^{0} ⟶ Const ∪ {procedure, cons, error, ⊥}
eval(P) = \{ \begin{matrix}c & if ⟨ ∅, P ⟩ ⟼^{∗} ⟨ H, l ⟩ and H(l) = c \\ procedure & if ⟨ ∅, P ⟩ ⟼^{∗} ⟨ H, l ⟩ and H(l) = (λx. M) \\ cons & if ⟨ ∅, P ⟩ ⟼^{∗} ⟨ H, l ⟩ and H(l) = (cons l_{1} l_{2}) \\ error & if ⟨ ∅, P ⟩ ⟼^{∗} error \\ ⊥ & if ∀i ∈ N ∃S_{i} such that ⟨ ∅, P ⟩ ⟼^{i} S_{i} \end{matrix}

Domains:

S ∈ State  ::= ⟨ H, M ⟩ | error  (States)
H ∈ Heap  ::= {l_{1} = h_{1}, …, l_{n} = h_{n}}  (Heaps)
l ∈ Loc  ::= ⋃_{x∈Vars} Loc_{x}  (Locations)
l_{x} ∈ Loc_{x}  (x-Locations)
E ∈ EvalCtxt ::= [ ] | (let (x E) M)  (Evaluation Contexts)

Transition Function: ⟨ H, E[ (let (x c) M) ] ⟩

⟼ ⟨ H ∪ {l_{x} = c}, E[ M[x ← l_{x}] ] ⟩  (bind-c)
where l_{x} = new(H, x)

⟨ H, E[ (let (x (λw. N)) M) ] ⟩

⟼ ⟨ H ∪ {l_{x} = (λw. N)}, E[ M[x ← l_{x}] ] ⟩  (bind-lam)
where l_{x} = new(H, x)

⟨ H, E[ (let (x (cons l_{y} l_{z})) M) ] ⟩

⟼ ⟨ H ∪ {l_{x} = (cons l′_{y} l′_{z}), l′_{y} = H(l_{y}), l′_{z} = H(l_{z})}, evcxtM[x ← l_{x}] ⟩  (bind-cons)
where l_{x} = new(H, x), l′_{y} = new(H, y), l′_{z} = new(H, z)

⟨ H, E[ (let (x (car l_{y})) M) ] ⟩

⟼ \{ \begin{matrix}⟨ H ∪ \{l_{x} = H(l_{z_{1}})\}, E[ M[x ← l_{x}] ] ⟩ & if H(l_{y}) = (cons l_{z_{1}} l_{z_{2}}) \\ where l_{x} = new(H, x) \\ error & if H(l_{y}) ≠ (cons l_{z_{1}} l_{z_{2}}) \end{matrix}  (car)

⟨ H, E[ (let (x (cdr l_{y})) M) ] ⟩

⟼ analogous to (car)  (cdr)

⟨ H, E[ (let (x (if l_{y} M_{1} M_{2})) M) ] ⟩

⟼ \{ \begin{matrix}⟨ H, E[ (let (x M_{1}) M) ] ⟩ & if H(l_{y}) ≠ nil \\ ⟨ H, E[ (let (x M_{2}) M) ] ⟩ & if H(l_{y}) = nil \end{matrix}  (if )

⟨ H, E[ (let (x (apply l_{y} l_{z})) M) ] ⟩

⟼ \{ \begin{matrix}⟨ H ∪ \{l_{w} = H(l_{z})\}, E[ (let (x N[w ← l_{w}]) M) ] ⟩ & if H(l_{y}) = (λw. N) \\ where l_{w} = new(H, w) \\ error & if H(l_{y}) ≠ (λw. N) \end{matrix} (apply)

⟨ H, E[ (let (x l_{y}) M) ] ⟩

⟼ ⟨ H ∪ {l_{x} = H(l_{y})}, E[ M[x ← l_{x}] ] ⟩  (bind-v)
where l_{x} = new(H, x)

Figure 2: The CS-Machine

3 Set-Based Analysis

The goal of set-based analysis is to produce information about the sets of values that program variables may assume during an execution. In general, the exact value set for each program variable is not computable, and therefore some notion of approximation is needed. Set-based analysis is based on an intuitive approximation that treats program variables as sets of values, and ignores the information regarding which specific value a variable represents at a given point in an execution. Since each value associated with a variable corresponds to a distinct location in our semantics, we express this notion of approximation by merging all locations allocated for each variable into a single abstract location. That is, we use each variable x as an abstract location representing all the locations in Loc_{x} that may be allocated for x. Thus, if P is the program being analyzed, then we use the set Vars_{P} of variables occurring in P as the set of abstract locations for the analysis of P.

We extend this notion of representation from variables to heap values as follows: Let Hval_{P} be the set of heap values that occur in the program P. Each heap value produced during the execution of P is obtained by substitution from a syntactic heap value in Hval_{P}. Therefore, we use each heap value h in Hval_{P} as an abstract value representing all substitution instances of h, i.e., all heap values obtained from h by substituting appropriate locations for the free variables of h. We call the resulting set of heap values the substitution closure of the heap value h. The substitution closure of a set of heap values is defined in a straightforward manner.

Definition 3.1. (Substitution Closure)

• For h ∈ Hval with F V [h] = {x_{1}, …, x_{n}}, the substitution closure of h is

Cl(h) = {h[x_{1} ← l_{x_{1}}, …, x_{n} ← l_{x_{n}}] | l_{x_{i}} ∈ Loc_{x_{i}}}

• For A ⊆ Hval, the substitution closure of A is

Cl(A) = ⋃_{h∈A} Cl(h)

Our analysis produces a finite table, called a set environment, that maps each program variable to a set of syntactic heap values from Hval_{P}. A set environment E is valid for the program P if, for each variable x, each heap value associated with x during an execution is in the substitution closure of E(x).

Definition 3.2. (Set environments, Validity) Let P be a program.

• A mapping E : Vars_{P} → P_{fin}(Hval_{P}) is a set environment for P.

• The relation P ⊧ E (read “P validates E”, or “E is valid for P ”) holds if ⟨ ∅, P ⟩ ⟼^{∗} ⟨ H, M ⟩ implies that H ⊧ E.

• The relation H ⊧ E holds if for all bindings (l_{x} = h) ∈ H, h ∈ Cl(E(x)).

We develop an analysis that produces valid set environments in two steps. To develop the specification phase of the analysis, we derive constraints on the sets of values that program variables may assume and prove the soundness of these constraints with respect to the abstract machine semantics. For the solution phase of the analysis we develop an algorithm that solves these constraints.

3.1 Deriving Set Constraints

Given a program P, a set constraint is of the form:

\frac{A_{P}}{B}

where A_{P} and B are statements concerning set environments, and A_{P} also depends on the program. A set environment E satisfies this constraint if whenever A holds for E and P, then B also holds for E. We show how, for each kind of term in P, the analysis must add certain constraints to the global set of program constraints:

• (let (x (λw. N)) M)

During execution, this source term will correspond to a run-time term (let (x (λw. N′)) M′), where N′ and M′ are substitution instances of N and M respectively. To record that x may be bound to a substitution instance of (λw. N), we require that E satisfies the following constraint:

\frac{(let (x (λw. N)) M) ∈ P}{(λw. N) ∈ E(x)}  (Cbind-lam^{P})

• (let (x (cons y z)) M)

During execution, this source term will correspond to a run-time term (let (x (cons l_{y} l_{z})) M′), where M′ is a substitution instance of M. To record that x may be bound to a heap value (cons l′_{y} l′_{z}), we require that E satisfies the following constraint:

\frac{(let (x (cons y z)) M) ∈ P}{(cons y z) ∈ E(x)}  (Cbind-lam^{P})

• (let (x h) M)

During execution, this source term will correspond to a run-time term (let (x h′) M′), where h′ and M′ are substitution instances of h and M respectively. To record that x may be bound to a substitution instance of h, we require that E satisfies the following constraint:

\frac{(let (x h) M) ∈ P}{h ∈ E(x)}  (Cbind-cons^{P})

• (let (x (car y)) M)

During execution, this term in the source program will correspond to the run-time term (let (x (car l_{y})) M′), where l_{y} is some location for y and M′ is a substitution instance of M. If the heap maps the location l_{y} to a pair (cons l_{z_{1}} l_{z_{2}}), then the evaluation of this expression will associate x with the heap value at location l_{z_{1}}. If we assume that E approximates the value sets of the program variables y and z_{1}, then E(y) includes (cons z_{1} z_{2}), and E(z_{1}) approximates the heap value at l_{z_{1}}. Therefore, we ensure that E accounts for the bindings created during the evaluation of this expression by demanding that E satisfies the following constraint:

\frac{(let (x (car y)) M) ∈ P  (cons z_{1} z_{2}) ∈ E(y)}{E(z_{1}) ⊆ E(x)}  (Ccar^{P})

No additional constraints are required for the error case, since whenever y does not denote a pair, an error state is immediately produced and no further bindings are created.

• (let (x (apply y z)) M)

Assume that E(y) includes (λw. N). Then the evaluation of this expression will associate the formal parameter w with one of the values of the argument variable z. Moreover, at the corresponding function return, the value of the “return” variable of the procedure may flow to the variable x. Thus, if FinalVar[ N ] is a function that determines the innermost (“result”) variable of N, then the crucial constraint for application expressions is as follows:

\frac{(let (x (apply y z)) M) ∈ P  (λw. N) ∈ E(y)}{E(z) ⊆ E(w)  E(FinalVar[ N ]) ⊆ E(x)}  (Capply^{P})

The definition of FinalVar is straightforward.

Definition 3.3. (FinalVar)

FinalVar : Λ_{a} ⟶ Vars
FinalVar[ x] = x
FinalVar[ (let (x ⋯) M) ] = FinalVar[ M ]

Examining each of the other classes of program terms in a similar manner results in a set of nine program-based set constraints: see Figure 3.

Set Constraints for a Sample Program To illustrate the derivation of set constraints, we consider the following program cons-it. The program defines a function cons-it that returns a cons-cell containing two copies of its argument, and the program then applies this function to the numbers 1 and 2, producing results pair_{1} and pair_{2} respectively, and finally returns the car of pair_{2}:

Set-Based Analysis for Full Scheme and Its Use in Soft-Typing 8

\frac{(let (x c) M) ∈ P}{c ∈ E(x)}  (Cbind-c^{P})

\frac{(let (x (λw. N)) M) ∈ P}{(λw. N) ∈ E(x)}  (Cbind-lam^{P})

\frac{(let (x (cons y z)) M) ∈ P}{(cons y z) ∈ E(x)}  (Cbind-cons^{P})

\frac{(let (x (car y)) M) ∈ P  (cons z_{1} z_{2}) ∈ E(y)}{E(z_{1}) ⊆ E(x)}  (Ccar^{P})

\frac{(let (x (cdr y)) M) ∈ P  (cons z_{1} z_{2}) ∈ E(y)}{E(z_{2}) ⊆ E(x)}  (Ccdr^{P})

\frac{(let (x (if y M_{1} M_{2})) M) ∈ P  h ∈ E(y)  h ≠ nil}{E(FinalVar[ M_{1} ]) ⊆ E(x)}  (Cif-true^{P})

\frac{(let (x (if y M_{1} M_{2})) M) ∈ P  nil ∈ E(y)}{E(FinalVar[ M_{2} ]) ⊆ E(x)}  (Cif-false^{P})

\frac{(let (x (apply y z)) M) ∈ P  (λw. N) ∈ E(y)}{E(z) ⊆ E(w)  E(FinalVar[ N ]) ⊆ E(x)}  (Capply^{P})

\frac{(let (x N) M) ∈ P}{E(FinalVar[ N ]) ⊆ E(x)}  (Cbind-v^{P})

Figure 3: Set Constraints on E with respect to P.

(let (cons-it (λx. (let (r (cons x x)) r)))

(let (t_{1} 1)

(let (pair_{1} (cons-it t_{1}))
(let (t_{2} 2)
(let (pair_{2} (cons-it t_{2}))

(let (a (car pair_{2})) a))))))

Instantiating the set constraints for this program produces the following constraints:

From Cbind-lam^{P}:  (λx. (let (r (cons x x)) r)) ∈ E(cons-it)  (1)
From Cbind-cons^{P}:  (cons x x) ∈ E(r)  (2)
From Cbind-c^{P} :  1 ∈ E(t_{1})  (3)
From Cbind-c^{P} :  2 ∈ E(t_{2})  (4)
From Capply^{P} :  \frac{(λw. N) ∈ E(cons-it)}{E(t_{1}) ⊆ E(w)  E(FinalVar[ N ]) ⊆ E(pair_{1})}  (5)
From Capply^{P} :  \frac{(λw. N) ∈ E(cons-it)}{E(t_{2}) ⊆ E(w)  E(FinalVar[ N ]) ⊆ E(funpair_{2})}  (6)
From Ccar^{P} :  \frac{(cons z_{1} z_{2}) ∈ E(pair_{2})}{E(z_{1}) ⊆ E(a)}  (7)

Constraints (1) through (4) are atomic constraints, and we satisfy these constraints by simply adding the appropriate bindings to E. To satisfy the inference constraints (5) through (7), we extend E as required by these constraints.

From (1), (3), (5) :  1 ∈ E(x)  (8)
From (1), (2), (5) :  (cons x x) ∈ E(pair_{1})  (9)
From (1), (4), (6) :  2 ∈ E(x)  (10)
From (1), (2), (6) :  (cons x x) ∈ E(pair_{2})  (11)
From (7), (8), (11) :  1 ∈ E(a)  (12)
From (7), (10), (11) :  2 ∈ E(a)  (13)

At this stage E is the set environment:

E(cons-it) = {(λx. (let (r (cons x x)) r))}
E(r) = {(cons x x)}
E(pair_{1}) = {(cons x x)}
E(pair_{2}) = {(cons x x)}

E(t_{1}) = {1}_{E(t_{2}) = {2}}_{E(x) = {1, 2}}_{E(a) = {1, 2}}

A quick examination of the set constraints shows that this set environment satisfies the constraints for the program cons-it. Furthermore, since each binding in E is required by these constraints, E is the smallest set environment satisfying the set constraints. Of course, E does not represent the exact set of variable bindings created during an execution. For example, the variable a only gets bound to the constant 1 during an execution, but according to E, the set of possible heap-values of a also includes the constant 2.

3.2 Soundness of the Set Constraints

Proving the soundness of the derived constraints requires showing that if a set environment E satisfies the set constraints for a given program P, then E must be valid for P.

Assume that E satisfies the set constraints relative to P. To prove that E is valid for P, we need to show that for any n, ⟨ ∅, P ⟩ ⟼^{n} ⟨ H, M ⟩ implies that H ⊧ E. The natural approach is to proceed by induction on n. However, as part of the proof, we will need to consider intermediate transitions from states other than ⟨ ∅, P ⟩. Therefore, we strengthen the induction hypothesis to:

S ⊧_{P} E and S ⟼ S′ implies S′ ⊧_{P} E

where the invariant relation S ⊧_{P} E (read “S validates E with respect to P ”) is an appropriately chosen relation that supports the proof of the induction hypothesis.^{3} We say that the relation S ⊧_{P} E holds for S = ⟨ H, M ⟩ if and only if H ⊧ E (see Definition 3.2) and M ⊧_{P} E. The new relation M ⊧_{P} E (read “M validates E with respect to P ”) requires that M is either derived via substitution from a term in P, or that M is a let-expression (let (x N) L) whose sub-terms satisfy the same relation, and that the set environment E accounts for the potential binding of x to the values FinalVar[ N ] can assume.

Definition 3.4. (Substitution Closure of a Term, M ⊧_{P} E, FinalVar, S ⊧_{P} E)

• For M ∈ Λ_{a}, the substitution closure of M is

Cl(M) = {M[x_{1} ← l_{x_{1}}, …, x_{n} ← l_{x_{n}}] | {x_{1}, …, x_{n}} ⊆ F V [M] and l_{x_{i}} ∈ Loc_{x_{i}}}

• M ⊧_{P} E holds if either:

1. M ∈ Cl(N) for some N ∈ P, or

2. M = (let (x N) L), N ⊧_{P} E, L ⊧_{P} E and E(FinalVar[ N ]) ⊆ E(x).

• The definition of FinalVar is extended to run-time terms (which may contain locations) as follows:

FinalVar : Λ_{a} ⟶ Vars
FinalVar[ x] = x
FinalVar[ l_{x}] = x
FinalVar[ (let (x ⋯) M) ] = FinalVar[ M ]

• S ⊧_{P} E holds if either:

1. S = ⟨ H, M ⟩, H ⊧ E and M ⊧_{P} E, or

       2. S = error.

Our chosen invariant relation supports the proof of the induction hypothesis: if the invariant holds for a given state S, then the invariant also holds for the successor of S.

Lemma 3.5 If S ⊧_{P} E, S⟼S′ and E satisfies the constraints relative to P, then S′ ⊧_{P} E.

Proof: By case analysis of the transition rule used for S ⟼ S′.

3The relation S ⊧_{P} E corresponds to the concretization function γ used in abstract interpretation.

• Suppose S ⟼ S′ via the transition rule (bind-lam). Then:

\begin{aligned}S & = & ⟨ H, E[ (let (x (λw. N)) M) ] ⟩ \\ S′ & = & ⟨ H ∪ \{l_{x} = (λw. N)\}, E[ M[x ← l_{x}] ] ⟩ \end{aligned}

By Lemma 3.6(1), (let (x (λw. N)) M) ⊧_{P} E. Since a lambda-expression is not a term, Definition 3.4 implies that (let (x (λw. N)) M) is a substitution instance of some term (let (x (λw. N′)) M′) in P, where N ∈ Cl(N′) and M ∈ Cl(M′). Constraint (Cbind-lam^{P}) implies that (λw. N′) ∈ E(x). Therefore (λw. N) ∈ Cl(E(x)) and H ∪ {l_{x} = (λw. N)} ⊧ E. From M ∈ Cl(M′) we know that M[x ← l_{x}] ∈ Cl(M′) and therefore M[x ← l_{x}] ⊧_{P} E. Also:

FinalVar[ (let (x (λw. N)) M) ] = FinalVar[ M ] = FinalVar[ M[x ← l_{x}] ]

by Lemma 3.6(3). Hence, by Lemma 3.6(2), E[ M[x ← l_{x}] ] ⊧_{P} E. Thus S′ ⊧_{P} E, and the claim holds for this case.

• The case where S ⟼ S′ via the transition rule (bind-c) holds by a similar argument.

• Suppose S ⟼ S′ via the transition rule (bind-cons). Then:

S = ⟨ H, E[ (let (x (cons l_{y} l_{z})) M) ] ⟩
S′ = ⟨ H ∪ {l_{x} = (cons l′_{y} l′_{z})}, E[ M[x ← l_{x}] ] ⟩

By Lemma 3.6(1), (let (x (cons l_{y} l_{z})) M) ⊧_{P} E. Definition 3.4 implies that (let (x (cons l_{y} l_{z})) M) is a substitution instance of some term (let (x (cons y z)) M′) in P, where M ∈ Cl(M′). Constraint (Cbind-cons^{P}) implies that (cons y z) ∈ E(x). Therefore (cons l′_{y} l′_{z}) ∈ Cl(E(x)) and H ∪ {l_{x} = (cons l′_{y} l′_{z})} ⊧ E. Also, E[ M[x ← l_{x}] ] ⊧_{P} E by the same reasoning as for the previous case. Hence S′ ⊧_{P} E.

• Suppose S ⟼ S′ via the transition rule (car). Then S is the state:

S = ⟨ H, E[ (let (x (car l_{y})) M) ] ⟩

If H(l_{y}) is not a pair, then S′ = error and the claim trivially holds. Next, consider the case where H(l_{y}) is the pair (cons l_{z_{1}} l_{z_{2}}). Then:

S′ = ⟨ H ∪ {l_{x} = H(l_{z_{1}})}, E[ M[x ← l_{x}] ] ⟩

Since H ⊧ E, H(l_{y}) ∈ Cl(E(y)), and thus (cons z_{1} z_{2}) ∈ E(y). By Lemma 3.6(1), (let (x (car l_{y})) M) ⊧_{P} E, and therefore Definition 3.4 implies that (let (x (car l_{y})) M) is a substitution instance of some term (let (x (car y)) M′) in P, where M ∈ Cl(M′). Constraint (Ccar^{P}) implies that E(z_{1}) ⊆ E(x), and therefore H(l_{z_{1}}) ∈ Cl(E(z_{1})) ⊆ Cl(E(x)). Thus H ∪ {l_{x} = H(l_{z_{1}})} ⊧ E. Also, E[ M[x ← l_{x}] ] ⊧_{P} E by the same reasoning as for the previous case. Hence S′ ⊧_{P} E.

• The case where S ⟼ S′ via the transition rule (cdr) holds by a similar argument.

• Suppose S ⟼ S′ via the transition rule (if ). Then S is the state:

⟨ H, E[ (let (x (if l_{y} M_{1} M_{2})) M) ] ⟩

Assume first that H(l_{y}) ≠ nil. Then:

S′ = ⟨ H, E[ (let (x M_{1}) M) ] ⟩

Since S ⊧_{P} E, there exists h ∈ E(y) with h ≠ nil. By Lemma 3.6(1), (let (x (if l_{y} M_{1} M_{2})) M) ⊧_{P} E, and therefore Definition 3.4 implies that the term (let (x (if l_{y} M_{1} M_{2})) M) is a substitution instance of some term (let (x (if y M′_{1} M′_{2})) M′) in P, where M_{1} ∈ Cl(M′_{1}) and M ∈ Cl(M′). By constraint (Cif-true^{P}), E(FinalVar[ M′_{1} ]) ⊆ E(x) and hence By Lemma 3.6(4), E(FinalVar[ M_{1} ]) ⊆ E(x). Thus (let (x M_{1}) M) ⊧_{P} E, and S′ ⊧_{P} E. The case where H(l_{y}) = nil holds by a similar argument.

• Suppose S ⟼ S′ via the transition rule (apply). Then S is the state:

S = ⟨ H, E[ (let (x (apply l_{y} l_{z})) M) ] ⟩

Assume first that H(l_{y}) = (λw. N). Then:

S′ = ⟨ H ∪ {l_{w} = H(l_{z})}, E[ (let (x N[w ← l_{w}]) M) ] ⟩

Since H ⊧ E, H(l_{y}) ∈ Cl(E(y)) and thus (λw. N′) ∈ E(y) with N ∈ Cl(N′). By Lemma 3.6(1), (let (x (apply l_{y} l_{z})) M) ⊧_{P} E, which implies that there exists (let (x (apply y z)) M′) ∈ P with M ∈ Cl(M′). By constraint (Capply^{P}), E(z) ⊆ E(w) and E(FinalVar[ N′]) ⊆ E(x). Hence H(l_{z}) ∈ Cl(E(w)) and thus H ∪ {l_{w} = H(l_{z})} ⊧ E. Furthermore, by Lemma 3.6(4), FinalVar[ N′] = FinalVar[ N ]. Hence E(FinalVar[ N ]) ⊆ E(x), which implies that (let (x N[w ← l_{w}]) M) ⊧_{P} E. Thus S′ ⊧_{P} E. If H(l_{y}) is not a procedure, then S′ = error and the claim trivially holds.

• Suppose S ⟼ S′ via the transition rule (bind-v). Then:

\begin{aligned}S & = & ⟨ H, E[ (let (x l_{y}) M) ] ⟩ \\ S′ & = & ⟨ H ∪ \{l_{x} = H(l_{y})\}, E[ M[x ← l_{x}] ] ⟩ \end{aligned}

By Lemma 3.6(1), (let (x l_{y}) M) ⊧_{P} E. By Definition 3.4, either E(y) = E(FinalVar[ l_{y}]) ⊆ E(x), or else (let (x y) M′) ∈ P, in which case by constraint (Cbind-v^{P}), we also have that E(y) ⊆ E(x). Since H(l_{y}) ∈ Cl(E(y)) ⊆ Cl(E(x)), H ∪ {l_{x} = H(l_{y})} ⊧ E. Therefore, S′ ⊧_{P} E.

The previous proof depends on the following lemma.

Lemma 3.6

1. If E[ M ] ⊧_{P} E then M ⊧_{P} E.

2. Suppose E[ M ] ⊧_{P} E and E satisfies the constraints relative to P. Then for all M′ such that M′ ⊧_{P} E and FinalVar[ M′] = FinalVar[ M ], we have that E[ M′ ] ⊧_{P} E.

3. For N ∈ Λ_{a}, FinalVar[ N ] = FinalVar[ N[x ← l_{x}] ].

4. If N ∈ Cl(N′), then FinalVar[ N ] = FinalVar[ N′].

Proof: The first two claims can be proven by induction on the structure of E; the third follows by induction on the structure of N. Claim 4 is a consequence of claim 3.

Since the invariant trivially holds for the initial state ⟨ ∅, P ⟩, it follows that the set constraints are sound, i.e., if E satisfies the set constraints relative to P, then E is a valid set environment for P.

Theorem 3.7 (Soundness of Constraints) If E satisfies the constraints relative to P, then P ⊧ E.

Proof: Suppose E satisfies the constraints relative to P, and that

⟨ ∅, P ⟩ ⟼^{∗} ⟨ H, M ⟩

By the definition of the invariant relation, ⟨ ∅, P ⟩ ⊧_{P} E. Therefore Lemma 3.5 implies that ⟨ H, M ⟩ ⊧_{P} E, which implies by definition that H ⊧ E. The latter is true for any state derivable from the initial state, hence P ⊧ E.

In summary, any set environment satisfying the set constraints with respect to a program P is a conservative approximation to the set of bindings created during the execution of P.

3.3 From Set Constraints to Set-Based Analysis

The class of set environments for a given program P, denoted SetEnv_{P}, forms a complete lattice under the natural pointwise partial ordering ⊑ defined by:

E_{1} ⊑ E_{2} if and only if ∀x ∈ Vars_{P} . E_{1}(x) ⊆ E_{2}(x)

The least set environment ⊥_{E} in the lattice is the trivial mapping: ⊥_{E}(x) = ∅. The size of the sets Vars_{P} and Hval_{P} is bounded by |P |, where |P | denotes the number of expressions in P. Therefore, the height of the lattice SetEnv_{P} is bounded by |P |^{2}.

Each set constraint Cx^{P} (where x ranges over bind-c, car, …, bind-v) can be interpreted as a monotonic function, also denoted by Cx^{P}, on this lattice. We define the function C_{P} to be the least upper bound of the functions Cbind-c^{P}, …, Cbind-v^{P}:

C_{P} : SetEnv_{P} ⟶ SetEnv_{P}
C_{P} (E) = Cbind-c^{P}(E) ⊔ ⋯ ⊔ Cbind-v^{P}(E)

Since the combined function C_{P} is also monotonic, the least fixpoint given by ⨆_{n∈N} C_{P}^{n}(⊥_{E}) exists. Moreover, since the height of the lattice is bounded by |P |^{2}, this fixpoint is reached within |P |^{2} steps. We define set-based analysis as the function that returns this least fixpoint.

Definition 3.8. (sba) The function sba : Λ_{a} ⟶ SetEnv_{P} is given by:

sba(P) = ⨆_{n≤|P |^{2}} C_{P}^{n}(⊥_{E})

Since the fixpoints of C_{P} are exactly the solutions to the set constraints, it follows that sba(P) is the least solution to the set constraints, and hence that sba(P) is a valid set environment for P.

Theorem 3.9 (Correctness of Set-Based Analysis) P ⊧ sba(P)

Proof: Since sba(P) is a solution to the set constraints, it follows by Theorem 3.7 that P ⊧ sba(P).

Appendix A contains a complete algorithm that calculates the set-based analysis of a program by generating and solving set constraints for that program.

4 Set-Based Analysis of Assignments

Realistic programming languages such as Scheme or ML provide a variety of imperative facilities in addition to a functional core language. These imperative constructs typically include destructive assignments and non-local control operators. In this section, we consider how to extend set-based analysis to a language with assignments. The following section deals with first-class continuations.

Let Λ_{a}^{!} be the extension of Λ_{a} with assignments:

M ∈ Λ_{a}^{!} ::= … | (let (x (set! v v)) M)

The evaluation of an assignment expression (let (x (set! y z)) M) assigns y to the value of z, and also binds x to this value, before continuing with the evaluation of M.

4.1 Semantics

We define the semantics of Λ_{a}^{!} by extending the CS-machine with an additional transition rule for assignment expressions:

⟨ H ∪ {l_{y} = h_{y}}, E[ (let (x (set! l_{y} l_{z})) M) ] ⟩

⟼ ⟨ H ∪ {l_{y} = h_{z}, l_{x} = h_{z}}, E[ M[x ← l_{x}] ] ⟩  (set!)
where h_{z} = H(l_{z}) and l_{x} = new(H ∪ {l_{y} = h_{y}}, x)

The evaluator for the extended language is defined in the usual manner (cmp. Figure 2).

4.2 Set-Based Analysis

4.2.1 Deriving Set Constraints

The derivation of a set-based analysis for Λ_{a}^{!} follows the development of Section 3. It yields one additional constraint, which accounts for the effect of assignment expressions. The new constraint states that for each expression of the form (let (x (set! y z)) M) ∈ P in the analyzed program, the values of z may flow to both x and y:

\frac{(let (x (set! y z)) M) ∈ P}{E(z) ⊆ E(y)  E(z) ⊆ E(x)}  (Cset!^{P})

4.2.2 Soundness of the Set Constraints

We prove the soundness of the set constraints for Λ_{a}^{!} by showing that every transition step preserves the invariant relation S ⊧_{P} E from Definition 3.4, which is naturally extended to Λ_{a}^{!}.

Lemma 4.1 If S ⊧_{P} E, S⟼S′ and E satisfies the constraints relative to P, then S′ ⊧_{P} E.

Proof:

By case analysis of the transition rule used for S ⟼ S′. The only case we need to consider concerns assignments, since all the other cases are analyzed in Lemma 3.5, and can be adopted without change.

Suppose S ⟼ S′ via the transition rule (set!). Then:

\begin{aligned}S & = & ⟨ H ∪ \{l_{y} = h_{y}\}, E[ (let (x (set! l_{y} l_{z})) M) ] ⟩ \\ S′ & = & ⟨ H ∪ \{l_{y} = h_{z}, l_{x} = h_{z}\}, E[ M[x ← l_{x}] ] ⟩ \end{aligned}

where h_{z} = H(l_{z}).

A straightforward adaptation of Lemma 3.6 to the language Λ_{a}^{!} implies that (let (x (set! l_{y} l_{z})) M) ⊧_{P} E. Therefore, this term is a substitution instance of some term (let (x (set! y z)) M′) in P, where M ∈ Cl(M′). From constraint (Cset!^{P}), E(z) ⊆ E(y) and E(z) ⊆ E(x). Hence h_{z} ∈ Cl(E(y)) and h_{z} ∈ Cl(E(x)), which implies that H ∪ {l_{y} = h_{z}, l_{x} = h_{z}} ⊧ E.

Furthermore, M ∈ Cl(M′) implies that M[x ← l_{x}] ∈ Cl(M′), and therefore E[ M[x ← l_{x}] ] ⊧_{P} E. Hence S′ ⊧_{P} E, and the claim holds for this case.

The rest of the verification of set-based analysis for Λ_{a}^{!} is adapted mutatis mutandis, which illustrates the flexibility of our semantic framework.

5 Set-Based Analysis of First-Class Continuations

In this section we extend our derivation of set-based analysis to a language that contains first-class continuations in addition to assignments and the functional core language^{4}. Let Λ_{a}^{!+c} be the following extension of Λ_{a}^{!}:

4Assignments and first-class continuations can be added in any order, or independently, to the functional core language.

M ∈ Λ_{a}^{!+c} ::= … | (let (x (letcc y N)) M)

The evaluation of a letcc-expression (letcc y N) captures the current evaluation context (or continuation) surrounding that expression, binds y to a location containing this continuation, and continues with the evaluation of N. An invocation of a captured continuation causes the current evaluation context to be discarded and replaced by the captured continuation.

5.1 Semantics

We define the semantics of Λ_{a}^{!+c} by appropriately extending the CS-machine. A continuation is a non-empty evaluation context, and we store captured continuations in the heap. Thus heaps bind locations to continuations in addition to binding locations to heap values:^{5}

H ∈ Heap ::= {l_{1} = h_{1}, …, l_{n} = h_{n}, l′_{1} = E_{1}, …, l′_{m} = E_{m}}
where E_{i} ≠ [ ]

We extend the CS-machine with an additional transition rule for capturing continuations, and modify the transition rule (apply) to correctly apply continuations as well as procedures: see Figure 4.

⟨ H, E[ (let (x (letcc y N)) M) ] ⟩

⟼ ⟨ H ∪ {l_{y} = E[ (let (x [ ]) M) ]}, E[ (let (x N[y ← l_{y}]) M) ] ⟩  (letcc)
where l_{y} = new(H, y)

⟨ H, E[ (let (x (apply l_{y} l_{z})) M) ] ⟩

⟼ \{ \begin{matrix}⟨ H ∪ \{l_{w} = H(l_{z})\}, E[ (let (x N[w ← l_{w}]) M) ] ⟩ & if H(l_{y}) = (λw. N) \\ where l_{w} = new(H, w) \\ ⟨ H ∪ \{l_{w} = H(l_{z})\}, E′[ N[w ← l_{w}] ] ⟩ & if H(l_{y}) = E′[ (let (w [ ]) N) ] \\ where l_{w} = new(H, w) \\ error & otherwise \end{matrix} (apply)

Figure 4: Additional Transition Rules for First-Class Continuations

The evaluator for the extended language is defined in the usual manner (cmp. Figure 2). If the evaluation of a program returns a captured continuation, then the extended evaluator simply returns the tag procedure.

5.2 Set-Based Analysis

The analysis of the language Λ_{a}^{!+c} requires an extended notion of set environments, since a heap now maps locations to both heap values and continuations. As before, we use elements of Hval_{P} to represent heap values, and we need to choose a finite set of abstract continuations to represent the continuations that may be captured during an execution. For set-based analysis, the crucial property of a continuation E[ (let (y [ ]) M) ] is that the variable y receives the argument value passed to the continuation. Therefore, we use the abstract continuation (cont y) to represent all continuations of the form E[ (let (y [ ]) M) ]. Let Cont_{P} denote the set {(cont y) | y ∈ Vars_{P} } of abstract continuations used for the analysis of the program P. A set environment is now a finite table that maps each program variable to a subset of Hval_{P} ∪ Cont_{P}. A set environment E is valid for P if for each heap value h associated with a variable x during an execution, h ∈ Cl(E(x)), and for each continuation E[ (let (y [ ]) M) ] associated with x during an execution, (cont y) ∈ E(x).

5For technical reasons that will become clear soon, we do not include continuations in the set of heap values.

Definition 5.1. (Cont_{P}, Set environments, Validity, H ⊧ E) Let P be a program.

• Cont_{P} = {(cont y) | y ∈ Vars_{P} }.

• A mapping E : Vars_{P} → P_{fin}(Hval_{P} ∪ Cont_{P}) is a set environment for P.

• A set environment E is valid for P if ⟨ ∅, P ⟩ ⟼^{∗} ⟨ H, M ⟩ implies that H ⊧ E.

• The relation H ⊧ E (read “H validates E”) holds if and only if:

– for all bindings (l_{x} = h) ∈ H, h ∈ Cl(E(x)), and

– for all bindings (l_{x} = E[ (let (y [ ]) M) ]) ∈ H, (cont y) ∈ E(x).

5.2.1 Deriving Set Constraints

The set constraints for Λ_{a}^{!+c} extend those for Λ_{a}^{!}. The additional constraints ensure that the set environment E accounts for the bindings created during the capture and invocation of continuations.

• (let (y (letcc x N)) M)

The evaluation of this expression during an execution captures some run-time evaluation context E[ (let (y [ ]) M) ] surrounding the letcc-expression, and binds x to this continuation. In addition, if the evaluation of N terminates, the value of the “return” variable of N may flow to the variable y. Thus, the crucial constraint for letcc expressions is as follows:

\frac{(let (y (letcc x N)) M) ∈ P}{(cont y) ∈ E(x)  E(FinalVar[ N ]) ⊆ E(y)}  (Cletcc^{P})

• (let (x (apply y z)) M)

Suppose that E(y) includes (cont w). Then, the variable y may denote a continuation of the form E[ (let (w [ ]) N) ] during an execution, and the evaluation of this application expression may pass the value of the argument variable z to the variable w. To ensure that the set environment E accounts for bindings created by such transitions, we require that E satisfies the following constraint:

\frac{(let (x (apply y z)) M) ∈ P  (cont w) ∈ E(y)}{E(z) ⊆ E(w)}  (Capply-k^{P})

Because continuations never return, no constraints concerning E are required for the return case.

5.2.2 Soundness of the Set Constraints

Proving the soundness of the set constraints for the extended language Λ_{a}^{!+c} requires showing that if a set environment E satisfies the set constraints for a given program P, then E must be valid for P. As before, the proof proceeds based on an induction hypothesis:

S ⊧_{P} E and S ⟼ S′ implies S′ ⊧_{P} E

where S ⊧_{P} E is an appropriately chosen invariant relation. For the analysis of the language Λ_{a}^{!+c}, we need to strengthen the invariant relation previously used for both Λ_{a} and Λ_{a}^{!}. The strengthened invariant relation ensures that only “proper” continuations are stored in the heap.

Definition 5.2. (H ⊧_{P} E, E ⊧_{P} E, S ⊧_{P} E)

• H ⊧_{P} E holds if H ⊧ E and for all (l_{x} = E) ∈ H, E ⊧_{P} E.

• E ⊧_{P} E holds for E = (let (x E′) L) if L ⊧_{P} E and either:

– E′ = [ ], or

– E′ ⊧_{P} E and E(FinalVar[ E′]) ⊆ E(x).

• S ⊧_{P} E holds if either:

1. S = ⟨ H, M ⟩, H ⊧_{P} E and M ⊧_{P} E, or

       2. S = error.

Our chosen invariant relation supports the proof of the induction hypothesis: if the invariant holds for a given state S, then the invariant also holds for the successor of S.

Lemma 5.3 If S ⊧_{P} E, S⟼S′ and E satisfies the constraints relative to P, then S′ ⊧_{P} E.

Proof: By case analysis of the rule used for S ⟼ S′. The only cases we need to consider concern continuation capture and invocation, since the other cases hold by the arguments used in Lemma 3.5 or Lemma 4.1, and can be adopted without change.

• Suppose S ⟼ S′ via the transition rule (letcc). Then:

S = ⟨ H, E[ (let (x (letcc y N)) M) ] ⟩
S′ = ⟨ H′, E[ (let (x N[y ← l_{y}]) M) ] ⟩

where H′ = H ∪ {l_{y} = E[ (let (x [ ]) M) ]}. Lemma 3.6(1) implies that (let (x (letcc y N)) M) ⊧_{P} E. Therefore, the term (let (x (letcc y N)) M) is a substitution instance of some term (let (x (letcc y N′)) M′) in P, where N ∈ Cl(N′) and M ∈ Cl(M′). By the constraint (Cletcc^{P}), (cont x) ∈ E(y), which implies that H′ ⊧ E. By Lemma 5.4, E[ (let (x [ ]) M) ] ⊧_{P} E, and hence H′ ⊧_{P} E. The constraint (Cletcc^{P}) also implies that E(FinalVar[ N′]) ⊆ E(x), and therefore by Lemma 3.6, parts 3 and 4, E(FinalVar[ N[y ← l_{y}] ]) ⊆ E(x). Hence (let (x N[y ← l_{y}]) M) ⊧_{P} E, S′ ⊧_{P} E, and the claim holds for this case.

• Suppose S ⟼ S′ via the transition rule (apply). Then S is the state:

⟨ H, E[ (let (x (apply l_{y} l_{z})) M) ] ⟩

Assume that H(l_{y}) = E′[ (let (w [ ]) N) ]. Then:

S′ = ⟨ H ∪ {l_{w} = H(l_{z})}, E′[ N[w ← l_{w}] ] ⟩

Since H ⊧ E, we know that (cont w) ∈ E(y). Lemma 3.6(1) implies that (let (x (apply l_{y} l_{z})) M) ⊧_{P} E, and hence (let (x (apply l_{y} l_{z})) M) is a substitution instance of some term (let (x (apply y z)) M′) ∈ P, where M ∈ Cl(M′). By constraint (Capply-k^{P}), E(z) ⊆ E(w). Thus H(l_{z}) ∈ Cl(E(w)) and H ∪ {l_{w} = H(l_{z})} ⊧ E. Furthermore, since E′[ (let (w [ ]) N) ] ⊧_{P} E, by Lemma 5.4 we have that E′[ N[w ← l_{w}] ] ⊧_{P} E. Hence S′ ⊧_{P} E, and the claim holds for this case.

The previous proof depends on the following lemma, and on a straightforward extension of Lemma 3.6 to Λ_{a}^{!+c}.

Lemma 5.4

1. If E[ (let (x (letcc y N)) M) ] ⊧_{P} E, then E[ (let (x [ ]) M) ] ⊧_{P} E.

2. If E′[ (let (w [ ]) N) ] ⊧_{P} E, then E′[ N[w ← l_{w}] ] ⊧_{P} E.

Proof: The proof of both parts proceeds by induction on the structure of E.

Theorem 5.5 (Soundness of Constraints for Λ_{a}^{!+c}) For P ∈ Λ_{a}^{!+c}, if E satisfies the constraints relative to P, then P ⊧ E.

Proof: Follows from Lemma 5.3, based on the argument used in Theorem 3.7.

The rest of the verification of set-based analysis is again straightforward.

6 Application: Soft Typing from Set-Based Analysis

The information produced by set-based analysis facilitates a variety of optimizations. Examples include partial evaluation [15], escape analysis [18], redundant test elimination [11], closure analysis [21], touch-optimization [8, 7], dead-code elimination, constant-folding and code hoisting. Here, we illustrate how set-based analysis applies to soft typing [4, 28, 1, 12, 14].

6.1 Soft Typing

The programming language Scheme [2] is a dynamically-typed language, which imposes no restrictions on the values that variables or expressions in a program may assume. Dynamictyping leads to a simple and flexible language suitable for rapid software development, but does not provide any compile-time guarantee that primitive operations are only applied to arguments of the appropriate type. Instead, each primitive operation typically performs a type-check on its arguments at run-time to ensure that they are of the appropriate type. Thus, for example, the operation car must first check that its argument is a pair, before it can extract the first component of that pair. Performing these type-checks can add a significant overhead to the execution time. For example, Wright [25:p. 105] reports that this cost is 22% of the execution time under Chez Scheme at optimize-level 2. Since Chez Scheme eliminates some run-time checks at optimize-level 2, a naïve compiler would spend an even greater fraction of the execution time performing these type-checks.

One of the goals^{6} of soft-typing is to reduce the overhead of dynamic typing by removing unnecessary type-checks wherever provably possible, without changing the semantics of programs. In this section, we develop a soft-typing algorithm that exploits the information produced by set based analysis for this purpose.

6.2 Non-Checking Primitives

The current language does not provide primitives that do not perform type-checks on their arguments. To express and verify a soft-typing algorithm that replaces the type-checking primitives car, cdr and apply by non-checking primitives, we extend the language Λ_{a}^{!+c} with non-checking forms of the type-checking primitive operations, denoted \underline{car}, \underline{cdr} and \underline{apply}, respectively:

M ::= …
| (let (x (\underline{car} y)) M)
| (let (x (\underline{cdr} y)) M)
| (let (x (\underline{apply} y z)) M)

As their name indicates, a non-checking operation behaves in the same manner as the original version as long as its arguments are of the appropriate type.^{7} If the argument is not of the appropriate type, the behavior of the non-checking variant is unspecified, and any arbitrary state may be produced. The extended language is called \underline{Λ_{a}^{!+c}}.

We define the semantics of the extended language \underline{Λ_{a}^{!+c}} by extending the CS-machine with the additional transition rules described in Figure 5. The evaluator for the extended

6Unlike other approaches to soft-typing [4, 28, 1], we are not concerned with inferring types for program

⟨ H, E[ (let (x (\underline{car} l_{y})) M) ] ⟩

⟼ \{ \begin{matrix}⟨ H ∪ \{l_{x} = H(l_{z_{1}})\}, E[ M[x ← l_{x}] ] ⟩ & if H(l_{y}) = (cons l_{z_{1}} l_{z_{2}}) \\ where l_{x} = new(H, x) \\ unspecified & if H(l_{y}) ≠ (cons l_{z_{1}} l_{z_{2}}) \end{matrix}  (\underline{car})

⟨ H, E[ (let (x (\underline{cdr} l_{y})) M) ] ⟩

⟼ analogous to (\underline{car})  (\underline{cdr})

⟨ H, E[ (let (x (\underline{apply} l_{y} l_{z})) M) ] ⟩

⟼ \{ \begin{matrix}⟨ H ∪ \{l_{w} = H(l_{z})\}, E[ (let (x N[w ← l_{w}]) M) ] ⟩ & if H(l_{y}) = (λw. N) \\ where l_{w} = new(H, w) \\ unspecified & if H(l_{y}) ≠ (λw. N) \end{matrix} (\underline{apply})

Figure 5: Transition Rules for Non-Checking Primitives

language, \underline{eval}, is defined in the usual way (cmp. Figures 2). Unlike eval, the evaluator \underline{eval} is no longer a total function. There are programs in \underline{Λ_{a}^{!+c}} for which the behavior of the evaluator \underline{eval} is unspecified because of the application of a non-checking operation to an argument of inappropriate type. Still, the two evaluators agree on programs in Λ_{a}^{!+c}.

Lemma 6.1 For P ∈ Λ_{a}^{!+c}, \underline{eval}(P) = eval(P).

6.3 The Soft Typing Algorithm

Our soft typing algorithm uses the results of set based analysis to replace the type-checking operations car, cdr and apply by the corresponding non-checking operation whenever possible, without changing the semantics of programs. For example, suppose that a program contains (let (x (car y)) M) and that set-based analysis proves that y is only bound to pairs. Then we can replace the expression with (let (x (\underline{car} y)) M), which the machine can execute without performing a type-check on y. In general, if the set environment produced by set-based analysis shows that the arguments of car, cdr or apply are always of the correct type, the soft-typing algorithm replaces the operation with its non-checking version. The soft-typing algorithm T , parameterized over a set environment E, is defined in Figure 6. If E is valid for the program being optimized, then the soft-typing algorithm T_{E} preserves the meaning of that program. For every transition step of the source program P there exists a corresponding transition step for the soft-typed program T_{E}(P). We extend T_{E} in a compatible manner to states to aid in the proof of this correspondence.

Lemma 6.2 (Step Correspondence) Let P be a program with a set environment E, and let S be a state for which E is valid.

1. Suppose S ⟼ S′. Then T_{E}(S) ⟼ T_{E}(S′).

variables and presenting these types to the programmer.

7We only consider procedures and not continuations to be an appropriate first argument to \underline{apply} in order to avoid the need for a type-dispatch on this argument within \underline{apply}.

T_{E} : Λ_{a}^{!+c} ⟶ \underline{Λ_{a}^{!+c}}
T_{E}[x] = x
T_{E}[(let (x c) M)] = (let (x c) T_{E}[M])
T_{E}[(let (x (λy. N)) M)] = (let (x (λy. T_{E}(N))) T_{E}[M])
T_{E}[(let (x (cons y z)) M)] = (let (x (cons y z)) T_{E}[M])
T_{E}[(let (x (car y)) M)] = \{ \begin{matrix}(let (x (\underline{car} y)) T_{E}[M]) & if E(y) ⊆ \{(cons z_{1} z_{2})\} \\ (let (x (car y)) T_{E}[M]) & if E(y) ⊈ \{(cons z_{1} z_{2})\} \end{matrix}
T_{E}[(let (x (cdr y)) M)] = analogous to car
T_{E}[(let (x (if y M_{1} M_{2})) M)] = (let (x (if y T_{E}[M_{1}] T_{E}[M_{2}])) T_{E}[M])
T_{E}[(let (x (apply y z)) M)] = \{ \begin{matrix}(let (x (\underline{apply} y z)) T_{E}[M]) & if E(y) ⊆ \{(λw. N)\} \\ (let (x (apply y z)) T_{E}[M]) & if E(y) ⊈ \{(λw. N)\} \end{matrix}
T_{E}[(let (x N) M)] = (let (x T_{E}[N]) T_{E}[M])
T_{E}[(let (x (set! y z)) M)] = (let (x (set! y z)) T_{E}[M])
T_{E}[(let (x (letcc y N)) M)] = (let (x (letcc y T_{E}[N])) T_{E}[M])

Figure 6: The soft-Typing Algorithm T

2. Suppose T_{E}(S) ⟼ S′′. Then there exists S′ such that S ⟼ S′ and T_{E}(S′) = S′′.

Proof:

The proof of both parts proceeds by induction on n and by case analysis of S ⟼ S′ and T_{E}(S) ⟼ S′′ respectively.

The Step Correspondence Lemma implies that a soft-typed program exhibits the same behavior as the corresponding source program.

Theorem 6.3 For any program P ∈ Λ_{a}^{!+c}, \underline{eval}(T_{sba(P)}(P)) = eval(P).

Proof: Both the fact that \underline{eval} is well-defined on T_{sba(P)}(P) and that the equality holds follow from Lemma 6.2.

In summary, the soft-typing algorithm removes redundant type-checks from programs based on the information produced by set-based analysis. This optimization algorithm is provably-correct with respect to the extended evaluator \underline{eval}. Any implementation that realizes \underline{eval} correctly can therefore make use of this optimization.

7 Related Work

The main contribution of our paper is an elegant and flexible derivation of set-based analysis. It substantially simplifies previous formulations [10, 11, 8, 7], and explains the underlying notion of approximation in a clear manner. Unlike the derivation and formalization of other approaches to program analysis, our derivation is not restricted to purely functional languages. Instead, it extends in a natural and straightforward manner to imperative features such as destructive assignments (Section 4) and non-local control operators (Section 5). This extensibility is essential for analyzing programs in languages with higher-order functions as well as imperative features. In this section, we compare our derivation with a number of comparable program analyzes, including an advanced type inference algorithm [1] and two recent variants [23, 13] of Shivers’ 0CFA [22]

Aiken et al. [1] develop a type inference algorithm for a purely functional language. They reduce the type inference problem to a system of type inclusion constraints, which are similar to our set constraints. They do not present a proof of their type soundness lemma, but indicate that this proof is based on the denotational semantics of their language. It is wellknown that extending type soundness proofs based on denotational semantics to a language with imperative features is complex and error-prone, even for a simple Hindley-Milner type system: see Tofte’s [24] discussion of Damas’s [3] faulty proof of a type soundness theorem. Extending the derivation and soundness proofs of Aiken et al.’s rich type system would be even more difficult and complex.

Stefanescu and Zhou [23] present an analysis for an intermediate closure-converted language. They start from an operational semantics in which each state is a set of bindings from locations to either values or expressions. A state transition arbitrarily chooses a location-expression binding and reduces that expression. Their analysis is parameterized by a function that maps each location created during an execution into a finite set of abstract locations. They derive a system of equations, similar to our set constraints, that relates the sets of abstract values that these abstract locations may assume. The result of their analysis is the least solution to the system of equations.

Their semantics is non-intuitive primarily because it uses bindings for two distinct purposes. States contain both location-value bindings, which correspond to our heap, and location-expression bindings, which essentially represents a flat version of our A-normal form control string. This flat representation does not maintain the control information provided by our control string; instead, their semantics evaluates available redexes in an indeterminate manner. This indeterminate behavior is a major obstacle to extending their approach to a language with any imperative features. The addition of destructive assignments is further complicated by the requirement of their indeterminate semantics that all transitions can only increase the set of bindings in a state, and cannot modify existing bindings.

Jagannathan and Weeks [13] develop an analysis for a higher-order language, starting from an unusual operational semantics that records a flow graph in which nodes represent location-value bindings and edges represent the flow of values between locations in a program. Like Stefanescu and Zhou, they parameterize their analysis over relations that describe which locations should be merged. The result of their analysis is the least fixpoint of an abstract transition function.

The complexity of their approach is primarily a result of their decision to analyze the source language, instead of a simplified intermediate form. Expressions in their language can be nested in arbitrarily complex fashions. Evaluating these expressions in a leftmostoutermost manner requires a complex strategy to locate the next redex in the program. Furthermore, the evaluation of nested expressions produces intermediate values not associated with program variables. To record these intermediate values, Jagannathan and Weeks label each program expression with a unique label, and then associate each intermediate value with the label of the corresponding expression. Thus, their semantics and their analysis record label-value associations in addition to the conventional variable-value associations. Our choice of an intermediate A-normal form representation avoids both of these complexities. Because the order of execution in our language follows the lexical nesting of let-expressions [9], control transfer is accomplished in a simple manner. Also, since every intermediate value in our language is named, we only need to record variable-value associations, and avoid the additional complexity of labeling each expression in the program [20].

Jagannathan and Weeks further complicate their rewriting semantics using labels of expressions within their state representation instead of the actual expressions themselves. Therefore, a state does not completely represent an intermediate stage of a computation and cannot be further evaluated without knowledge of the original source program. In addition, their state representation does not contain any explicit control information. Instead, they use the subtle trick of extracting control information from the edges of their flow-graph. Specifically, when the body of a function terminates, they retrieve the label of the expression to which the result of the function body “flows”, and then transfer control to that expression. It is not obvious how this technique extends to complex control operators such as exceptions or call/cc.

A final disadvantage of Jagannathan and Weeks derivation is that their analysis is defined via a complex abstract transition function. This monolithic definition does not provide the insight and understanding that the specification of set-based analysis in terms of set constraints provides.

Wright and Felleisen [26] describe a simple and flexible strategy for proving the type soundness of Hindley-Milner-style polymorphic type systems. Their approach is based on a reduction semantics that easily extends to encompass imperative constructs, and adapts subject reduction theorems from combinatory logic to programming languages. Our derivation of set-based analysis exploits similar techniques. Specifically, our derivation is also based on a reduction semantics, and Lemma 3.5 can be viewed as a subject reduction lemma: it states that the reduction of a state preserves correctness with respect to any set environment satisfying the set constraint. Like Wright and Felleisen’s approach, our derivation extends to additional imperative facilities in a straightforward manner. We expect that this flexibility is a result of the subject reduction technique common to both.

8 Conclusion

Static information about program behavior is crucial for the generation of efficient code for advanced languages. Unfortunately, the derivation of an analysis to compute such information for higher-order languages is subtle and complex, and is closely tied to the formulation of the semantics of the language. Many analyses that were originally developed for a purely functional language can be difficult if not impossible to extend to languages with additional imperative features. This combination of complexity and inflexibility is a major obstacle to exploiting these analyses in realistic compilers.

Our derivation of set-based analysis avoids these complexities and limitations. We formulate our derivation for the language of A-normal forms, since this language constitutes an ideal intermediate representation for compilers [9]. The simplicity of our derivation follows both from our use of the A-normal form language, and from our text-based reduction semantics, which explicitly models the allocation of objects into a global heap, and which records information that associates each run-time value with the corresponding syntactic value. Our use of A-normal forms simplifies our reduction semantics, since the order of execution follows the lexical nesting of let-expressions. In addition, A-normal forms are ideally suited to the derivation of analyses, since all intermediate values in the language are named, and there is no need for the additional complexity of labeling each expression in the program. We derive our analysis directly from the reduction semantics, thus avoiding the intermediate steps of Heintze’s derivation, and we exploit the information recorded by our semantics to express our set constraints on a finite lattice of set environments, instead of on the infinite lattice required by Heintze’s approach.

Extending our derivation to accommodate additional language facilities is straightforward. We have seen how the derivation extends to languages with destructive assignments and first class continuations, thus providing the first soundness proof of set-based analysis for these imperative features. Additional features such as exceptions or communication channels are also easily incorporated. The primary reason for the extensibility of our derivation is the flexibility of our semantics. Since the semantics allocates all values into a global heap, it easily extends to include assignments or cycle-creating constructs such as letrec. The semantics also exposes the entire state of the evaluation at each intermediate step, which facilitates the inclusion of non-local control operators such as first-class continuations or exceptions.

Our derivation can also be modified to produce a more accurate (but more expensive) analysis. One possible approach is to apply Heintze’s technique of polyvariance [11], which is equivalent to creating different “versions” of certain functions in the source program by preceding the analysis by a series of β_{v} “expansion” steps.

A more general approach requires modifying our semantics to expose additional details. Specifically, it involves extracting the environment and continuation components of the control string, and expressing them as separate components of each intermediate state. The resulting semantics is essentially a CESK-machine [6, 5] specialized to A-normal forms. Based on this semantics we can follow our derivation to develop a number of different constraint-based analyses, with different cost-performance tradeoffs.^{8} It is also possible to develop a general analysis framework that is parameterized in a fashion similar to Jagannathan and Weeks’s framework [13]. A particular instance of this framework is created by specifying relations that describe which locations created during program execution should be merged. Instances of this framework include set-based analysis, as well as a number of more precise analyses.

A Set-Based Analysis Algorithm

A complete set-based analysis algorithm for a Scheme-like language containing both assignments and first-class continuations is included in Figures 7 through 9. The algorithm is written in Scheme extended with a special form match for pattern matching [27].

The function SBA traverses an expression to derive the set constraints for that expression. Certain set constraints cannot be satisfied immediately. Consider, for example, the expression (let (x (set! y z)) M). The constraint Cset!^{P} requires that all values in E(z)

8See [8, 7] for a derivation of set-based analysis from a parallel CEK-machine.

;; inputs: a term M
;; outputs: calculates FinalVar[ M ]
;; effects: derives the set constraints for M,
;;  and invokes a constraint solver on these constraints

(define SBA

(lambda (M )

(match M [(? variable? x) x] [‘(let (,x ,exp) ,body) (begin

(match exp [(? constant? c) (new-value! x c)] [‘(cons ,y1 ,y2 ) (new-value! x ‘(cons ,y1 ,y2 ))] [‘(lambda ,y ,N ) (let ([finalvar-N (SBA N )])

(new-value! x ‘(lambda ,y ,N ,finalvar-N )))] [‘(car ,y) (new-constraint! y ‘(propagate-car-to ,x))] [‘(cdr ,y) (new-constraint! y ‘(propagate-cdr-to ,x))] [‘(if ,y ,M1 ,M2 ) (let ([finalvar-M1 (SBA M1 )][finalvar-M2 (SBA M2 )])

(new-constraint! y ‘(conditional-prop #t ,finalvar-M1 ,x)) (new-constraint! y ‘(conditional-prop #f ,finalvar-M2 ,x)))]

[‘(apply ,y ,z) (new-constraint! y ‘(application ,x ,z))] [‘(set! ,y ,z) (new-constraint! z ‘(propogate-to ,y)) (new-constraint! z ‘(propogate-to ,x))] [‘(letcc ,y ,N ) (let ([finalvar-N (SBA N )])

(new-constraint! finalvar-N ‘(propogate-to ,x))

(new-value! y ‘(cont ,x)))] [ ; Must be a term (let ([finalvar-exp (SBA exp)])

(new-constraint! finalvar-exp ‘(propagate-to ,x)))]) (SBA body)]))))

Figure 7: The Set-Based Analysis Algorithm

must be in E(x), but the set E(z) may not yet be known. Therefore, the function SBA associates a constraint ‘(propagate-to ,x) with the variable z. This constraint is applied (via the function interpret-constraint) to each value that is added to E(z), and propagates that value to E(x).

The functions new-value! and new-constraint! associate values and constraints, respectively, with variables. The function interpret-constraint ensures that each constraint on a variable is satisfied for all possible values of that variable, by creating additional values or new constraints as necessary.

The worst-case time complexity of the algorithm is O(|P |^{3}), which can be verified as

;; inputs: a variable and a value
;; outputs: void
;; effects: adds the value to E(var), and applies the appropriate constraints to that value

(define new-value!

(lambda (var value)

(unless (in-E? var value) (add-to-E! var value) (foreach-in-C var (lambda (constraint) (interpret-constraint constraint value))))))

;; inputs: a variable and a constraint
;; outputs: void
;; effects: associates the constraint with var, and applies the constraint to all values in E(var)

(define new-constraint!

(lambda (var constraint)

(unless (in-C? var constraint) (add-to-C! var constraint) (foreach-in-E var (lambda (value) (interpret-constraint constraint value))))))

;; inputs: a constraint and a value
;; outputs: void
;; effects: ensures that the constraint is satisfied, given that the constraint
;;  and the value are associated with the same variable

(define interpret-constraint

(lambda (constraint value)

(match (cons constraint value) [‘((propagate-to ,x) . ,v) (new-value! x v)] [‘((propagate-car-to ,x) . (cons ,y1 ,y2 )) (new-constraint! y1 ‘(propagate-to ,x))] [‘((propagate-cdr-to ,x) . (cons ,y1 ,y2 )) (new-constraint! y2 ‘(propagate-to ,x))] [‘((application ,result ,arg) . (lambda ,para , ,finalvar)) (new-constraint! finalvar ‘(propagate-to ,result)) (new-constraint! arg ‘(propagate-to ,para))] [‘((application ,result ,arg) . (cont ,x)) (new-constraint! arg ‘(propagate-to ,x))] [‘((conditional-prop ,test ,from ,to) . ,value) (when (eq? (null? value) test) (new-constraint! from ‘(propagate-to ,to)))] [ (void)])))

Figure 8: The Set-Based Analysis Algorithm: Auxiliary Functions 1

follows: We assume that the functions in-E?, add-to-E!, in-C? and add-to-C! operate in constant time, and that the functions foreach-in-E and foreach-in-C operate in time linear in the number of elements in the appropriate set.

Each call of the functions new-value! and new-constraint! takes constant time, excluding the time spent in the body of the respective unless expressions. The number of variables, the number of values, and the number of constraints are all O(|P |). Therefore the test conditions of each unless expression can succeed at most O(|P |^{2}) times, and function interpret-constraint is called at most O(|P |^{3}) times. Each call of interpret-constraint terminates in constant time. Therefore, the entire algorithm takes O(|P |^{3}) time.

;; The following three functions maintain a mapping E from program ;; variables to sets of values

;; inputs: a variable and a value
;; outputs: returns true if E(var) contains the value
;; effects: none

(define in-E? (lambda (var value) …))

;; inputs: a variable and a value
;; outputs: void
;; effects: adds value to E(var)

(define add-to-E! (lambda (var value) …))

;; inputs: a variable and a function
;; outputs: none
;; effects: applies fn to each value in E(var)

(define foreach-in-E (lambda (var fn) …))

;; The following three functions maintain a mapping C from program ;; variables to sets of constraints

;; inputs: a variable and a constraint
;; outputs: returns true if C(var) contains the constraint
;; effects: none

(define in-C? (lambda (var constraint) …))

;; inputs: a variable and a constraint
;; outputs: void
;; effects: adds constraint to C(var)

(define add-to-C! (lambda (var constraint) …))

;; inputs: a variable and a function
;; outputs: none
;; effects: applies fn to each constraint in E(var)

(define foreach-in-C (lambda (var fn) …))

Figure 9: The Set-Based Analysis Algorithm: Auxiliary Functions 2

Acknowledgements We thank Nevin Neintze for discussions on set-based analysis and for access to his implementation of set-based analysis for ML. We also thank Chris Colby and Stephanie Weirich for comments on an earlier version of this paper.

References

[1] Aiken, A., Wimmers, E. L., and Lakshman, T. K. Soft typing with conditional types. In Proceedings of the ACM Sigplan Conference on Principles of Programming Languages (1994), pp. 163–173.

[2] Clinger, W., and Jonathan Rees, e. The revised^{4} report on the algorithmic language scheme. ACM Lisp Pointers 4, 3 (July 1991).

[3] Damas, L. M. M. Type Assignment in Programming Languages. PhD thesis, University of Edinburgh, 1985.

[4] Fagan, M. Soft Typing. PhD thesis, Rice University, 1990.

[5] Felleisen, M., and Friedman, D. P. A calculus for assignments in higher-order languages. In Conference Record of the 14th Annual ACM Symposium on Principles of Programming Languages (Munich, West Germany, Jan. 1987), pp. 314–345.

[6] Felleisen, M. The Calculi of Lambda-v-CS-Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Indiana University, 1987.

[7] Flanagan, C., and Felleisen, M. Well-founded touch optimization for futures. Rice University Computer Science TR94-239.

[8] Flanagan, C., and Felleisen, M. The semantics of future and its use in program optimizations. In Proceedings of the ACM Sigplan Conference on Principles of Programming Languages (1995), pp. 209–220.

[9] Flanagan, C., Sabry, A., Duba, B. F., and Felleisen, M. The essence of compiling with continuations. In Proceedings of the ACM Sigplan Conference on Programming Language Design and Implementation (1993), pp. 237–247.

[10] Heintze, N. Set Based Program Analysis. PhD thesis, Carnegie Mellon University, 1992.

[11] Heintze, N. Set-based analysis of ML programs. In Proceedings of the 1990 ACM Conference on Lisp and Functional Programming (1994), pp. 306–317.

[12] Henglein, F. Dynamic typing: syntax and proof theory. Science of Computer Programming 22 (1994), 197–230.

[13] Jagannathan, S., and Weeks, S. A unified treatment of flow analysis in higherorder languages. In 22nd ACM Symposium on Principles of Programming Languages (1995), pp. 393–407.

[14] Jagannathan, S., and Wright, A. Effective flow analysis for avoiding run-time checks. , 1995.

[15] Malmkjaer, K., Heintze, N., and Danvy, O. ML partial evaluation using setbased analysis. Tech. Rep. CMU-CS-94-129, Carnegie Mellon University, 1994.

[16] Milner, R., Tofte, M., and Harper, R. The Definition of Standard ML. MIT Press, 1990.

[17] Morrisett, G., Felleisen, M., and Harper, R. Abstract models of memory management. In Functional Programming and Computer Architecture (1995). To appear.

[18] Park, Y. G., and Goldberg, B. Escape analysis on lists. In Proceedings of the ACM Sigplan Conference on Programming Language Design and Implementation (June 1992), pp. 116–127.

[19] Rozas, G. J. Liar, an Algol-like compiler for scheme. Master’s thesis, Massachusetts Institute of Technology, January 1984.

[20] Sabry, A., and Felleisen, M. Is continuation-passing useful for data flow analysis. In Proceedings of the ACM Sigplan Conference on Programming Language Design and Implementation (1994), pp. 1–12.

[21] Shao, Z., and Appel, A. Space-efficient closure representations. In Proceedings of the ACM Symposium on Lisp and Functional Programming (1994), pp. 150–161.

[22] Shivers, O. Control-flow Analysis of Higher-Order Languages or Taming Lambda. PhD thesis, Carnegie-Mellon University, 1991.

[23] Strfanescu, D., and Zhou, Y. An equational framework for the flow analysis of higher order functional programs. In LFP (1994), pp. 318–327.

[24] Tofte, M. Operational Semantics and Polymorphic Type Inference. PhD thesis, University of Edinburgh, 1987.

[25] Wright, A. Practical Soft Typing for Scheme. PhD thesis, Rice University, 1994.

[26] Wright, A., and Felleisen, M. A syntactic approach to type soundness. Tech. Rep. 160, Rice University, 1991.

[27] Wright, A. K., and Duba, B. F. Pattern matching for Scheme. Unpublished

manuscript, 1993. Available at "ftp://cs.rice.edu/public/wright/match.ps.Z".

[28] Wright, A. and R. Cartwright. A practical soft type system for scheme. In Proceedings of the 1990 ACM Conference on Lisp and Functional Programming (1994), pp. 250–262.