X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768

R. Milner and R. Weyhrauch, Proving compiler correctness in a mechanized logic, Proc. 7th Annual Machine Intelligence Workshop, pp.51-72, 1972.

J. Tristan and X. Leroy, A simple, verified validator for software pipelining, 37th symposium Principles of Programming Languages, pp.83-92, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00529836

X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and understanding bugs in C compilers, Programming Language Design and Implementation, 2011.