The Coq Proof Script Visualiser (coq-psv)
Logic in Computer Science
2021-01-20 v1 Computers and Society
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.
Keywords
Cite
@article{arxiv.2101.07761,
title = {The Coq Proof Script Visualiser (coq-psv)},
author = {Mario Frank},
journal= {arXiv preprint arXiv:2101.07761},
year = {2021}
}
Comments
This contribution was presented during a talk at the Coq Workshop 2020, affiliated with the IJCAR 2020