Knjižnice, napisane v Coq u
stalin-sort
Dodajte algoritem za razvrščanje po Stalinu v katerem koli jeziku, ki vam je všeč ❣️, če vam je všeč, nam dajte ⭐️.
- 1.2k
- MIT
UniMath
Namen te knjižnice coq je formalizirati velik del matematike z uporabo enoličnega vidika.
- 853
- GNU General Public License v3.0
magmide
Odvisno tipiziran dokazni jezik, namenjen delujočim inženirjem programske opreme omogočiti dokazljivo pravilno golo kodo.
- 771
fiat-crypto
Generacija kriptografske primitivne kode s strani Fiata.
- 594
- GNU General Public License v3.0
CoqGym
Učno okolje za dokazovanje izrekov s pomočnikom za dokazovanje Coq.
- 332
- GNU Lesser General Public License v3.0 only
verdi-raft
Izvedba protokola porazdeljenega soglasja Raft, preverjena v Coq z uporabo ogrodja Verdi.
- 168
- BSD 2-clause "Simplified"
analysis
Analysis Library, skladna z matematičnimi komponentami (od math-comp).
- 158
- GNU General Public License v3.0
fiat
Večinoma avtomatizirana sinteza pravilnih programov za konstrukcijo.
- 140
- GNU General Public License v3.0
kami
Platforma za parametrično specifikacijo strojne opreme na visoki ravni in njeno modularno preverjanje (avtor mit-plv).
- 126
- MIT
toychain
Minimalistično soglasje o verigi blokov, implementirano in preverjeno v Coq.
- 106
- BSD 2-clause "Simplified"
koika
Osnovni jezik za načrtovanje strojne opreme na podlagi pravil 🦑.
- 104
- GNU General Public License v3.0 only
silveroak
Uradna specifikacija in preverjanje strojne opreme, zlasti za varnost in zasebnost.
- 97
- Apache License 2.0
coq-library-undecidability
Knjižnica mehaniziranih dokazov neodločljivosti v pomočniku za dokazovanje Coq.
- 96
- GNU General Public License v3.0
vericert
Formalno preverjeno orodje za sintezo na visoki ravni, ki temelji na CompCert in je napisano v Coq..
- 71
- GNU General Public License v3.0 only
scala-escape
Vtičnik prevajalnika za nadzor življenjskih dob objektov v Scali (avtor TiarkRompf).
- 62
- BSD 3-clause "New" or "Revised"