Conditional Lambda-Theories and the Verification of Static Properties of Programs

Mitchell Wand^{∗} Zheng-Yu Wang^{∗}

College of Computer Science Northeastern University 360 Huntington Avenue, 161CN Boston, MA 02115, USA

June 29, 1994

Abstract

We present a proof that a simple compiler correctly uses the static properties in its symbol table. We do this by regarding the target code produced by the compiler as a syntactic variant of a λ-term. In general, this λ-term C may not be equal to the semantics S of the source program: they need be equal only when information in the symbol table is valid. We formulate this relation as a conditional λ-judgement \overline{Γ} ⊃ S = C, where \overline{Γ} is a formula that represents the invariants implicit in symbol table Γ. We present rules of inference for conditional λ-judgements and prove their soundness. We then use these rules to prove the correctness of a simple compiler that relies on a symbol table. The form of the proof suggests that such proofs may be largely mechanizable.

1 Introduction

In a series of papers in 1982–83, we argued that target code produced by a compiler was a syntactic variant of the continuation semantics of the source program [14, 15, 16]. A compiler could be proved correct by showing that its output on any phrase represented a λ-term equal (convertible) to the term given by the semantics for the phrase. A machine could be proved correct by showing that it simulated the reduction of the λ-term represented by its instruction stream.

∗Work supported by the National Science Foundation under grant number CCR-8801591. A preliminary version of this report appeared in Proc. 5th IEEE Symposium on Logic in Computer Science (1990), 321–332.

If we consider optimizing compilers, however, this situation changes. The semantics of a phrase in the source language is a λ-term that is (by the assumption of compositionality) independent of the context in which the phrase occurs. An optimizing compiler, on the other hand, may produce different terms for a given phrase, depending on the context in which the phrase is located. For example, the semantics of an identifier might be a λ-term which consults the environment and, depending on the value found, does one of various things to it (e.g. pass it, coerce it, dereference it, etc.). A compiler, however, might consult the symbol table and produce a term which does exactly one of those things to the run-time value.

The semantics and the compiled term need be equal only when the assumptions in the symbol table happen to be true. We explored this notion of conditional equality, in a model-theoretic setting, in [9]. Our goal in this paper is to explore these ideas in a proof-theoretic setting. By using a proof-theoretic setting, we hope to capture the patterns of reasoning involved in such proofs, in order to eventually provide general metatheorems and automated support.

In Section 2, we present the semantics and the compiler. We also introduce higher-order abstract assembly language (HOAL), a restriction on continuation-passing style that we will use for our target language. Both the semantics and the machine use the untyped λ-calculus. The semantics uses tagged values to model types and uses these tags at runtime to decide whether to dereference an identifier lookup. The machine, like most real machines, does not use tagged values; the compiler uses a symbol table to decide at compile time whether or not an identifier lookup should be dereferenced. The task of the proof is to establish that these decisions are made consistently.

In Section 3, we introduce conditional λ-judgements, which express the conditional equality suggested above. These judgements are of the form Δ ⊃ M = N, where Δ is a conjunction of equalities and other well-behaved formulas. We state some natural rules for deriving such judgements, and prove their soundness in models of the untyped lambda-calculus. In section 4, we give an outline of the correctness proof. We state the induction hypothesis and suggest why a number of simpler alternatives are not adequate. In Section 5, we present a sketch of the proof, including most of the most difficult cases. We suggest how the proof reduces the correctness problem to a set of verification conditions, similar in spirit to those generated by traditional partial-correctness methods. A more detailed account of the proof may be found in [20].

2 The Semantics and the Compiler

We model both the semantics and the compiler as syntax-directed transducers, taking phrases of the source language as input and producing untyped λ-terms in continuation-passing style as output. Because the input and output terms can be interpreted in the same λ-models, it is possible to show them equal (not just congruent). We allow our output terms to have free variables, and we use binding in these terms to model binding in the source language. This convention follows e.g. [3, 5, 11], and is in contrast with the more conventional practice of using environments to model binding. We will now discuss the language of output terms, the source language, the target language, and the compiler in more detail.

2.1 The Semantic Language

The semantics and the compiler both transform the source language into terms of an untyped λ-calculus that we call the semantic language. This is an untyped λ-calculus with a set of constant symbols 0, 1, 2, … as numerals, a constant Eq that computes arithmetic equality on numerals, and a constant + which computes the sum of two numerals. In addition, we have the constants Int, Bool, and Loc, which are used as tags, and an equality constant that works on them. Last, we have a distinguished error value.

We adopt the convention that constants are in capitalized roman font (e.g. Eq); common combinators are written in lower-case roman (e.g. first), and special-purpose combinators are written in italic (e.g. tag).

Although the semantic language is untyped, we will establish some conventions for modelling a few types that are used in the language semantics.

We model sum types using the usual tagged-pair construction. We write (tag v) to extract the tag and (data v) to extract the data. We use case as syntactic sugar for a conditional that branches on the tag of a value; we assume that case returns the error value if the value does not match any of the given tags.

Similarly, we model the store in our semantic language as a pair consisting of an integer pointing to the first free location, and a function from L-values (numerals) to R-values. Hence we write (first σ) to extract the freelocation pointer, and define the combinator contents = λlσ.(second σ)l to dereference a location. Note that unlike [9], we do not distinguish pointers to integers from pointers to booleans.

A model of this language is a model of the untyped λ-calculus with distinguished for each of the constants in the language, such that equality and addition operators work as indicated. Such models are easy to construct based on an ordinary λ-model.

2.2 The Source Language

We next see how the semantics of our source language can be expressed in this semantic language.

Our source language contains integer, boolean, integer-variable, and boolean-variable types, with identifier and addition expressions, assignment commands, compound commands, loops, and two kinds of declaration commands (for values and variables). Except for procedures, these seem to encompass the critical difficulties in the theorems we wish to prove.

Denoted values are integers, booleans, and L-values (represented by numerals); these are tagged by Int, Bool, and Loc. R-values are integers and booleans, tagged with Int and Bool.

Figure 1 gives the grammar of the language; Figure 2 shows selected portions of semantics, with auxiliaries given in Figure 3. In the semantics, v_{I} is a λ-variable associated with source identifier I, and v, v_{1}, etc., are always fresh variables. To simplify notation, we use E for the semantic valuation on all the syntactic categories of the source language.

As suggested above, this is a concrete semantics: rather than producing a value, it produces a term in the semantic language. A conventional environment-style semantics specifies a value by producing a closed term in some λ-calculus, which in turn has a value in some model. Here we have relaxed the requirement that the output term be closed. We model scoping relations in the source language by scoping relations in the semantic language, like [3, 5, 11], rather than by using explicit environments. Whenever

