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

Autor: Cousineau, Denis, Crance, Enzo, Mahboubi, Assia
Přispěvatelé: Bourke, Timothy, Chantal Keller, Timothy Bourke, Mitsubishi Electric R&D Centre Europe [France] (MERCE-France), Mitsubishi Electric [France], Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-École Centrale de Nantes (Nantes Univ - ECN), Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST), Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Nantes Université (Nantes Univ)
Jazyk: francouzština
Rok vydání: 2022
Předmět:
Zdroj: Journées Francophones des Langages Applicatifs
JFLA 2022-33èmes Journées Francophones des Langages Applicatifs
JFLA 2022-33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.261-263
Popis: National audience; 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.
Databáze: OpenAIRE
Externí odkaz: