Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit

DOI10.1016/J.ENTCS.2012.06.009MaRDI QIDQ5170238zbMATH OpenOpenAlexWikidataFDO

Authors Makarius Wenzel

Publication date 22 July 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2012.06.009

zbMATH Keywords

asynchronous proof processingIsabellejEditre-use of editor and IDE frameworksScala

Mathematics Subject Classification ID

Recommendations

• Asynchronous user interaction and tool integration in Isabelle/PIDE
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• Isabelle as document-oriented proof assistant
• Interaction with formal mathematical documents in Isabelle/PIDE
• Managing proof documents for asynchronous processing

Cites work

• A Framework for Interactive Proof
• A proof-centric approach to mathematical assistants
• scientific article; zbMATH DE number 1629953 (Why is no real title available?)
• Managing proof documents for asynchronous processing
• User interaction with the Matita proof assistant
• Web interfaces for proof assistants

Cited in

(10)

• CICM'21 systems entries
• Interaction with formal mathematical documents in Isabelle/PIDE
• Asynchronous user interaction and tool integration in Isabelle/PIDE
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• Asynchronous processing of Coq documents: from the kernel up to the user interface
• Automatic proof and disproof in Isabelle/HOL
• Managing proof documents for asynchronous processing
• Combining source, content, presentation, narration, and relational representation
• Isabelle as document-oriented proof assistant
• Interactive simplifier tracing and debugging in Isabelle

Describes a project that uses

Uses Software

• Isabelle
• ML
• Proof General
• Matita
• Isabelle/jEdit
• Scala
• jEdit
• Proof General Kit
• Poly/ML
• Emacs

This page was built for publication: Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5170238)