Proof in Context — Web Editing with Rich, Modeless Contextual Feedback
The Agora system is a prototypical Wiki for formal mathematics: a web-based system for collaborating on formal mathematics, intended to support informal documentation of formal developments. This system requires a reusable proof editor component, both for collaborative editing of documents, and for...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2013-07-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1307.1943v1 |
| _version_ | 1819068102418104320 |
|---|---|
| author | Carst Tankink |
| author_facet | Carst Tankink |
| author_sort | Carst Tankink |
| collection | DOAJ |
| description | The Agora system is a prototypical Wiki for formal mathematics: a web-based system for collaborating on formal mathematics, intended to support informal documentation of formal developments. This system requires a reusable proof editor component, both for collaborative editing of documents, and for embedding in the resulting documents. This paper describes the design of Agora's asynchronous editor, that is generic enough to support different tools working on editor content and providing contextual information, with interactive theorem proverss being a special, but important, case described in detail for the Coq theorem prover. |
| first_indexed | 2024-12-21T16:28:49Z |
| format | Article |
| id | doaj.art-ac0122644b0548a793af127bd89e164f |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-21T16:28:49Z |
| publishDate | 2013-07-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-ac0122644b0548a793af127bd89e164f2022-12-21T18:57:24ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-07-01118Proc. UITP 2012425610.4204/EPTCS.118.3Proof in Context — Web Editing with Rich, Modeless Contextual FeedbackCarst TankinkThe Agora system is a prototypical Wiki for formal mathematics: a web-based system for collaborating on formal mathematics, intended to support informal documentation of formal developments. This system requires a reusable proof editor component, both for collaborative editing of documents, and for embedding in the resulting documents. This paper describes the design of Agora's asynchronous editor, that is generic enough to support different tools working on editor content and providing contextual information, with interactive theorem proverss being a special, but important, case described in detail for the Coq theorem prover.http://arxiv.org/pdf/1307.1943v1 |
| spellingShingle | Carst Tankink Proof in Context — Web Editing with Rich, Modeless Contextual Feedback Electronic Proceedings in Theoretical Computer Science |
| title | Proof in Context — Web Editing with Rich, Modeless Contextual Feedback |
| title_full | Proof in Context — Web Editing with Rich, Modeless Contextual Feedback |
| title_fullStr | Proof in Context — Web Editing with Rich, Modeless Contextual Feedback |
| title_full_unstemmed | Proof in Context — Web Editing with Rich, Modeless Contextual Feedback |
| title_short | Proof in Context — Web Editing with Rich, Modeless Contextual Feedback |
| title_sort | proof in context web editing with rich modeless contextual feedback |
| url | http://arxiv.org/pdf/1307.1943v1 |
| work_keys_str_mv | AT carsttankink proofincontextwebeditingwithrichmodelesscontextualfeedback |