⟨type⟩ ::= Int | Bool | Int-Loc | Bool-Loc
⟨exp⟩ ::= ⟨identifier⟩ | (⟨exp⟩ + ⟨exp⟩)
⟨cmd⟩ ::= ⟨identifier⟩:= ⟨exp⟩
| (⟨cmd⟩; ⟨cmd⟩)
| while ⟨exp⟩ do ⟨cmd⟩
| dcl ⟨type⟩ ⟨identifier⟩ = ⟨exp⟩ in ⟨cmd⟩

Figure 1: Grammar of the Source Language

an identifier I is free in a term e of the source language, then a corresponding variable v_{I} will be free in the semantics E[[e]]. In Reynolds’ terminology, this makes scoping a primary attribute of the semantics, rather than a secondary one. See also [17].

Figure 4 gives the obvious static typing rules; the key judgement is Γ ⊢ c wf, which asserts that command c is well-formed in symbol table Γ. In these figures, we have shown only the clauses for integers and integervariables; the clauses for booleans are similar. One may assign only to an identifier of type integer- or boolean-variable.

Note that there is no obvious connection between these typing rules and the semantic valuations: there is no semantics for the typing rules. Our goal is to fill this gap.

2.3 The Target Language

The target language of our compiler is a set of terms in the semantic language. These terms constitute a higher-order abstract assembly language (HOAL), that is, the higher-order abstract syntax of an ordinary assembly language [2, 6]. These terms will contain variables, this time corresponding to machine registers, and we again use the scoping properties of the semantic language to model the register setting and use patterns of the assembly code.

For example, consider a simple addition instruction add r_{1}, r_{2}, r_{3} , which puts the sum of the contents of registers r_{1} and r_{2} in register r_{3}, and goes on to the next instruction. Since we must take control flow into account we E[[I]] = λκ.case (tag v_{I})

Int : κv_{I}

Bool : κv_{I}
Loc : λσ.κ(contents(data v_{I})σ)σ

E[[(e_{1} + e_{2})]] = λκ.E[[e_{1}]](λv_{1}.E[[e_{2}]](λv_{2}. add v_{1}v_{2}κ)))

E[[I := e]] = λκ.E[[e]](λv.case (tag v_{I})

Loc : store v(data v_{I})κ)

E[[(c_{1}; c_{2})]] = λκ.E[[c_{1}]](E[[c_{2}]]κ)

E[[while e do c]] = λκ. fix(λθ.E[[e]](λv. cond(data v)(E[[c]]θ)κ))

E[[dcl Int I = e in c]] = λκ.E[[e]](λv_{I}.E[[c]]κ)

E[[dcl Int-Loc I = e in c]] = λκ.E[[e]](λv. newloc(λv_{I}. store v(data v_{I})(E[[c]]κ)))

Figure 2: Semantics of the Source Language (extract)

consider instead the instruction stream add r_{1}, r_{2}, r_{3}; C beginning with our addition instruction. It is clear that r_{1} and r_{2} are “free” in this sequence, because the meaning of the sequence depends on their values. The register r_{3}, however, is not free, since it is set rather than referenced. In fact, the addition instruction binds r_{3} for the remainder of the sequence C. Therefore we define the abstract syntax of add r_{1}, r_{2}, r_{3}; C to be

add r_{1} r_{2} (λr_{3}.C)

for some combinator add. Furthermore, given this syntax, it is reasonably clear that the semantics of add ought to be

add = λxyκ.κ(x + y)

Similarly, a register-move instruction can be modelled as move r_{1}(λr_{2}.C) where move = λvκσ.κvσ, and a memory-fetch instruction can be modelled as fetch r_{1}(λr_{2}.C) where fetch = λvκσ.κ(contents σv)σ.

Such terms can be given an operational semantics by a machine that simulates their reduction sequences. The state of the machine will be a tag = first data = second add = λvwκ.case (tag v)

Int : case (tag w)

Int : κ(pair Int ((data v) + (data w)))

contents = λnσ.(second σ)n

newloc = λκσ.κ(pair Loc (first σ))(pair((first σ) + 1)(second σ))

store = λvnκσ.κ(pair(first σ)

(λm.(cond(Eq n m)
v
((second σ) m))))

Figure 3: Semantic Auxiliaries

triple, written ⟨C, Σ, σ⟩, consisting of an HOAL term C, a substitution Σ mapping λ-variables (including the free variables of C) to constants or closed abstractions (what [10] calls closed values), and a store σ. The substitution Σ represents the contents of the target machine’s registers.

The state ⟨C, Σ, σ⟩ is a representation of the term (CΣ)σ obtained by actually performing the substitution Σ on C and applying the resulting term to the store σ. The machine operates by simulating the reduction of (CΣ)σ. By using the semantics of the combinators, we can work out the reduction rules to discover that every term (CΣ)σ reduces in a few steps (usually 1 or 2) to another term of the form (C′Σ)′σ′. Thus we can simulate this reduction by giving the machine an operational semantics which rewrites ⟨C, Σ, σ⟩ to ⟨C′, Σ′, σ′⟩. Thus, given a denotational semantics for our machine instructions, we derive an operational semantics by inheriting the operational semantics of the λ-calculus.

For example, let us consider reducing the state ⟨add r_{1}r_{2}(λr_{3}.C), Σ, σ⟩.

⟨add r_{1}r_{2}(λr_{3}.C), Σ, σ⟩ ≡ add(r_{1}Σ)(r_{2}Σ)((λr_{3}.C)Σ)σ
→ ((λr_{3}.C)Σ)((r_{1}Σ) + (r_{2}Σ))σ  (definition of add)
→ (C(Σ[r_{3} := ((r_{1}Σ) + (r_{2}Σ))]))σ (since Σ is closed)

Γ a partial map from ⟨identifier⟩ to ⟨type⟩

\frac{Γ(I) = Int or Γ(I) = Int-Loc}{Γ ⊢ I : Int}

\frac{Γ(I) = Bool or Γ(I) = Bool-Loc}{Γ ⊢ I : Bool}

\frac{Γ ⊢ e_{1} : Int Γ ⊢ e_{2} : Int}{Γ ⊢ (e_{1} + e_{2}) : Int}

\frac{Γ(I) = Int-Loc Γ ⊢ e : Int}{Γ ⊢ I := e wf}

