Releases: deividrvale/nijn-coq-script-generation
Releases · deividrvale/nijn-coq-script-generation
First Release of public API
This release describes the first version of the public API for ONijn.
Please check https://deividrvale.github.io/nijn-coq-script-generation/onijn/index.html for more details on this release.
This version is attached, as software artifact, to the paper "Certifying Higher-Order Polynomial Interpretation", by Niels van der Weide, Deivid Vale, and Cynthia Kop.
First Public Release Version
This is the first public release version of ONijn. It can correctly generate proof scripts from proof trace files.
Please, check the documention for more details.