P. Aczel, An Introduction to Inductive Definitions, Handbook of Mathematical Logic, volume 90 of Studies in Logics and the Foundations of Mathematics, pp.739-782, 1997.
DOI : 10.1016/S0049-237X(08)71120-0

S. Agerholm, Domain theory in HOL, Higher Order Logic Theorem Proving and its Applications, Workshop HUG '93, pp.295-309, 1994.
DOI : 10.1007/3-540-57826-9_143

A. W. Appel, Modern Compiler Implementation in ML, 1998.
DOI : 10.1017/CBO9780511811449

A. W. Appel, Foundational proof-carrying code, Logic in Computer Science, pp.247-258, 2001.

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

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 (TPHOLs), volume 3603 of Lecture Notes in Computer Science, pp.50-65, 2005.
DOI : 10.1007/11541868_4

G. Barthe, P. Courtieu, G. Dufay, S. Melo, and . Sousa, Tool-Assisted Specification and Verification of the JavaCard Platform, Proceedings of AMAST'02, pp.41-59, 2002.
DOI : 10.1007/3-540-45719-4_4

G. Barthe, B. Grégoire, C. Kunz, and T. Rezk, Certificate translation for optimizing compilers, Static Analysis, 13th Int. Symp., SAS 2006, pp.301-317, 2006.
DOI : 10.1145/1538917.1538919

N. Benton, A. Kennedy, and C. Varming, Some Domain Theory and Denotational Semantics in Coq, Theorem Proving in Higher Order Logics, 22nd International Conference, pp.115-130, 2009.
DOI : 10.1007/3-540-60275-5_72

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

Y. Bertot, Coq in a hurry Tutorial available at http://cel.archives-ouvertes.fr/ inria-00001173, 2008.

Y. Bertot, Theorem-proving support in programming language semantics, From Semantics to Computer Science ? Essays in Honour of Gilles Kahn, pp.337-362, 2009.
DOI : 10.1017/CBO9780511770524.016
URL : https://hal.archives-ouvertes.fr/inria-00160309

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

Y. Bertot, B. Grégoire, and X. Leroy, A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis, Types for Proofs and Programs, pp.66-81, 2004.
DOI : 10.1007/11617990_5
URL : https://hal.archives-ouvertes.fr/inria-00289549

Y. Bertot and V. Komendantsky, Fixed point semantics and partial recursion in Coq, Proceedings of the 10th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '08, pp.89-96, 2008.
DOI : 10.1145/1389449.1389461
URL : https://hal.archives-ouvertes.fr/inria-00190975

D. Cachera, T. P. Jensen, D. Pichardie, and V. Rusu, Extracting a data flow analyser in constructive logic, Theoretical Computer Science, vol.342, issue.1, pp.56-78, 2005.
DOI : 10.1016/j.tcs.2005.06.004
URL : https://hal.archives-ouvertes.fr/inria-00564633

G. J. Chaitin, Register allocation and spilling via graph coloring, Symposium on Compiler Construction) of SIGPLAN Notices, pp.98-105, 1982.
DOI : 10.1145/989393.989403

S. Coupet-grimal and W. Delobel, A Uniform and Certified Approach for Two Static Analyses, Types for Proofs and Programs, pp.115-137, 2004.
DOI : 10.1007/11617990_8

M. A. Dave, Compiler verification, ACM SIGSOFT Software Engineering Notes, vol.28, issue.6, pp.2-2, 2003.
DOI : 10.1145/966221.966235

X. Feng, R. Ferreira, and Z. Shao, On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning, Programming Languages and Systems, 16th European Symposium on Programming, pp.173-188, 2007.
DOI : 10.1007/978-3-540-71316-6_13

A. C. Fox, Formal Specification and Verification of ARM6, Theorem Proving in Higher Order Logics, 16th International Conference, pp.25-40, 2003.
DOI : 10.1007/10930755_2

