News
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.