PIDE for Asynchronous Interaction with Coq

Carst Tankink 1, *
* Auteur correspondant
Abstract : This paper describes the initial progress towards integrating the Coq proof assistant with the PIDE architecture initially developed for Isabelle [3]. The architecture is aimed at asynchronous, parallel interaction with proof assistants, and is tied in heavily with a plugin that allows the jEdit editor to work with Isabelle. We have made some generalizations to the PIDE architecture to accommodate for more provers than just Isabelle, and adapted Coq to understand the core protocol: this delivered a working system in about two man-months.
Type de document :
Communication dans un congrès
User Interfaces for Theorem Provers, Jul 2014, Vienna, Austria. 167, pp.73 - 83, 2014, 〈10.4204/EPTCS.167.9〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01091907
Contributeur : Carst Tankink <>
Soumis le : dimanche 7 décembre 2014 - 17:26:02
Dernière modification le : jeudi 9 février 2017 - 15:47:59
Document(s) archivé(s) le : lundi 9 mars 2015 - 06:08:55

Fichier

uitp-2014.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Collections

Citation

Carst Tankink. PIDE for Asynchronous Interaction with Coq. User Interfaces for Theorem Provers, Jul 2014, Vienna, Austria. 167, pp.73 - 83, 2014, 〈10.4204/EPTCS.167.9〉. 〈hal-01091907〉

Partager

Métriques

Consultations de la notice

80

Téléchargements de fichiers

50