Publication
Collaborative Interactive Theorem Proving with Clide
Martin Ring; Christoph Lüth
In: G. Klein; R. Gamboa (Hrsg.). Interactive Theorem Proving ITP 2014. International Conference on Interactive Theorem Proving (ITP-2014), located at Vienna Summer of Logic, July 14-17, Wien, Austria, Pages 467-482, Lecture Notes in Computer Science (LNCS), Vol. 8558, Springer Verlag, 7/2014.
Abstract
This paper introduces Clide, a collaborative web interface for the
Isabelle theorem prover. The interface allows a document-oriented
interaction with Isabelle very much like Isabelle's desktop interface.
Moreover, it allows users to jointly edit Isabelle proof scripts over the
web; editing operations are synchronised to all users who have opened the
proof script.
The paper describes motivation, user experience, implementation and system
architecture of Clide. The implementation is based on the theory of
operational transformations; its key concepts have been formalised in
Isabelle, its correctness proven and critical parts of the implementation
on the server are generated from the formalisation, thus increasing
confidence in the system.