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

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

  1. Hupel, Lars; Kuncak, Viktor: Translating scala programs to isabelle/HOL. System description (2016)
  2. Nakasho, Kazuhisa; Shidama, Yasunari: Documentation generator focusing on symbols for the HTML-ized Mizar Library (2015)
  3. Hupel, Lars: Interactive simplifier tracing and debugging in Isabelle (2014)
  4. Pąk, Karol: Improving legibility of natural deduction proofs is not trivial (2014)
  5. Ring, Martin; Lüth, Christoph: Collaborative interactive theorem proving with Clide (2014)
  6. 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)
  7. 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)
  8. Lüth, Christoph; Ring, Martin: A web interface for Isabelle: the next generation (2013)
  9. Wenzel, Makarius: Shared-memory multiprocessing for interactive theorem proving (2013)
  10. Jucovschi, Constantin: Cost-effective integration of MKM semantic services into editing environments (2012)
  11. Wenzel, Makarius: Isabelle/jEdit -- a prover IDE within the PIDE framework (2012)
  12. Wenzel, Makarius: Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit (2012)
  13. Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias: Automatic proof and disproof in Isabelle/HOL (2011)
  14. Horozal, Fulya; Iacob, Alin; Jucovschi, Constantin; Kohlhase, Michael; Rabe, Florian: Combining source, content, presentation, narration, and relational representation (2011)
  15. Wenzel, Makarius: Isabelle as document-oriented proof assistant (2011)