An approach to compiler correctness
Laurian M. Chirica, David F. Martin · ACM SIGPLAN Notices · 1975
This paper is a preliminary report on an experiment in applying Floyd's method of inductive assertions to the compiler correctness problem. Practical postfix translators are considered, and the semantics of source and object languages are characterized by Floyd verification conditions. Compiler correctness proofs are partitioned into two parts. The first part deals with proofs of the syntactic and translational phase of compilation, and generates semantic equivalence theorems which are proved in the second part. These techniques are illustrated by a small example.