Modular Compiler Verification A Refinement-Algebraic Approach Advocating Stepwise Abstraction - Müller-Olm, Markus; Müller-Olm, Markus (Springer Berlin Heidelberg : Imprint: Springer, 1997)