Je prépare en ce moment une thèse sur la programmation avec types dépendents sous la direction de Conor McBride au sein du groupe MSP de l'Université de Strathclyde (Glasgow - Écosse).
Je suis également impliqué dans le projet Coqtail où je formalise en Coq des résultats sur les séries entières.
Je m'intéresse particulièrement à la logique (constructiviste) et à sa relation avec la notion de calcul. Cela passe bien entendu par la théorie des types (dépendents) pour la logique (que ce soit au tableau ou via un assistant de preuve tel que Coq) et pour le calcul (avec un langage de programmation équipé de types dépendents tel qu' Agda).
-
-
