Skip to content

Coq Coq Correct!
Compare
Choose a tag to compare
@mattam82 mattam82 released this 16 Nov 13:24
CoqCoqCorrect
914e4c6
This commit was signed with the committer’s verified signature.
mattam82 Matthieu Sozeau
GPG key ID: 5560E767972A4459
Verified
Learn about vigilant mode.

Snapshot of MetaCoq - accompanying material of the article:

Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. 2020. Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq. Proc. ACM Program. Lang. 4, POPL, Article 8 (January 2020), 28 pages. https://doi.org/10.1145/3371076

See the README.md file for instructions on how to install and browse the sources.

Assets 2
Loading