\frac{Γ[I : Int] ⊢ c wf}{Γ ⊢ dcl Int I = e in c wf}

\frac{Γ[I : Int-Loc] ⊢ c wf}{Γ ⊢ dcl Int-Loc I = e in c wf}

Figure 4: Static Typing Rules (extract)

Therefore we define the action of the machine on the add instruction as

⟨add r_{1}r_{2}(λr_{3}.C), Σ, σ⟩ ⇒ ⟨C, Σ[r_{3} := ((r_{1}Σ) + (r_{2}Σ))], σ⟩

which simulates the reduction of the term, as desired. The last step relies on the fact that Σ is closed (see [18]). Note that the reduction sequence for this closure does just what an addition instruction normally does: it goes on to execute the code sequence C in a substitution where r_{3} is bound to the sum of the contents of r_{1} and r_{2}. Here Σ is single-threaded [12], so that we can model this operation by a destructively-updated register file.

The complete target language is shown in Figure 5. It has 10 machine instructions plus a label operation (which is treated as an assembly-language directive). Using calculations like those above, it can be shown that these instructions model a register machine in which these instruction behave in the expected way. The only complication is the treatment of fix and goto, which can be modelled as in [16]. Note that the machine works on untagged quantities. Note also that sp is a reserved register that is used as a

move r_{1}(λr_{2}.C)  move = λvκ.κv
fetch r_{1}(λr_{2}.C)  fetch = λvκσ.κ(contents vσ)σ
store r_{1}r_{2}C  store = store
add r_{1}r_{2}(λr_{3}.C)  add = λv_{1}v_{2}κ.κ(v_{1} + v_{2})
branch r_{1}C_{1}C_{2}  branch = cond
newloc C  newloc = λκ. newloc(λv.κ(data v))
push r_{1} sp(λ sp .C) push = λvsκ.κ(pair v s)
pop sp(λr_{1} sp .C) pop = λsκ.κ(first s)(second s)
halt r_{1}  halt = λv.v
goto θ  goto = λθ.θ
fix(λθ.C)  fix = fix

Figure 5: Machine Instructions

stack pointer. We will use bold-face type for machine instructions and fixed registers (in this example, sp is the only such register).

Our compiler is shown in Figure 6. It takes three arguments: the source phrase to be compiled, a symbol table, and a continuation term, which is the HOAL term representing the continuation context. In the compiler, r_{I} is a λ-variable associated with source identifier I, and r, r_{1}, etc., are always fresh variables (registers). We do not deal with register spilling, but it is easy to choose these variables so that registers are reused whenever possible [4]. The code for a declaration pushes the saved value on a stack (kept in register sp) and restores the value after the body. This is discussed in more detail in Section 5.6. Note that we have arranged the code for the declaration cases to suggest the usual division of assembly code into lines; each line beginning with a push, newloc, etc. corresponds to a single assembly-language instruction of our abstract machine. In fact, if we adhere to the convention that the scope of a λ-term λx.M extends as far as possible to the right, the parentheses around each of the λ’s in Figure 6 are strictly speaking unnecessary. For more examples, see [18].

The compiler is syntax-directed in its first argument, but it may consult its second argument arbitrarily to determine the output term. In particular, our compiler uses its symbol table to determine whether to emit a move or a fetch instruction for an identifier in an expression. This is the same choices that the semantics makes at run time using tagged values. Our goal is to prove by denotational techniques that the compiler always makes the same choice as the semantics.

3 Conditional λ-theories

We now build some general-purpose machinery for dealing with conditional λ-theories, which we will later apply to prove the correctness of our compiler.

Let G be a set of formulas which include all the λ-equalities (formulas of the form M = N, where M and N are λ-terms) and which is closed under substitution of λ-terms for individual variables, and which has a notion of truth ⊧ in any λ-model, subject to the usual condition that if M is any λ-model, and ρ is an environment over M, then ρ ⊧ G[M/x] iff ρ[(M(M)ρ)/x] ⊧ G, where M(M)ρ is the denotation of λ-term M in environment ρ of λ-model M. If Δ is a conjunction of formulas from G, we write ρ ⊧ Δ if every formula in Δ is true at ρ, and we write Δ[M/x] for the conjunction obtained by applying substitution [M/x] to each formula in Δ.

A conditional λ-judgement over G is of the form Δ ⊃ G, where G is a formula of G and Δ is a conjunction of formulas from G. If M is any λ-model, and ρ is an environment over M, we say that that a conditional λ-judgement Δ ⊃ G is true at ρ iff either G is true at ρ or some formula in Δ is false at ρ. We say Δ ⊃ G is true in M iff it is true at every environment over M. We write Δ ⊃ G rather than Δ ⊢ G to emphasize this notion of material implication and to avoid suggesting that the formulas in Δ are implicitly universally quantified.

Figure 7 shows the rules of inference we will use. This system was used inter alia in [17] to prove the correctness of a deBruijn-style lexicaladdressing algorithm. We write ⊢ Δ ⊃ G to indicate that Δ ⊃ G is provable using these rules. The rules are divided into two groups: the first four, which are structural rules, and the last three, which import the theory of the λ-calculus into the new theory. A conditional λ-theory over G is a set of formulas from G that is closed under the rules of Figure 7.

We begin by considering the case in which G is just the λ-equalities. In this case we can state some easy soundness and conservative extension results:

Proposition 1 For each rule in Figure 7, if the hypotheses are true in a λ-model M, then the conclusion is true also.

C[[I]]ΓK = \{ \begin{matrix}move r_{I}K & if Γ(I) = Int or Bool \\ fetch r_{I}K & if Γ(I) = Int-Loc or Bool-Loc \end{matrix} C[[(e_{1} + e_{2})]]ΓK = C[[e_{1}]]Γ(λr_{1}.C[[e_{2}]]Γ(λr_{2}. add r_{1}r_{2}K))) C[[I := e]]ΓK = C[[e]]Γ(λr. store rr_{I}K) C[[(c_{1}; c_{2})]]ΓK = C[[c_{1}]]Γ(C[[c_{2}]]ΓK) C[[while e do c]]ΓK = fix(λθ.C[[e]]Γ(λr.branch r

(C[[c]]Γ(goto θ))

K))

C[[dcl Int I = e in c]]ΓK = C[[e]]Γ(λr.

push r_{I} sp(λ sp .

move r(λr_{I}.
C[[c]](Γ[I : Int-Loc])
pop sp(λr_{I} sp .
K))))

