Proving compiler correctness with evolving algebra specifications

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.