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
[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, to appear in Higher-Order and Symbolic Computation.
[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.
[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, accepted for publication in Higher-Order and Symbolic Computation.
[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.