C[[dcl Int-Loc I = e in c]]ΓK = C[[e]]Γ(λr.

push r_{I} sp(λ sp .

newloc(λr_{I}.
store rr_{I}

C[[c]](Γ[I : Int-Loc])

pop sp(λr_{I} sp .
K))))

Figure 6: The Compiler

\frac{G ∈ Δ}{Δ ⊃ G} use
\frac{Δ ⊃ G}{Δ, Δ′ ⊃ G} weakening
\frac{Δ ⊃ G}{Δ[N/x] ⊃ G[N/x]} instantiation
\frac{Δ ⊃ G Δ, G ⊃ H}{Δ ⊃ H} cut
\frac{λ ⊢ M = N}{∅ ⊃ M = N} λ
\frac{Δ ⊃ M = M′ Δ ⊃ N = N′}{Δ ⊃ MN = M′N′} congruence
\frac{Δ ⊃ M = M′ x ∉ vars(Δ)}{Δ ⊃ (λx.M) = (λx.M′)} ξ

Figure 7: Rules of inference for conditional λ-judgements

Proof: All the cases are easy except for instantiation and ξ, which require that the hypotheses hold for all environments ρ in the model, not just the current one. Let us work out the case for instantiation. Fix a λ-model M and assume that for all environments ρ in M, ρ ⊧ Δ ⊃ G. We need to show that for all ρ, ρ ⊧ Δ[M/x] ⊃ G[M/x]. Assume that ρ ⊧ Δ[M/x]. Then, by the satisfaction condition on ⊧, ρ[v/x] ⊧ Δ, where v is the denotation of M at ρ. Therefore ρ[v/x] ⊧ G, by the truth of the Δ ⊃ G, and hence ρ ⊧ G[M/x], as desired, by the satisfaction condition. The proof for the ξ rule is similar. QED

Proposition 2 If a conditional λ-judgement is provable from the rules of Figure 7, then it is true in every λ-model.

Proof: Immediate. QED

Theorem 1 If a conditional λ-judgement ∅ ⊃ M = N is provable using the rules of Figure 7, then M and N are interconvertible.

Proof: By the completeness theorem, if two λ-terms are equal in every model, then they are interconvertible. QED

For our examples, we will consider a somewhat larger conditional λtheory. We will choose our λ-terms to be those of our semantic language, and choose G to include equalities M = N and formulas of the form M < N. Let G_{1} be the set of all finite conjunctions of formulas of these two forms. This will be the set of potential Δ’s.

The formula M < N is defined to be true at environment ρ of model M if the λ-terms M and N each denote (in environment ρ) the value of one of the numeral constants, and the numeral corresponding to M is less than the numeral corresponding to N. We will occasionally write M < N < P for the obvious conjunction.

We will also need some axioms, shown in Figure 8, for manipulating implications involving numerals. Each of the rules are guarded by 0 < n so that they will be sound in any λ-model. This allows us to keep a conservative extension property:

Theorem 2 Let Φ be a translation of the semantic language to the pure λcalculus, in which each of the numeric constants is translated to a combinator for some set of numerals. Then an equation M = N is provable in the conditional λ-calculus iff Φ(M) and Φ(N) are interconvertible.

0 < 1
n < m & m < p ⊃ n < p
0 < n ⊃ n < n + 1

0 < n & n < m ⊃ (Eq n m) = False

0 < n ⊃ (Eq n n) = True

Figure 8: Axioms for numerical formulas

Proof: Under the interpretation Φ, each of the axioms in Figure 8 is true in any λ-model. Now consider a proof of M = N from the axioms in Figure 8 and the rules of Figure 7. Apply the interpretation Φ to every formula in the proof. The resulting proof is now a derivation of Φ(M) = Φ(N) from statements true in every λ-model, using rules that are sound in every λmodel. So Φ(M) = Φ(N) is true in every λ-model, and the result follows by completeness. QED

We use 0 < n as a guard because we will need to express numerical inequality when dealing with allocation. So we will start all the counters in our machines at 1. An alternative would be to have both < and ≤ in the theory.

We will also use a fixpoint induction rule, shown in Figure 9. In this rule, Y denotes the usual fixpoint combinator, and Ω denotes Y I. We state this as an infinitary rule, so that the user of the system can prove all the hypotheses using any induction principle that applies. This rule is sound in any model in which every universe has a bottom element and in which functions preserve increasing chains. Let Y denote the λ-theory of this class of models. By the same reasoning as above, we can conclude that any equation M = N deducible using the rules of Figures 7 and 8 plus this fixed point rule is already in Y.

\frac{Δ ⊃ M^{(n)}Ωx = N^{(n)}Ωx for all n}{Δ ⊃ Y Mx = Y Nx} fixpoint

Figure 9: Fixpoint induction rule

4 Finding the Induction Hypothesis

The symbol table expresses the assumptions that the compiler makes about the state of the machine when the code is executed. We can express this as a conditional λ-judgement by defining, for each symbol table Γ, a set of formulas \overline{Γ}. These formulas express, for each I in Γ, the relationship between the variable v_{I} in the semantics and the register r_{I} in the machine.

To do this, we introduce a new judgement, which we call a congruence assertion. The congruence assertion v ∼ r : α asserts that the value v in the semantics corresponds, as a quantity of type α, to (the contents of) the register r in the machine.

The next step is to interpret each congruence assertion into a formula in G_{1} . We do this by cases, depending on the type α:

1. t ∼ t′ : Int is interpreted as (tag t) = Int & (data t) = t′.

2. t ∼ t′ : Bool is interpreted as (tag t) = Bool & (data t) = t′

3. t ∼ t′ : Int-Loc is interpreted as

(tag t) = Loc & 0 < (data t) & (data t) < (first σ) & 0 < t′ & t′ < (first σ′) & (tag (contents(data t)σ)) = Int & (data (contents(data t)σ)) = (contents t′σ′)

Note that σ and σ′ appear free in these formulas.

4. t ∼ t′ : Bool-Loc is interpreted as

(tag t) = Loc & 0 < (data t) & (data t) < (first σ) & 0 < t′ & t′ < (first σ′) & (tag (contents(data t)σ)) = Bool & (data (contents(data t)σ)) = (contents t′σ′)

For scalar quantities (integers or booleans), this is straightforward: v ∼ r : Int asserts that v has the appropriate tag and its data field is equal to r. In the case of locations, we also need to specify the relationship between the store σ used by the semantics and the store σ′ used by the compiled code. Therefore we interpret v ∼ r : Int-Loc to assert that the tag of v is Loc, that v and r each point into the allocated area of their respective stores, and that their contents correspond as integers. v ∼ r : Bool-Loc is defined similarly. Note that σ and σ′ appear free in these formulas.

