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'm head of the Gallium research team, part of the Paris-Rocquencourt research center of INRIA, located in the western suburbs of Paris.

News

[07/2007] Prize: I am honored to receive the 2007 Michel Monpetit prize of the French Academy of Sciences.

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

[07/2007] Draft paper: Formal verification of translation validators: A case study on instruction scheduling optimizations, with Jean-Baptiste Tristan, submitted to a conference.

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

[02/2007] Draft paper: Coinductive big-step operational semantics, with Hervé Grall, submitted to a journal. Accompanied with a Coq development.

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

[08/2006] Publication: Formal verification of a C compiler front-end, with Sandrine Blazy and Zaynah Dargaye. Proceedings of Formal Methods 2006, LNCS 4085.

[03/2006] Publication: Coinductive big-step operational semantics. Proceedings of ESOP 2006, LNCS 3924. Accompanying Coq development: (1) semantics.v; (2) typing.v; (3) compilation.v.

[01/2006] Coq development: Commented Coq development for the Compcert certified compiler back-end.

[01/2006] Publication: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. Proceedings of POPL 2006.