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

News

[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, accepted for publication in Journal of Automated Reasoning. 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, accepted for publication 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, accepted for publication 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.

[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] Publication: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. Proceedings of POPL 2006.