Now we can define the proposition \overline{Γ} of a symbol table Γ as:

\overline{Γ} = ⋀\{ v_{I} ∼ r_{I} : α | I : α ∈ Γ \}.

v_{I} and r_{I} are called associated variables of Γ. We are intentionally ambiguous as to whether \overline{Γ} consists of congruence assertions or their interpretations in G_{1}. We will occasionally write \overline{Γ} as \overline{Γ}[σ, σ′] to remind the reader that σ and σ′ are free in \overline{Γ} when it is interpreted in G_{1}.

We can now consider the form of the correctness result for our compiler. The obvious hypothesis is

Induction Hypothesis, Version 1 For any command c, any term K and any symbol table Γ such that c is well-formed in Γ,

⊢ \overline{Γ}[σ, σ′] ⊃ E[[c]]Kσ = C[[c]]ΓKσ′

Here we have stated the hypothesis for commands; a similar hypothesis must be stated for expressions as well. K ranges over terms in the semantic language. Normally K will denote a command continuation, but this concept is external to our semantic language, which is untyped. The left-hand side is actually (E[[c]])Kσ, the application of the term E[[c]] to K and σ, while the right-hand side is actually (C[[c]]ΓK)σ′, the application of the term C[[c]]ΓK to σ′. We must be careful about this distinction in situations such as applying substitution to a term.

Unfortunately, this induction hypothesis is not adequate. To see why, consider the semantics and the compiler for a compound command:

E[[(c_{1}; c_{2})]] = λκ.E[[c_{1}]](E[[c_{2}]]κ)
C[[(c_{1}; c_{2})]]ΓK = C[[c_{1}]]Γ(C[[c_{2}]]ΓK)

If κ = K, then we can apply the continuation hypothesis at c_{2} to deduce that \overline{Γ}[σ, σ′] ⊃ E[[c_{2}]]Kσ = C[[c_{2}]]ΓKσ′. However, this does not allow us to apply the induction hypothesis at c_{1}, because the induction hypothesis requires equality, not just conditional equality. We therefore generalize the induction hypothesis to

Induction Hypothesis, Version 2 For any command c, and any terms K and K′ and any symbol table Γ such that c is well-formed in Γ, if

⊢ \overline{Γ}[σ, σ′] ⊃ Kσ = K′σ′

then

⊢ \overline{Γ}[σ, σ′] ⊃ E[[c]]Kσ = C[[c]]ΓK′σ′

This version of the induction hypothesis is adequate to prove the correctness of the compound-command line above, but it is not sufficient to deal with addition expressions, which are given by:

E[[(e_{1} + e_{2})]] = λκ.E[[e_{1}]](λv_{1}.E[[e_{2}]](λv_{2}. add v_{1}v_{2}κ)))
C[[(e_{1} + e_{2})]]ΓK′ = C[[e_{1}]]Γ(λr_{1}.C[[e_{2}]]Γ(λr_{2}. add r_{1}r_{2}K′))

Here there are additional variables in the continuations which do not appear in Γ. We need to state the relationships between v_{1} and r_{1}, and between v_{2} and r_{2}.

To handle this, we must expand the left-hand sides of the λ-judgements in our induction hypothesis to look something like Δ&\overline{Γ}, where Δ is a set of congruence assertions about the variables which appear in the continuations but not in the command c. We will need to keep track of assumptions about program variables, temporary variables, and variables which are kept on the value stack sp. More precisely:

A set Δ of congruence assertions is admissible for Γ iff each element of Δ is of the form v ∼ t : α, where v is a variable not associated with Γ, v occurs in Δ exactly once, and t is either a variable which is non-associated and occurs in Δ once, or a term of form (first (second^{(n)} sp)) for some integer n and a fixed stack pointer variable sp.

The induction hypothesis would then look something like:

Induction Hypothesis, Version 3 For any command c, any terms K and K′, any symbol table Γ such that c is well-formed in Γ, and any set of congruence assertions Δ that is admissible for Γ, if

⊢ (Δ&\overline{Γ})[σ, σ′] ⊃ Kσ = K′σ′

then

⊢ (Δ&\overline{Γ})[σ, σ′] ⊃ E[[c]]Kσ = C[[c]]ΓK′σ′

Unfortunately, this is still not enough: for (Δ & \overline{Γ}) to be strong enough to serve as an invariant, we need to add information about possible aliasing between different location variables. In our language there is no aliasing. To represent this fact, for each Δ and Γ, we produce a proposition Δ ⊗ Γ ∈ G_{1} consisting of the conjunction of

1. The interpretation of each congruence assertion in Δ.

2. The interpretation of each congruence assertion in Γ.

3. The equations (Eq(data v) (data v′)) = False, (Eq r r′) = False for each pair of distinct assertions v ∼ r : α, v′ ∼ r′ : α′ (α, α′ = Int-Loc or Bool-Loc) in Δ ∪ Γ.

4. 0 < (first σ) and 0 < (first σ′).

The equations in the third set of formulas assert that whenever v ∼ r : α, v′ ∼ r′ : α′ are distinct pairs of congruent variables that denote locations, their values are distinct. Thus two program variables never alias the same location. The formulas in the last set assert that the free-location counters in σ and σ′ are valid integers.

As usual, we will occasionally write (Δ ⊗ Γ)[σ, σ′] when it is necessary to remind the reader that σ and σ′ occur free in these formulas. We will also occasionally write Δ_{1} ⊗ Δ_{2} ⊗ Γ for the obvious associative extension.

In our language, there is no aliasing. In a more complex language, we would need assertions saying that two variables in the semantics denoted the same location if and only if the corresponding variables in the target code codesignated. Note that our system is designed to allow the compiler to do optimizations which change the usage of the store, though our compiler does not take advantage of this.

This leads us to our final version of the induction hypothesis:

Induction Hypothesis, Version 4 For any command c, any terms K and K′, any symbol table Γ such that c is well-formed in Γ, and any set of congruence assertions Δ admissible for Γ, if

⊢ (Δ ⊗ Γ)[σ, σ′] ⊃ Kσ = K′σ′

then

⊢ (Δ ⊗ Γ)[σ, σ′] ⊃ E[[c]]Kσ = C[[c]]ΓK′σ′

5 Main Result

This version of the induction hypothesis is adequate to carry through the induction, and to deduce that the compiled version of the entire (closed) program is equal to the semantics in the theory Y. We will also need analogous induction hypothesis for each of the syntactic categories in the language. We now state the entire theorem:

