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

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

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

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

Mathematics Subject Classification ID

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

Cites Work

• 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
• Title not available (Why is that?)
• 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 (3)

• Traf: a graphical proof tree viewer cooperating with Coq through Proof General
• 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 (rough diamond)

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