Coqpie: an IDE aimed at improving proof development productivity (rough diamond)

DOI10.1007/978-3-319-43144-4_32MaRDI QIDQ2829283zbMATH OpenOpenAlexFDO

Authors S. Smith

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)

Recommendations

• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• scientific article; zbMATH DE number 1629953
• Recycling proof patterns in Coq: case studies
• A Short Presentation of Coq
• CtCoq: a system presentation

Cites work

• scientific article; zbMATH DE number 1479613 (Why is no real title available?)
• Asynchronous processing of Coq documents: from the kernel up to the user interface
• Asynchronous user interaction and tool integration in Isabelle/PIDE
• Compositional computational reflection
• Dependencies in formal mathematics: applications and extraction for Coq and Mizar
• Effective interactive proofs for higher-order imperative programs
• Modular deductive verification of multiprocessor hardware designs
• Proviola: a tool for proof re-animation
• Theorem Proving in Higher Order Logics
• Towards Formal Proof Script Refactoring

Cited in

(3)

• Traf: a graphical proof tree viewer cooperating with Coq through Proof General
• CoqPIE
• Isabelle/jEdit – A Prover IDE within the PIDE Framework

Describes a project that uses

Uses Software

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

This page was built for publication: Coqpie: an IDE aimed at improving proof development productivity (rough diamond)

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