Theorem 3 (Main Theorem) In the following, K, K′, H, H′, etc., range over λ-terms, Γ ranges over symbol tables, Δ ranges over sets of congruence assertions admissible for Γ, and v and r are fresh variables that do not appear anywhere else in the context.

1. If e is an expression such that Γ ⊢ e : Int and

⊢ (Δ ⊗ Γ ⊗ (v ∼ r : Int))[σ, σ′] ⊃ Hvσ = H′rσ′

then

⊢ (Δ ⊗ Γ)[σ, σ′] ⊃ E[[e]]Hσ = C[[e]]ΓH′σ′

2. If e is an expression such that Γ ⊢ e : Bool and

⊢ (Δ ⊗ Γ ⊗ (v ∼ r : Bool))[σ, σ′] ⊃ Hvσ = H′rσ′

then

⊢ (Δ ⊗ Γ)[σ, σ′] ⊃ E[[e]]Hσ = C[[e]]ΓH′σ′

3. If c is a command such that Γ ⊢ c : wf and

⊢ (Δ ⊗ Γ)[σ, σ′] ⊃ Kσ = K′σ′

then

⊢ (Δ ⊗ Γ)[σ, σ′] ⊃ E[[c]]Kσ = C[[c]]ΓK′σ′

Proof: The proof proceeds by structural induction on the proof that c is well-formed in Γ. We consider each case in turn, in increasing order of complexity. We present here only the main parts of the proof. More details may be found in [20].

5.1 Identifiers

There is one subcase for each possible value of Γ(I). Each subcase is a straightforward calculation. Here H and H′ normally denote expression continuations; the antecedent of the conditional states that given congruent values and congruent stores, H and H′ return the same answer.

5.2 Compound Commands

For a compound command (c_{1}; c_{2}) we have

E[[c_{1}; c_{2}]] = λκ.E[[c_{1}]](E[[c_{2}]]κ)
C[[c_{1}; c_{2}]]ΓK′ = C[[c_{1}]]Γ(C[[c_{2}]]ΓK′)

If we assume that

⊢ (Δ ⊗ Γ)[σ, σ′] ⊃ Kσ = K′σ′

then by the induction hypothesis at c_{2} we get

⊢ (Δ ⊗ Γ)[σ, σ′] ⊃ E[[c_{2}]]Kσ = C[[c_{2}]]ΓK′σ′

so by the induction hypothesis again at c_{1}, we get

⊢ (Δ ⊗ Γ)[σ, σ′] ⊃ E[[c_{1}]](E[[c_{2}]]K)σ = C[[c_{1}]]Γ(C[[c_{2}]]ΓK′)σ′.

as desired.

5.3 Expressions

The proof is similar to that for compound commands; the only complication is keeping track of the congruence between the intermediate variables v_{1}, v_{2} and r_{1}, r_{2}.

5.4 Loops

For a loop while e_{bool} do c we have

E[[while e_{bool} do c]] = λκ. fix(λθ.E[[e_{bool}]](λv.(cond (data v) (E[[c]]θ) κ)))

C[[while e_{bool} do c]]ΓK′ = fix(λθ′.C[[e_{bool}]]Γ(λr.branch r

(C[[c]]Γ(goto θ′))
K′))

Since each side is a fixpoint, let θ_{n}, θ′_{n} denote the successive iterations. We can show, by induction on n, that for each n,

⊢ Δ ⊗ Γ ⊃ θ_{n}σ = θ′_{n}σ′

The induction step is a calculation similar to those for compound commands. From this we apply the fixpoint rule to obtain the desired result.

This leaves two cases: assignments and declarations. These are more involved, so we will present them in more detail.

5.5 Assignment Commands

Assume that Γ ⊢ I := e wf.

We need to show that for all Δ, if

⊢ Δ ⊗ Γ ⊃ Kσ = K′σ′  (1)

then

⊢ Δ ⊗ Γ ⊃ E[[I := e]]Kσ = C[[I := e]]ΓK′σ′

Expanding the definitions of E[[I := e]] and C[[I := e]]ΓK′, the needed conclusion is equivalent to

⊢ Δ ⊗ Γ ⊃
E[[e]](λv.case (tag v_{I})
Loc : store v(data v_{I})K)σ
= C[[e]]Γ(λr. store rr_{I}K′)σ′

By the induction hypothesis for e, it will suffice to show that the two continuations are congruent, i.e., that

⊢ Δ ⊗ (v ∼ r : Int) ⊗ Γ ⊃
(λv.case (tag v_{I})
Loc : store v(data v_{I})K)vσ
= (λr. store rr_{I}K′)rσ′

Since Γ ⊢ I := e wf, we know that Γ(I) = Int-Loc, so the formulas generated from Γ include tag v_{I} = Loc. This and β-reduction simplify the needed conclusion to

⊢ Δ ⊗ (v ∼ r : Int) ⊗ Γ ⊃
store v(data v_{I})Kσ
= store rr_{I}K′σ′

(2)

By expanding the definitions of store and store, this reduces to

⊢ Δ ⊗ (v ∼ r : Int) ⊗ Γ ⊃ Kσ_{1} = K′σ′_{1}  (3)

where σ_{1} and σ′_{1} are the terms given by

σ_{1} = (pair(first σ)
(λm.(cond(Eq(data v_{I}) m)
v
((second σ) m))))
σ′_{1} = (pair(first σ′)
(λm′.(cond(Eq r m′)
r
((second σ′) m′))))

Assuming (1), we need to establish (3). Let Σ be the substitution which assigns σ_{1} and σ′_{1} to σ and σ′ respectively. Then we can take the Σ instance of (1) to get

⊢ (Δ ⊗ Γ)[σ_{1}, σ′_{1}] ⊃ Kσ_{1} = K′σ′_{1}  (4)

From this we can obtain (3) by the cut rule if we can establish the “verification condition”

⊢ Δ ⊗ (v ∼ r : Int) ⊗ Γ ⊃ (Δ ⊗ Γ)[σ_{1}, σ′_{1}]  (5)

where the right-hand side denotes the conjunction of the finitely many formulas in (Δ ⊗ Γ)Σ. This verification condition may be established via tedious but straightforward reasoning; the tricky part is using the anti-aliasing equations to establish that updating the store to obtain σ_{1} and σ_{1} does not falsify any of the assumptions in (Δ ⊗ Γ). This is done by taking each of the desired congruence assertions and using the anti-aliasing equations to guarantee that the locations in question are either (a) different from the updated locations, and therefore unchanged or (b) are the updated locations, and are congruent by the assumption that the assignment command is wellformed (and therefore assigns an integer to integer location). Details may be found in [20]. This reasoning is reminiscent of the reasoning typically used in proofs about arrays in Hoare logic [13].

