A Verified Run-Time Structure for Pure PreScheme^{∗}

Dino P. Oliva Mitchell Wand College of Computer Science Northeastern University 360 Huntington Avenue, 161CN Boston, MA 02115, USA oliva@corwin.ccs.northeastern.edu wand@flora.ccs.northeastern.edu

September 18, 1992

Abstract

This document gives a summary of activities under MITRE Corporation Contract Number F19628-89-C-0001. It gives an operational semantics of an abstract machine for Pure PreScheme and of its implementation as a run-time structure on an Motorola 68000 microprocessor. The relationship between these two models is stated formally and proved.

1 Introduction

The goal of this project was to develop a verified compiler for the Vlisp PreScheme programming language^{1}. PreScheme is a restricted dialect of Scheme. It is simpler than Scheme in the data types it supports, in its treatment of procedure objects, and because it makes very limited use of the run-time stack.

In this compiler, PreScheme is first translated by a series of source-to-source transformations [9] into a kernel language called Pure PreScheme. In [8], we presented a denotational semantics for Pure PreScheme, gave a compiler from Pure PreScheme to a byte-code like abstract machine, and proved the correctness of this compiler. We also presented a preliminary implementation of the compiler.

∗This report was sponsored by The MITRE Corporation, and is the Final Report for MITRE Contract Number F19628-89-C-001. The final preparation of the report was also supported in part by NSF and DARPA under NSF grants CCR-9002253 and CCR-9014603.

1Vlisp PreScheme is a descendent of the PreScheme programming language developed by Kelsey and Rees for the Scheme 48 run-time system[5]. While the two languages share many properties, they have developed independently since mid-1990.

In the course of developing the compiler, it became clear that the most important issue was choosing a representation for the various quantities manipulated by the abstract machine. The abstract machine was essentially a tree-manipulating system, but the manipulations it performed were highly restricted, so that efficient representations were possible.

During 1991–92, we developed an attractive methodology, based on the concept of storage layout relations, for formalizing these representation decisions. A storage layout relation is an inductively-defined relation between states of the concrete and abstract machines. This idea was introduced by Hannan [4] in the case where the portion of the state that was represented in this way was static. We extended the techniques of [4] to deal with dynamic state, as this is by far the more common (and interesting) case. Some preliminary work on this methodology was presented in [12]. In this report, we apply this methodology to the Pure PreScheme compiler.

This report is organized as follows: We first present the abstract machine for Pure PreScheme and its operational semantics. The abstract machine manipulates combinator terms that are essentially trees. (For details on the source language, see [8].) In the concrete machine, the abstract structures of the abstract machine are represented in a linear memory model. In Section 3, we outline this architecture and present a formalization of the relationship between the abstract and concrete machine states. In Section 4 we prove some basic properties of these relations. In Section 5, we present the operational semantics of the concrete machine, and in Section 6, we state the connection between the concrete machine and the source language, and present the proof in detail. Finally, in Section 7 we discuss our implementation, and in Section 8 we present some conclusions.

We use the term “run-time structure” to suggest the package of representation decisions that allow an abstract machine to be implemented on a given target machine: how the resources of the abstract machine are laid out and represented in memory. Thus our proof is a verification of the correctness of this design. We do not prove the correctness of the full implementation, as that would require a semantics of the target machine instruction set, a much more difficult task. However, in practice this seems not to be so difficult, as the operations of our concrete machine can be easily implemented once the representation is chosen. Nor do we deal with the issues concerning the representation of treelike abstract-machine code in a linear program store; some of the issues related to this are discussed in Section 3.2.5.

2 The Abstract Machine

The compiler for PurePreScheme produces code for an abstract machine consisting of a runtime environment, u, and a stack of stackable values, ζ, and a heap h.

Though the machine is defined denotationally, machine configurations are given an operational semantics by inheritance from the operational semantics (that is, the reduction behavior) of the lambda-calculus. The bytecode terms are carefully defined so that if π is a legal bytecode program, then πuζh reduces to a term π′u′ζ′h′ in some small number of reduction steps. Furthermore, since all these terms are in continuation-passing style, there is essentially only one such reduction that is possible. Therefore we can interpret this reduction sequence as a step in the operational semantics of the machine: ⟨π, u, ζ, h⟩ ⟹ ⟨π′, u′, ζ′, h′⟩.

The bytecodes π are given by the grammar:

π ::= (constant ϵπ)
| (fetch-local ιπ)
| (fetch-global ιπ)
| (goto π)
| (label π)
| (jmp νπ_{1} … π_{ν})
| (save-env π)
| (restore-env π)
| (update-store ιπ)
| (prim-apply νυπ)
| (restore-env/ignore π)
| (update-store/ignore ιπ)
| (prim-apply/ignore νυπ)
| (brf π_{1}π_{2})
| (add-to-env νπ)
| (add-to-env^{∗} π)
| (tail-call ν)
| (halt)
| (add-global-to-env^{∗} π)
| (closerecs (π_{1} … π_{n}) π)

The runtime display u is described by the following grammar:

u ::= emptydisplay | (extends_{r l}(v_{1} … v_{n})u′) | (extends_{r g} αu′)

The stack consists of a list of stackable values given by the following grammar:

v ::= ⟨proc, ⟨π, u_{0}⟩⟩
| ⟨env, u⟩
| ⟨int, n⟩
| ⟨bool, b⟩
| ⟨char, c⟩
| ⟨string, s⟩
| ⟨hptr, n⟩
| ⟨quote, d⟩

These values are procedures (closed in a global environment u_{0}, to be described later), environments, and other values, which we call immediate values. These are integers, booleans, characters, strings, pointers into the heap (Lvalues), and quotations. L-values are tagged integers. Quotations represent data returned by primitives for use only with other primitives (primitives like make-vector, vector-ref, etc).

The heap for the abstract machine consists of three components: a map from heap pointers (as above) to immediate values, an integer (representing a freelocation counter), and an unspecified third element. The first two components are used for ordinary mutable variables. The third component can be manipulated only by primitives (primitives like make-vector, vector-ref, etc); it plays a role analogous to that of the file system in a conventional language semantics. We use the notation h.1, h.2, and h.3 for the three components.

A program consists of a preamble, consisting of a sequence of add-global-to-env^{∗} instructions followed by a closerecs instruction, followed by a bytecode term π that does not contain any add-global-to-env^{∗} or closerecs instructions. The purpose of this preamble is to establish the invariants necessary for the proper operation of the rest of the machine. In this report we will be primarily concerned with the operation of the main program.

The operational semantics of each machine instruction is shown in Figure 1. If the machine state does not match any of the left-hand sides in Figure 1, then the machine goes into an error state and halts, returning the value ⟨error⟩. Similarly, if deref′ is given a second argument that is not of the form ⟨hptr, l⟩, the machine halts, returning ⟨error⟩. In Figure 1, we have used h′ as the variable ranging over heaps because this is the variable that will be used in our proofs, in which abstract-machine quantities typically appear on the right-hand sides of correspondence assertions, as in Section 3.

The machine halts normally by executing a halt instruction, returning the value ⟨ok, v⟩ for some value v.

2 THE ABSTRACT MACHINE 5

Abstract machine:

⟨(constant ϵπ), u, ζ, h′⟩ ⟹ ⟨π, u, (ϵ :: ζ), h′⟩
⟨(fetch-local ιπ), u, ζ, h′⟩ ⟹ ⟨π, u, (u(ι) :: ζ), h′⟩
⟨(fetch-global ιπ), u, ζ, h′⟩ ⟹ ⟨π, u, ((deref′ h′ u(ι)) :: ζ), h′⟩
⟨(goto π), u, ζ, h′⟩ ⟹ ⟨π, u, ζ, h′⟩
⟨(label π), u, ζ, h′⟩ ⟹ ⟨π, u, ζ, h′⟩
⟨(jmp νπ_{1} … π_{ν}), u, ⟨int, n⟩ :: ζ), h′⟩ ⟹ ⟨(list-ref n (π_{1} … π_{n}u)), u, ζ, h′⟩
⟨(save-env π), u, ζ, h′⟩ ⟹ ⟨π, u, (⟨env, u⟩ :: ζ), h′⟩
⟨(restore-env π), u, (v :: ⟨env, u′⟩ :: ζ), h′⟩ ⟹ ⟨π, u′, (v :: ζ), h′⟩
⟨(update-store ιπ), u, (v :: ζ), h′⟩ ⟹ ⟨π, u, (v :: ζ), (update u(i) v h′)⟩
⟨(prim-apply nυπ), u, (v_{1} :: …:: v_{n} :: ζ), h′⟩ ⟹ ⟨π, u, (w_{1} :: ζ), h′_{1}⟩

where (w_{1}, h′_{1}) = (apply-prim′ υ(v_{1} … v_{n})h′)

⟨(restore-env/ignore π), u, (⟨env, u′⟩ :: ζ), h′⟩ ⟹ ⟨π, u′, ζ, h′⟩
⟨(update-store/ignore ιπ), u, (v :: ζ), h′⟩ ⟹ ⟨π, u, ζ, (update u(i) v h′)⟩
⟨(prim-apply/ignore νυπ), u, ζ_{1}, h′⟩ ⟹ ⟨π, u, ζ, h′_{1}⟩

where ζ_{1} = (v_{1} :: …:: v_{ν} :: ζ) and (w_{1}, h′_{1}) = (apply-prim′ υ(v_{1} … v_{n})h′)

