Isabelle/jEdit -- a prover IDE within the PIDE framework PIDE is a general framework for document-oriented prover interaction and integration, based on a bilingual architecture that combines ML and Scala [2]. The overall aim is to connect LCF-style provers like Isabelle [5, {S}6] (or Coq [5, {S}4] or HOL [5, {S}1]) with sophisticated front-end technology on the JVM platform, overcoming command-line interaction at last.

References in zbMATH (referenced in 29 articles , 1 standard article )

Showing results 1 to 20 of 29.
Sorted by year (citations)

1 2 next

  1. Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian: Big math and the one-brain barrier: the tetrapod model of mathematical knowledge (2021)
  2. Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2020)
  3. Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius: Relational data across mathematical libraries (2019)
  4. Wenzel, Makarius: Interaction with formal mathematical documents in Isabelle/PIDE (2019)
  5. Avigad, Jeremy (ed.); Blanchette, Jasmin Christian (ed.); Klein, Gerwin (ed.); Paulson, Lawrence (ed.); Popescu, Andrei (ed.); Snelting, Gregor (ed.): Introduction to “Milestones in interactive theorem proving” (2018)
  6. Jensen, Alexander Birch; Larsen, John Bruntse; Schlichtkrull, Anders; Villadsen, Jørgen: Programming and verifying a declarative first-order prover in Isabelle/HOL (2018)
  7. Mendes, Alexandra; Ferreira, João F.: Towards verified handwritten calculational proofs (short paper) (2018)
  8. Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2018)
  9. Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
  10. Hupel, Lars; Kuncak, Viktor: Translating scala programs to isabelle/HOL. System description (2016)
  11. Kohlhase, Michael; Rabe, Florian: QED reloaded: towards a pluralistic formal library of mathematical knowledge (2016)
  12. Roe, Kenneth; Smith, Scott: Coqpie: an IDE aimed at improving proof development productivity. (rough diamond) (2016)
  13. Nakasho, Kazuhisa; Shidama, Yasunari: Documentation generator focusing on symbols for the HTML-ized Mizar library (2015)
  14. Wenzel, Makarius: Interactive theorem proving from the perspective of Isabelle/Isar (2015)
  15. Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Showing invariance compositionally for a process algebra for network protocols (2014)
  16. Hupel, Lars: Interactive simplifier tracing and debugging in Isabelle (2014)
  17. Pąk, Karol: Improving legibility of natural deduction proofs is not trivial (2014)
  18. Ring, Martin; Lüth, Christoph: Collaborative interactive theorem proving with Clide (2014)
  19. Wenzel, Makarius: Asynchronous user interaction and tool integration in Isabelle/PIDE (2014)
  20. Barras, Bruno; del Carmen González Huesca, Lourdes; Herbelin, Hugo; Régis-Gianas, Yann; Tassi, Enrico; Wenzel, Makarius; Wolff, Burkhart: Pervasive parallelism in highly-trustable interactive theorem proving systems (2013)

1 2 next