5.6 Variable Declaration Commands

We call (5) a verification condition by analogy with the formulas traditionally “left over to do by hand” in Hoare-style partial correctness logics; like such verification conditions, this one asserts that a desired condition is left invariant under the operation of the program. The other cases follow a similar pattern: lambda-calculus reasoning allows us to symbolically execute the source and target programs; we then generate verifications which allow us to stitch together a proof. The analogy extends further: reasoning about scalar (register) variables is handled easily by substitution in the lambda-calculus, just as in Hoare logic, but reasoning about the store and aliasing involves calculations like those required for reasoning about arrays [13].

Consider the case of variable declarations; value declarations are similar but a little easier because they do not involve the store. Let M denote the phrase

dcl Int-Loc I = e in c

Then the semantics is given by

E[[M]] = λκ.E[[e]](λv. newloc(λv_{I}. store vv_{I}(E[[c]]κ)))

The intention of command M is that the expression e should be evaluated and its value assigned to a newly-allocated memory location. Then the command c should be executed in an environment in which I is bound to the new cell. In the semantics, given continuation κ, e is evaluated with a continuation that calls the result v. A new location is allocated, with a continuation that calls it v_{I}. The value v is stored in location v_{I}, and then the command c is executed. Any occurrences of I in c will appear as occurrences of v_{I} in E[[c]]κ, which will be bound by the λv_{I}.

The compiled code, shown in Figure 6, has the same elements, except that it must also deal with saving the old value of the variable being declared, which may appear free in the continuation term K′. It does this by pushing the old value onto a stack sp. Notice also that c is compiled in the augmented symbol table Γ[I : Int-Loc]. These details are not necessary in a semantics (since β-reduction does all this for free), but must be managed explicitly by a compiler.

These details make the proof for this case worth discussing. We assume that

⊢ Δ ⊗ Γ ⊃ Kσ = K′σ′  (6)

We need to show that

⊢ Δ ⊗ Γ ⊃ (E[[M]])Kσ = (C[[M]]ΓK′)σ′  (7)

Working out the left side, and being careful with variable captures, we see that

(E[[M]])K = E[[e]]{(λv. newloc(λv_{I}.
store v(data v_{I})(E[[c]](K[w/v_{I}]))))}[v_{I}/w]

where w is a fresh variable. Comparing this with the definition of C[[M]]ΓK′, which begins with C[[e]]Γ, we conclude that we can use the induction hypothesis at e to deduce (7) if we can prove that

⊢ Δ ⊗ (v ∼ r : Int) ⊗ Γ ⊃
{newloc(λv_{I}. store v(data v_{I})(E[[c]]K[w/v_{I}])))σ}[v_{I}/w]
= (push r_{I} sp λ sp . newloc λr_{I}.
store rr_{I}(C[[c]]Γ_{1}K′_{1}))σ′

(8)

where K′_{1} is pop sp λr_{I} sp .K′ and Γ_{1} is Γ[I : Int-Loc]. We can now symbolically execute the combinators on each side to find a substitution Σ such that (8) is equivalent to

⊢ Δ ⊗ (v ∼ r : Int) ⊗ Γ ⊃
{(E[[c]]K[w/v_{I}])σ}Σ = {C[[c]]Γ_{1}K′_{1}σ′}Σ

(9)

In this case, Σ is given by

Σ_{2} = [(pair Loc (first σ))/v_{I}, (first σ′)/r_{I}, σ_{1}/σ, σ′_{1}/σ′, v_{I}/w, (pair r_{I} sp)/ sp] where

σ_{1} = (pair((first σ) + 1)

(λm.(cond(Eq (first σ) m) v

((second σ) m))))
σ′_{1} = (pair((first σ′) + 1)

(λm.(cond(Eq (first σ′) m)

r
((second σ′) m))))

It remains to show that (6) implies (9). We begin by observing that \overline{Γ} consists of some congruence assertions \overline{Γ_{0}}, possibly plus the assertion v_{I} ∼ r_{I} : α where α is the type of I in Γ, if any. We can therefore rewrite (6) as

⊢ Δ ⊗ (v_{I} ∼ r_{I} : α) ⊗ \overline{Γ_{0}} ⊃ Kσ = K′σ′  (10)

Let Σ_{2} denote the substitution

[(first sp)/r_{I}, (second sp)/ sp, w/v_{I}]

Then λ ⊢ K′Σ_{2} = K′_{1}. Furthermore KΣ_{2} ≡ K[w/v_{I}], and \overline{Γ_{0}}Σ_{2} ≡ \overline{Γ_{0}}. Therefore, if we take the Σ_{2} instance of (10) we get

⊢ ΔΣ_{2} ⊗ (w ∼ first sp : α) ⊗ \overline{Γ_{0}} ⊃ K[w/v_{I}]σ = K′_{1}σ′  (11)

By weakening, we get

⊢ ΔΣ_{2} ⊗ (w ∼ first sp : α) ⊗ \overline{Γ_{0}} ⊗ (v_{I} ∼ r_{I} : Int-Loc)
⊃ K[w/v_{I}]σ = K′_{1}σ′

(12)

We now observe that \overline{Γ_{0}} & (v_{I} ∼ r_{I} : Int-Loc) is just \overline{Γ_{1}}. Furthermore, applying the substitution Σ_{2} to Δ produces another set of admissible congruence assertions. (Note that Σ effectively increments all the stack references.)

Therefore we can apply the induction hypothesis at c to deduce from (12) that

⊢ ΔΣ_{2} ⊗ (w ∼ first sp : α) ⊗ \overline{Γ_{0}} ⊗ (v_{I} ∼ r_{I} : Int-Loc)
⊃ (E[[c]])K[w/v_{I}]σ = (C[[c]]Γ_{1}K′_{1})σ′

(13)

If we take the Σ instance of this equation, we get

⊢ ΔΣ_{2}Σ ⊗ (w ∼ first sp : α)Σ ⊗
\overline{Γ_{0}}Σ ⊗ (v_{I} ∼ r_{I} : Int-Loc)Σ ⊃
{(E[[c]])K[w/v_{I}]σ}Σ = {(C[[c]]Γ_{1}K′_{1})σ′}Σ

(14)

The conclusion of (14) matches that of (9), so we can finish the proof of (9) by the cut rule if we can prove the verification condition

