I am a senior researcher at INRIA, currently on leave at Ecole Polytechnique. As such:

• I am head of the Informatics Department of Polytechnique; which means I am the main person in charge for teaching of Computer Science.

• Until 2012, I was leading the Typical team, located at the LIX laboratory.

• I used to be a member of the mathematical components team of the INRIA/Microsoft Research joint centre.

Research

My research interests lie in the formalization of mathematical reasoning and its mechanical verification through proof systems, especially Coq. I am particularly interested by proofs involving computations and evolutions of type theory making this easier.

Publications and papers

A video lecture (in french) about formal proofs which involve computations

Some other stuff for a (slightly) wider audience.

A short CV.