|
|
|---|
|
|
|
|---|
J. McCarthy and J. Painter, “Correctness of a
Compiler for Arithmetic Expressions”, Proceedings of Symposia in
Applied Mathematics, 19, American Mathematical Society, 1967.
Relevance: an early (perhaps the first) compiler proof
This paper by gives a conventional “hand proof” (not a mechanized proof) of the correctness of a compiler for simple arithmetic expressions. It demonstrates the use of an operational semantics for the underlying machine.
This was a famous and popular challenge problem in the early history of formal methods. See Chapter 17 bib::bm79 for a mechanized proof a similar result and a discussion of the history of the mechanization of such compiler proofs.