The Coq Proof Script Visualiser (coq-psv)
Mario Frank
TL;DR
The paper introduces coq-psv, a visualization tool that converts Coq proof scripts into printable table formats in LaTeX or PDF, aiding education and review without requiring Coq execution.
Contribution
It provides a novel proof visualization method that produces printable proof representations, facilitating easier review and teaching of formal proofs.
Findings
Supports both education and review processes
Produces easily printable proof representations
Does not require Coq to review proofs
Abstract
In this work, we present a visualisation tool that is able to process Coq proof scripts and generate a table representation of the contained proofs as or PDF files. This tool has the aim to support both education and review processes as all proof steps can be visualised. Thus, there is no need to use Coq in order to review proofs or use them as examples in teaching. In contrast to the usual approach of visualising proofs as hypertext or markdown documents, the generated files can be easily printed.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMathematics, Computing, and Information Processing · Logic, programming, and type systems · Software Engineering and Design Patterns