CtCoq: a system presentation

DOI10.1007/3-540-61511-3_85MaRDI QIDQ4647518zbMATH OpenOpenAlexFDO

Authors Janet Bertot, Yves Bertot

Publication date 15 January 2019

Published in Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61511-3_85

Mathematics Subject Classification ID

Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Recommendations

• A Short Presentation of Coq
• A graphical user interface for formal proofs in geometry
• scientific article; zbMATH DE number 1629953
• scientific article; zbMATH DE number 1696760
• Traf: a graphical proof tree viewer cooperating with Coq through Proof General

Cited in

(4)

• Coq and hardware verification: a case study
• Traf: a graphical proof tree viewer cooperating with Coq through Proof General
• Asynchronous processing of Coq documents: from the kernel up to the user interface
• Coqpie: an IDE aimed at improving proof development productivity (rough diamond)

Describes a project that uses

Uses Software

• Centaur
• CtCoq
• Coq

This page was built for publication: CtCoq: a system presentation

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