- En thèse depuis Octobre 2021 sous la direction de Olivier Hermant et de Gilles Dowek.
- Membre du CRI au Mines Paris et de l'équipe Deducteam du LMF.
Recherche
Je m'intéresse à la théorie des types, à la réécriture, aux assistants de preuve, et à l'intéropérabilité entre les systèmes de preuve. J'étudie l'expression de la théorie de Coq dans le LambdaPi-calcul modulo theory. Je vise en particulier l'expression du polymorphisme d'univers d'une théorie imprédicative. Mon travail s'articule autour de l'outil Dedukti, une implémentation du LambdaPi-calcul modulo theory.
Mes objectifs principaux sont les suivants.
- Traduire le Calcul des Castructions avec polymorphisme d'univers dans Dedukti.
- Traduire Coq dand Dedukti.
- Simplifier des preuves (mathématiques inversées).
- Utiliser Dedukti pour partager des preuves en logique du premier ordre vers les langages de tactiques d'assistants de preuve.
Enseignement
- 2023/2024 - ENS Paris-Saclay
- TD de programmation (C et assembleur, L3)
- Projet programmation fonctionnelle (allocateur mémoire et compilateur C écrit en OCaml, L3).
- Projet programmation objet (jeu de simulation écrit en Scala, L3).
- 2022/2023 - ENS Paris-Saclay
- Projet programmation fonctionnelle (compilateur Go écrit en OCaml, L3).
- Projet programmation objet (jeu de stratégie écrit en Scala, L3).
- TD de réseaux (M1)
- 2021/2022
- TD de programmation et algorithmique ENSTA Paris (C, L3)
- TD de programmation et algorithmique IUT Orsay (C++, L1)
Contact
En cas de questions de recherche ou d'enseignement, n'hésitez pas à m'envoyer un mail à yoan.geran (at) minesparis (dot) psl (dot) eu.