G. Gonthier, Formal proof ? the four-color theorem. Notices of the, pp.1382-1393, 2008.

T. Hardin, L. Maranget, and B. Pagano, Functional runtime systems within the lambda-sigma calculus, Journal of Functional Programming, vol.8, issue.2, pp.131-176, 1998.
DOI : 10.1017/S0956796898002986
URL : https://hal.archives-ouvertes.fr/hal-01199543

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259

A. Hobor, A. W. Appel, and F. Z. Nardelli, Oracle Semantics for Concurrent Separation Logic, Programming Languages and Systems, 17th European Symposium on Programming, pp.353-367, 2008.
DOI : 10.1007/978-3-540-78739-6_27

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

G. Klein, Operating system verification???An overview, Sadhana, vol.9, issue.3, pp.27-69, 2009.
DOI : 10.1007/s12046-009-0002-4
URL : http://doi.org/10.1007/s12046-009-0002-4

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

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, 2008.
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768

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

G. Li, S. Owens, and K. Slind, Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic, Programming Languages and Systems, 16th European Symposium on Programming, pp.205-219, 2007.
DOI : 10.1007/978-3-540-71316-6_15

T. Lindholm and F. Yellin, The Java Virtual Machine Specification. The Java Series, 1999.

N. Marti, R. Affeldt, and A. Yonezawa, Formal Verification of the Heap Manager of an Operating System Using Separation Logic, Formal Methods and Software Engineering, 8th Int. Conf. ICFEM 2006, pp.400-419, 2006.
DOI : 10.1007/11901433_22

J. Mccarthy and J. Painter, Correctness of a compiler for arithmetic expressions, of Proc. of Symposia in Applied Mathematics, pp.33-41, 1967.
DOI : 10.1090/psapm/019/0242403

J. C. Michael and . Gordon, Mechanizing programming logics in higher-order logic, Current Trends in Hardware Verification and Automatic Theorem Proving, pp.387-439, 1988.

R. Milner, M. Tofte, R. Harper, and D. Macqueen, The definition of Standard ML (revised), 1997.

R. Milner and R. Weyhrauch, Proving compiler correctness in a mechanized logic, Proc. 7th Annual Machine Intelligence Workshop, pp.51-72, 1972.

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

P. D. Mosses, Denotational Semantics, pp.577-631, 1990.
DOI : 10.1016/B978-0-444-88074-1.50016-0

S. S. Muchnick, Advanced compiler design and implementation, 1997.

M. O. Myreen and M. J. Gordon, Hoare Logic for Realistically Modelled Machine??Code, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2007, pp.568-582, 2007.
DOI : 10.1007/978-3-540-71209-1_44

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

P. W. O-'hearn, J. C. Reynolds, and H. Yang, Local reasoning about programs that alter data structures, Computer Science Logic, 15th Int. Workshop, CSL 2001, pp.1-19, 2001.

C. Paulin-mohring, A constructive denotational semantics for Kahn networks in Coq, From Semantics to Computer Science ? Essays in Honour of Gilles Kahn, pp.383-414, 2009.
DOI : 10.1017/CBO9780511770524.018
URL : https://hal.archives-ouvertes.fr/inria-00431806

L. C. Paulson, Set theory for verification. II: Induction and recursion, Journal of Automated Reasoning, vol.11, issue.3, pp.167-215, 1995.
DOI : 10.1007/BF00881916

B. C. Pierce, Types and Programming Languages, 2002.

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

J. Reynolds, Definitional interpreters revisited. Higher-Order and Symbolic Computation, pp.355-361, 1998.

J. C. Reynolds, Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp.55-74, 2002.
DOI : 10.1109/LICS.2002.1029817

S. Sarkar, P. Sewell, F. Zappa-nardelli, S. Owens, T. Ridge et al., The semantics of x86-CC multiprocessor machine code, 36th symposium Principles of Programming Languages, pp.379-391, 2009.

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

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