Managing proof documents for asynchronous processing

DOI10.1016/J.ENTCS.2008.12.097MaRDI QIDQ5166497zbMATH OpenOpenAlexFDO

Authors Holger Gast

Publication date 27 June 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.2008.12.097

zbMATH Keywords

software architectureasynchronous proof processingusability of interactive provers

Mathematics Subject Classification ID

Recommendations

• Asynchronous user interaction and tool integration in Isabelle/PIDE
• Asynchronous processing of Coq documents: from the kernel up to the user interface
• Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit
• Interaction with formal mathematical documents in Isabelle/PIDE
• Interactive theorem proving from the perspective of Isabelle/Isar

Cites work

• scientific article; zbMATH DE number 1629953 (Why is no real title available?)
• scientific article; zbMATH DE number 986405 (Why is no real title available?)
• scientific article; zbMATH DE number 1006119 (Why is no real title available?)
• scientific article; zbMATH DE number 2090295 (Why is no real title available?)
• Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors
• Mathematical Knowledge Management
• \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems

Cited in

(3)

• Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit
• Asynchronous user interaction and tool integration in Isabelle/PIDE
• Asynchronous processing of Coq documents: from the kernel up to the user interface

Describes a project that uses

Uses Software

• SWT
• Proof General
• Mizar
• Isabelle/Isar

This page was built for publication: Managing proof documents for asynchronous processing

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