Isabelle/jEdit

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

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

1 2 next

  1. Dubut, Jérémy; Yamada, Akihisa: Fixed points theorems for non-transitive relations (2022)
  2. Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian: Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge (2021)
  3. Foster, Simon; Nemouchi, Yakoub; Gleirscher, Mario; Wei, Ran; Kelly, Tim: Integration of formal proof into unified assurance cases with Isabelle/SACM (2021)
  4. Líška, Martin; Lupták, Dávid; Novotný, Vít; Růžička, Michal; Shminke, Boris; Sojka, Petr; Štefánik, Michal; Wenzel, Makarius: CICM’21 systems entries (2021)
  5. Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2020)
  6. Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius: Relational data across mathematical libraries (2019)
  7. Wenzel, Makarius: Interaction with formal mathematical documents in Isabelle/PIDE (2019)
  8. 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)
  9. Jensen, Alexander Birch; Larsen, John Bruntse; Schlichtkrull, Anders; Villadsen, Jørgen: Programming and verifying a declarative first-order prover in Isabelle/HOL (2018)
  10. Mendes, Alexandra; Ferreira, João F.: Towards verified handwritten calculational proofs (short paper) (2018)
  11. Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2018)
  12. Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
  13. Hupel, Lars; Kuncak, Viktor: Translating Scala programs to Isabelle/HOL. System description (2016)
  14. Kohlhase, Michael; Rabe, Florian: QED reloaded: towards a pluralistic formal library of mathematical knowledge (2016)
  15. Roe, Kenneth; Smith, Scott: Coqpie: an IDE aimed at improving proof development productivity (rough diamond) (2016)
  16. Nakasho, Kazuhisa; Shidama, Yasunari: Documentation generator focusing on symbols for the HTML-ized Mizar library (2015)
  17. Wenzel, Makarius: Interactive theorem proving from the perspective of Isabelle/Isar (2015)
  18. Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Showing invariance compositionally for a process algebra for network protocols (2014)
  19. Hupel, Lars: Interactive simplifier tracing and debugging in Isabelle (2014)
  20. Pąk, Karol: Improving legibility of natural deduction proofs is not trivial (2014)

1 2 next