N. Benton, A. Kennedy, and C. Varming, Some Domain Theory and Denotational Semantics in Coq, Proc. of TPHOLs '09, pp.115-130, 2009.
DOI : 10.1007/3-540-60275-5_72

Y. Bertot, Structural Abstract Interpretation: A Formal Study Using Coq, Language Engineering and Rigorous Software Development, pp.153-194, 2008.
DOI : 10.1007/978-3-540-31987-0_3
URL : https://hal.archives-ouvertes.fr/inria-00329572

S. Blazy and X. Leroy, Mechanized Semantics for the Clight Subset of the C Language, Journal of Automated Reasoning, vol.29, issue.6, pp.263-288, 2009.
DOI : 10.1007/s10817-009-9148-3
URL : https://hal.archives-ouvertes.fr/inria-00352524

P. Cousot, Visiting Professor at the MIT Aeronautics and Astronautics Department , Course 16

P. Cousot, The calculational design of a generic abstract interpreter, Calculational System Design. NATO ASI Series F. IOS Press, 1999.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/inria-00528590

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The ASTRÉEASTR´ASTRÉE analyser, Proc. of ESOP'05, pp.21-30, 2005.

M. J. Gordon, Mechanizing Programming Logics in Higher Order Logic, Current Trends in Hardware Verfication and Automatic Theorem Proving, pp.387-439, 1988.
DOI : 10.1007/978-1-4612-3658-0_10

X. Leroy, Mechanized semantics, with applications to program proof and compiler verification, lecture given at the, 2009.

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, Proc. of POPL'06, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

A. Miné, Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors, Proc. of ESOP'04, pp.3-17, 2004.
DOI : 10.1007/978-3-540-24725-8_2

T. Nipkow, Winskel is (almost) Right: Towards a Mechanized Semantics Textbook, Formal Aspects of Computing, vol.10, issue.2, pp.171-186, 1998.
DOI : 10.1007/s001650050009

D. Pichardie, Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés, 2005.

D. Pichardie, Building certified static analysers by modular construction of wellfounded lattices, Proc. of FICS'08, pp.225-239, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00332365

G. D. Plotkin, A structural approach to operational semantics, Journal of Logic and Algebraic Programming, pp.60-6117, 2004.

X. Rival and L. Mauborgne, The trace partitioning abstract domain, ACM Transactions on Programming Languages and Systems, vol.29, issue.5, 2007.
DOI : 10.1145/1275497.1275501

M. Sozeau and N. Oury, First-Class Type Classes, Proc. of TPHOLs, pp.278-293, 2008.
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864