Modern Compiler Implementation in ML, 1998. ,
DOI : 10.1017/CBO9780511811449
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
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
TVOC: A Translation Validator for Optimizing Compilers, Computer Aided Verification, 17th International Conference, CAV 2005, pp.291-295, 2005. ,
DOI : 10.1007/11513988_29
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
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
Certificate translation for optimizing compilers, Static Analysis, 13th Int. Symp., SAS 2006, pp.301-317, 2006. ,
DOI : 10.1145/1538917.1538919
Certificate??Translation??in??Abstract??Interpretation, 17th European Symposium on Programming, pp.368-382, 2008. ,
DOI : 10.1007/978-3-540-78739-6_28
Biorthogonality, step-indexing and compiler correctness, International Conference on Functional Programming, pp.97-108, 2009. ,
Functional elimination of phi-instructions, Proc. 5th Workshop on Compiler Optimization meets Compiler Verification Electronic Notes in Theoretical Computer Science, pp.3-20, 2006. ,
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
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
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
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
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
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
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
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
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
Register allocation and spilling via graph coloring, Symposium on Compiler Construction, SIGPLAN Notices, pp.98-105, 1982. ,
DOI : 10.1145/989393.989403
Type-preserving compilation for large-scale optimizing object-oriented compilers, In: Programming Language Design and Implementation, pp.183-192, 2008. ,
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 certified type-preserving compiler from lambda calculus to assembly language. In: Programming Language Design and Implementation, pp.54-65, 2007. ,
Formal specification and development of an Ada compiler, IEEE Conf. on Soft. Engineering, pp.430-440, 1984. ,
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
Vérification formelle d'un compilateur pour langages fonctionnels, 2009. ,
Compiler verification, ACM SIGSOFT Software Engineering Notes, vol.28, issue.6, pp.2-2, 2003. ,
DOI : 10.1145/966221.966235
Mechanized verification of compiler backends, In: Int. Workshop on Software Tools for Technology Transfer BRICS Notes, vol.984, pp.13-24, 1998. ,
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
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
Bulldog: a compiler for VLSI architectures ACM Doctoral Dissertation Awards series, 1986. ,
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
Formal Specification and Verification of ARM6, 16th International Conference, pp.25-40, 2003. ,
DOI : 10.1007/10930755_2
Iterated register coalescing, ACM Transactions on Programming Languages and Systems, vol.18, issue.3, pp.300-324, 1996. ,
DOI : 10.1145/229542.229546
Verification of Compilers, Lecture Notes in Computer Science, vol.1710, pp.201-230, 1999. ,
DOI : 10.1007/3-540-48092-7_10
Compilation des termes de preuves: un (nouveau) mariage entre Coq et OCaml, 2003. ,
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
Formal proof, Notices of the American Mathematical Society, vol.55, issue.11, pp.1370-1380, 2008. ,
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
Accurate garbage collection in an uncooperative environment, International Symposium on Memory Management 2002, SIGPLAN Notices, pp.150-156, 2003. ,
Oracle Semantics for Concurrent Separation Logic, 17th European Symposium on Programming, pp.353-367, 2008. ,
DOI : 10.1007/978-3-540-78739-6_27
Catching and Identifying Bugs in Register Allocation, Static Analysis, 13th Int. Symp., SAS 2006, pp.281-300, 2006. ,
DOI : 10.1007/11823230_19
The Zipper, Journal of Functional Programming, vol.7, issue.5, pp.549-554, 1997. ,
DOI : 10.1017/S0956796897002864
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
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
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
Basic-block graphs: Living dinosaurs?, Proc. Compiler Construction '98, pp.65-79, 1998. ,
DOI : 10.1007/BFb0026423
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
Proving correctness of compiler optimizations by temporal logic, 29th symposium Principles of Programming Languages, pp.283-294, 2002. ,
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
Pervasive compiler verification In: 3rd Int, Workshop on Systems Software Verification, Electronic Notes in Theoretical Computer Science, pp.23-40, 2008. ,
Automated soundness proofs for dataflow analyses and transformations via local rules, 32nd symposium Principles of Programming Languages, pp.364-377, 2005. ,
Java bytecode verification: algorithms and formalizations, Journal of Automated Reasoning, vol.3034, pp.235-269, 2003. ,
URL : https://hal.archives-ouvertes.fr/hal-01499939
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
The Compcert verified compiler, software and commented proof Available at http://compcert.inria, 2009. ,
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
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
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
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
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
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
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
Correctness of a compiler for arithmetic expressions, Proc. of Symposia in Applied Mathematics, pp.33-41, 1967. ,
DOI : 10.1090/psapm/019/0242403
Differential testing for software, Digital Technical Journal, vol.10, issue.1, pp.100-107, 1998. ,
Proving compiler correctness in a mechanized logic, Proc. 7th Annual Machine Intelligence Workshop, Machine Intelligence, pp.51-72, 1972. ,
A mechanically verified language implementation, Journal of Automated Reasoning, vol.5, issue.4, pp.461-492, 1989. ,
DOI : 10.1007/BF00243133
Piton: a mechanically verified assembly-language, 1996. ,
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
From System F to typed assembly language, ACM Transactions on Programming Languages and Systems, vol.21, issue.3, pp.528-569, 1999. ,
Advanced compiler design and implementation, 1997. ,
Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction, Lecture Notes in Computer Science, vol.1283, 1997. ,
DOI : 10.1007/BFb0027453
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
Translation validation for an optimizing compiler In: Programming Language Design and Implementation, pp.83-95, 2000. ,
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
Oracle-based checking of untrusted software, 28th symposium Principles of Programming Languages, pp.142-154, 2001. ,
Resources, concurrency and local reasoning, Theoretical Computer Science, vol.37513, pp.271-307, 2007. ,
The Verisoft project, 2003. ,
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
Interprétation abstraite en logique intuitionniste: extraction d'analyseurs Java certifiés, University Rennes, vol.1, 2005. ,
Translation validation, TACAS '98, pp.151-166, 1998. ,
DOI : 10.1007/BFb0054170
The SSA representation framework: semantics, analyses and GCC implementation, 2006. ,
URL : https://hal.archives-ouvertes.fr/pastel-00002281
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
Credible compilation with pointers, Proc. FLoC Workshop on Run-Time Result Verification, 1999. ,
Symbolic transfer function-based approaches to certified compilation, 31st symposium Principles of Programming Languages, pp.1-13, 2004. ,
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
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
Java and the Java Virtual Machine, 2001. ,
DOI : 10.1007/978-3-642-59495-3
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
Compiler verification for C0 (intermediate report), 2005. ,
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
Verified validation of Lazy Code Motion In: Programming Language Design and Implementation, pp.316-326, 2009. ,
VOC, Electronic Notes in Theoretical Computer Science, vol.65, issue.2, pp.2-18, 2002. ,
DOI : 10.1016/S1571-0661(04)80393-1