The early Lisp systems did not build closures. They used the so-called dynamic binding convention. Here is the Lisp-style evaluator.
Definition:
The actual Lisp 1.5 evaluator was defined like this (see Lisp 1.5 Programmer's Manual, MIT Press, 1962, p.13).
The sense in which the first evaluation is correct is given in CN93,
16 where I prove a theorem relating to
. The result
uses the definition of close from those notes.
Theorem For all closed terms