PIDE for Asynchronous Interaction with Coq
In: UITP User Interfaces for Theorem Provers User Interfaces for Theorem Provers, Jul 2014, Vienna, Austria. pp.73-83, ⟨10.4204/EPTCS.167.9⟩ Electronic Proceedings in Theoretical Computer Science, Jg. 167 (2014), Heft Proc. UITP 2014, S. 73-83
Online
unknown
Zugriff:
This paper describes the initial progress towards integrating the Coq proof assistant with the PIDE architecture initially developed for Isabelle. 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.
Comment: In Proceedings UITP 2014, arXiv:1410.7850
| Titel: |
PIDE for Asynchronous Interaction with Coq
|
|---|---|
| Autor/in / Beteiligte Person: | Tankink, Carst ; Symbolic Special Functions : Fast and Certified (SPECFUN) ; Inria Saclay - Ile de France ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) |
| Link: | |
| Zeitschrift: | UITP User Interfaces for Theorem Provers User Interfaces for Theorem Provers, Jul 2014, Vienna, Austria. pp.73-83, ⟨10.4204/EPTCS.167.9⟩ Electronic Proceedings in Theoretical Computer Science, Jg. 167 (2014), Heft Proc. UITP 2014, S. 73-83 |
| Veröffentlichung: | arXiv, 2014 |
| Medientyp: | unknown |
| DOI: | 10.48550/arxiv.1410.8221 |
| Schlagwort: |
|
| Sonstiges: |
|