Monsieur Cyril COHEN
Cyril COHEN soutiendra son habilitation à diriger des recherches (HDR) en Section CNU n°27 – Informatique, Discipline : Informatique le 10 septembre 2026 à 14h.
Résumé de la thèse
Cette thèse d’habilitation a pour but de réduire l’écart entre mathématiques formelles et informelles en fournissant des extensions au prouveur Rocq, en adoptant le point de vue selon lequel la théorie des types est un langage assembleur et en fournissant des « compilateurs » qui prennent un langage utilisateur simplifié et qui effectuent des opérations complexes pour soulager les utilisateurs et utilisatrices d’une logistique logicielle superflue et les aider à se concentrer sur la signification mathématique de leur formalisation. Elle est constituée de quatre parties principales. La première partie décrit une rétrospective historique et un état de l’art qui se concentrent sur les pré-requis nécessaires aux contributions de cette thèse d’habilitation. Dans la deuxième partie, Cyril COHEN décrit d’abord Hierarchy Builder, un outil destiné à faciliter la description et l’utilisation de hiérarchies algébriques. Il décrit ensuite Trocq, un calcul et prototype d’implémentation pour effectuer des substitutions entre types distincts, sans utiliser l’axiome d’univalence, tout en étant solidement ancré dans les fondements univalents. Un troisième outil, appelé« tactiques near » est un ensemble de tactiques dont le but est d’imiter un raisonnement informel en apparence, tout en étant vérifié par Rocq. La troisième partie illustre les besoins et apports des outils par rapport à deux formalisations majeures auxquelles Cyril COHEN a pris part. Il décrit d’abord une preuve formelle entièrement constructive du théorème de Galois qui établit l’équivalence entre résolubilité des extensions de corps et résolubilité du groupe de Galois correspondant, et son application à la preuve du théorème d’Abel–RufÏni, qui établit l’impossibilité de résoudre par radicaux une équation générale de degré cinq ou plus. Il décrit ensuite une construction formelle de la théorie de la mesure, ainsi que de l’intégrale et mesure de Lebesgue, en s’appuyant fortement sur Hierarchy Builder. Dans la dernière partie du document, il montre comment ses contributions et leurs extensions futures peuvent être utilisées pour réunifier un corpus important de développements formels, en présentant un projet de refactorisation à grande échelle, ainsi que des conditions nécessaires à sa réalisation.
Devant un jury composé de :
- Monsieur Andrej BAUER, professeur
- Monsieur Antoine CHAMBERT-LOIR, professeur des universités
- Monsieur David MONNIAUX, directeur de recherche
- Madame Sandrine BLAZY, professeure des universités
- Monsieur Florent HIVERT, professeur des universités
- Madame Sophie MOREL, directrice de recherche
- Monsieur Michele PAGANI, professeur des universités
Gratuit
Disciplines