Publication

Collaborative Interactive Theorem Proving with Clide

Martin Ring, Christoph Lüth

In: G. Klein, R. Gamboa (editor). 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) 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.

Projekte

Weitere Links

main-final.pdf (pdf, 534 KB)

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