Correctness of a Compiler for Arithmetic Expressions

Correctness of a Compiler for Arithmetic Expressions by John McCarthy and James Painter may have been the first formal proof of the correctness of a compiling algorithm. Using abstract syntax and Lisp-style recursive definitions made the formulas short.

.dvi, .pdf and .ps versions are also available.

Up to: McCarthy home page

I welcome comments, and you can send them by clicking on