@techreport{NordioMuellerMeyer08,
 author = {M. Nordio and P. M{\"u}ller and B. Meyer},
 title = {Formalizing Proof-Transforming Compilation of Eiffel Programs},
 institution = {ETH Zurich},
 year = {2008},
 number = {587},
}