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

A. W. Appel, Foundational proof-carrying code, In: Logic in Computer Science, pp.247-258, 2001.
DOI : 10.1109/fits.2003.1264926

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.2076

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

C. W. Barrett, Y. Fang, B. Goldberg, Y. Hu, A. Pnueli et al., TVOC: A Translation Validator for Optimizing Compilers, Computer Aided Verification, 17th International Conference, CAV 2005, pp.291-295, 2005.
DOI : 10.1007/11513988_29

G. Barthe, P. Courtieu, G. Dufay, and S. Melo-de-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, J. Forest, D. Pichardie, and V. Rusu, Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant, Functional and Logic Programming , 8th Int. Symp. FLOPS, pp.114-129, 2006.
DOI : 10.1007/11737414_9

URL : https://hal.archives-ouvertes.fr/inria-00564237

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

G. Barthe and C. Kunz, Certificate??Translation??in??Abstract??Interpretation, 17th European Symposium on Programming, pp.368-382, 2008.
DOI : 10.1007/978-3-540-78739-6_28

N. Benton and C. K. Hur, Biorthogonality, step-indexing and compiler correctness, International Conference on Functional Programming, pp.97-108, 2009.

L. Beringer, Functional elimination of phi-instructions, Proc. 5th Workshop on Compiler Optimization meets Compiler Verification Electronic Notes in Theoretical Computer Science, pp.3-20, 2006.

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

S. Beyer, C. Jacobi, D. Kröning, D. Leinenbach, and W. Paul, Putting it all together ??? Formal verification of the VAMP, International Journal on Software Tools for Technology Transfer, vol.20, issue.2, pp.411-430, 2006.
DOI : 10.1007/s10009-006-0204-6

S. Blazy, Z. Dargaye, and X. Leroy, Formal Verification of a C Compiler Front-End, FM 2006: Int. Symp. on Formal Methods, pp.460-475, 2006.
DOI : 10.1007/11813040_31

URL : https://hal.archives-ouvertes.fr/inria-00106401

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

J. O. Blech, S. Glesner, J. Leitner, and S. Mülling, Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL, Proc. COCV Workshop (Compiler Optimization meets Compiler Verification), Electronic Notes in Theoretical Computer Science, pp.33-51, 2005.
DOI : 10.1016/j.entcs.2005.02.042

H. J. Boehm, Threads cannot be implemented as a library, Programming Language Design and Implementation 2005, pp.261-268, 2005.
DOI : 10.1145/1065010.1065042

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.308.5939

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, SIGPLAN Notices, pp.98-105, 1982.
DOI : 10.1145/989393.989403

J. Chen, C. Hawblitzel, F. Perry, M. Emmi, J. Condit et al., Type-preserving compilation for large-scale optimizing object-oriented compilers, In: Programming Language Design and Implementation, pp.183-192, 2008.

L. Chirica and A. Martin, Toward compiler implementation correctness proofs, ACM Transactions on Programming Languages and Systems, vol.8, issue.2, pp.185-214, 1986.
DOI : 10.1145/5397.30847

A. J. Chlipala, A certified type-preserving compiler from lambda calculus to assembly language. In: Programming Language Design and Implementation, pp.54-65, 2007.

G. Clemmensen and O. Oest, Formal specification and development of an Ada compiler, IEEE Conf. on Soft. Engineering, pp.430-440, 1984.

S. Coupet-grimal and W. Delobel, A Uniform and Certified Approach for Two Static Analyses, Lecture Notes in Computer Science, vol.3839, pp.115-137, 2004.
DOI : 10.1007/11617990_8

Z. Dargaye, Vérification formelle d'un compilateur pour langages fonctionnels, 2009.

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

A. Dold, T. Gaul, and W. Zimmermann, Mechanized verification of compiler backends, In: Int. Workshop on Software Tools for Technology Transfer BRICS Notes, vol.984, pp.13-24, 1998.

A. Dold and V. Vialard, A Mechanically Verified Compiling Specification for a Lisp Compiler, Proc. FST TCS 2001, pp.144-155, 2001.
DOI : 10.1007/3-540-45294-X_13

E. Eide and J. Regehr, Volatiles are miscompiled, and what to do about it, Proceedings of the 7th ACM international conference on Embedded software, EMSOFT '08, pp.255-264, 2008.
DOI : 10.1145/1450058.1450093

J. R. Ellis, Bulldog: a compiler for VLSI architectures ACM Doctoral Dissertation Awards series, 1986.

