Articles
Correctness of a Compiler for Arithmetic Expressions
This paper contains a proof of the correctness of a simple compiling algorithm for compiling arithmetic expressions into machine language. It may have been the first such formal proof.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.
Download the article in PDF.
