A. J. Ahmed, Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types, Programming Languages and Systems, 15th European Symposium on Programming, pp.69-83, 2006.
DOI : 10.1017/S0956796800000125

A. W. Appel and S. Blazy, Separation Logic for Small-Step cminor, Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs, pp.5-21, 2007.
DOI : 10.1007/978-3-540-74591-4_3

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

G. Barthe, B. Grégoire, C. Kunz, and T. Rezk, Certificate translation for optimizing compilers, ACM Transactions on Programming Languages and Systems, vol.31, issue.5, p.31, 2009.
DOI : 10.1145/1538917.1538919

N. Benton and C. Hur, Biorthogonality, step-indexing and compiler correctness, International Conference on Functional Programming, pp.97-108, 2009.

F. Besson, D. Cachera, T. P. Jensen, and D. Pichardie, Certified Static Analysis by Abstract Interpretation, Foundations of Security Analysis and Design, pp.223-257, 2009.
DOI : 10.1145/1146809.1146811

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

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., A static analyzer for large safety-critical software, Programming Language Design and Implementation 2003, pp.196-207, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00128135

S. Boldo, J. Filliâtre, and G. Melquiond, Combining Coq and Gappa for Certifying Floating-Point Programs, Intelligent Computer Mathematics, pp.59-74, 2009.
DOI : 10.1109/TC.2008.200

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

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock et al., seL4, Communications of the ACM, vol.53, issue.6, pp.107-115, 2010.
DOI : 10.1145/1743546.1743574

A. J. Kornecki and J. Zalewski, The qualification of software development tools from the DO-178B certification perspective. CrossTalk, 2006.

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

G. C. Necula, Translation validation for an optimizing compiler, Programming Language Design and Implementation, pp.83-95, 2000.

A. Pnueli, M. Siegel, and E. Singerman, Translation validation, TACAS '98, pp.151-166, 1998.
DOI : 10.1007/BFb0054170

Z. Shao, V. Trifonov, B. Saha, and N. Papaspyrou, A type system for certified binaries, ACM Transactions on Programming Languages and Systems, vol.27, issue.1, pp.1-45, 2005.
DOI : 10.1145/1053468.1053469

J. Souyris, V. Wiels, D. Delmas, and H. Delseny, Formal Verification of Avionics Software Products, FM 2009: Formal Methods, pp.532-546, 2009.
DOI : 10.1007/978-3-642-05089-3_34

J. Tristan and X. Leroy, Verified validation of Lazy Code Motion, Programming Language Design and Implementation, pp.316-326, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00415865

H. Tuch, G. Klein, and M. Norrish, Types, bytes, and separation logic, 34th symposium Principles of Programming Languages, pp.97-108, 2007.

J. Yang and C. Hawblitzel, Safe to the last instruction: automated verification of a type-safe operating system, Programming Language Design and Implementation 2010, pp.99-110, 2010.