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 :

Logiciel :

Publications et présentations :

Enseignement