| 2017 | PLDI | A formally verified compiler for Lustre. | Timothy Bourke, Llio Brun, Pierre-variste Dagand, Xavier Leroy, Marc Pouzet, Lionel Rieg |
| 2016 | ICALP | Formally Verifying a Compiler: What Does It Mean, Exactly? | Xavier Leroy |
| 2015 | POPL | A Formally-Verified C Static Analyzer. | Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie |
| 2014 | FMCAD | Compiler verification for fun and profit. | Xavier Leroy |
| 2014 | ITP | Formal C Semantics: CompCert and the C Standard. | Robbert Krebbers, Xavier Leroy, Freek Wiedijk |
| 2014 | SEFM | Formal Proofs of Code Generation and Verification Tools. | Xavier Leroy |
| 2013 | ARITH | A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. | Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond |
| 2012 | APLAS | Mechanized Semantics for Compiler Verification. | Xavier Leroy |
| 2012 | CPP | Mechanized Semantics for Compiler Verification. | Xavier Leroy |
| 2012 | CPP | A Formally-Verified Alias Analysis. | Valentin Robert, Xavier Leroy |
| 2012 | ESOP | Validating LR(1) Parsers. | Jacques-Henri Jourdan, Franois Pottier, Xavier Leroy |
| 2012 | POPL | A mechanized semantics for C++ object construction and destruction, with applications to resource management. | Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy |
| 2011 | CGO | Formally verifying a compiler: Why? How? How far? | Xavier Leroy |
| 2011 | DATE | Towards Formally Verified Optimizing Compilation in Flight Control Software. | Ricardo Bedin Frana, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris |
| 2011 | POPL | Verified squared: does critical software deserve verified tools? | Xavier Leroy |
| 2011 | POPL | Formal verification of object layout for c++ multiple inheritance. | Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy |
| 2010 | CC | Validating Register Allocation and Spilling. | Silvain Rideau, Xavier Leroy |
| 2010 | POPL | A simple, verified validator for software pipelining. | Jean-Baptiste Tristan, Xavier Leroy |
| 2009 | PLDI | Verified validation of lazy code motion. | Jean-Baptiste Tristan, Xavier Leroy |
| 2008 | POPL | Formal verification of translation validators: a case study on instruction scheduling optimizations. | Jean-Baptiste Tristan, Xavier Leroy |
| 2007 | LPAR | Mechanized Verification of CPS Transformations. | Zaynah Dargaye, Xavier Leroy |
| 2007 | MEMOCODE | Formal verification of an optimizing compiler. | Xavier Leroy |
| 2006 | ESOP | Coinductive Big-Step Operational Semantics. | Xavier Leroy |
| 2006 | FM | Formal Verification of a C Compiler Front-End. | Sandrine Blazy, Zaynah Dargaye, Xavier Leroy |
| 2006 | POPL | Formal certification of a compiler back-end or: programming a compiler with a proof assistant. | Xavier Leroy |
| 2005 | ICFEM | Formal Verification of a Memory Model for | Sandrine Blazy, Xavier Leroy |
| 2004 | ESOP | Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types. | Tom Hirschowitz, Xavier Leroy, J. B. Wells |
| 2003 | ESOP | Computer Security from a Programming Language and Static Analysis Perspective. | Xavier Leroy |
| 2003 | GPCE | Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection. | Cristiano Calcagno, Walid Taha, Liwen Huang, Xavier Leroy |
| 2003 | PPDP | Compilation of extended recursion in call-by-value functional languages. | Tom Hirschowitz, Xavier Leroy, J. B. Wells |
| 2002 | ESOP | Mixin Modules in a Call-by-Value Setting. | Tom Hirschowitz, Xavier Leroy |
| 2002 | ICFP | A compiled implementation of strong reduction. | Benjamin Grgoire, Xavier Leroy |
| 2001 | CAV | Java Bytecode Verification: An Overview. | Xavier Leroy |
| 1999 | POPL | Type-Based Analysis of Uncaught Exceptions. | Franois Pessaux, Xavier Leroy |
| 1998 | POPL | Security Properties of Typed Applets. | Xavier Leroy, Franois Rouaix |
| 1995 | POPL | Applicative Functors and Fully Transparent Higher-Order Modules. | Xavier Leroy |
| 1994 | POPL | Manifest Types, Modules, and Separate Compilation. | Xavier Leroy |
| 1993 | POPL | A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML. | Damien Doligez, Xavier Leroy |
| 1993 | POPL | Polymorphism by Name for References and Continuations. | Xavier Leroy |
| 1992 | POPL | Unboxed Objects and Polymorphic Typing. | Xavier Leroy |
| 1991 | POPL | Polymorphic Type Inference and Assignment. | Xavier Leroy, Pierre Weis |