Yves Bertot, Benjamin Grégoire, Xavier Leroy. A structured approach to proving compiler optimizations based on dataflow analysis.
Types for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. pp.66-81,
⟨10.1007/11617990⟩.
⟨inria-00289549⟩