⟨(brf π_{1}π_{2}), u, (⟨bool, b⟩ :: ζ), h′⟩ ⟹ ⟨(choose b π_{1}π_{2}), u, ζ, h′⟩
⟨(add-to-env νπ), u, (v_{1} :: …:: v_{ν} :: ζ), h′⟩ ⟹ ⟨π, (extends_{r l} u (v_{1} … v_{ν})), ζ, h′⟩
⟨(add-to-env^{∗} π), u, (v :: ζ), h′⟩ ⟹ ⟨π, (extends_{r l} u (v)), ζ, h′⟩
⟨(tail-call ν), u, ζ_{1}, h′⟩ ⟹ ⟨π, (extends_{r l} u_{0} (v_{1} … v_{ν})), ⟨⟩, h′⟩

where ζ_{1} = (⟨proc, ⟨π, u_{0}⟩⟩ :: v_{1} :: …:: v_{ν} :: ζ)

⟨(halt), u, (v :: ζ), h′⟩ ⟹ ⟨ok, v⟩
⟨(add-global-to-env^{∗} π), u, (v :: ζ), h′⟩ ⟹

⟨π, (extends_{r g} u (new h′)), ζ, (update(new h′) v h′)⟩

⟨(closerecs (π_{1} … π_{n}) π), u, ζ), h′⟩ ⟹

⟨π, (fix(λu′ .(extends_{r l} u (⟨proc, ⟨π_{1}, u′⟩⟩ … ⟨proc, ⟨π_{n}, u′⟩⟩)))), ζ, h′⟩

Auxiliaries: (deref′ h ⟨hptr, l⟩) = (h.1)(⟨hptr, l⟩) (list-ref ν(ππ^{∗})) = ((ν = 0) → π, (list-ref (ν − 1)π^{∗}))

(choose b π π′) = (b → π, π′)

Figure 1: Operational Semantics of the Abstract Machine

3 Storage Layout

The concrete machine uses a store to represent the environment and stack of the abstract machine. It also has a heap which corresponds to the heap of the abstract machine. The concrete heap is like the abstract heap except that its Lvalues are untagged integers, and its first component contains immediate values in their concrete representation.

The concrete machine uses two pointers into the store, sp and up, to represent the stack and the environment; the way in which these pointers accomplish this task is the major subject of this section. Thus the state of the concrete machine is of the form ⟨π, up, sp, σ, h⟩.

In this section the representation of the abstract machine by the concrete machine is formalized. To aid in the intuition behind these formalisms, we will first give an informal sketch of the representation. We will then present the formal definitions.

The key to the representation is that any PreScheme program uses only a bounded amount of space. By analyzing the program, we may define two constants for that program. The first, N, is the total amount of environment space required by the program. The second, N_{0}, is the amount of space initially required by the environment for globals and procedure declarations. These constants are easily calculated (see Theorem 3) and are used for setting the initial parameters of the concrete machine.

3.1 Informal Presentation

We can take advantage of this by using locations 0 through N of the concrete machine’s store for the environment u, and the locations above N for the local stack ζ.

We can describe the representation pictorially as follows:

1. Stackable values (integers, booleans, characters, strings, procedures, environments). For efficiency purposes, runtime tags are not used. This restricts our correctness result but only for those programs that result in an error. All quantities are represented by a single machine word (i.e. one space in σ). Strings and procedures are represented by pointers into a static space; since all procedures in a PreScheme share the same environment, there is no need for a separate environment pointer in a procedure object. Environments need to be stacked, but they are not expressible; when stacked they are represented as pointers to the environment representation. As all other data is either immediate or a pointer to static space, these environment pointers are the only real “pointers” in the system (that is, they are the only references that can potentially dangle).

2. Runtime environment u. As all values are represented by 1 word in memory, this suggests that u be represented by locations 0 through up in σ:

up : u(0) ; u(1) ; …; 0

3. The local stack z. Since all values are represented by a single word in σ and that u ranges between 0 and N, a local stack ζ = (v_{1} :: v_{2} :: …:: v_{n} :: ⟨⟩) can be represented using σ as a stack growing upward from position N +1:

sp : v_{1} ; v_{2} ; …; v_{n} ; N

In the initial startup of the machine, up is started at −1 and the stack pointer sp starts at N, so that both the environment and stack are empty. The prelude to the program allocates globals with a sequence of add-global-to-env instructions, followed by a closerecs instruction. The effect of these instructions is to create an environment u_{0} in which all the global procedures are closed. At this point up has value N_{0}. This is the ground configuration which is used as a reference for all tail calls.

After the globals and procedures have been allocated, up will have value N_{0} and will not drop below this value for the remainder of program execution. This configuration is the ‘ground configuration’ as it is the configuration restored at tail call:

… stack space
sp = N
… environment space
up = N_{0} : π_{1} global procedures

(π_{2}) / …

a_{1} pointers to mutable global variables in heap

(a_{2}) / …

0  a_{n}

3.2 Formal Presentation

To formalize this representation, we will have one storage layout relation for each kind of data manipulated by the abstract and concrete machines. These are: immediate data, stackable values, stacks, environments, heaps, and programs. These will be defined by simultaneous induction. The definition of the relations is a relatively straightforward transcription of the data in the diagrams above; the primary difficulty is in guarding against off-by-one errors.

3.2.1 Relating Immediate Data

ϵ ≃ ϵ′ ⟺
either ϵ′ = ⟨int, n⟩ and ϵ = n
or  ϵ′ = ⟨bool, b⟩ and ϵ = b
or  ϵ′ = ⟨char, c⟩ and ϵ = c
or  ϵ′ = ⟨string, s⟩ and ϵ = s
or  ϵ′ = ⟨hptr, l⟩ and ϵ = l
or  ϵ′ = ⟨quote, d⟩ and ϵ = d

3.2.2 Relating Stackable Values

(σ, b) ⊧_{V} c ≃ v ⟺
either v = ⟨proc, ⟨π, u_{0}⟩⟩ and c = π
or  v = ⟨env, u⟩ and c ≤ b
and (σ, b) ⊧_{U} c ≃ u
or  c ≃ v

Here u_{0} denotes the environment at the end of the prelude; all procedures in a PreScheme program are closed in this environment, and are therefore mutually recursive.

The parameter b marks the upper boundary of environment space; the condition on environments ensures that no environment pointer is ever dangling. This parameter will almost always be up.

The last line refers to c and v as immediate data, as above.

3.2.3 Relating Pointers and Stacks

(σ, b) ⊧_{Z} ⟨p, p′⟩ ≃ ζ ⟺
either ζ = ⟨⟩ and p = p′
or  ζ = (z :: ζ′) and p > p′ and (σ, b) ⊧_{V} σ(p) ≃ z
and (σ, b) ⊧_{Z} ⟨p − 1, p′⟩ ≃ ζ′

Here the stack elements are in locations p′ + 1 through p, so p = p′ marks an empty stack. In the proof, p′ will always be N.

3.2.4 Relating Pointers and Environments

(σ, b) ⊧_{U} p ≃ u ⟺
either u = emptydisplay and p = −1
or  u = (extends_{r l}(v_{1} … v_{n})u′) and p ≤ up
and (σ, b) ⊧_{V} σ(p) ≃ v_{n} … (σ, b) ⊧_{V} σ(p − (n − 1))) ≃ v_{1}
and (σ, b) ⊧_{U} (p − n) ≃ u′
or  u = (extends_{r g} αu′) and p ≤ up
and σ(p) ≃ α
and (σ, b) ⊧_{U} (p − 1) ≃ u′

3.2.5 Relating Programs

Programs in the concrete and abstract machines differ only in the format of the literals embedded in them. The complete definition is shown in Figure 2.

We do not bother linearizing the code in the concrete machine. It would be relatively easy to extend the current proof to use a representation of the concrete-machine code in a linear store, along the lines of [12], since the program store is static. It would be a more substantial task to prove the correctness of the translator that converts from an abstract-machine program, which is tree-like in its structure, to a corresponding state of the program store. This program might be dubbed a linearizer or an assembler. Such an assembler-correctness proof would deal with the specifics of the translation process and would resemble in its specificity and level, the compiler-correctness proof of [8]. We have good ideas about how this proof should be structured, and we will report on this later, either in Oliva’s forthcoming Ph.D. thesis or a separate technical report.

3.2.6 Relating Heaps

As discussed above, the concrete machine’s heap also consists of three components. The first component maps untagged integers to immediate values in their concrete representation, the second component is an integer-valued free-storage counter, and the third component is the same as that for the abstract machine. Heaps correspond if their free-storage counters and third components agree, and if the allocated portions of their first components correspond:

h_{c} ≃ h_{a} ⟺
h_{a}.2 = h_{c}.2
and (∀i : 0 ≤ i ≤ h_{c}.2)(h_{c}.1(i) ≃ h_{a}.1(⟨hptr, i⟩))
and h_{a}.3 = h_{c}.3

3 STORAGE LAYOUT 10 π_{c} ≃ π_{a} ⟺

