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) befindet sich Vienna Summer of Logic July 14-17 Wien Austria Seiten 467-482 Lecture Notes in Computer Science (LNCS) 8558 Springer Verlag 7/2014.


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.


Weitere Links

main-final.pdf (pdf, 534 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence