@techreport{NordioMuellerMeyer08, author = {Martin Nordio and Peter M{\"u}ller and Bertrand Meyer}, title = {Formalizing Proof-Transforming Compilation of Eiffel Programs}, institution = {ETH Zurich}, year = {2008}, number = {587}, urltopdf = {http://se.inf.ethz.ch/people/nordio/papers/NordioMuellerMeyer08.pdf} }