PhD and Habilitation theses

[1] Sandrine Blazy. Sémantiques formelles. Habilitation à diriger les recherches, Université Évry Val d'Essone, October 2008. [ bib | HAL online | Local copy ]
[2] Zaynah Dargaye. Vérification formelle d'un compilateur pour langages fonctionnels. PhD thesis, Université Paris 7 Diderot, July 2009. [ bib | HAL online ]
[3] Jean-Baptise Tristan. Formal verification of translation validators. PhD thesis, Université Paris 7 Diderot, November 2009. [ bib | HAL online ]

Articles in journals

[1] Sandrine Blazy. Comment gagner confiance en C ? Technique et Science Informatiques, 26(9):1195--1200, 2007. [ bib | HAL online | Local copy ]
[2] Laurence Rideau, Bernard Paul Serpette, and Xavier Leroy. Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves. Journal of Automated Reasoning, 40(4):307--326, 2008. [ bib | HAL online | Local copy | At publisher's ]
[3] Xavier Leroy and Sandrine Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 41(1):1--31, 2008. [ bib | HAL online | Local copy | At publisher's ]
[4] Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107--115, 2009. [ bib | HAL online | Local copy | At publisher's ]
[5] Zaynah Dargaye and Xavier Leroy. A verified framework for higher-order uncurrying optimizations. Higher-Order and Symbolic Computation, 22(3):199--231, 2009. [ bib | Local copy | At publisher's ]
[6] Sandrine Blazy and Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263--288, 2009. [ bib | HAL online | Local copy | At publisher's ]
[7] Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363--446, 2009. [ bib | HAL online | Local copy | At publisher's ]
[8] Xavier Leroy and Hervé Grall. Coinductive big-step operational semantics. Information and Computation, 207(2):284--304, 2009. [ bib | HAL online | Local copy | At publisher's ]
[9] Xavier Leroy. Comment faire confiance à un compilateur? La Recherche, 440, April 2010. Les cahiers de l'INRIA. [ bib | Local copy | At publisher's ]
[10] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. Verified compilation of floating-point computations. Journal of Automated Reasoning, 54(2):135--163, 2015. [ bib | Local copy | At publisher's ]

Proceedings of international refereed conferences and workshops

[1] Sandrine Blazy and Xavier Leroy. Formal verification of a memory model for C-like imperative languages. In International Conference on Formal Engineering Methods (ICFEM 2005), volume 3785 of Lecture Notes in Computer Science, pages 280--299. Springer, 2005. [ bib | HAL online | Local copy | At publisher's ]
[2] Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. Formal verification of a C compiler front-end. In FM 2006: Int. Symp. on Formal Methods, volume 4085 of Lecture Notes in Computer Science, pages 460--475. Springer, 2006. [ bib | HAL online | Local copy | At publisher's ]
[3] Xavier Leroy. Coinductive big-step operational semantics. In European Symposium on Programming (ESOP'06), volume 3924 of Lecture Notes in Computer Science, pages 54--68. Springer, 2006. [ bib | HAL online | Local copy | At publisher's ]
[4] Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd ACM symposium on Principles of Programming Languages, pages 42--54. ACM Press, 2006. [ bib | HAL online | Local copy | At publisher's ]
[5] Yves Bertot, Benjamin Grégoire, and Xavier Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In Types for Proofs and Programs, Workshop TYPES 2004, volume 3839 of Lecture Notes in Computer Science, pages 66--81. Springer, 2006. [ bib | HAL online | Local copy | At publisher's ]
[6] Andrew W. Appel and Xavier Leroy. A list-machine benchmark for mechanized metatheory (extended abstract). In Proc. Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP'06), volume 174/5 of Electronic Notes in Computer Science, pages 95--108, 2007. [ bib | HAL online | Local copy | At publisher's ]
[7] Richard Bonichon, David Delahaye, and Damien Doligez. Zenon: an extensible automated theorem prover producing checkable proofs. In Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007, volume 4790 of Lecture Notes in Artificial Intelligence, pages 151--165. Springer, 2007. [ bib | HAL online | Local copy | At publisher's ]
[8] Zaynah Dargaye and Xavier Leroy. Mechanized verification of CPS transformations. In Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007, volume 4790 of Lecture Notes in Artificial Intelligence, pages 211--225. Springer, 2007. [ bib | HAL online | Local copy | At publisher's ]
[9] Sandrine Blazy. Experiments in validating formal semantics for C. In Proceedings of the C/C++ Verification Workshop, pages 95--102. Technical report ICIS-R07015, Radboud University Nijmegen, 2007. [ bib | HAL online | Local copy ]
[10] Andrew W. Appel and Sandrine Blazy. Separation logic for small-step Cminor. In Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007, volume 4732 of Lecture Notes in Computer Science, pages 5--21. Springer, 2007. [ bib | HAL online | Local copy | At publisher's ]
[11] Pierre Letouzey. Extraction in Coq: An overview. In Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008, volume 5028 of Lecture Notes in Computer Science, pages 359--369. Springer, 2008. [ bib | HAL online | At publisher's ]
[12] Yves Bertot and Vladimir Komendantsky. Fixed point semantics and partial recursion in Coq. In 10th int. ACM SIGPLAN conference on Principles and Practice of Declarative Programming (PPDP 2008), pages 89--96. ACM Press, 2008. [ bib | HAL online | At publisher's ]
[13] Jean-Baptiste Tristan and Xavier Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations. In Proceedings of the 35th ACM Symposium on Principles of Programming Languages (POPL'08), pages 17--27. ACM Press, January 2008. [ bib | HAL online | Local copy | At publisher's ]
[14] Sandrine Blazy and Benoît Robillard. Live-range unsplitting for faster optimal coalescing. In Proceedings of the ACM SIGPLAN/SIGBED 2009 conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2009), pages 70--79. ACM Press, 2009. [ bib | HAL online | Local copy | At publisher's ]
[15] Jean-Baptiste Tristan and Xavier Leroy. Verified validation of Lazy Code Motion. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'09), pages 316--326, 2009. [ bib | HAL online | Local copy | At publisher's ]
[16] Silvain Rideau and Xavier Leroy. Validating register allocation and spilling. In Compiler Construction (CC 2010), volume 6011 of Lecture Notes in Computer Science, pages 224--243. Springer, 2010. [ bib | Local copy | At publisher's ]
[17] Jean-Baptiste Tristan and Xavier Leroy. A simple, verified validator for software pipelining. In Proceedings of the 37th ACM Symposium on Principles of Programming Languages (POPL'10), pages 83--92. ACM Press, 2010. [ bib | Local copy | At publisher's ]
[18] Xavier Leroy. Verified squared: does critical software deserve verified tools? In 38th symposium Principles of Programming Languages, pages 1--2. ACM Press, 2011. Abstract of invited lecture. [ bib | Local copy | At publisher's ]
[19] Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. Towards optimizing certified compilation in flight control software. In Workshop on Predictability and Performance in Embedded Systems (PPES 2011), volume 18 of OpenAccess Series in Informatics, pages 59--68. Dagstuhl Publishing, 2011. [ bib | Local copy | At publisher's ]
[20] Valentin Robert and Xavier Leroy. A formally-verified alias analysis. In Certified Programs and Proofs (CPP 2012), volume 7679 of Lecture Notes in Computer Science, pages 11--26. Springer, 2012. [ bib | Local copy | At publisher's ]
[21] Xavier Leroy. Mechanized semantics for compiler verification. In Ranjit Jhala and Atsushi Igarashi, editors, Programming Languages and Systems, 10th Asian Symposium, APLAS 2012, volume 7705 of Lecture Notes in Computer Science, pages 386--388. Springer, 2012. Abstract of invited talk. [ bib | Local copy | At publisher's ]
[22] Jacques-Henri Jourdan, François Pottier, and Xavier Leroy. Validating LR(1) parsers. In Programming Languages and Systems -- 21st European Symposium on Programming, ESOP 2012, volume 7211 of Lecture Notes in Computer Science, pages 397--416. Springer, 2012. [ bib | Local copy | At publisher's ]
[23] Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. Formally verified optimizing compilation in ACG-based flight control software. In Embedded Real Time Software and Systems (ERTS 2012), 2012. [ bib | Local copy ]
[24] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A formally-verified C compiler supporting floating-point arithmetic. In ARITH, 21st IEEE International Symposium on Computer Arithmetic, pages 107--115. IEEE Computer Society Press, 2013. [ bib | Local copy ]

Proceedings of national conferences and workshops

[1] Zaynah Dargaye. Décurryfication certifiée. In Journées Francophones des Langages Applicatifs (JFLA'07), pages 119--134. INRIA, 2007. [ bib | HAL online | Local copy ]
[2] Sandrine Blazy, Benoît Robillard, and Eric Soutif. Coloration avec préférences dans les graphes triangulés. In Journées Graphes et Algorithmes (JGA'07), November 2007. [ bib | Local copy ]
[3] Sandrine Blazy, Benoît Robillard, and Éric Soutif. Coloration avec préférences: complexité, inégalités valides et vérification formelle. In ROADEF'08, 9e congrès de la Société Française de Recherche Opérationnelle et d'Aide à la Décision, 2008. [ bib | HAL online ]
[4] Sandrine Blazy, Benoît Robillard, and Eric Soutif. Vérification formelle d'un algorithme d'allocation de registres par coloration de graphes. In Journées Francophones des Langages Applicatifs (JFLA'08), pages 31--46, Étretat, France, January 2008. [ bib | HAL online | Local copy ]
[5] Stéphane Glondu. Extraction certifiée dans Coq-en-Coq. In Journées Francophones des Langages Applicatifs (JFLA'09), pages 105--118. INRIA, 2009. [ bib | HAL online | Local copy ]

Book chapters

[1] Yves Bertot. Structural abstract interpretation: A formal study using Coq. In Ana Bove and Jorge Sousa Pinto, editors, Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, volume 5520 of Lecture Notes in Computer Science, pages 153--194. Springer, 2009. [ bib | HAL online | At publisher's ]
[2] Yves Bertot. Theorem proving support in programming language semantics. In Y. Bertot, G. Huet, J.-J. Lévy, and G. Plotkin, editors, From Semantics to Computer Science -- Essays in Honour of Gilles Kahn, pages 337--362. Cambridge University Press, 2009. [ bib | At publisher's ]
[3] Xavier Leroy. Mechanized semantics. In Logics and languages for reliability and security, volume 25 of NATO Science for Peace and Security Series D: Information and Communication Security, pages 195--224. IOS Press, 2010. [ bib | Local copy | At publisher's ]
[4] Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. The CompCert memory model. In Andrew W. Appel, editor, Program Logics for Certified Compilers. Cambridge University Press, April 2014. [ bib | Local copy ]

Technical reports

[1] Andrew W. Appel and Xavier Leroy. A list-machine benchmark for mechanized metatheory. Research report 5914, INRIA, 2006. [ bib | HAL online ]
[2] Yves Bertot. Theorem proving support in programming language semantics. Research report 6242, INRIA, 2007. [ bib | HAL online ]
[3] Andrew W. Appel and Sandrine Blazy. Separation logic for small-step Cminor (extended version). Research report 6138, INRIA, 2007. 29 pages. [ bib | HAL online ]
[4] Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. The CompCert memory model, version 2. Research report RR-7987, INRIA, June 2012. [ bib | Local copy ]

Preprints

[1] Yves Bertot. Extending the calculus of constructions with Tarski's fix-point theorem. 2006. [ bib | HAL online ]