Ma recherche porte sur les preuves formelles, les méthodes formelles et le système de preuves Coq . J'ai été longtemps chercheur à l'INRIA, et suis actuellement détaché pour diriger le département d'Informatique de l'Ecole Polytechnique. My research is about formal proofs, formal methods, logic and the proof assistant Coq. I have been with INRIA for a long time and am currently heading the CS department of Ecole Polytechnique.