A. W. Appel, Hints on proving theorems in Twelf, 2000.

A. W. Appel and X. Leroy, List-machine exercise, 2006.

A. W. Appel, P. A. Mellì-es, C. D. Richards, and J. Vouillon, A very modal model of a modern, major, general type system, Proc. 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'07), pp.109-122, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00150978

B. E. Aydemir, A. Bohannon, M. Fairbairn, J. N. Foster, B. C. Pierce et al., Mechanized Metatheory for the Masses: The PoplMark Challenge, Int. Conf. on Theorem Proving in Higher Order Logics Lecture Notes in Computer Science, pp.50-65, 2005.
DOI : 10.1007/11541868_4

. Springer-verlag, URL http, 2005.

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

O. Danvy, Defunctionalized interpreters for programming languages, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pp.131-142, 2008.
DOI : 10.1145/1411203.1411206
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.685.1361

D. Delahaye, C. Dubois, and J. F. Etienne, Extracting Purely Functional Contents from Logical Inductive Types, Theorem Proving in Higher Order Logics, pp.70-85, 2007.
DOI : 10.1007/978-3-540-74591-4_7
URL : https://hal.archives-ouvertes.fr/hal-01125370

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, pp.619-695, 2006.
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), pp.2-11, 2005.

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 and H. Grall, Coinductive big-step operational semantics, Information and Computation, vol.207, issue.2, pp.284-304, 2009.
DOI : 10.1016/j.ic.2007.12.004
URL : https://hal.archives-ouvertes.fr/inria-00309010

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, CADE-16: Proceedings of the 16th International Conference on Automated Deduction, pp.202-206, 1999.
DOI : 10.1007/3-540-48660-7_14

S. Weirich, URL http://lists.seas.upenn, Experience report with Twelf, 2005.

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

D. Wu, A. W. Appel, and A. Stump, Foundational proof checkers with small witnesses, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming , PPDP '03, pp.264-274, 2003.
DOI : 10.1145/888251.888276
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.525.5571