Correctness of a compiler for arithmetic expressions
John McCarthy, James A. Painter · Proceedings of symposia in applied mathematics · 1967
This paper contains a proof of the correctness of a simple compiling algorithm for compiling arithmetic expressions into machine language. The definition of correctness, the formalism used to express the description