Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant.
33rd Symposium Principles of Programming Languages (POPL 2006), Jan 2006, Charleston, SC, United States. pp.42--54,
⟨10.1145/1111037.1111042⟩.
⟨inria-00000963⟩