Proof Visualisation and Transformation

This project aims at improving the readability and tracability of proofs (especially Coq proof scripts) by transforming them into a table representation.

An implementation is given by the Coq Proof Script Tools (Coq-PST), formerly named Coq Proof Script Visualiser (Coq-PSV).

We are planning to publish an updated version ov Coq-PST by the end of Dec. 2022 or in January 2023 and more details on Coq-PST will be given soon.

Please feel free to give us some feedback or wishes.

The (old) Coq-PSV page is located here, for reference.