I am a researcher at Inria and professeur attaché at the ENS Paris-Saclay.
I am a member of the Laboratoire de Méthodes Formelles, in the Deducteam team where we develop the logical framework Dedukti.
I am interested in the formalization of mathematics, in proof processing systems, in the physics of computation, in the safety of aerospace systems, and in the epistemology and ethics of informatics. Here is the list of my scientific papers, philosophical papers, and some books.
I have recieved the Prix scientifique Philips pour les jeunes in 1982, the European Philips contest for young researchers and inventors in 1983, the Prix d'Alembert des lycéens awarded by the Société mathématique de France in 2000, the Grand prix de philosophie awarded by the Académie française in 2007, the prix La science se livre, awarded by the département des Hauts-de-seine, with Serge Abiteboul, in 2018, the Grand prix Inria - Académie des sciences in 2023, and the Médaille Histoire des Sciences et Épistémologie de l'Académie des sciences in 2024.
I contribute to the Logique course in the third year of the bachelor degree. This is a flipped-classroom course, the videos are there. I teach the course Foundations of proof systems at the MPRI. Here are its course notes Proofs in theories. Here are the videos of ten lectures of 1:30 each of the course the principles of programming languages I taught at École polytechnique.
Some of my course notes have been published, as books, others are on line.
I am a member of the of the Comité national pilote d'éthique du numérique, of the scientific board of the Societé informatique de France, of the Comite national francais d'histoire et de philosophie des sciences et des techniques and of the Conseil supérieur des programmes. In the past, I have been a member of the Commission de réflexion sur l'Éthique de la Recherche en sciences et technologies du Numérique d'Allistene, of the Conseil national du numérique, of the scientific board of La main à la pâte, and of the scientfic board of theInstitut des hautes études pour la science et la technologie.
Since 2005, I have been intrested in education and I have tried to draw the attention of the adminstration to the need of introducing computer science in K-12. I have been a member of the Committee apointed by the Minister of Education to suggest a computer science curiculum for senior high school students, this has lead to the curiculum published in the Bulletin officiel on October 13th 2011. I have participated to the report of the Academy of Sciences L'enseignement de l'informatique - Il est urgent de ne plus attendre.
I also have been a consultant for the National Institute of Aerospace, a lab of the NASA Langley research center. Among other things, I have participated to the development and the proof of ACCoRD, an Airborne Coordinated Conflict Resolution and Detection system.
I try to make science popular with books, videos, from may 2014 to june 2021, I wrote a monthly column in Pour la Science.