Isabelle/PIDE
Isabelle/PIDE as Platform for Educational Tools. The Isabelle/PIDE platform addresses the question whether proof assistants of the LCF family are suitable as technological basis for educational tools. The traditionally strong logical foundations of systems like HOL, Coq, or Isabelle have so far been counter-balanced by somewhat inaccessible interaction via the TTY (or minor variations like the well-known Proof General / Emacs interface). Thus the fundamental question of math education tools with fully-formal background theories has often been answered negatively due to accidental weaknesses of existing proof engines. The idea of “PIDE” (which means “Prover IDE”) is to integrate existing provers like Isabelle into a larger environment, that facilitates access by end-users and other tools. We use Scala to expose the proof engine in ML to the JVM world, where many user-interfaces, editor frameworks, and educational tools already exist. This shall ultimately lead to combined mathematical assistants, where the logical engine is in the background, without obstructing the view on applications of formal methods, formalized mathematics, and math education in particular
Keywords for this software
References in zbMATH (referenced in 12 articles )
Showing results 1 to 12 of 12.
Sorted by year (- Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius: Relational data across mathematical libraries (2019)
- Kaliszyk, Cezary (ed.); Brady, Edwin (ed.); Kohlhase, Andrea (ed.); Sacerdoti Coen, Claudio (ed.): Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8--12, 2019. Proceedings (2019)
- Kaliszyk, Cezary; Pąk, Karol: Semantics of Mizar as an Isabelle object logic (2019)
- Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
- Wenzel, Makarius: Interaction with formal mathematical documents in Isabelle/PIDE (2019)
- Mendes, Alexandra; Ferreira, João F.: Towards verified handwritten calculational proofs (short paper) (2018)
- Carter, Nathan C.; Monks, Kenneth G.: A web-based toolkit for mathematical word processing applications with semantics (2017)
- Hupel, Lars; Kuncak, Viktor: Translating scala programs to isabelle/HOL. System description (2016)
- Roe, Kenneth; Smith, Scott: Coqpie: an IDE aimed at improving proof development productivity. (rough diamond) (2016)
- Nakasho, Kazuhisa; Shidama, Yasunari: Documentation generator focusing on symbols for the HTML-ized Mizar library (2015)
- Wenzel, Makarius: Asynchronous user interaction and tool integration in Isabelle/PIDE (2014)
- Wenzel, Makarius: Isabelle/jEdit -- a prover IDE within the PIDE framework (2012)