A. W. Appel and X. Leroy, A list-machine benchmark for mechanized metatheory, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00077531

B. E. Aydemir, A. Bohannon, N. Foster, B. Pierce, D. Vytiniotis et al., The POPLmark challenge, 2005.

Y. Bertot and P. Castran, 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

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
DOI : 10.1145/1146809.1146811

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

X. Leroy, Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant, POPL'06: 33rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

J. S. Moore, A mechanically verified language implementation, Journal of Automated Reasoning, vol.5, issue.4, pp.461-492, 1989.
DOI : 10.1007/BF00243133

J. S. Moore, Piton: a mechanically verified assembly-language, 1996.

F. Pfenning and C. Schuermann, Twelf user's guide, version 1, 2002.

F. Pfenning and C. Schürmann, System Description: Twelf ??? A Meta-Logical Framework for Deductive Systems, The 16th International Conference on Automated Deduction, 1999.
DOI : 10.1007/3-540-48660-7_14

M. Strecker, Formal Verification of a Java Compiler in Isabelle, Proc. Conference on Automated Deduction (CADE), pp.63-77, 2002.
DOI : 10.1007/3-540-45620-1_5

A. K. Wright and M. Felleisen, A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994.
DOI : 10.1006/inco.1994.1093

URL : http://doi.org/10.1006/inco.1994.1093