GitHub topics: coq-extraction
rocq-community/buchberger
Verified implementation in Coq of Buchberger's algorithm for computing Gröbner bases [maintainer=@palmskog]
Language: Coq - Size: 272 KB - Last synced at: 2 months ago - Pushed at: over 1 year ago - Stars: 10 - Forks: 1
dcastrop/coq-hylomorphisms
(Terminating) hylomorphisms in Coq
Language: Coq - Size: 833 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 1 - Forks: 0
rocq-community/bits
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
Language: Coq - Size: 188 KB - Last synced at: 2 months ago - Pushed at: 4 months ago - Stars: 23 - Forks: 7
rocq-community/bertrand
Coq proof of Bertrand's postulate on existence of primes [maintainer=@thery]
Language: Coq - Size: 252 KB - Last synced at: 2 months ago - Pushed at: 11 months ago - Stars: 3 - Forks: 3
rocq-community/stalmarck
Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]
Language: Coq - Size: 374 KB - Last synced at: 15 days ago - Pushed at: 10 months ago - Stars: 1 - Forks: 3
boulme/ImpureDemo
A Coq library to embed Impure OCaml oracles in certified Coq code
Language: Coq - Size: 58.6 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0
boulme/Impure
A Coq library to embed Impure OCaml oracles in certified Coq code
Language: Coq - Size: 35.2 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 3 - Forks: 0
rocq-community/chapar
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
Language: Coq - Size: 1.94 MB - Last synced at: about 5 hours ago - Pushed at: over 1 year ago - Stars: 32 - Forks: 7
jinxinglim/coq-formalized-divide-and-conquer
This respository contains the formalization of different variations of divide-and-conquer algorithm design paradigm for lists. As a case study, we will see how these different variations lead to different sorting algorithms.
Language: Coq - Size: 42 KB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 3 - Forks: 0
rocq-community/huffman
Correctness proof of the Huffman coding algorithm in Coq [maintainer=@palmskog]
Language: Coq - Size: 1.11 MB - Last synced at: 3 days ago - Pushed at: over 1 year ago - Stars: 14 - Forks: 4
boulme/satans-cert
Certifying Answers of Boolean SAT-Solvers (with a proof combining Coq and OCaml typecheckers)
Language: Coq - Size: 30.4 MB - Last synced at: about 2 years ago - Pushed at: about 6 years ago - Stars: 2 - Forks: 0