Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface

DOI10.1007/978-3-319-22102-1_4zbMath1465.68275arXiv1506.05605OpenAlexW2963412521MaRDI QIDQ2945623

Enrico Tassi, Carst Tankink, Bruno Barras

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)

Related Items (2)

CoqPIE: An IDE Aimed at Improving Proof Development Productivity ⋮ Semantics of Mizar as an Isabelle object logic

Uses Software

• Coq
• Isabelle/HOL
• Proof General
• Coqoon

Cites Work

• Unnamed Item
• A compact kernel for the calculus of inductive constructions
• Isabelle/HOL. A proof assistant for higher-order logic
• Collaborative Interactive Theorem Proving with Clide
• Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
• Isabelle as Document-Oriented Proof Assistant
• A Machine-Checked Proof of the Odd Order Theorem

This page was built for publication: Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface