This document contains a preliminary version. It demonstrates the
  Verifix techniques for the the construction of a correct compiler.
  Thus, it is built up step by step, following the current results
  of the Verifix project.

  Existing works on the construction of correct compilers have at
  least one of the following drawbacks: (i) correct compilers do not
  compile into machine code of existing processors. Instead they
  compile into programs of an abstract machine which ignores
  limitations and properties of real-life processors. (ii) the code
  generated by correct compilers is orders of magnitudes slower than
  the code generated by unverified compilers. (iii) the considered
  source language is much less complex than real-life programming
  languages (often functional languages or simple while-languages.
  This report defines a classical compilation from a while-language
  with parameterless recursive procedures (IS0) into
  machine code of the DEC-Alpha processor family and proves its
  correctness.