G. Barthe, G. Dufay, L. Jakubiec, S. Melo-de-sousa, and B. Serpette, A Formal Executable Semantics of the JavaCard Platform, Proceedings of ESOP'01, pp.302-319, 2001.
DOI : 10.1007/3-540-45309-1_20

G. Barthe, M. Ruys, and H. Barendregt, A two-level approach towards lean proof-checking, TYPES '95: Selected papers from the International Workshop on Types for Proofs and Programs, pp.16-35, 1996.
DOI : 10.1007/3-540-61780-9_59

S. Berghofer and T. Nipkow, Executing Higher Order Logic, Lecture Notes in Computer Science, vol.2277, pp.24-40, 2000.
DOI : 10.1007/3-540-45842-5_2

Y. Bertot, A certified compiler for an imperative language, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00073199

Y. Bertot, Formalizing a JVML Verifier for Initialization in a Theorem Prover, Computer Aided Verification (CAV'2001), pp.14-24, 2001.
DOI : 10.1007/3-540-44585-4_3

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development , Coq'Art:the Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

Y. Bertot and R. Fraer, Reasoning with executable specifications, TAP- SOFT'95, pp.531-545, 1995.
DOI : 10.1007/3-540-59293-8_218
URL : https://hal.archives-ouvertes.fr/inria-00073912

P. Borras, D. Clément, T. Despeyroux, J. Incerpi, G. Kahn et al., Centaur: the system, Third Symposium on Software Development Environments, 1988.
URL : https://hal.archives-ouvertes.fr/inria-00075774

S. Boutin, Using reflection to build efficient and certified decision procedures, TACS'97, 1997.
DOI : 10.1007/BFb0014565
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.7587

A. Chaieb, Proof-Producing Program Analysis, Lecture Notes in Computer Science, vol.4281, pp.287-301, 2006.
DOI : 10.1007/11921240_20
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.72.3773

R. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer et al., Implementing mathematics with the Nuprl proof development system, 1986.

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. David, Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés, 2005.

W. Edsger and . Dijkstra, A discipline of Programming, 1976.

G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy et al., The Coq Proof Assistant User's Guide. INRIA, 1993.

J. Filliâtre, Proof of Imperative Programs in Type Theory, International Workshop TYPES'98, 1998.
DOI : 10.1007/3-540-48167-2_6

J. C. Michael, T. F. Gordon, and . Melham, Introduction to HOL : a theorem proving environment for higher-order logic, 1993.

C. A. and R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, 1969.

G. Kahn, Natural semantics, Programming of Future Generation Computers. North-Holland, 1988.
DOI : 10.1007/BFb0039592
URL : https://hal.archives-ouvertes.fr/inria-00075953

P. Letouzey, A New Extraction for Coq, TYPES 2002, 2003.
DOI : 10.1007/3-540-39185-1_12
URL : https://hal.archives-ouvertes.fr/hal-00150914

O. Müller, T. Nipkow, O. David-von-oheimb, . Slotosch, . Holcf et al., HOLCF = HOL + LCF, Journal of Functional Programming, vol.9, issue.2, pp.191-223, 1999.
DOI : 10.1017/S095679689900341X

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.9270

C. Lawrence, T. Paulson, and . Nipkow, Isabelle : a generic theorem prover, Lecture Notes in Computer Science, vol.828, 1994.

D. Terrasse, Encoding natural semantics in Coq, AMAST'95, 1995.
DOI : 10.1007/3-540-60043-4_56

J. Van-den, B. Berg, and . Jacobs, The loop Compiler for Java and JML, TACAS 2001, pp.299-312, 2001.
DOI : 10.1007/3-540-45319-9_21

O. David-von, Analyzing Java in Isabelle/HOL, Formalization, Type Safety, and Hoare Logic, 2000.

G. Winskel, The Formal Semantics of Programming Languages, an introduction. Foundations of Computing, 1993.

. Unité-de-recherche-inria-sophia and . Antipolis, route des Lucioles -BP 93 -06902 Sophia Antipolis Cedex (France) Unité de recherche INRIA Futurs : Parc Club Orsay Université -ZAC des Vignes 4, 2004.

I. Unité-de-recherche and . Lorraine, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès-Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rhône-Alpes : 655, avenue de l'Europe -38334 Montbonnot Saint-Ismier (France) Unité de recherche INRIA Rocquencourt, Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex