Mes thèmes de recherche s'intègrent aux domaines suivants, avec notamment la correspondance fondamentale entre preuves et programmes comme ligne directrice :

- Théorie de la preuve : logique classique, théorie des types, interprétations calculatoires, ...

- Fondements des langages de programmation : opérateurs de contrôle, délimiteurs, machines abstraites, effets de bord, appel par nécessité, systèmes de types, ...

- Assistants de preuves : développement du système Rocq (ex-Coq)