S. Blazy and X. Leroy, Formal Verification of a Memory Model for C-Like Imperative Languages, Proc. of Int. Conf. on Formal Engineering Methods (ICFEM), pp.280-299, 2005.
DOI : 10.1007/11576280_20

URL : https://hal.archives-ouvertes.fr/inria-00077921

M. A. Dave, Compiler verification, ACM SIGSOFT Software Engineering Notes, vol.28, issue.6, pp.2-2, 2003.
DOI : 10.1145/966221.966235

E. Börger, N. Fruja, V. Gervasi, and R. Stärk, A high-level modular definition of the semantics of <mml:math altimg="si1.gif" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:mi mathvariant="normal">C</mml:mi><mml:mo>???</mml:mo></mml:math>, Theoretical Computer Science, vol.336, issue.2-3, pp.235-284, 2005.
DOI : 10.1016/j.tcs.2004.11.008

Y. Gurevich and J. Huggins, The semantics of the C programming language, Proc. of CSL'92, pp.274-308

G. Klein and T. Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems, vol.28, issue.4, 2004.
DOI : 10.1145/1146809.1146811

D. Leinenbach, W. Paul, and E. Petrova, Towards the formal verification of a C0 compiler, Proc. Conf. on Software Engineering and Formal Methods (SEFM), pp.2-11, 2005.

X. Leroy, The Compcert certified compiler back-end ? commented Coq development, 2006.

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, Proc. Symp. Principles Of Programming Languages (POPL), pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

V. Nepomniaschy, I. Anureev, and A. Promsky, Verification-oriented language Clight and its structural operational semantics, Ershov Memorial Conference, pp.103-111, 2003.
DOI : 10.1007/978-3-540-39866-0_12

M. Norrish, C formalised in HOL, 1998.

N. Papaspyrou, A formal semantics for the C programming language, 1998.

M. Strecker, Compiler verification for C0, 2005.