PIDE for Asynchronous Interaction with Coq

Carst Tankink
(Inria Saclay - Île-de-France)

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.

In Christoph Benzmüller and Bruno Woltzenlogel Paleo: Proceedings Eleventh Workshop on User Interfaces for Theorem Provers (UITP 2014), Vienna, Austria, 17th July 2014, Electronic Proceedings in Theoretical Computer Science 167, pp. 73–83.
Published: 29th October 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.167.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org