either π_{a} = (constant ϵ′π′_{a}) and π_{c} = (constant ϵπ′_{c})
and ϵ ≃ ϵ′ and π′_{c} ≃ π′_{a}
or  π_{a} = (fetch-local ιπ′_{a}) and π_{c} = (fetch-local ιπ′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (fetch-global ιπ′_{a}) and π_{c} = (fetch-global ιπ′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (goto π′_{a}) and π_{c} = (goto π′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (label π′_{a}) and π_{c} = (label π′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (jmp νπ_{a}_{1} … π_{a}_{ν}) and π_{c} = (jmp νπ_{c}_{1} … π_{c}_{ν})
and π_{c}_{1} ≃ π_{a}_{1} … and π_{c}_{ν} ≃ π_{a}_{ν}
or  π_{a} = (save-env π′_{a}) and π_{c} = (save-env π′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (restore-env π′_{a}) and π_{c} = (restore-env π′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (update-store ιπ′_{a}) and π_{c} = (update-store ιπ′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (prim-apply νυπ′_{a}) and π_{c} = (prim-apply νυπ′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (restore-env/ignore π′_{a}) and π_{c} = (restore-env/ignore π′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (update-store/ignore ιπ′_{a}) and π_{c} = (update-store/ignore ιπ′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (prim-apply/ignore νυπ′_{a}) and π_{c} = (prim-apply/ignore νυπ′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (brf π_{a}_{1}π_{a}_{2}) and π_{c} = (brf π_{c}_{1}π_{c}_{2})
and π_{c}_{1} ≃ π_{a}_{1} and π_{c}_{2} ≃ π_{a}_{2}
or  π_{a} = (add-to-env νπ′_{a}) and π_{c} = (add-to-env νπ′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (add-to-env^{∗} π′_{a}) and π_{c} = (add-to-env^{∗} π′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (tail-call ν) and π_{c} = (tail-call ν)
or  π_{a} = (halt) and π_{c} = (halt)
or  π_{a} = (add-global-to-env^{∗} π′_{a}) and π_{c} = (add-global-to-env^{∗} π′_{c})
and π′_{c} ≃ π′_{a}
or  π_{a} = (closerecs (π_{a}_{1} … π_{a}_{n}) π′_{a}) and π_{c} = (closerecs (π_{c}_{1} … π_{c}_{n}) π′_{c})
and π_{c}_{1} ≃ π_{a}_{1} … and π_{c}_{n} ≃ π_{a}_{n} and π′_{c} ≃ π′_{a}

Figure 2: Correspondence of concrete and abstract machine code 3.3 Relating the Abstract and Concrete Machines

We can now define the correspondence between abstract and concrete machine states.

Restating the discussion of initialization at the end of Section 3.1, the effect of the prelude is to establish the invariants

N_{0} ≤ up ≤ N ≤ sp

and

(σ, u_{0}) ⊧_{U} N_{0} ≃ u_{0}

The first invariant expresses the disjointness of the environment and stack spaces, and the second establishes the correct representation of the globals.

Definition 1 We say a concrete machine state ⟨π, up, sp, σ, h⟩ corresponds to an abstract machine state ⟨π′, u, ζ, h′⟩ (written ⟨π, up, sp, σ, h⟩ ≃ ⟨π′, u, ζ, h′⟩) if and only if the following conditions are satisfied:

1. π ≃ π′,

2. (σ, up) ⊧_{U} up ≃ u,

3. (σ, up) ⊧_{Z} (sp, N) ≃ ζ,

4. h ≃ h′

5. N_{0} ≤ up ≤ N ≤ sp, and

6. (σ, u_{0}) ⊧_{U} N_{0} ≃ u_{0}

4 Basic Properties of the Representation

Before proceeding, we state several lemmas that express the basic properties of these relations. These will be used continually in the proof.

Lemma 1 (Immediate Values) If c ≃ v as immediate values, then for all σ and b, (σ, b) ⊧_{V} c ≃ v.

Proof: Immediate from the definition of ⊧_{V}.

Definition 2 We say σ =_{[p,p′]} σ′ if p ≤ p′ and (∀x : p ≤ x ≤ p′)(σ(x) = σ′(x)).

Lemma 2 (Free-Storage Lemma) 1. If (σ, b) ⊧_{V} c ≃ v and σ =_{[0,b]} σ′ then (σ′, b) ⊧_{V} c ≃ v.

2. If (σ, b) ⊧_{Z} ⟨p, p′⟩ ≃ ζ and σ =_{[0,b]} σ′ and σ =_{[p′+1,p]} σ′ then (σ′, b) ⊧_{Z} ⟨p, p′⟩ ≃ ζ.

3. If (σ, b) ⊧_{U} p ≃ u and σ =_{[0,p]} σ′ then (σ′, b) ⊧_{U} p ≃ u.

Proof: By induction on the definitions of ⊧_{V} , ⊧_{Z}, and ⊧_{U}.

1. Given (σ, b) ⊧_{V} c ≃ v and σ =_{[0,b]} σ′, there are three cases we must consider:

(a) v = ⟨proc, ⟨π, u⟩⟩ and c = π If this is true, it is true regardless of σ hence (σ′, b) ⊧_{V} c ≃ v.

(b) v = ⟨env, u⟩ and c ≤ b and (σ, b) ⊧_{U} c ≃ u Given this and σ =_{[0,b]} σ′ then by induction we can conclude (σ′, b) ⊧_{U} c ≃ u and hence (σ′, b) ⊧_{V} c ≃ v.

(c) σ(p) = v.val If this is true, it is true regardless of σ hence (σ′, b) ⊧_{V} c ≃ v.

2. Given (σ, b) ⊧_{Z} ⟨p, p′⟩ ≃ ζ and σ =_{[0,b]} σ′ and σ =_{[p′+1,p]} σ′ there are two cases to consider:

(a) ζ = ⟨⟩ and p = p′ If this is true, it is true regardless of σ hence (σ′, b) ⊧_{Z} ⟨p, p′⟩ ≃ ζ.

(b) ζ = (z :: ζ′) and p > p′ and (σ, b) ⊧_{V} σ(p) ≃ z and (σ, b) ⊧_{Z} ⟨p − 1, p′⟩ ≃ ζ′

• Given (σ, b) ⊧_{V} σ(p) ≃ z and σ =_{[0,b]} σ′ and σ(p) = σ′(p) then by induction we can conclude (σ′, b) ⊧_{V} σ′(p) ≃ z.

• Given (σ, b) ⊧_{Z} ⟨p − 1, p′⟩ ≃ ζ′ then by induction we can conclude (σ′, b) ⊧_{Z} ⟨p − 1, p′⟩ ≃ ζ′.

hence (σ′, b) ⊧_{Z} ⟨p, p′⟩ ≃ ζ.

3. Given (σ, b) ⊧_{U} p ≃ u and σ =_{[0,b]} σ′ there are three cases to consider:

(a) u = emptydisplay and p = −1 If this is true, it is true regardless of σ hence (σ′, b) ⊧_{U} p ≃ u.

(b) u = (extends_{r l}(v_{1} … v_{n})u′) and p ≤ b and (σ, b) ⊧_{V} σ(p) ≃ v_{n} … (σ, up) ⊧_{V} b ≃ σ(p − (n − 1)))v_{1} and (σ, b) ⊧_{U} (p − n) ≃ u′

• Given (σ, b) ⊧_{V} σ(p) ≃ v_{n} … (σ, b) ⊧_{V} σ(p − (n − 1)) ≃ v_{1}, p ≤ b and σ =_{[0,b]} σ′ then by induction we can conclude (σ′, b) ⊧_{V} σ′(p) ≃ v_{n} … (σ′, b) ⊧_{V} σ′(p − (n − 1)) ≃ v_{1}.

• Given (σ, b) ⊧_{U} (p − n) ≃ u′ and (p − n) < p ≤ b then by induction we can conclude (σ′, b) ⊧_{U} (p − n) ≃ u′.

hence (σ′, b) ⊧_{U} p ≃ u.

(c) u = (extends_{r g} αu′) and p ≤ b and σ(p) ≃ α and (σ, b) ⊧_{U} (p − 1) ≃

u′ • Given σ(p) ≃ α, p ≤ b and σ =_{[0,b]} σ′ we can conclude σ′(p) ≃ α.

• Given (σ, b) ⊧_{U} (p − 1) ≃ u′ and (p − 1) < p ≤ b then by

induction we can conclude (σ′, b) ⊧_{U} (p − 1) ≃ u′. hence (σ′, b) ⊧_{U} p ≃ u.

□

Lemma 3 If (σ, b) ⊧_{V} c ≃ v and b ≤ b′ then (σ, b′) ⊧_{V} c ≃ v.

Proof: The parameter b is only used in the case (σ, b) ⊧_{V} c ≃ ⟨env, u⟩. In that case, c ≤ b ≤ b′, so (σ, b′) ⊧_{V} c ≃ ⟨env, u⟩. The rest of the proof follows by tedious induction.

□

Lemma 4 If (σ, b) ⊧_{U} p ≃ u then (σ, b) ⊧_{V} σ(p − ι) ≃ u(ι).

Proof: by induction on ι.

1. Given ι = 0 and (σ, b) ⊧_{U} p ≃ u there are three cases we must consider:

• u = emptydisplay and p = −1 hence an error occurs and nothing is guaranteed.

• u = (extends_{r l}(v_{1} … v_{n})u′) and (σ, b) ⊧_{V} σ(p) ≃ v_{n} … (b, σ) ⊧_{V} σ(p − (n − 1))) ≃ v_{1} and (σ, b) ⊧_{U} (p − n) ≃ u′ hence u(0) = v_{n} and (σ, b) ⊧_{V} σ(p − 0) ≃ u(0)

• u = (extends_{r g} αu′) and σ(p) ≃ α and (σ, b) ⊧_{U} (p − 1) ≃ u′ hence u(0) = α and (σ, b) ⊧_{V} σ(p − 0) ≃ u(0)

2. Assume induction for 0 ≤ ι < N and prove for N. Again there are three cases we must consider:

• u = emptydisplay and p = −1 hence an error occurs and nothing is guaranteed.

• u = (extends_{r l}(v_{1} … v_{n})u′) and (σ, b) ⊧_{V} σ(p) ≃ v_{n} … (σ, b) ⊧_{V} σ(p − (n − 1))) ≃ v_{1} and (σ, up) ⊧_{U} (p − n) ≃ u′ hence if N ≤ n then u(N) = v_{N} and (σ, b) ⊧_{V} σ(p − (N − 1)) ≃ u(N) otherwise if N > n then by induction we have (σ, b) ⊧_{V} σ(p − (N − n)) ≃ u′(N − n).

• u = (extends_{r g} αu′) and σ(p) ≃ α and (σ, b) ⊧_{U} (p − 1) ≃ u′ hence by induction we have (σ, b) ⊧_{V} σ(p − 1) ≃ u′(N − 1).

□

5 The Concrete Machine

We define the operational semantics of the concrete machine by considering the representation of each possible abstract machine state, so that the concrete machine simulates the behavior of the abstract machine. That is, if C_{1} ≃ A_{1} and A_{1} ⟹ A_{2}, then we want the concrete machine to send C_{1} to some state C_{2} such that C_{2} ≃ A_{2}.

In general, this will not be possible, since the concrete machine does not have tags to distinguish different data types. The abstract machine uses these tags to distinguish an error state. Since the concrete machine cannot mimic this behavior, we will require the concrete machine to behave correctly only if A_{2} is not an error state. If A_{2} is an error state, the behavior of the concrete machine is unspecified. Similarly, if A_{1} is an abstract-machine state with some arbitrary program π, executing it may cause other errors, such as underflowing the stack or overflowing the environment. In general, we will only be able to perform this simulation when A_{1} is a state arising from reducing a properly compiled Pure PreScheme program.

It seems possible to derive the behavior of the concrete machine from this specification, but we have no formal way of doing this at present. Instead, we developed the operational semantics of the concrete machine informally, using the specification for guidance, and proved its correctness post hoc. This proof will constitute the main part of this report.

The operational semantics of the concrete machine is shown in Figure 3. apply-prim is unspecified, but it must satisfy the constraint that when apply-prim and apply-prim′ are applied to congruent arguments, they return congruent immediate values and congruent heaps.

6 Main Theorem

As suggested previously, the concrete and abstract machines are related by a property like the following:

Let A_{1} and A_{2} be states of the abstract machine and C_{1} and C_{2} be states of the concrete machine. If C_{1} ≃ A_{1}, A_{1} ⟹ A_{2}, and C_{1} ⟹ C_{2}, then C_{2} ≃ A_{2}.

Unfortunately, this is impossible, since arbitrary states A_{1} of the abstract machine may break the concrete machine by making the environment grow too large, by putting environments in places where the values are required to be expressible, etc. However this result does hold where A_{1} is a state that arises when the abstract machine is started with a correctly compiled Pure PreScheme program.

6 MAIN THEOREM 15

Concrete machine:

⟨(constant ϵπ), up, sp, σ, h⟩ ⟹ ⟨π, up, sp +1, σ[ϵ/ sp +1], h⟩
⟨(fetch-local ιπ), up, sp, σ, h⟩ ⟹ ⟨π, up, sp +1, σ[(lookup ι up σ)/sp + 1], h⟩
⟨(fetch-global ιπ), up, sp, σ, h⟩ ⟹ ⟨π, up, sp +1, σ[(deref h (lookup ι up σ))/sp + 1], h⟩
⟨(goto π), up, sp, σ, h⟩ ⟹ ⟨π, up, sp, σ, h⟩
⟨(label π), up, sp, σ, h⟩ ⟹ ⟨π, up, sp, σ, h⟩
⟨(jmp νπ_{1} … π_{ν}), up, sp, σ, h⟩ ⟹ ⟨(list-ref σ(sp) (π_{1} … π_{ν})), up, sp, σ, h⟩
⟨(save-env π), up, sp, σ, h⟩ ⟹ ⟨π, up, sp +1, σ[up /sp + 1], h⟩
⟨(restore-env π), up, sp, σ, h⟩ ⟹ ⟨π, σ(sp −1), sp −1, σ[σ(sp)/sp − 1], h⟩
⟨(update-store ιπ), up, sp, σ, h⟩ ⟹ ⟨π, up, sp, σ, (update σ(up −ι) σ(sp) h)⟩
⟨(prim-apply νυπ), up, sp, σ, h⟩ ⟹ ⟨π, up, sp −(ν − 1), σ[w_{1}/ sp −(ν − 1)], h_{1}⟩

where (w_{1}, h_{1}) = (apply-prim υ (collect σ sp ν) h)

⟨(restore-env/ignore π), up, sp, σ, h⟩ ⟹ ⟨π, σ(sp), sp −1, σ, h⟩
⟨(update-store/ignore ιπ), up, sp, σ, h⟩ ⟹ ⟨π, up, sp −1, σ, (update σ(up −ι) σ(sp))⟩
⟨(prim-apply/ignore νυπ), up, sp, σ, h⟩ ⟹ ⟨π, up, sp −ν, σ, h_{1}⟩

where (w_{1}, h_{1}) = (apply-prim υ (collect σ sp ν) h)

⟨(brf π_{1}π_{2}), up, sp, σ, h⟩ ⟹ ⟨(choose σ(sp) π_{1}π_{2}), up, sp −1, σ, h⟩
⟨(add-to-env νπ), up, sp, σ, h⟩ ⟹ ⟨π, (up +ν), (sp −ν), (copy σν(up +1) sp), h⟩
⟨(add-to-env^{∗} π), up, sp, σ, h⟩ ⟹
⟨π, up +1, sp −1, (σ[σ(sp)/ up +1]), h⟩
⟨(tail-call ν), up, sp, σ, h⟩ ⟹ ⟨σ(sp), (N_{0} + ν), (N − 1), σ_{1}, h⟩

where σ_{1} = (copy σ ν (N_{0} + 1) (sp −1))

⟨(halt), up, sp, σ, h⟩ ⟹ ⟨ok, σ(sp)⟩
⟨(add-global-to-env^{∗} π), up, sp, σ, h⟩ ⟹

⟨π, up +1, sp −1, (σ[(new h)/(up +1)]), (update (new h) σ(sp) h)⟩

⟨(closerecs (π_{1} … π_{n}) π), up, sp, σ, h⟩ ⟹ ⟨π, up +n, sp, σ_{1}, h⟩

where σ_{1} = (spread σ(up +n) (π_{1} … π_{n}))

Auxiliaries: (deref h l) = (h.1)(l)

(list-ref ν(ππ^{∗})) = (ν = 0) → π, (list-ref (ν − 1)π^{∗})

(choose b ππ′) = (b → π, π′)(lookup ι up σ) = σ(up −ι) (copy σ ν d s) = (ν = 0) → σ, (copy σ[σ(s)/d] (ν − 1) (d + 1) (s − 1))

(spread σ ν ⟨⟩) = σ

(spread σ ν (v :: v^{∗})) = (spread σ[v/ν] (ν − 1) v^{∗})
(collect σi 0) = ⟨⟩

(collect σi ν) = σ(i) :: (collect σ (i − 1) (ν − 1)) Figure 3: Operational Semantics of the Concrete Machine

To make this connection, we need to recall the main theorem from [8]. That report introduced a compiler function CE, which took a Pure PreScheme program, and a symbol table, and produced an abstract machine program π which took a display u, a stack ζ, and a heap h and produced an answer. The semantics of Pure PreScheme programs was expressed with a valuation E which took a program p, an environment ρ, and a heap h to an answer. These valuations were related by the main theorem of [8]:

Theorem 1 (Compiler Correctness) If p is a Pure PreScheme program and h_{0} the empty heap, then

(CE[[p]]∅) emptydisplay h_{0} = E[[p]]∅h_{0}

Pure Prescheme has evolved somewhat since the proof in [8] was done. These changes are summarized as follows:

• The simple form choose has been modified to reflect the same syntax as the Scheme case statement. While the semantics remain the same, this change allows Pure PreScheme programs to be executed directly by Scheme implementations.

• The tail recursive forms let and let ∗ have been added as simple forms. The semantics of these two new syntactic forms is based upon the semantics of the pre-existing tail recursive forms and are straightforward.

• The simple form case, formerly choose, has been added as a tail recursive form. Similarly, the semantics of this new form is based upon the semantics of the pre-existing simple form and is straightforward.

The changes to the language are minor but greatly enhance its utility. The added symmetry in the syntax makes it more intuitive for programmers to work with while the ability to execute Pure PreScheme programs in Scheme greatly facilitates program development.

The proof of Theorem 1 requires only minor changes to account for these modifications. The inductive hypotheses used in the proof remain the same. The only changes in the proof are the addition of two cases in the proof of equivalence of simple forms and compiled simple forms, and one case in the equivalence of tail-recursive forms and compiled tail recursive forms. These new cases follow the same form as the previous cases and are easy to show; the proof for the simple-expression let may be found in Appendix A. We now use the main theorem with confidence that it holds for the existing version of Pure PreScheme.

Recall that answers are either of the form ⟨ok, v⟩ or ⟨error⟩. We can state the following corollary to the Compiler Correctness Theorem:

Theorem 2 (Correctness of the Abstract Machine) If E[[p]]∅h_{0} = ⟨ok, v⟩, then in the abstract machine

⟨CE[[p]]∅, emptydisplay, ⟨⟩, h_{0}⟩ ⟹^{∗} ⟨ok, v⟩

Proof: If E[[p]]∅h_{0} = ⟨ok, v⟩, then (CE[[p]]∅) emptydisplay h_{0}. But the abstract machine simulates a quasi leftmost reduction sequence, which is always normalizing[1]. So the abstract machine must eventually reduce to ⟨ok, v⟩. □

Note that for type-checked PreScheme programs, such as the Scheme 48 Virtual Machine, these restrictions are moot, because the typing rules guarantee that the program will never reach an error state.

In addition to this basic result, we will need the following lemma about the behavior of the abstract machine on validly compiled Pure PreScheme programs:

Theorem 3 (Bounded Space) If p is a valid Pure PreScheme program, then there exist integers N_{0} and N such that for any state ⟨π, u, ζ, h⟩ in the computation sequence of ⟨CE[[p]]∅, emptydisplay, ⟨⟩, h_{0}⟩, N_{0} ≤ |dom(u)| ≤ N.

Proof: (Sketch) According to the grammar in [8], a Pure PreScheme program p must consist of a setof global simple declarations followed by a set of local procedure declarations followed by a tail-recursive expression. Let N_{0} be total number of global simple declarations and local procedure declarations, and let N be N_{0} plus the deepest lexical depth in the program. Since all procedures are closed in the global environment, which has N_{0} elements, it must be that N_{0} ≤ |dom(u)|; the usual argument about static scoping establishes |dom(u)| ≤ N. A completely formal proof would have to consider the details of the syntax of Pure PreScheme and the compiler. This would be exhaustive but probably unenlightening [3]. □

Let conc be the operation that converts an abstract machine program to a concrete machine program by removing the tags on the operands of all the constant instructions, so for all abstract-machine programs π, conc(π) ≃ π. Now we can state the main theorem:

Theorem 4 (Main Theorem) If p is a Pure PreScheme program, and E[[p]]∅h_{0} = ⟨ok, v⟩, where v is immediate data, then there exist values of N_{0} and N such that

⟨conc(CE[[p]]∅), −1, N, σ_{0}, h_{0}⟩ ⟹^{∗} ⟨ok, v_{c}⟩

and v_{c} ≃ v.

Proof: Choose N_{0} and N as in Theorem 3. Let A_{k} and C_{k} denote the states of the abstract and concrete machines, respectively, after k steps. We will show that for all sufficiently large k, either C_{k} ≃ A_{k} or both machines halt with corresponding answers.

We observe that the programs for both the concrete and abstract machines begin with a sequence of add-global-to-env^{∗} instructions, followed by a closerecs instruction. These instructions establish the invariant that C_{k} ≃ A_{k}. Let k_{0} be the number of steps to execute these instructions. We then show the following:

For all k ≥ k_{0}, C_{k} ≃ A_{k}.

For the basis, we must establish that C_{k_{0}} ≃ A_{k_{0}}. We defer this to the end of the proof.

For the induction case, we must show that if C_{k} ≃ A_{k}, then C_{k+1} ≃ A_{k+1}. We do this by analysis of each instruction. In each case, we assume that ⟨π, up, sp, σ, h⟩ ≃ ⟨π′, u, ζ, h′⟩, and therefore that

1. π ≃ π′,

2. (σ, up) ⊧_{U} up ≃ u,

3. (σ, up) ⊧_{Z} (sp, N) ≃ ζ,

4. h ≃ h′

5. N_{0} ≤ up ≤ N ≤ sp, and

6. (σ, u_{0}) ⊧_{U} N_{0} ≃ u_{0}

We proceed by cases on the form of the conclusion that π ≃ π′.

1. Assume we have

⟨(constant ϵπ), up, sp, σ, h⟩ ≃ ⟨(constant ϵ′π′), u, ζ, h′⟩

We must show that

⟨π, up, sp +1, σ′, h⟩ ≃ ⟨π′, u, ϵ :: ζ, h′⟩

where σ′ = σ[ϵ/ sp +1]. We consider each of the required conditions for ≃ in turn:

(a) π ≃ π′ by the definition of ≃ for programs.

(b) We have (σ, up) ⊧_{U} up ≃ u. Since sp > up, we have by lemma 2.2 that (σ′, up) ⊧_{U} up ≃ u.

(c) Since ϵ and ϵ′ are immediate data, we have by lemma 1 that (σ′, up) ⊧_{V} ϵ ≃ ϵ′. Since (σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ ζ, then by lemma 2.3, (σ′, up) ⊧_{Z} ⟨sp, N⟩ ≃ ζ. Therefore (σ′, up) ⊧_{Z} ⟨sp +1, N⟩ ≃ (ϵ′ :: ζ)

(d) h ≃ h′ by assumption.

(e) N_{0} ≤ up ≤ N ≤ sp, so N_{0} ≤ up ≤ N ≤ sp +1

(f) (σ′, u_{0}) ⊧_{U} N_{0} ≃ u_{0} is true by lemma 2.2.

Thus, for each case, we will have six conditions to verify. For the rest of the proof, we will omit those conditions that are verified by arguments like those here, and include the verification only of the conditions pertaining to changed components of the abstract machine (e.g. ζ here), or of those conditions that are dangerous (i.e., those that require more delicate arguments). In most cases that will leave only one or two conditions to verify.

2. Assume we have ⟨(fetch-local ιπ), up, sp, σ, h⟩ ≃ ⟨(fetch-local ιπ′), u, ζ, h′⟩

We must show that

⟨π, up, sp +1, σ′, h⟩ ≃ ⟨π′, u, (u(ι) :: ζ), h′⟩

where σ′ = σ[(lookup ι up σ)/ sp +1].

We need to show that (σ′, up) ⊧_{Z} ⟨sp +1, N⟩ ≃ (u(ι) :: ζ). We know from the assumption that (σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ ζ, and therefore (σ′, up) ⊧_{Z} ⟨sp, N⟩ ≃ ζ. By the definition of ⊧_{Z}, it will suffice to show that (σ′, up) ⊧_{V} σ′(sp +1) ≃ u(ι). Now, σ′(sp +1) = (lookup ι up σ) = σ(up −ι) = σ′(up −ι), so it will suffice to show that (σ′, up) ⊧_{V} σ′(up −ι) ≃ u(ι). But this follows by lemma 2.2 from that fact that (σ′, up) ⊧_{U} up ≃ u.

3. Assume we have ⟨(fetch-global ιπ), up, sp, σ, h⟩ ≃ ⟨(fetch-global ιπ′), u, ζ, h′⟩

We must show that

⟨π, up, sp +1, σ′, h⟩ ≃ ⟨π, u, ((deref′ h′ (u(ι))) :: ζ), h′⟩

where σ′ = σ[(deref h (lookup ι up σ))/sp + 1].

We have (σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ ζ, and therefore (σ′, up) ⊧_{Z} ⟨sp, N⟩ ≃ ζ. So we need only show that (σ′, up) ⊧_{V} (deref h (lookup ι up σ)) ≃ (deref′ h′ (u(ι))) But this follows immediately from the definition of congruent heaps.

4. Assume we have ⟨(goto π), up, sp, σ, h⟩ ≃ ⟨(goto π′), u, ζ, h′⟩

We must show that

⟨π, up, sp, σ, h⟩ ≃ ⟨π′, u, ζ, h′⟩

All the conditions follow immediately.

5. The case of label is the same as goto.

6. Assume we have

⟨(jmp νπ_{1} … π_{ν}), up, sp, σ, h⟩ ≃ ⟨(jmp νπ′_{1} … π′_{ν}), u, (⟨int, n⟩ :: ζ), h′⟩

We must show that

⟨(list-ref σ(sp) (π_{1} … π_{ν}), up, sp, σ, h⟩ ≃ ⟨(list-ref n (π′_{1} … π′_{ν})), u, ζ, h′⟩

We have (σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ (⟨int, n⟩ :: ζ), so (σ, up) ⊧_{V} σ(sp) ≃ ⟨int, n⟩. Therefore, by the definition of ⊧_{V}, we have σ(sp) = n. Hence if (list-ref σ(sp) (π_{1} … π_{ν})) = π_{j}, then (list-ref n (π′_{1} … π′_{ν})) = π′_{j}, and π_{j} ≃ π′_{j} by assumption.

7. Assume we have ⟨(save-env π), up, sp, σ, h⟩ ≃ ⟨(save-env π′), u, ζ, h′⟩

We must show that

⟨π, up, sp +1, σ′, h⟩ ≃ ⟨π′, u, (⟨env, u⟩ :: ζ), h′⟩

where σ′ = σ[up /sp + 1]. We check the requirements:

We know by that (σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ ζ, so (σ′, up) ⊧_{Z} ⟨sp, N⟩ ≃ ζ. Similarly, (σ, up) ⊧_{U} up ≃ u, so (σ′, up) ⊧_{U} up ≃ u as well. Hence, by the definition of ⊧_{V}, (σ′, up) ⊧_{V} up ≃ ⟨env, υ⟩. Therefore, since σ′(sp +1) = up, (σ′, up) ⊧_{Z} ⟨sp +1, N⟩ ≃ (⟨env, u⟩ :: ζ), as desired.

8. Assume we have

⟨(restore-env π), up, sp, σ, h⟩ ≃ ⟨(restore-env π′), u, (v :: ⟨env, u′⟩ :: ζ), h′⟩

We must show that

⟨π, σ(sp −1), sp −1, σ′, h⟩ ≃ ⟨π′, u′, (v :: ζ), h′⟩

where σ′ = σ[σ(sp)/sp − 1]

(σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ (v :: ⟨env, u′⟩ :: ζ). Hence (σ, up) ⊧_{V} σ(sp −1) ≃ ⟨env, u′⟩, and therefore (σ, up) ⊧_{U} σ(sp −1) ≃ u′.

(σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ (v :: ⟨env, u′⟩ :: ζ). Therefore (σ, up) ⊧_{V} σ(sp) ≃ v. Since σ′(sp −1) = σ(sp), it follows that (σ, up) ⊧_{V} σ′(sp −1) ≃ v, so by lemma 2.1, (σ′, up) ⊧_{V} σ′(sp −1) ≃ v. Also, by lemma 2.3, we have (σ′, up) ⊧_{Z} ⟨sp −2, N⟩ ≃ ζ. Therefore, by the definition of ⊧_{Z}, we have (σ′, up) ⊧_{Z} ⟨sp −1, N⟩ ≃ (v :: ζ)

9. Assume we have

⟨(update-store ιπ), up, sp, σ, h⟩ ≃ ⟨(update-store ιπ′), u, (v :: ζ), h′⟩ We must show that

⟨π, up, sp, σ, (update σ(up −ι) σ(sp) h)⟩ ≃ ⟨π′, u, (v :: ζ), (update u(i) v h′)⟩

By assumption, we have (σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ (v :: ζ), so (σ, up) ⊧_{V} sp ≃ v. Since (σ, up) ⊧_{U} up ≃ u, we have (σ, up) ⊧_{V} σ(up −i) ≃ u(i). Also by assumption we have h ≃ h′. Therefore it follows that (update σ(up −ι) σ(sp) h) ≃ (update u(i) v h).

10. Assume we have

⟨(prim-apply n v π), up, sp, σ, h⟩ ≃ ⟨(prim-apply n v′ π′), u, ζ_{1}, h′⟩

where ζ_{1} = (v_{1} :: …:: v_{n} :: ζ). We must show that

⟨π, up, sp −n + 1), σ′, h_{1}⟩ ≃ ⟨π′, u, (w′_{1} :: ζ), h′_{1}⟩

where

            (w_{1}, h_{1}) = apply-prim v (collect σ sp n)h

σ′ = σ[w_{1}/ sp −n + 1]
(w′_{1}, h′_{1}) = apply-prim′ v′ (v_{1} :: …:: v_{n} :: ⟨⟩)

(σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ (v_{1} :: …:: v_{n} :: ζ), so by the definition of ⊧_{Z} we have

(σ, up) ⊧_{V} σ(sp) ≃ v_{1}
(σ, up) ⊧_{V} σ(sp −1) ≃ v_{2}
…
(σ, up) ⊧_{V} σ(sp −n + 1) ≃ v_{n}
(σ, up) ⊧_{Z} ⟨sp −n, N⟩ ≃ ζ

Furthermore, (collect σ sp n) = (σ(sp) … σ(sp −n + 1)), so the arguments to apply-prim and apply-prim′ are componentwise congruent. Therefore we have h_{1} ≃ h′_{1} and w_{1} ≃ w′_{1} (as immediate data). So (σ′, up) ⊧_{V} w_{1} ≃ w′_{1}.

Now, σ′(sp −n + 1) = w_{1}, so (σ′, up) ⊧_{V} σ′(sp −n + 1) ≃ w′_{1}, and furthermore (σ′, up) ⊧_{Z} ⟨sp −n, N⟩ ≃ ζ, so we conclude that (σ′, up) ⊧_{Z} ⟨sp −n + 1, N⟩ ≃ (w_{1} :: ζ), as desired.

11. The cases for restore-env/ignore, update-store/ignore, and prim-apply/ignore are similar to the corresponding value-returning instructions.

12. Assume we have

⟨(brf π_{1} π_{2}), up, sp, σ, h⟩ ≃ ⟨(brf π′_{1} π′_{2}), u, (⟨bool, b⟩ :: ζ), h′⟩

We must show that

⟨(choose σ(sp) π_{1} π_{2}), up, sp −1, σ, h⟩ ≃ ⟨(choose b π′_{1} π′_{2}), u, ζ, h′⟩

π_{1} ≃ π′_{1} and π_{2} ≃ π′_{2} and (σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ (⟨bool, b⟩ :: ζ). Therefore (σ, up) ⊧_{V} sp ≃ ⟨bool, b⟩, so σ(sp) = b. Hence (choose σ(sp) π_{1}π_{2}) ≃ (choose b π′_{1}π′_{2})

(σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ (v :: ζ). Therefore (σ, up) ⊧_{Z} ⟨sp −1, N⟩ ≃ ζ

13. Assume we have ⟨(add-to-env νπ), up, sp, σ, h⟩ ≃ ⟨(add-to-env νπ′), u, (v_{1} :: …:: v_{ν} :: ζ), h′⟩

We must show that

⟨π, (up +ν), (sp −ν), σ′, h⟩ ≃ ⟨π′, u′, ζ, h′⟩

where σ′ = (copy σ ν (up +1) sp) and u′ = (extends_{r l} u (v_{1} … v_{ν}))

(σ, up) ⊧_{U} up ≃ υ and (σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ (v_{1} :: …:: v_{ν} :: ζ). Therefore for 1 ≤ j ≤ ν, we have (σ, up) ⊧_{V} σ(sp −j + 1) ≃ v_{j}. By the definition of copy we have σ′(up +j) = σ(sp −j + 1), so (σ, up) ⊧_{V} σ′(up +j) ≃ v_{j}. Since σ and σ’ agree up to up, we get (σ′, up) ⊧_{V} σ′(up +j) ≃ v_{j}, so by the definition of ⊧_{V} we have (σ′, up +ν) ⊧_{V} σ′(up +j) ≃ v_{j}. So, by the definition of ⊧_{U}, (σ′, up +ν) ⊧_{U} (up +ν) ≃ (extends_{r l} u (v_{1} … v_{ν}))

(σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ (v_{1} :: …:: v_{ν} :: ζ). Hence (σ′, up) ⊧_{Z} ⟨sp −ν, N⟩ ≃ ζ, and therefore (σ′, up +ν) ⊧_{V} ⟨sp −ν, N⟩ ≃ ζ.

Last, we must show that up +ν ≤ N. By Theorem 3, we know that |dom(extends_{r l} u (v_{1} … v_{ν}))| ≤ N. But the left-hand side of this inequality is equal to up +ν.

14. The case of add-to-env^{∗} is similar to add-to-env, but simpler since it adds only a single item to the environment.

15. Assume we have ⟨(tail-call ν), up, sp, σ, h⟩ ≃ ⟨(tail-call ν), u, (⟨proc, ⟨π, u_{0}⟩⟩ :: v_{1} :: …:: v_{ν} :: ζ), h′⟩

We must show that

⟨σ(sp), (N_{0} + ν), (N − 1), s_{1}, h⟩ ≃ ⟨π, (extends_{r l} u_{0} (v1 … v_{ν})), ⟨⟩, h′⟩

where σ_{1} = (copy σ ν (N_{0} + 1) (sp −1))

(a) (σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ (⟨proc, ⟨π, u⟩⟩ :: v_{1} :: …:: v_{ν} :: ζ). Therefore σ(sp) = π, by the definition of ⊧_{Z}.

(b) We calculate:

(σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ (⟨proc, ⟨π, u⟩⟩ :: v_{1} :: …:: v_{ν} :: ζ) assumption
for 1 ≤ j ≤ ν, (σ, up) ⊧_{V} σ(sp −j) ≃ v_{j}  definition of ⊧_{Z}
for 1 ≤ j ≤ ν, σ_{1}(N_{0} + 1 + j) = σ(sp −j)  definition of copy
for 1 ≤ j ≤ ν, (σ, up) ⊧_{V} σ_{1}(N_{0} + 1 + j) ≃ v_{j}  substituting equals for equals
for 1 ≤ j ≤ ν, (σ, N_{0}) ⊧_{V} σ_{1}(N_{0} + 1 + j) ≃ v_{j}  v_{j} are all expressed values
for 1 ≤ j ≤ ν, (σ_{1}, N_{0}) ⊧_{V} σ_{1}(N_{0} + 1 + j) ≃ v_{j}  lemma 2.1
(σ, N_{0}) ⊧_{U} N_{0} ≃ u_{0}  assumption
(σ_{1}, N_{0}) ⊧_{U} N_{0} ≃ u_{0}  lemma 2.2
(σ_{1}, N_{0}) ⊧_{U} N_{0} + ν ≃ (extends_{r l} u_{0} (v1 … v_{ν}))  definition of ⊧_{U}
(σ_{1}, N_{0} + ν) ⊧_{U} N_{0} + ν ≃ (extends_{r l} u_{0} (v1 … v_{ν}))  padding lemma

We know that the v_{j} are all expressed values because otherwise the state A_{k+1} = ⟨π, (extends_{r l} u_{0} (v1 … v_{ν})), ⟨⟩, h′⟩ would not be a legal abstract-machine state, which would contradict the assumption that the A_{k} are all legal states.

(c) (σ′, up) ⊧_{Z} ⟨N − 1, N⟩ ≃ ⟨⟩

16. Assume we have ⟨(halt), up, sp, σ, h⟩ ≃ ⟨(halt), u, (v :: ζ), h′⟩

We must show that σ(sp) ≃ v. Now, from the statement of the theorem, v must be immediate data, so the required conclusion follows immediately from (σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ (v :: ζ).

17. Last, if the state ⟨π, u, ζ, h′⟩ of the abstract machine does not match the left-hand side of any of the rules of section 2, then the abstract machine goes to an error state. This contradicts the assumptions of the theorem, so this case can never arise.

This completes the induction step. We now return to the base case. The machines start in states

⟨π, −1, N, σ_{0}, h_{0}⟩

for the concrete machine and

⟨π′, emptydisplay, ⟨⟩, h′_{0}⟩

for the abstract machine. Comparing these states with the definition of ≃ for states, we see that all of the conditions for correspondence hold, except for N_{0} ≤ up and (σ, u_{0}) ⊧_{U} N_{0} ≃ u_{0} Let ≃_{0} denote this weakened relation.

The programs π and π′ begin with a sequence of add-global-to-env^{∗} instructions. We first show that these instructions preserve ≃_{0}. Assume we have

⟨(add-global-to-env^{∗} π), up, sp, σ, h⟩ ≃_{0} ⟨(add-global-to-env^{∗} π), u, ζ, h′⟩

We must show that

⟨π, up +1, sp, σ_{1}, h_{1}⟩ ≃_{0} ⟨π, u_{1}, ζ, h′_{1}⟩

where

σ_{1} = (σ[(new h)/(up +1)])
h_{1} = (update (new h) 0 h)
u_{1} = (extends_{r g} u (new h′))
h′_{1} = (update (new h′) ⟨int, 0⟩ h′)

For the interesting components, we calculate as follows:

(σ, up) ⊧_{U} up ≃ u  assumption
(σ_{1}, up +1) ⊧_{U} up ≃ u  lemma 2.2

(new h) ≃ (new h′)

(σ_{1}, up +1) ⊧_{U} up +1 ≃ (extends_{r g} u (new h′))  definition of ⊧_{U}.
(σ, up) ⊧_{Z} ⟨sp, N⟩ ≃ (v :: ζ)  assumption
(σ, up) ⊧_{Z} ⟨(sp −1), N⟩ ≃ ζ  definition of ⊧_{Z}

(σ_{1}, up +1) ⊧_{Z} ⟨(sp −1), N⟩ ≃ ζ

h ≃ h′  assumption

(new h) ≃ (new′ h′) (update (new h) 0 h) ≃ (update (new h′) ⟨int, 0⟩ h′) h_{1} ≃ h′_{1} up +1 ≤ N because ⟨π, u_{1}, ζ, h′_{1}⟩ is a valid abstract-machine state, and there-

fore up +1 = |dom(u_{1})| ≤ N.

So the add-global-to-env^{∗} instructions preserve ≃_{0}. Last, we turn to the closerecs instruction that concludes the prelude. Assume we have

⟨(closerecs (π_{1} … π_{n}) π), up, sp, σ, h⟩ ≃_{0} ⟨(closerecs (π′_{1} … π′_{n}) π′), u, ζ, h′⟩

We must show that

⟨π, up +n, sp, σ′, h⟩ ≃ ⟨π′, u_{0}, ζ, h′⟩

where σ′ = (spread σ(up +n) (π_{1} … π_{n})) u_{0} = (fix(λu′ .(extends_{r l} u (⟨proc, ⟨π′_{1}, u′⟩⟩ … ⟨proc, ⟨π′_{n}, u′⟩⟩))))

Note that here we need to establish ≃, not ≃_{0}.

At the end of this instruction, we have up = N_{0}, by the definition of N_{0}. By the definition of σ′, for 1 ≤ i ≤ n we have σ′(up +n − i + 1) = π_{n−i}, so

(σ′, up) ⊧_{V} σ′(up +n − i + 1) ≃ ⟨proc, ⟨π′_{i}, u_{0}⟩⟩, and (σ′, up) ⊧_{U} up ≃ u, so by the definition of ⊧_{U} we have (σ′, up) ⊧_{U} up +n ≃ u_{1}, where

u_{1} = (extends_{r l} u (⟨proc, ⟨π′_{1}, u_{0}⟩⟩ … ⟨proc, ⟨π′_{n}, u_{0}⟩⟩))

But u_{1} is just one unwinding of u_{0}, so u_{1} = u_{0}.

All the other conditions are established trivially. This completes the establishment of the invariant, and therefore establishes the base step. □

7 Implementation

An assembler for PreScheme was developed in parallel with this specification. It generates code for the Motorola 68000. Representing the concrete model with the 68000 requires a mapping similar to one between the abstract and concrete machine just detailed. This section informally describes that mapping.

Immediate data is modeled via a 32 bit quantity (4 bytes). Thus immediate data can be stored directly in any of the 68000 registers (D0–D7 and A0–A7) or in 4 consecutive bytes of user memory.

The concrete machine’s store, σ, is modeled by 68000 with the user stack and its stack pointer, sp, is modeled by the 68000 stack pointer SP (a.k.a. address register A7). The environment register, up, is modeled by the address register A1. For efficiency, the initial environment pointer, N_{0}, and initial stack pointer, N, are also kept in address registers for quick reset on tail call.

Two details must be noted in using the 68000 user stack as described. First, 68000 user stack grows downward rather than upward so rather than increment the stack pointer on a push, it must be decremented (similarly for popping et al). Second, to decrement the stack pointer by one unit of immediate data, SP must be decremented by 4, the number of bytes necessary to represent the immediate data.

Procedures are represented by their effective addresses. When the initial environment u_{0} is being created, these effective addresses (which are 32 bit quantities) are pushed on the stack. On tail-call, the effective address is loaded from the stack into the program counter.

The environment representation is almost completely analogous to that of the concrete machine, with environment values kept in the first 4 ∗ N bytes of the stack. The local stack is handled almost completely analogously as well. The only difference is that for efficiency, the top 8 values of the local stack are cached in in the data registers.

Representation of the concrete machine’s heap is done differently for the different components of the heap. The first component of the heap, the store for mutable variables, is kept directly in the first 4∗j bytes of the user stack (where j is the number of global variables in the program being compiled). The second component of the heap, which tells how many objects are stored in the first component, remains constant during the execution of a given Pure PreScheme program after the initial environment has been established (in particular, it is also j). It is modeled implicitly through the correctness of the instructions manipulating mutable data. The third component of the heap, that which the primitives manipulate, are handled by the primitives (usually via operating system calls).

Performance of the compiler is difficult to measure as there is no other Pure PreScheme compiler available. As an alternative, we decided to test our compiler

Fibonacci Pure PreScheme Chez Scheme gcc
20  0.4s  0.7s 0.3s
22  0.9s  1.8s 0.8s
24  2.4s  4.8s 2.0s
26  6.3s  12.5s 5.3s
28  16.4s  32.9s 13.9s
29  26.5s  53.5s 22.4s

Figure 4: Pure PreScheme vs. Chez Scheme vs. C

against Chez Scheme, an optimizing native code Scheme compiler, and against gcc, a standard C compiler, on an unloaded Sun 3/160.

The test case we used was a Pure PreScheme version of Fibonacci, using an explicit array to model the recursion stack. This test duplicates the general structure of the Vlisp VM. The results summarized in Figure 4 indicate that our compiler produces code executing about twice as fast as the code produced by Chez Scheme (Chez/PPS = 2.01). To make the test as fair as possible, we used fixnum operators in the Chez Scheme version, and set Chez Scheme’s optimization level 3 to produce maximum inlining.

We conjecture that most of the difference between the PPS compiler and Chez Scheme is accounted for by the extra operations that Scheme must perform in order to do garbage collection. For example, Chez sets a byte in a “dirty vector” for each vector-set! to support the generational garbage collector. According to Kent Dybvig [personal communication] this costs 4–5 instructions and some extra memory traffic for each assignment. Our benchmark and the VM are both quite vector-intensive.

This data supports Kelsey’s thesis about PreScheme: that by restricting the language, we can obtain much better performance. We therefore tested our benchmark against a straightforward transcription of the fibonacci program into C. In the C version, tail-recursion is replaced by explicit goto’s. The C version also uses malloc to allocate the array dynamically, just as the PPS version does. We were pleased to see that our code ran within 20% of the speed of the code produced by gcc (PPS/C = 1.18).

Thus, the code produced by this verified compiler was competitive with conventionally produced code.

8 Conclusions

We have presented a verified storage layout for a Pure PreScheme compiler. The proof verifies that an abstract machine that manipulates trees and a concrete machine that manipulates realistic data structures always produce corresponding results. From this experience we can draw a number of conclusions.

Our approach factored the correctness proof into two basic layers:

1. Proof of correctness of the compiler, which translates from the source language to abstract-machine code. This was the part reported in [8].

2. Proof of correctness of the implementation of the abstract machine. In this report we prove the correctness of the run-time structure of our implementation; the issue of translation from abstract to concrete machine code will be reported separately.

This factorization proved to be a successful decomposition. The factoring of the proof into the correctness of the compiler and the correctness of the implementation of the abstract machine allows us to use both denotational and operational reasoning to their best advantage. Furthermore, each portion of the proof gave us confidence in a different part of the implementation.

The proof of correctness of the run-time structure is operational, rather than denotational, in its structure: that is, it proceeds by induction on the number of steps taken by the machine, rather than on the size of the program. We believe this is a fundamental improvement. Previous proofs of compiler correctness, such as those in [6, 10] were highly complex because they used induction on the construction of reflexive domains as a denotational analog to induction on length of computation. Our proof would likely be just as complex had we adopted this strategy (see [13] for an attempt to do a much smaller problem in a purely denotational style). By using induction on computation length directly, we avoid this indirection. Furthermore, since we deal directly with terms (trees) rather than with their denotations, we avoid the complication of “inclusive predicates,” with their attendant complexity.

The implementation experience showed that having a validated compiler and run-time structure eliminated most bugs in the areas covered by the proofs. The various delivered versions of the compilers had a number of bugs, but these were almost entirely in one of two categories:

1. Incompatibilities with the PreScheme front end [9] (errors in syntax, missing primitives, etc.). These were artifacts of the circumstance that the various portions of the compiler, including the interface with the front end, were developed concurrently.

2. Problems with the assembly code sequences generated for the concretemachine instructions. These were mostly minor in nature (registers not being saved across routine calls, etc.), and were below the grain of the proof. Extending the proof to reach this level would require an extremely detailed model of the behavior of the machine and operating system (see, e.g. [7]). In practice, however, the concrete machine was at a sufficiently low level that implementation of the primitives was easy.

The method of formalizing storage layout relations seems to be flexible enough to model standard representation strategies. More of these are presented in [12].

The proofs resemble traditional Hoare-style verification proofs, but seem quite stylized and may be amenable to mechanical proof-checking. This work extends the realm of “dull” proofs from the byte-code compiler level [2, 11] to something much closer to an ordinary “compiler-writer’s abstract machine.” We believe this is a mark of success for this effort.

The performance of the PPS compiler was competitive with conventionally produced code. On a small benchmark, the code produced by the PPS compiler ran within 20% of the code produced by gcc for a simple-minded transcription of the benchmark into C. Therefore, use of a verified compiler need not entail catastrophic performance penalties.

In this report, we did not deal with the correctness of the translation from abstract to concrete machine code. For the machines in this report, this is trivial, consisting simply of translation of literals from tagged to untagged form. The real compiler, however, translates the tree-like abstract-machine code to a linear representation. This more complex representation requires two additional portions in the proof:

1. The storage layout relation for programs would have to be modified to formalize the linear representation, and the proof of correctness of the concrete machine (the main theorem of this report) would have to be modified accordingly. This should be easy, since, unlike the other components of the machines, the program store remains constant during execution. The outlines of the proof are clear in [4, 12].

2. We would then have to show that our translator converts an abstractmachine program to corresponding state of the program store. Such an assembler-correctness proof would deal with the specifics of the translation process and would resemble in its specificity and level, the compilercorrectness proof of [8]. We have good ideas about how this proof should be structured, and we will report on this later, either in Oliva’s forthcoming Ph.D. thesis or a separate technical report.

One surprise in the development of the proof was the necessity to import information from higher levels in the compilation process. We were unable to prove the congruence between abstract and concrete machines except for programs that were in the image of the compiler.

For the Scheme VM, this restriction was not important, because the VM is type-correct. This guarantees that it will never reach an error state, so all the error tests were guaranteed to succeed. However, it would be desirable to formulate a cleaner version of the correctness result.

One way to do this might be to factor the proof as follows: Call an abstractmachine program (N_{0}, N)-bounded iff the conclusion of the Bounded Space Theorem holds for it. Then we believe that the Main Theorem holds for any (N_{0}, N)- bounded abstract-machine program. However, we did not have time to verify that this is the only information needed from the correctness proof of [8].

We believe the problem of needing to import information from higher levels of the compiler is related to the issue of incorporating flow analyses, which similarly verify the maintenance of non-local invariants, into compiler correctness proofs. In this case, we needed to rely on the invariance of N_{0} ≤ |dom(u)| ≤ N, which is not possible to verify locally without additional information. The operational type-soundness of the program is another such invariant. We believe that developing a systematic way of incorporating such information is the most important outstanding problem in semantics-based compiler correctness.

A Compiling Simple Let Expressions

In this appendix we show the correctness of compiling simple let expressions. Correctness of simple let^{∗} expressions and the analogous simple commands follow similarly.

We begin by showing the denotational definition of the simple let:

SE[[(let (LSD) S)]] = λρκ.DL[[LSD]]ρ(λϵ^{∗}.SE[[S]]ρ[(map (in D) ϵ^{∗})/GL[[LSD]]]κ)

Using our standard methodology, we derive the compiler semantics to be:

CSE[[(let (LSD) S)]] = λγπ.(save-env (CDL[[LSD]]γ (add-to-env (CSE[[S]] (extends_{c l} γ GL[[LSD]]) (restore-env π)))))

where the new machine instructions are defined as:

save-env = λπ.λuζ.πu(u :: ζ)

restore-env = λπ.λuζ.π(top (pop-first 1 ζ))((top ζ) :: (pop-first 2 ζ))

Recall that to prove correctness of the compiler we must prove that execution of the compiled simple expression, let, results in same value computed by the denotational definition. Formally stated, the induction hypothesis for simple expressions was:

(CSE[[S]]γπ)uζ = SE[[S]](u ∘ γ)(λϵ.πu(ϵ :: ζ))

Proof of correctness for the let progresses as the other alternatives for simple expressions:

(CSE[[(let (LSD) S)]])uζ

= (save-env (CDL[[LSD]]γ(add-to-env (CSE[[S]] (extends_{c l} γ GL[[LSD]]) (restore-env π)))))uζ

= (CDL[[LSD]]γ(add-to-env (CSE[[S]] (extends_{c l} γ GL[[LSD]]) (restore-env π))))u(u :: ζ)

= DL[[LSD]](u ∘ γ)(λϵ^{∗}.(add-to-env (CSE[[S]] (extends_{c l} γ GL[[LSD]]) (restore-env π)))u(ϵ^{∗} : u :: ζ))

= DL[[LSD]](u ∘ γ)(λϵ^{∗}.(CSE[[S]] (extends_{c l} γ GL[[LSD]]) (restore-env π))(extends_{r l} uϵ^{∗})(u :: ζ))

= DL[[LSD]](u ∘ γ)(λϵ^{∗}.SE[[S]] (u ∘ γ)[(map (in D) ϵ^{∗})/GL[[LSD]]] (λϵ.(restore-env π)(extends_{r l} uϵ^{∗})(ϵ :: u :: ζ)))

= DL[[LSD]](u ∘ γ)(λϵ^{∗}.SE[[S]] (u ∘ γ)[(map (in D) ϵ^{∗})/GL[[LSD]]](λϵ.πu(ϵ :: ζ)))

= SE[[(let (LSD) S)]](u ∘ γ)(λϵ.πu(ϵ :: ζ))

References

[1] Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, 1981.

[2] William Clinger. The Scheme 311 Compiler: An Exercise in Denotational Semantics. In Proc. 1984 ACM Symposium on Lisp and Functional Programming, pages 356–364, August 1984.

[3] Edsger W. Dijkstra. Speech at the Occasion of an Anniversary. In Selected Writings On Computing: A Personal Perspective, pages 50–53. Springer-Verlag, 1982.

[4] John Hannan. Making Abstract Machines Less Abstract. In J. Hughes, editor, Functional Programming Languages and Computer Architecture, 5th ACM Conference, volume 523 of Lecture Notes in Computer Science, pages 618–635. Springer-Verlag, Berlin, Heidelberg, and New York, 1991.

[5] Richard Kelsey. PreScheme: A dialect of Scheme for Systems Programming. in preparation, 1993.

[6] R. Milne and Christopher Strachey. A Theory of Programming Language Semantics. Chapman and Hall, London, 1976. Also Wiley, New York.

[7] J Strother Moore. A Mechanically Verified Language Implementation. Technical Report 30, Computational Logic Inc., Austin, TX, September 1988. also appeared in J. of Computer-Aided Deduction.

[8] Dino P. Oliva and Mitchell Wand. A Verified Compiler for Pure PreScheme. Technical Report NU-CCS-92-5, Northeastern University College of Computer Science, February 1992.

[9] J. D. Ramsdell, W. M. Farmer, J. D. Guttman, L. G. Monk, and V. Swarup. The vlisp PreScheme Front End. M 92B098, The MITRE Corporation, 1992.

[10] Joseph E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, MA, 1977.

[11] Mitchell Wand. Deriving Target Code as a Representation of Continuation Semantics. ACM Transactions on Programming Languages and Systems, 4(3):496–517, July 1982.

[12] Mitchell Wand and Dino P. Oliva. Proving the Correctness of Storage Representations. In Proc. 1992 ACM Symposium on Lisp and Functional Programming, pages 151–160, 1992.

[13] Mitchell Wand and Zheng-Yu Wang. Conditional Lambda-Theories and the Verification of Static Properties of Programs. In Proc. 5th IEEE Symposium on Logic in Computer Science, pages 321–332, 1990.