Xavier Leroy's mugshot

Hello and welcome to my corner of the Web. I'm a senior computer scientist interested in all scientific aspects of computer programming. I work at INRIA, a French public research institute in computer science and applied mathematics. I lead the Gallium research team, part of the Paris-Rocquencourt research center of INRIA.

News

[10/2014] Publication: Verified compilation of floating-point computations, with Sylvie Boldo, Jacques-Henri Jourdan, and Guillaume Melquiond, to appear in Journal of Automated Reasoning.

[09/2014] Software and Coq development: version 2.4 of Compcert is released, featuring a revised handling of single-precision floating-point computations.

[06/2014] Conference: I have the pleasure of co-chairing the program committee of CPP 2015, with Alwen Tiu. CPP is the conference on Certified Programs and Proofs, and is for the first time colocated with POPL 2015 in Mumbai, India. Consider submitting!

[05/2014] Software and Coq development: release of Compcert version 2.3, integrating Jacques-Henri Jourdan's formally-verified parser.

[04/2014] Book chapter: Andrew Appel's book Program Logics for Certified Compilers is published. It contains much material about CompCert, including a chapter on the CompCert memory model written by Andrew Appel, Sandrine Blazy, Gordon Stewart and I.

[02/2014] Software and Coq development: release of Compcert version 2.2, with two new static analyses (value analysis and need analysis) that enable more optimizations.

[06/2013] Software and Coq development: version 2.0 of the Compcert C verified compiler is released. It features the long-awaited support for 64-bit integers, as well as a new register allocator -- decidedly "2.0" material!

[01/2013] Software and Coq development: release of version 1.12 of the Compcert C verified compiler.

[01/2013] Publication: A Formally-Verified C Compiler Supporting Floating-Point Arithmetic, with Sylvie Boldo, Jacques-Henri Jourdan, and Guillaume Melquiond, 21st IEEE ARITH conference, April 2013.

[12/2012] Award: I am deeply honored to receive the Microsoft Research Verified Software Milestone Award in recognition of my work on CompCert.

[10/2012] Publication: A formally-verified alias analysis, with Valentin Robert, conference CPP 2012.

[07/2012] Software and Coq development: release of version 1.11 of the Compcert C verified compiler. Now with a fully-verified handling of floating-point arithmetic. (See paper above).

[06/2012] Tech report: The CompCert memory model, version 2, with Andrew Appel, Sandrine Blazy, and Gordon Stewart, INRIA research report RR-7987. Everything you (n)ever wanted to know about recent evolutions of the CompCert memory model.

[03/2012] Software and Coq development: release of version 1.10 of the Compcert C verified compiler.

[01/2012] Publication: Validating LR(1) parsers, with Jacques-Henri Jourdan and François Pottier, symposium ESOP 2012.

[12/2011] Publication: Formally verified optimizing compilation in ACG-based flight control software, with Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Marc Pantel and Jean Souyris, symposium ERTS2 2012.

[11/2011] Publication: A mechanized semantics for C++ object construction and destruction, with applications to resource management, with Tahina Ramananandro and Gabriel Dos Reis. POPL 2012.

[10/2011] Award: along with Sandrine Blazy, Zaynah Dargaye and Jean-Baptiste Tristan, I received the 2011 La Recherche award in Information Sciences for our work on the CompCert verified C compiler.

[08/2011] Software and Coq development: release of version 1.9 of the Compcert C verified compiler.

[06/2011] Course material: Proving a compiler: mechanized verification of program transformations and static analyses, lecture given at the Oregon Programming Languages Summer School 2011

[04/2011] Publication: A list-machine benchmark for mechanized metatheory, with Andrew Appel and Robert Dockins, to appear in Journal of Automated Reasoning.

[01/2011] Publication: Towards optimizing certified compilation in flight control software, with Ricardo Bedin França, Denis Favre-Felix, Marc Pantel and Jean Souyris, workshop PPES 2011.

