Isabelle/jEdit – A Prover IDE within the PIDE Framework
From MaRDI portal
Publication:2907353
DOI10.1007/978-3-642-31374-5_38zbMATH Open1360.68769arXiv1207.3441OpenAlexW1719912185MaRDI QIDQ2907353FDOQ2907353
Authors: Makarius Wenzel 
Publication date: 7 September 2012
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Abstract: PIDE is a general framework for document-oriented prover interaction and integration, based on a bilingual architecture that combines ML and Scala. The overall aim is to connect LCF-style provers like Isabelle (or Coq or HOL) with sophisticated front-end technology on the JVM platform, overcoming command-line interaction at last. The present system description specifically covers Isabelle/jEdit as part of the official release of Isabelle2011-1 (October 2011). It is a concrete Prover IDE implementation based on Isabelle/PIDE library modules (implemented in Scala) on the one hand, and the well-known text editor framework of jEdit (implemented in Java) on the other hand. The interaction model of our Prover IDE follows the idea of continuous proof checking: the theory source text is annotated by semantic information by the prover as it becomes available incrementally. This works via an asynchronous protocol that neither blocks the editor nor stops the prover from exploiting parallelism on multi-core hardware. The jEdit GUI provides standard metaphors for augmented text editing (highlighting, squiggles, tooltips, hyperlinks etc.) that we have instrumented to render the formal content from the prover context. Further refinement of the jEdit display engine via suitable plugins and fonts approximates mathematical rendering in the text buffer, including symbols from the TeX repertoire, and sub-/superscripts. Isabelle/jEdit is presented here both as a usable interface for current Isabelle, and as a reference application to inspire further projects based on PIDE.
Full work available at URL: https://arxiv.org/abs/1207.3441
Recommendations
- Isabelle as document-oriented proof assistant
- Coqpie: an IDE aimed at improving proof development productivity (rough diamond)
- Isabelle's metalogic: formalization and proof checker
- Combining Isabelle and QEPCAD-B in the Prover’s Palette
- Isabelle/HOL. A proof assistant for higher-order logic
- Eisbach: a proof method language for Isabelle
- Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit
- The Isabelle/Naproche natural language proof assistant
- scientific article; zbMATH DE number 4072441
Cited In (18)
- Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
- The Imandra Automated Reasoning System (System Description)
- Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit
- Mechanizing a process algebra for network protocols
- Title not available (Why is that?)
- Translating Scala programs to Isabelle/HOL. System description
- Asynchronous user interaction and tool integration in Isabelle/PIDE
- Isabelle/jEdit
- PIDE
- Isabelle as document-oriented proof assistant
- Interaction with formal mathematical documents in Isabelle/PIDE
- A Framework for Interactive Proof
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Title not available (Why is that?)
- A web interface for Isabelle: the next generation
- Coqpie: an IDE aimed at improving proof development productivity (rough diamond)
- JTabWb: a Java framework for implementing terminating sequent and tableau calculi
- Interactive simplifier tracing and debugging in Isabelle
Uses Software
This page was built for publication: Isabelle/jEdit – A Prover IDE within the PIDE Framework
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2907353)
