An abstract type for constructing tactics in Coq

Arnaud Spiwack 1, 2
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : The Coq proof assistant is a large development, a lot of which happens to be more or less dependent on the type of tactics. To be able to perform tweaks in this type more easily in the future, we propose an API for building tactics which doesn't need to expose the type of tactics and yet has a fairly small amount of primitives. This API accompanies an entirely new implementation of the core tactic engine of Coq which aims at handling more gracefully existential variables (aka. metavariables) in proofs - like in more recent proof assistants like Matita and Agda2. We shall, then, leverage this newly acquired independence of the concrete type of tactics from the API to add backtracking abilities.
Type de document :
Communication dans un congrès
Proof Search in Type Theory, Jul 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

Littérature citée [4 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00502500
Contributeur : Arnaud Spiwack <>
Soumis le : jeudi 15 juillet 2010 - 10:36:26
Dernière modification le : mercredi 25 avril 2018 - 10:45:26
Document(s) archivé(s) le : mardi 23 octobre 2012 - 10:20:58

Fichier

tactics.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00502500, version 1

Collections

Citation

Arnaud Spiwack. An abstract type for constructing tactics in Coq. Proof Search in Type Theory, Jul 2010, Edinburgh, United Kingdom. 2010. 〈inria-00502500〉

Partager

Métriques

Consultations de la notice

268

Téléchargements de fichiers

168