Trakt : Uniformiser les types pour automatiser les preuves (démonstration) - Trente-Troisièmes Journées Francophones des Langages Applicatifs Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

Trakt : Uniformiser les types pour automatiser les preuves (démonstration)

Résumé

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, le type Z des entiers binaires, dans la bibliothèque standard de Coq, représente les entiers relatifs tout comme le type ssrint, des entiers unaires, fourni par la bibliothèque MathComp. En pratique, cette situation familière en programmation est un frein à la preuve formelle automatique. Dans cet article, nous présentons trakt, un outil dont l'objectif est de faciliter l'accès des utilisateurs de Coq aux tactiques d'automatisation, pour la représentation des théories décidables de leur choix. Cet outil construit une formule auxiliaire à partir d'un but utilisateur, et une preuve que cette dernière implique ce but initial. La formule auxiliaire est conçue pour être adaptée aux outils de preuve automatique (lia, SMTCoq, etc). Cet outil est extensible, grâce à une API permettant à l'utilisateur de définir plusieurs natures de plongements dans un jeu de structures de données de référence. Le méta-langage Coq-Elpi, utilisé pour l'implémentation, fournit des facilités bienvenues pour la gestion des lieurs et la mise en oeuvre des parcours de termes en jeu dans ces tactiques.
Fichier principal
Vignette du fichier
jfla22_paper_9.pdf (179.13 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte

Dates et versions

hal-03626851 , version 1 (31-03-2022)

Identifiants

  • HAL Id : hal-03626851 , version 1

Citer

Denis Cousineau, Enzo Crance, Assia Mahboubi. Trakt : Uniformiser les types pour automatiser les preuves (démonstration). JFLA 2022 - 33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.261-263. ⟨hal-03626851⟩
89 Consultations
71 Téléchargements

Partager

Gmail Facebook X LinkedIn More