Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development ? Coq'Art: The Calculus of Inductive Constructions, EATCS Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

E. Eide and J. Regehr, Volatiles are miscompiled, and what to do about it, Proceedings of the 7th ACM international conference on Embedded software, EMSOFT '08, pp.255-264, 2008.
DOI : 10.1145/1450058.1450093
URL : http://www.cs.utah.edu/~regehr/papers/emsoft08-preprint.pdf

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/978-3-642-59495-3
URL : https://hal.archives-ouvertes.fr/inria-00360768

J. Mccarthy and J. Painter, Correctness of a compiler for arithmetic expressions, of Proc. of Symposia in Applied Mathematics, pp.33-41, 1967.
DOI : 10.1090/psapm/019/0242403

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

X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and understanding bugs in C compilers, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp.283-294, 2011.
DOI : 10.1145/2345156.1993532