Je suis docteur en informatique de l'université Paris XI (LRI) ou j'ai effectuée ma thèse sous la direction de Christine Paulin-Mohring. J'ai soutenu ma thèse sur Un environnement pour la programmation avec types dépendants et je suis maintenant en post-doc dans le projet Ynot à Harvard.

Mes recherches se situent au confluent de la logique et de l'informatique, de l'étude de la théorie des types et la conception de langages fonctionnels à types dépendants à la preuve interactive et automatique. Je suis particulièrement intéressé par l'utilisation d'assistant de preuves pour la vérification de logiciels et de preuves formelles.

Je suis l'un des développeurs principaux de l'assistant de preuve Coq et j'ai réalisé des développements significatifs dans ce système utilisant les nouveaux outils que j'ai conçu: Program et les classes de type. J'ai travaillé récemment autour de la compilation du filtrage dépendant et la réécriture. Je fais partie du projet GoNative visant à donner des garanties vérifiables pour l'exécution de code natif.