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

[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.