[11/2010] Publication: Formal verification of object layout for C++ multiple inheritance, with Tahina Ramananandro and Gabriel Dos Reis, POPL 2011.

[09/2010] Software and Coq development: release of version 1.8 of the Compcert C verified compiler.

[04/2010] Popular science: Comment faire confiance à un compilateur? (in French). A short introduction to compiler verification, published in the French magazine La Recherche, april 2010 issue.

[03/2010] Software and Coq development: release of version 1.7 of the Compcert C verified compiler, featuring a new C type-checker/elaborator/simplifier and a refined memory model.

[12/2009] Publication: Validating register allocation and spilling, with Silvain Rideau, Compiler Construction 2010.

[12/2009] Publication: A verified framework for higher-order uncurrying optimizations, with Zaynah Dargaye, Higher-Order and Symbolic Computation 22(3).

[11/2009] Publication: A formally verified compiler back-end. My ars magna on the Compcert verified back-end (80 pages!), now published in Journal of Automated Reasoning 43(4).

[11/2009] Publication: A simple, verified validator for software pipelining, with Jean-Baptiste Tristan, POPL 2010.

[08/2009] Course material: Mechanized semantics, with applications to program proof and compiler verification, lecture given at the 2009 Marktoberdorf summer school.

[08/2009] Software and Coq development: release of version 1.5 of the Compcert C verified compiler. Now with full support for goto statements!

[07/2009] Nostalgia: the books Le langage Caml (1993; 1999) and Manuel de référence du langage Caml (1993) are now freely available in PDF format.

[04/2009] Publication: Formal verification of a realistic compiler. A short overview of the CompCert verified compiler, published in Communications of the ACM, July 2009, along with a perspective written by Greg Morrisett.

[04/2009] Software and Coq development: release of version 1.4 of the Compcert C verified compiler.

[03/2009] Publication: Verified validation of Lazy Code Motion, with Jean-Baptiste Tristan, PLDI 2009.

[02/2009] Publication: Compilation of extended recursion in call-by-value functional languages, with Tom Hirschowitz and J. B. Wells, published in Higher-Order and Symbolic Computation 22(1).

[01/2009] Publication: Mechanized semantics for the Clight subset of the C language, with Sandrine Blazy, published in Journal of Automated Reasoning 43(3).

[12/2008] Software: release of Objective Caml version 3.11.

[08/2008] Software and Coq development: release of version 1.3 of the Compcert C verified compiler.

[03/2008] Software and Coq development: first public release of the Compcert C verified compiler.

[02/2008] Publication: Formal verification of a C-like memory model and its uses for verifying program transformations, with Sandrine Blazy, published in Journal of Automated Reasoning 41(1). Accompanied with a Coq development.

[02/2008] Talk: Du langage à l'action: compilation et typage (in French), tutorial lecture given at Collège de France in Gérard Berry's course. A video of the lecture is available.

[12/2007] Publication: Coinductive big-step operational semantics, with Hervé Grall, published in Information and Computation. Accompanied with a Coq development.

[12/2007] Publication: Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves, with Laurence Rideau and Bernard Paul Serpette, published in Journal of Automated Reasoning. Accompanied with a Coq development.

[11/2007] Publication: Formal verification of translation validators: A case study on instruction scheduling optimizations, with Jean-Baptiste Tristan, POPL 2008.

[10/2007] Award: I am honored to be awarded the 2007 Michel Monpetit prize of the French Academy of Sciences.

[09/2007] New journal: Journal of Formalized Reasoning. A great venue for publishing mechanized formalizations and verifications.

[08/2007] Coq development: Commented Coq development for the Compcert verified compiler.

[07/2007] Publication: Mechanized verification of CPS transformations, with Zaynah Dargaye, LPAR 2007.

[06/2007] Event: A colloquium in honor of Gérard Huet, in Paris, June 22-23, 2007.

[01/2007] Technical report and Coq development: A solution to the POPLmark challenge, based on a locally nameless representation of terms in the style of McKinna and Pollack.