Nā hale waihona puke i kākau ʻia ma Coq
stalin-sort
Hoʻohui i kahi algorithm ʻano stalin ma kekahi ʻōlelo āu e makemake ai ❣️ inā makemake ʻoe e hāʻawi mai iā mākou i kahi ⭐️.
- 1.2k
- MIT
UniMath
Ke manaʻo nei kēia waihona coq e hoʻokumu i kahi kino nui o ka makemakika me ka hoʻohana ʻana i ka manaʻo univalent.
- 853
- GNU General Public License v3.0
magmide
ʻO kahi ʻōlelo hōʻoia i hoʻopaʻa ʻia i hoʻopaʻa ʻia i manaʻo ʻia e hoʻopaʻa pono i nā code metala ʻole e hiki ai ke hana i nā ʻenekini polokalamu.
- 771
CoqGym
He Kaiapuni aʻo no ka Theorem Hōʻoia me ke kōkua hōʻoia Coq.
- 332
- GNU Lesser General Public License v3.0 only
verdi-raft
ʻO kahi hoʻokō o ka protocol consensus i hāʻawi ʻia ʻo Raft, i hōʻoia ʻia ma Coq me ka hoʻohana ʻana i ka framework Verdi.
- 168
- BSD 2-clause "Simplified"
analysis
ʻO ka Hale Waihona Puke Hoʻonaʻauao kūpono nā Māhele Matematika (ma ka math-comp).
- 158
- GNU General Public License v3.0
fiat
ʻO ka hapa nui o ka Synthesis Automated o nā papahana Correct-by-Construction.
- 140
- GNU General Public License v3.0
kami
He Papahana no ke Kiʻekiʻe-Level Parametric Hardware Specification a me kona Modular Verification (e mit-plv).
- 126
- MIT
toychain
Ua hoʻokō ʻia a hōʻoia ʻia kahi ʻaelike blockchain minimalistic ma Coq.
- 106
- BSD 2-clause "Simplified"
koika
He ʻōlelo koʻikoʻi no ka hoʻolālā ʻana i nā lako ma muli o ke kānāwai 🦑.
- 104
- GNU General Public License v3.0 only
silveroak
ʻO ka ʻōlelo kikoʻī a me ka hōʻoia ʻana o ka hāmeʻa, ʻoi aku ka palekana a me ka pilikino.
- 97
- Apache License 2.0
coq-library-undecidability
ʻO kahi waihona o nā hōʻoia undecidability mechanized i ka Coq proof assistant..
- 96
- GNU General Public License v3.0
vericert
ʻO kahi mea hana synthesis kiʻekiʻe i hōʻoia ʻia e pili ana i CompCert a kākau ʻia ma Coq..
- 71
- GNU General Public License v3.0 only
scala-escape
ʻO kahi plug-in compiler e hoʻomalu i ke ola o nā mea ma Scala (na TiarkRompf).
- 62
- BSD 3-clause "New" or "Revised"