A computer Proof of the Correctness of a Simple Optimizing Compiler for Expressions.
STANFORD RESEARCH INST MENLO PARK CALIF
Pagination or Media Count:
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.
- Computer Programming and Software