Traf: a graphical proof tree viewer cooperating with Coq through Proof General

DOI10.1007/978-3-030-02768-1_9MaRDI QIDQ6166143zbMATH OpenOpenAlexFDO

Authors Hideyuki Kawabata, Yuta Tanaka, Mai Kimura, Tetsuo Hironaka

Publication date 2 August 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-02768-1_9

zbMATH Keywords

Coqinteractive theorem proverproof generalproof tree viewerreadability of proof scripts

Mathematics Subject Classification ID

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

Recommendations

• ProofViz: an interactive visual proof explorer
• CtCoq: a system presentation
• scientific article; zbMATH DE number 1629953
• A graphical language for proof strategies
• Coqpie: an IDE aimed at improving proof development productivity (rough diamond)

Cited in

(3)

• MikiBeta : A General GUI Library for Visualizing Proof Trees
• CtCoq: a system presentation
• ProofViz: an interactive visual proof explorer

This page was built for publication: Traf: a graphical proof tree viewer cooperating with Coq through Proof General

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