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

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

  1. Pąk, Karol: Improving legibility of natural deduction proofs is not trivial (2014)
  2. 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)
  3. 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)
  4. Lüth, Christoph; Ring, Martin: A web interface for Isabelle: the next generation (2013)
  5. Wenzel, Makarius: Shared-memory multiprocessing for interactive theorem proving (2013)
  6. Jucovschi, Constantin: Cost-effective integration of MKM semantic services into editing environments (2012)
  7. Wenzel, Makarius: Isabelle/jEdit -- a prover IDE within the PIDE framework (2012)
  8. Wenzel, Makarius: Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit (2012)
  9. Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias: Automatic proof and disproof in Isabelle/HOL (2011)
  10. Horozal, Fulya; Iacob, Alin; Jucovschi, Constantin; Kohlhase, Michael; Rabe, Florian: Combining source, content, presentation, narration, and relational representation (2011)
  11. Wenzel, Makarius: Isabelle as document-oriented proof assistant (2011)