This repository used to hold the Abstract Consistency Properties framework, which is now in the Archive of Formal Proofs.
It now holds a completeness proof for Andrews' Q0 based on the Metatheory of Q0 AFP entry by Javier Díaz.
| Name | Name | Last commit date | ||
|---|---|---|---|---|
This repository used to hold the Abstract Consistency Properties framework, which is now in the Archive of Formal Proofs.
It now holds a completeness proof for Andrews' Q0 based on the Metatheory of Q0 AFP entry by Javier Díaz.