PIDE for Asynchronous Interaction with Coq
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...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2014-10-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1410.8221v1 |
| _version_ | 1818262453425799168 |
|---|---|
| author | Carst Tankink |
| author_facet | Carst Tankink |
| author_sort | Carst Tankink |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-12T19:03:22Z |
| format | Article |
| id | doaj.art-ab09fc9c8b364e3aa37bd345eb7274f0 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-12T19:03:22Z |
| publishDate | 2014-10-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-ab09fc9c8b364e3aa37bd345eb7274f02022-12-22T00:15:01ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-10-01167Proc. UITP 2014738310.4204/EPTCS.167.9:10PIDE for Asynchronous Interaction with CoqCarst Tankink0 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.http://arxiv.org/pdf/1410.8221v1 |
| spellingShingle | Carst Tankink PIDE for Asynchronous Interaction with Coq Electronic Proceedings in Theoretical Computer Science |
| title | PIDE for Asynchronous Interaction with Coq |
| title_full | PIDE for Asynchronous Interaction with Coq |
| title_fullStr | PIDE for Asynchronous Interaction with Coq |
| title_full_unstemmed | PIDE for Asynchronous Interaction with Coq |
| title_short | PIDE for Asynchronous Interaction with Coq |
| title_sort | pide for asynchronous interaction with coq |
| url | http://arxiv.org/pdf/1410.8221v1 |
| work_keys_str_mv | AT carsttankink pideforasynchronousinteractionwithcoq |