A computer Proof of the Correctness of a Simple Optimizing Compiler for Expressions.
Boyer,Robert S, J Strother Moore · Defense Technical Information Center (DTIC) · 1977
This paper presents an automatic computer proof of the correctness of a simple optimizing compiler for expressions. The proof was produced by a new theorem prover, resembling the Boyer-Moore Pure LISP Theorem Prover but operating on a much richer domain of functions and objects.