X. Feng, Z. Ni, Z. Shao, and Y. Guo, An open framework for foundational proof-carrying code, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation , TLDI '07, pp.67-78, 2007.
DOI : 10.1145/1190315.1190325

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

L. George and A. W. Appel, Iterated register coalescing, ACM Transactions on Programming Languages and Systems, vol.18, issue.3, pp.300-324, 1996.
DOI : 10.1145/229542.229546

G. Goos and W. Zimmermann, Verification of Compilers, Lecture Notes in Computer Science, vol.1710, pp.201-230, 1999.
DOI : 10.1007/3-540-48092-7_10

B. Grégoire, Compilation des termes de preuves: un (nouveau) mariage entre Coq et OCaml, 2003.

S. Gulwani and G. C. Necula, A Polynomial-Time Algorithm for Global Value Numbering, Static Analysis, 11th Int. Symposium, SAS 2004, pp.212-227, 2004.
DOI : 10.1007/978-3-540-27864-1_17

T. C. Hales, Formal proof, Notices of the American Mathematical Society, vol.55, issue.11, pp.1370-1380, 2008.

P. H. Hartel and L. A. Moreau, Formalizing the safety of Java, the Java virtual machine, and Java card, ACM Computing Surveys, vol.33, issue.4, pp.517-558, 2001.
DOI : 10.1145/503112.503115

F. Henderson, Accurate garbage collection in an uncooperative environment, International Symposium on Memory Management 2002, SIGPLAN Notices, pp.150-156, 2003.

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

Y. Huang, B. R. Childers, and M. L. Soffa, Catching and Identifying Bugs in Register Allocation, Static Analysis, 13th Int. Symp., SAS 2006, pp.281-300, 2006.
DOI : 10.1007/11823230_19

G. P. Huet, The Zipper, Journal of Functional Programming, vol.7, issue.5, pp.549-554, 1997.
DOI : 10.1017/S0956796897002864

M. Huisman and B. Jacobs, Java Program Verification via a Hoare Logic with Abrupt Termination, Fundamental Approaches to Software Engineering, 3rd Int. Conf. FASE 2000, pp.284-303, 2000.
DOI : 10.1007/3-540-46428-X_20

G. A. Kildall, A unified approach to global program optimization, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '73, pp.194-206, 1973.
DOI : 10.1145/512927.512945

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

J. Knoop, D. Koschützki, and B. Steffen, Basic-block graphs: Living dinosaurs?, Proc. Compiler Construction '98, pp.65-79, 1998.
DOI : 10.1007/BFb0026423

J. Knoop, O. Rüthing, and B. Steffen, Optimal code motion: theory and practice, ACM Transactions on Programming Languages and Systems, vol.16, issue.4, pp.1117-1155, 1994.
DOI : 10.1145/183432.183443

D. Lacey, N. D. Jones, E. Van-wyk, and C. C. Frederiksen, Proving correctness of compiler optimizations by temporal logic, 29th symposium Principles of Programming Languages, pp.283-294, 2002.

D. Leinenbach, W. Paul, and E. Petrova, Towards the formal verification of a C0 compiler: code generation and implementation correctness, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), pp.2-11, 2005.
DOI : 10.1109/SEFM.2005.51

D. Leinenbach and E. Petrova, Pervasive compiler verification In: 3rd Int, Workshop on Systems Software Verification, Electronic Notes in Theoretical Computer Science, pp.23-40, 2008.

S. Lerner, T. Millstein, E. Rice, and C. Chambers, Automated soundness proofs for dataflow analyses and transformations via local rules, 32nd symposium Principles of Programming Languages, pp.364-377, 2005.

X. Leroy, Java bytecode verification: algorithms and formalizations, Journal of Automated Reasoning, vol.3034, pp.235-269, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01499939

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, 33rd symposium Principles of Programming Languages, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

X. Leroy, The Compcert verified compiler, software and commented proof Available at http://compcert.inria, 2009.

X. Leroy and S. Blazy, Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations, Journal of Automated Reasoning, vol.17, issue.5???6, pp.1-31, 2008.
DOI : 10.1007/s10817-008-9099-0

URL : https://hal.archives-ouvertes.fr/inria-00289542

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

P. Letouzey, A New Extraction for Coq, Lecture Notes in Computer Science, vol.2646, pp.200-219, 2002.
DOI : 10.1007/3-540-39185-1_12

URL : https://hal.archives-ouvertes.fr/hal-00150914

