Managing proof documents for asynchronous processing

DOI10.1016/J.ENTCS.2008.12.097zbMATH Open1291.68342OpenAlexW2127073439MaRDI QIDQ5166497FDOQ5166497

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

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

zbMATH Keywords

software architectureasynchronous proof processingusability of interactive provers

Mathematics Subject Classification ID

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems
• Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors
• Mathematical Knowledge Management

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

Uses Software

• Isabelle/Isar
• Mizar
• Proof General
• SWT

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)