CoqPIE: An IDE Aimed at Improving Proof Development Productivity

DOI10.1007/978-3-319-43144-4_32zbMath1478.68437OpenAlexW2495149520MaRDI QIDQ2829283

No author found.

Publication date: 27 October 2016

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

Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_32

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

CoqPIE

Uses Software

• Coq
• Isabelle
• Proviola
• Proof General
• Isabelle/jEdit
• Isabelle/PIDE
• CtCoq
• Coqoon
• PeaCoq
• GitHub

Cites Work

• Unnamed Item
• Modular deductive verification of multiprocessor hardware designs
• Compositional Computational Reflection
• Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
• Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar
• Effective interactive proofs for higher-order imperative programs
• Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface
• Proviola: A Tool for Proof Re-animation
• Towards Formal Proof Script Refactoring
• Theorem Proving in Higher Order Logics

This page was built for publication: CoqPIE: An IDE Aimed at Improving Proof Development Productivity