Asynchronous processing of Coq documents: from the kernel up to the user interface

DOI10.1007/978-3-319-22102-1_4MaRDI QIDQ2945623zbMATH OpenOpenAlexFDO

Authors Bruno Barras, Carst Tankink, Enrico Tassi

Publication date 14 September 2015

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

Full work available at URL https://arxiv.org/abs/1506.05605

Mathematics Subject Classification ID

Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: The work described in this paper improves the reactivity of the Coq system by completely redesigning the way it processes a formal document. By subdividing such work into independent tasks the system can give precedence to the ones of immediate interest for the user and postpones the others. On the user side, a modern interface based on the PIDE middleware aggregates and present in a consistent way the output of the prover. Finally postponed tasks are processed exploiting modern, parallel, hardware to offer better scalability.

Recommendations

• Managing proof documents for asynchronous processing
• Asynchronous user interaction and tool integration in Isabelle/PIDE
• Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit
• CtCoq: a system presentation
• Interaction with formal mathematical documents in Isabelle/PIDE

Cites work

• scientific article; zbMATH DE number 1629953 (Why is no real title available?)
• A compact kernel for the calculus of inductive constructions
• A machine-checked proof of the odd order theorem
• Asynchronous user interaction and tool integration in Isabelle/PIDE
• Collaborative Interactive Theorem Proving with Clide
• Isabelle as document-oriented proof assistant
• Isabelle/HOL. A proof assistant for higher-order logic

Cited in

(4)

• Distributed parallel build for the Isabelle archive of formal proofs
• Semantics of Mizar as an Isabelle object logic
• Coqpie: an IDE aimed at improving proof development productivity (rough diamond)
• Managing proof documents for asynchronous processing

Describes a project that uses

Uses Software

• Coqoon
• Proof General
• Isabelle/HOL
• Coq

This page was built for publication: Asynchronous processing of Coq documents: from the kernel up to the user interface

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