Chercheur à l’Inria, professeur à l’ENS de Paris-Saclay et membre du CNNum. Il travaille sur la formalisation des mathématiques, le traitement des démonstrations, la physique du calcul, la sûreté aéronautique et l'enseignement, l'épistémologie et l'éthique de l'informatique.