P. Letouzey, Extraction in Coq: An Overview, CiE Lecture Notes in Computer Science, vol.5028, pp.359-369, 2008.
DOI : 10.1007/978-3-540-69407-6_39

URL : https://hal.archives-ouvertes.fr/hal-00338973

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

G. Li and K. Slind, Compilation as Rewriting in Higher Order Logic, Lecture Notes in Computer Science, vol.4603, pp.19-34, 2007.
DOI : 10.1007/978-3-540-73595-3_3

C. Lindig, Random testing of C calling conventions, Proceedings of the Sixth sixth international symposium on Automated analysis-driven debugging , AADEBUG'05, pp.3-12, 2005.
DOI : 10.1145/1085130.1085132

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

W. M. Mckeeman, Differential testing for software, Digital Technical Journal, vol.10, issue.1, pp.100-107, 1998.

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

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.

G. Morrisett, K. Crary, N. Glew, and D. Walker, Stack-based typed assembly language, Journal of Functional Programming, vol.12, issue.1, pp.43-88, 2002.
DOI : 10.1007/bfb0055511

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.124.2163

G. Morrisett, D. Walker, K. Crary, and N. Glew, From System F to typed assembly language, ACM Transactions on Programming Languages and Systems, vol.21, issue.3, pp.528-569, 1999.

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

M. Müller-olm, Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction, Lecture Notes in Computer Science, vol.1283, 1997.
DOI : 10.1007/BFb0027453

G. C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.106-119, 1997.
DOI : 10.1145/263699.263712

G. C. Necula, Translation validation for an optimizing compiler In: Programming Language Design and Implementation, pp.83-95, 2000.

G. C. Necula, S. Mcpeak, S. P. Rahul, and W. Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Compiler Construction, 11th International Conference, pp.213-228, 2002.
DOI : 10.1007/3-540-45937-5_16

G. C. Necula and S. P. Rahul, Oracle-based checking of untrusted software, 28th symposium Principles of Programming Languages, pp.142-154, 2001.

O. 'hearn and P. W. , Resources, concurrency and local reasoning, Theoretical Computer Science, vol.37513, pp.271-307, 2007.

W. Paul, The Verisoft project, 2003.

P. Jones, S. L. Ramsey, N. Reig, and F. , C-???: A Portable Assembly Language that Supports Garbage Collection, PPDP'99: International Conference on Principles and Practice of Declarative Programming, pp.1-28, 1999.
DOI : 10.1007/10704567_1

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

A. Pnueli, M. Siegel, and E. Singerman, Translation validation, TACAS '98, pp.151-166, 1998.
DOI : 10.1007/BFb0054170

S. Pop, The SSA representation framework: semantics, analyses and GCC implementation, 2006.
URL : https://hal.archives-ouvertes.fr/pastel-00002281

L. Rideau, B. P. Serpette, and X. Leroy, Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves, Journal of Automated Reasoning, vol.13, issue.12, pp.307-326, 2008.
DOI : 10.1007/s10817-007-9096-8

URL : https://hal.archives-ouvertes.fr/inria-00289709

M. Rinard and D. Marinov, Credible compilation with pointers, Proc. FLoC Workshop on Run-Time Result Verification, 1999.

X. Rival, Symbolic transfer function-based approaches to certified compilation, 31st symposium Principles of Programming Languages, pp.1-13, 2004.

B. K. Rosen, M. N. Wegman, and F. K. Zadeck, Global value numbers and redundant computations, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '88, pp.12-27, 1988.
DOI : 10.1145/73560.73562

Z. Shao, V. Trifonov, B. Saha, and N. Papaspyrou, A type system for certified binaries, ACM Transactions on Programming Languages and Systems, vol.27, issue.1, pp.1-45, 2005.
DOI : 10.1145/1053468.1053469

R. Stärk, J. Schmid, and E. Börger, Java and the Java Virtual Machine, 2001.
DOI : 10.1007/978-3-642-59495-3

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

M. Strecker, Compiler verification for C0 (intermediate report), 2005.

J. B. Tristan and X. Leroy, Formal verification of translation validators: A case study on instruction scheduling optimizations, 35th symposium Principles of Programming Languages, pp.17-27, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00289540

J. B. Tristan and X. Leroy, Verified validation of Lazy Code Motion In: Programming Language Design and Implementation, pp.316-326, 2009.

L. D. Zuck, A. Pnueli, Y. Fang, and B. Goldberg, VOC, Electronic Notes in Theoretical Computer Science, vol.65, issue.2, pp.2-18, 2002.
DOI : 10.1016/S1571-0661(04)80393-1