Proving compiler correctness with evolving algebra specifications
Bernhard Beckert, Haehnle, Reiner · 1996
The purpose of this note is to define a framework for proving compiler correctness with evolving algebra (EA) specifications. Although our specific domain is the verification of a Prolog-to-WAM compiler, we think that our considerations are fairly general and they should be useful in other areas as well. First we define our general view of the semantics of a programming language, of how semantics can be specified using EAs, and of compiler correctness; then we describe how the correctness of a compiler may be proven; and finally we point out the differences to the approach of Egon Boerger and Dean Rosenzweig and to the notion of correctness as commonly used in logic.