Prétraitement compositionnel en Coq
Mercredi 10 juillet 2024 à 14h
ÉNS Paris-Saclay, salle 1Z31, Lien Zoom.
Abstract. This thesis presents a new methodology for preprocessing goals in the Coq proof assistant in order to send them to an automatic solver. This methodology consists of composing atomic and certifying transformations based on the goal to be proven. We will first present the library of transformations that we have written, then we will present an orchestrating tool for these transformations, which aims to be generic. This has led to the implementation of a new 'push-button' tactic called 'snipe' for Coq.
Résumé. Cette thèse présente une nouvelle méthodologie de prétraitement de buts de l'assistant de preuve Coq afin de les envoyer à un prouveur automatique. Cette méthodologie consiste à composer des transformations atomiques et certifiantes en fonction du but à prouver. Nous présenterons d'abord la bibliothèque de transformations que nous avons écrite, puis nous présenterons un outil d'ordonnancement pour ces transformations, qui se veut générique. Le tout a conduit à l'implémentation une nouvelle tactique 'pousse-bouton' appelée 'snipe' pour Coq.
The manuscript is available here.
Jury members :
- Sylvie Boldo, directrice de recherche Inria - Examinatrice
- Sylvain Boulmé, maître de conférences de l'Université Grenoble-Alpes - Rapporteur et examinateur
- Yannick Forster, chargé de recherche Inria - Examinateur
- Nicolas Tabareau, directeur de recherche Inria - Rapporteur et examinateur
- Sophie Tourret, chargée de recherche Inria - Examinatrice
Thesis advisors: Valentin Blot, Gilles Dowek, Chantal Keller