Βιβλιοθήκες γραμμένες σε Coq

safegcd-bounds

Όρια στις επαναλήψεις divsteps στο safegcd.
  • 45

unbound

Replib: generic programming & Unbound: γενική επεξεργασία συνδετικών.
  • 40
  • BSD 3-clause "New" or "Revised"

coq-simple-io

IO για την Gallina.
  • 27
  • MIT

aneris

Λογική προγράμματος για την ανάπτυξη και την επαλήθευση κατανεμημένων συστημάτων.
  • 25
  • MIT

cps

Μια επισημοποίηση των υπολογισμών στυλ συνεχούς μετάβασης στο Coq [WIP] (από takanuva).
  • 20
  • BSD 3-clause "New" or "Revised"

comonad-transformers

Μετασχηματιστές Comonad Haskell 98 - από το 4.0 έχουν συγχωνευθεί στο πακέτο Comonad..
  • 12
  • BSD 3-clause "New" or "Revised"

friscv

Υλοποίηση CPU RISCV στο SystemVerilog.
  • 10
  • MIT

doubly-generic

Arity-generic datatype-generic, or double-generic, προγραμματισμός σε Coq..
  • 4
  • MIT

Doubly-Linked-List-VST

Το τελικό έργο για το CS2603 (2021 Άνοιξη), με στόχο την επαλήθευση μιας διπλά συνδεδεμένης βιβλιοθήκης λιστών χρησιμοποιώντας VST. Συνεργασία με τον @karzexcc.
  • 2
  • GNU General Public License v3.0 only

recross-coq

Μηχανή Regexp στο Coq για επίλυση σταυρόλεξων regexp.
  • 0
  • GNU General Public License v3.0 only

coq-proof

Coq Proof για αλγόριθμο HashgraphTrim.
  • 0