Correctness of a compiler for a Lisp subset
Ralph L. London · 1972
Excerpts of a proof of correctness of a running Lisp compiler for the PDP-10 computer are given. Included are the rationale for presenting this proof and a discussion of an actual extension of the proof to another compiler.