مكتبات مكتوبة بلغة Coq
UniMath
تهدف مكتبة coq هذه إلى إضفاء الطابع الرسمي على مجموعة كبيرة من الرياضيات باستخدام وجهة نظر أحادية..
- 853
- GNU General Public License v3.0
magmide
لغة إثبات مكتوبة بشكل يعتمد عليه تهدف إلى جعل رمز معدني مكشوف صحيحًا ممكنًا لمهندسي البرمجيات العاملين.
- 771
CoqGym
بيئة تعليمية لإثبات النظرية مع مساعد إثبات Coq.
- 332
- GNU Lesser General Public License v3.0 only
verdi-raft
تطبيق بروتوكول توافق توزيع Raft ، تم التحقق منه في Coq باستخدام إطار عمل Verdi.
- 168
- BSD 2-clause "Simplified"
analysis
مكتبة تحليل متوافقة مع المكونات الرياضية (بواسطة شركات الرياضيات).
- 158
- GNU General Public License v3.0
kami
نظام أساسي لمواصفات الأجهزة البارامترية عالية المستوى والتحقق المعياري الخاص بها (بواسطة mit-plv).
- 126
- MIT
coq-library-undecidability
مكتبة من البراهين الآلية لعدم القدرة على اتخاذ القرار في مساعد إثبات Coq.
- 96
- GNU General Public License v3.0
vericert
أداة تجميع عالية المستوى تم التحقق منها رسميًا استنادًا إلى CompCert ومكتوبة بلغة Coq.
- 71
- GNU General Public License v3.0 only
scala-escape
مكون إضافي للمترجم للتحكم في عمر الكائن في Scala (بواسطة TiarkRompf).
- 62
- BSD 3-clause "New" or "Revised"