Proof in Context — Web Editing with Rich, Modeless Contextual Feedback

Carst Tankink
(Institute for Computing and Information Science, Radboud University Nijmegen)

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.

In Cezary Kaliszyk and Christoph Lüth: Proceedings 10th International Workshop On User Interfaces for Theorem Provers (UITP 2012), Bremen, Germany, July 11th 2012, Electronic Proceedings in Theoretical Computer Science 118, pp. 42–56.
Published: 5th July 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: