Abstract Mathematical Knowledge Management (MKM), as a field, has seen tremendous
growth in the last few years. This period was one where many research threads were started …

We present in this paper the design of a graphical user interface to deal with proofs in
geometry. The software developed combines three tools: a dynamic geometry software to …

Historically, the LCF tradition of interactive theorem proving was tied to the read-eval-print
loop, with sequential and synchronous evaluation of prover commands given on the …

Hybrid systems verification is quite important for developing correct controllers for physical
systems, but is also challenging. Verification engineers, thus, need to be empowered with …

Isabelle/PIDE has emerged over more than 10 years as the standard Prover IDE for
interactive theorem proving in Isabelle. The well-established Archive of Formal Proofs (AFP) …

After several decades, most proof assistants are still centered around TTY-based interaction
in a tight read-eval-print loop. Even well-known Emacs modes for such provers follow this …

The beginnings of the Isabelle Prover IDE framework (Isabelle/PIDE) go back to the year
2008. This is a report on the project after 10 years, with system descriptions for various PIDE …

This article describes an architecture for creating responsive web interfaces for proof
assistants. The architecture combines current web development technologies with the …

User interfaces for interactive proof assistants have always lagged behind those for
mainstream programming languages. Whereas integrated development environments …

Proof assistants in the LCF tradition, such as Coq, Isabelle, and the HOL family, are
notorious for old-fashioned command-line interaction with input and output of plain text …