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
[07/2011] Draft paper: A mechanized semantics for C++ object construction and destruction, with applications to resource management, with Tahina Ramananandro and Gabriel Dos Reis, submitted to a conference.
[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.
[07/2009] Draft paper: A list-machine benchmark for mechanized metatheory, with Andrew Appel and Robert Dockins, submitted to a journal.
[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.