2011): Isabelle as Document-oriented Proof Assistant

Abstract. Proof assistants in the LCF tradition, such as Coq, Isabelle, and the HOL family, are notorious for old-fashioned command-line inter-action with input and output of plain text. Established prover interfaces like Proof General merely add a thin layer on top of the read-eval-print loop in the background. More sophisticated mathematical editors, Web-services, Wiki-servers for mathematical content do exist, but any project that aims at fully formal proof-checking struggles with recurrent prob-lems posed by ancient prover engines. Taking the perspective of Isabelle, we discuss common problems and so-lutions that have emerged in the past few years, to fit the prover smoothly into a document-oriented environment with rich semantic annotations for formal sources. For example, this enables a conventional editor frame-work to present formal content provided by the prover, without having to understand logic itself (or re-implement a prover). This can be achieved with minimal changes on the editor and prover side, but the combination is able to support the usual metaphors of squiggly underline, tooltips, popups etc. that are now commonplace in browsers or IDEs. Many of these document-oriented traits of current Isabelle are sufficiently general to be transferred to other provers. If such principles are becoming routinely available in LCF-style provers, building combined mathemati-cal assistants should become more feasible.