CoqPIE: An IDE Aimed at Improving Proof Development Productivity

DOI10.1007/978-3-319-43144-4_32zbMATH Open1478.68437OpenAlexW2495149520MaRDI QIDQ2829283FDOQ2829283

S. Smith, Author name not available (Why is that?)

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)

Cites Work

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

Cited In (2)

• CoqPIE
• Isabelle/jEdit – A Prover IDE within the PIDE Framework

Uses Software

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

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

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