⊢ Δ ⊗ (v_{I} ∼ r_{I} : Int-Loc) ⊗ Γ ⊃

ΔΣ_{2}Σ ⊗

(w ∼ first sp : Int-Loc)Σ ⊗ \overline{Γ_{0}}Σ ⊗ (v_{I} ∼ r_{I} : Int-Loc)Σ

(15)

These are Hoare-style verification conditions which are tediously verified; the only tricky part is checking that the newly allocated cell does not alias any cell declared in Δ_{1} or Γ. Such a non-aliasing proof provides an answer to the old question of “what makes the free-list free?” [5].

6 Conclusions

We have presented a proof that a simple compiler correctly uses the static properties in its symbol table. The proof has several desirable features:

It allows us to prove the interconvertibility of the compiled code and the semantics of the source code, without becoming involved in model-theoretic details; previous proofs depended, at least on the surface, on details of models (bottom elements, etc.) There are details, of course, such as those involving aliasing, but these appear to reflect real details that compiler-writers must wrestle with, rather than choices in the mathematical superstructure.

Most of the proof is quite simple and can be thought of as a straightforward inductive proof that the compiled code and semantics are equal (as in [18]), except that the equality is now revealed as equality in some type that might be described as a polymorphic quotient of the type of command continuations. (∀Δ(Ccont /(Δ ⊗ Γ)) would be suggestive, though as yet unrigorous, notation). This is suggested by the proofs for compound commands.

The only difficult portions concern assignment and declaration, as these change the store and the symbol table. Nonetheless, these cases reduce to the proof of verification conditions similar to those for traditional imperative programs. This suggests that these proofs may likewise be systematized.

The proof is formulated to allow extension to compilers that perform optimizations which alter the use of the store (e.g. changing an Int-Loc to an Int if it is never assigned to after its declaration, or reclaiming storage). While our compiler does not actually perform such optimizations, a compiler which did so would still be provably correct using our induction hypotheses.

The proof technique presented here also has drawbacks:

The extension to procedures, in particular to first-class procedures in imperative languages, seems difficult, as such a procedure must be polymorphic in the constraints Δ corresponding to its call sites, which are of course not visible from the text where the procedure is defined. See [8] for a useful catalog of pathologies.

It is daunting in its complexity, even for the very simple analysis presented here. In some respects it reflects the practical limits of purely denotational reasoning. While most of the details (e.g. those concerning aliasing) represent real potential bugs, another framework might organize these in some better and more comprehensible way. In particular, dividing up the proof into denotational and operational portions, as in [19], might lead to much simpler and more obvious proofs.

Despite these difficulties, we conjecture that some form of these proofs will carry over to the flow analyses used in conventional compiler technology. We believe that the propositions used in these proofs are related to those considered in abstract interpretation [1]. We hope to be able to combine these techiques to get comprehensible proofs for more realistic optimizing compilers.

Acknowledgements

We thank the members of the Northeastern University Semantics Seminar, most notably Carl Woolf and Dino Oliva, for listening to us and making helpful comments as we presented and debugged several versions of the proof.

References

[1] Abramsky, S., and Hankin, C. (eds.) Abstract Interpretation of Declarative Languages, Ellis Horwood, Chichester, and John Wiley, New York, 1987.

[2] Appel, A.W., and Jim, T., “Continuation-Passing, Closure-Passing Style,” Conf. Rec. 16th ACM Symp. on Principles of Programming Languages (1989), 293–302.

[3] Church, A. “A formulation of the simple theory of types,” J. of Symbolic Logic 5 (1940), 56–68.

[4] Friedman, D.P., Wand, M., and Haynes, C.T., Essentials of Programming Languages, MIT Press, Cambridge, Massachusetts, and McGraw-Hill, New York, 1992.

[5] Halpern, J. Y., Meyer, A.R., and Trakhtenbrot, B. A., “The Semantics of Local Storage, or What Makes the Free-List Free?” Proc. 11th ACM Symp. on Principles of Programming Languages (1984), 245–257.

[6] Kelsey, R., and Hudak, P. “Realistic Compilation by Program Transformation,” Conf. Rec. 16th Ann. ACM Symp. on Principles of Programming Languages (1989), 281–292.

[7] Meyer, A.R. “What Is a Model of the Lambda Calculus?” Information and Control 52 (1982), 87–122.

[8] Meyer, A.R., and Sieber, K. “Towards Fully Abstract Semantics for Local Variables: Preliminary Report,” Conf. Rec. 15th ACM Symp. on Principles of Programming Languages (1988), 191–203.

[9] Montenyohl, M., and Wand, M., “Incorporating Static Analysis in a Semantics-Based Compiler,” Information and Computation 82 (1989) 151–184.

[10] Plotkin, G.D. “Call-by-Name, Call-by-Value and the λ-Calculus,” Theoret. Comp. Sci. 1 (1975) 125–159.

[11] Reynolds, J.C. “The Essence of Algol,” in Algorithmic Languages, (J. W. deBakker and J.C. van Vliet, eds.) North-Holland, Amsterdam, 1981, pp. 345–372.

[12] Schmidt, D.A. “Detecting Global Variables in Denotational Semantics,” ACM TOPLAS 7 (1985) 299–310.

[13] Suzuki, N. “Automatic Verification of Programs with Complex Data Structures,” dissertation, Stanford University, 1976.

[14] Wand, M. “Semantics-Directed Machine Architecture” Conf. Rec. 9th ACM Symp. on Principles of Prog. Lang. (1982), 234–241.

[15] Wand, M. “Deriving Target Code as a Representation of Continuation Semantics” ACM Trans. on Prog. Lang. and Systems 4, 3 (July, 1982) 496–517.

[16] Wand, M. “Loops in Combinator-Based Compilers,” Info. and Control 57, 2–3 (May/June, 1983), 148–164.

[17] Wand, M. “A Short Proof of the Lexical Addressing Algorithm,” Info. Proc. Letters 35 (1990), 1–5.

[18] Wand, M. “On the Correctness of Procedure Representations in Higher-Order Assembly Language” Proc. MFPS ’91 (S. Brookes, ed.) Springer Lecture Notes in Computer Science, to appear.

[19] Wand, M. and Oliva, D.P. “Proving the Correctness of Storage Representations,” submitted for publication.

[20] Wand, M., and Wang, Z.-Y. “Conditional Lambda-Theories and the Verification of Static Properties of Programs,” Northeastern University College of Computer Science Technical Report NU-CCS-90-24, November, 1990.