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 26 articles , 1 standard article )

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

1 2 next

  1. Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius: Relational data across mathematical libraries (2019)
  2. Wenzel, Makarius: Interaction with formal mathematical documents in Isabelle/PIDE (2019)
  3. 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)
  4. Mendes, Alexandra; Ferreira, João F.: Towards verified handwritten calculational proofs (short paper) (2018)
  5. Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2018)
  6. Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
  7. Hupel, Lars; Kuncak, Viktor: Translating scala programs to isabelle/HOL. System description (2016)
  8. Kohlhase, Michael; Rabe, Florian: QED reloaded: towards a pluralistic formal library of mathematical knowledge (2016)
  9. Roe, Kenneth; Smith, Scott: Coqpie: an IDE aimed at improving proof development productivity. (rough diamond) (2016)
  10. Nakasho, Kazuhisa; Shidama, Yasunari: Documentation generator focusing on symbols for the HTML-ized Mizar library (2015)
  11. Wenzel, Makarius: Interactive theorem proving from the perspective of Isabelle/Isar (2015)
  12. Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Showing invariance compositionally for a process algebra for network protocols (2014)
  13. Hupel, Lars: Interactive simplifier tracing and debugging in Isabelle (2014)
  14. Pąk, Karol: Improving legibility of natural deduction proofs is not trivial (2014)
  15. Ring, Martin; Lüth, Christoph: Collaborative interactive theorem proving with Clide (2014)
  16. Wenzel, Makarius: Asynchronous user interaction and tool integration in Isabelle/PIDE (2014)
  17. 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)
  18. Lange, Christoph; Caminati, Marco B.; Kerber, Manfred; Mossakowski, Till; Rowat, Colin; Wenzel, Makarius; Windsteiger, Wolfgang: A qualitative comparison of the suitability of four theorem provers for basic auction theory (2013)
  19. Lüth, Christoph; Ring, Martin: A web interface for Isabelle: the next generation (2013)
  20. Wenzel, Makarius: Shared-memory multiprocessing for interactive theorem proving (2013)

1 2 next