Proof in Context -- Web Editing with Rich, Modeless Contextual Feedback
This addresses the need for better collaboration tools in formal mathematics, though it is incremental as it builds on existing web-based and theorem prover systems.
The paper tackles the problem of creating a reusable proof editor component for collaborative formal mathematics by designing Agora's asynchronous editor, which supports different tools providing contextual information, with a detailed implementation for the Coq theorem prover.
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.