Asynchronous user interaction and tool integration in Isabelle/PIDE

DOI10.1007/978-3-319-08970-6_33MaRDI QIDQ2879273zbMATH OpenOpenAlexFDO

Authors Makarius Wenzel

Publication date 8 September 2014

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08970-6_33

Mathematics Subject Classification ID

Recommendations

• Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit
• Interaction with formal mathematical documents in Isabelle/PIDE
• Managing proof documents for asynchronous processing
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• A web interface for Isabelle: the next generation

Cited in

(14)

• scientific article; zbMATH DE number 7649970 (Why is no real title available?)
• Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit
• Translating Scala programs to Isabelle/HOL. System description
• scientific article; zbMATH DE number 7756106 (Why is no real title available?)
• Isabelle as document-oriented proof assistant
• Shared-memory multiprocessing for interactive theorem proving
• From LCF to Isabelle/HOL
• Interaction with formal mathematical documents in Isabelle/PIDE
• Semantics of Mizar as an Isabelle object logic
• Asynchronous processing of Coq documents: from the kernel up to the user interface
• A web interface for Isabelle: the next generation
• Coqpie: an IDE aimed at improving proof development productivity (rough diamond)
• Managing proof documents for asynchronous processing
• Interactive simplifier tracing and debugging in Isabelle

Describes a project that uses

Uses Software

• Isabelle/PIDE
• Scala
• Isabelle/jEdit
• PIDE
• Matita
• Proof General
• Isabelle/HOL
• Isabelle
• Dafny
• Coq

This page was built for publication: Asynchronous user interaction and tool integration in Isabelle/PIDE

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