ActivitĂ©s đ§
Sujet de thĂšse
Dans un assistant de preuve comme Coq, un mĂȘme objet mathĂ©matique peut souvent ĂȘtre formalisĂ© par diffĂ©rentes structures de donnĂ©es. Par exemple, les nombres entiers peuvent ĂȘtre reprĂ©sentĂ©s par divers encodages (unaire, binaire, etc.). En pratique, cette situation familiĂšre en programmation est un frein Ă la preuve formelle automatique. Le sujet global de ma thĂšse Ă©tait lâutilisation de la mĂ©ta-programmation pour crĂ©er des outils de prĂ©-traitement des Ă©noncĂ©s Ă prouver dans Coq, exploitant des relations plus ou moins riches entre des types.
Lors de ma premiĂšre annĂ©e, jâai dĂ©veloppĂ© un prototype de greffon de prĂ©-traitement pour Coq, Trakt. Ici, la notion de relation entre types est une possibilitĂ© de plongement dâun type source vers un type cible. Lâoutil parcourt rĂ©cursivement lâĂ©noncĂ© Ă prouver et fabrique un nouvel Ă©noncĂ© ainsi quâune preuve permettant de remplacer lâancien Ă©noncĂ© par le nouveau de façon certifiĂ©e. Trakt a Ă©tĂ© intĂ©grĂ© avec succĂšs Ă SMTCoq, un greffon dâautomatisation des preuves permettant de connecter Coq Ă des solveurs SMT. Ensuite, je me suis concentrĂ© sur Trocq, un deuxiĂšme prototype de greffon basĂ© sur la paramĂ©tricitĂ©, oĂč les relations entre les types se placent dans une hiĂ©rarchie de structures qui varie entre une relation sans structure et une Ă©quivalence de types.
Jâai Ă©crit mes greffons pour Coq dans le langage Coq-Elpi, une implĂ©mentation de λProlog avec un accĂšs Ă lâAPI de Coq et des facilitĂ©s pour manipuler des termes Coq.
Contributions scientifiques
ThĂšse de doctorat :
- Méta-programmation pour le transfert de preuve en théorie des types dépendants
Version 1.1, soutenue le 19/12/2023
[PDF (français, mode clair)] [PDF (français, mode sombre)]
[PDF (anglais, mode clair)] [PDF (anglais, mode sombre)]
Logiciel :
Trocq
Greffon de paramétricité pour Coq
[site web dépÎt]Trakt
Greffon de pré-traitement des énoncés Coq avant automatisation
[site web] [dépÎt]
Publications et présentations :
Trocq: Proof Transfer for Free, With or Without Univalence
avec Cyril Cohen et Assia Mahboubi
ESOP 2024 [pré-publication]Compositional pre-processing for automated reasoning in dependent type theory
avec Valentin Blot, Denis Cousineau, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi et Pierre Vial
CPP 2023 [DOI] [planches]Trakt: a generic pre-processing tactic for theory-based proof automation
avec Denis Cousineau et Assia Mahboubi
Coq Workshop 2022 [résumé] [planches] [vidéo]Trakt : uniformiser les types pour automatiser les preuves
avec Denis Cousineau et Assia Mahboubi
JFLA 2022 [résumé]
Enseignement
Programmation par contraintes
12h de CM, 14h de TP
2023, INSA RennesAlgorithmique avancée
~30h de TP
2021, IUT de Nantes