مكتبات مكتوبة بلغة Coq

CompCert

مترجم لغة C المعتمد رسميا من CompCert.
  • 1.6k
  • GNU General Public License v3.0

stalin-sort

أضف خوارزمية فرز ستالين بأي لغة تريدها ❣️ إذا كنت تحب ، فامنحنا ⭐️.
  • 1.2k
  • MIT

Coq-HoTT

مكتبة Coq لنظرية النوع Homotopy.
  • 1.2k
  • GNU General Public License v3.0

UniMath

تهدف مكتبة coq هذه إلى إضفاء الطابع الرسمي على مجموعة كبيرة من الرياضيات باستخدام وجهة نظر أحادية..
  • 853
  • GNU General Public License v3.0

magmide

لغة إثبات مكتوبة بشكل يعتمد عليه تهدف إلى جعل رمز معدني مكشوف صحيحًا ممكنًا لمهندسي البرمجيات العاملين.
  • 771

fiat-crypto

إنشاء كود التشفير البدائي بواسطة شركة فيات.
  • 594
  • GNU General Public License v3.0

math-comp

المكونات الرياضية.
  • 501

CoqGym

بيئة تعليمية لإثبات النظرية مع مساعد إثبات Coq.
  • 332
  • GNU Lesser General Public License v3.0 only

sail-riscv

نموذج الشراع RISC-V.
  • 306
  • GNU General Public License v3.0

proofs

مستودعي الشخصي للرياضيات التي تم التحقق منها رسميًا..
  • 259
  • GNU General Public License v3.0

hacspec

لغة مواصفات لأوليات التشفير..
  • 218
  • MIT

Coq-Equations

حزمة تعريف دالة لـ Coq.
  • 197
  • GNU Lesser General Public License v3.0 only

verdi-raft

تطبيق بروتوكول توافق توزيع Raft ، تم التحقق منه في Coq باستخدام إطار عمل Verdi.
  • 168
  • BSD 2-clause "Simplified"

jasmin

لغة للتشفير عالي التأكيد وعالي السرعة (بواسطة jasmin-lang).
  • 159
  • MIT

analysis

مكتبة تحليل متوافقة مع المكونات الرياضية (بواسطة شركات الرياضيات).
  • 158
  • GNU General Public License v3.0

fiat

توليف مؤتمت في الغالب لبرامج التصحيح حسب البناء.
  • 140
  • GNU General Public License v3.0

advent-of-coq-2018

ظهور الكود 2018 ، في Coq! (https://adventofcode.com/2018).
  • 139

fourcolor

  • 131
  • GNU General Public License v3.0

kami

نظام أساسي لمواصفات الأجهزة البارامترية عالية المستوى والتحقق المعياري الخاص بها (بواسطة mit-plv).
  • 126
  • MIT

corn

  • 108
  • GNU General Public License v3.0 only

toychain

تم تنفيذ إجماع blockchain في أضيق الحدود والتحقق منه في Coq.
  • 106
  • BSD 2-clause "Simplified"

koika

لغة أساسية لتصميم الأجهزة المستندة إلى القواعد 🦑.
  • 104
  • GNU General Public License v3.0 only

silveroak

المواصفات الرسمية والتحقق من الأجهزة ، خاصة للأمان والخصوصية..
  • 97
  • Apache License 2.0

coq-library-undecidability

مكتبة من البراهين الآلية لعدم القدرة على اتخاذ القرار في مساعد إثبات Coq.
  • 96
  • GNU General Public License v3.0

ConCert

إطار عمل للتحقق الذكي من العقد في Coq.
  • 92
  • MIT

riscv-coq

مواصفات RISC-V في Coq.
  • 87
  • BSD 3-clause "New" or "Revised"

vericert

أداة تجميع عالية المستوى تم التحقق منها رسميًا استنادًا إلى CompCert ومكتوبة بلغة Coq.
  • 71
  • GNU General Public License v3.0 only

hs-to-coq

تحويل كود مصدر Haskell إلى كود مصدر Coq..
  • 69
  • MIT

scala-escape

مكون إضافي للمترجم للتحكم في عمر الكائن في Scala (بواسطة TiarkRompf).
  • 62
  • BSD 3-clause "New" or "Revised"

rupicola

Gallina إلى مجموعة أدوات التجميع Bedrock2.
  • 46
  • MIT