A Web Interface for Isabelle: The Next Generation

Christoph Lüth, Martin Ring

In: Jacques Carette (editor). Conferences on Intelligent Computer Mathematics CICM 2013. Conferences on Intelligent Computer Mathematics (CICM-13) Pages 326-329 Lecture Notes in Artificial Intelligence (LNAI) 7961 Springer 7/2013.


We present Clide, a web interface for the interactive theorem prover Isabelle. Clide uses latest web technology and the Isabelle/PIDE framework to implement a web-based interface for asynchronous proof document management that competes with, and in some aspects even surpasses, conventional user interfaces for Isabelle such as Proof General or Isabelle/jEdit.

main.pdf (pdf, 269 KB)

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