Certifying Answers of Boolean SAT-Solvers (with a proof combining Coq and OCaml typecheckers)
-
Updated
Apr 8, 2019 - Coq
#
coq-extraction
Here are 11 public repositories matching this topic...
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.
coq
sorting-algorithms
coq-formalization
formal-verification
divide-and-conquer
coq-tactic
coq-extraction
-
Updated
Oct 31, 2022 - Coq
Correctness proof of the Huffman coding algorithm in Coq [maintainer=@palmskog]
-
Updated
Dec 30, 2023 - Coq
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
distributed-systems
key-value
ocaml
coq
causal-consistency
coq-extraction
docker-coq-action
nix-action
-
Updated
Dec 30, 2023 - Coq
Verified implementation in Coq of Buchberger's algorithm for computing Gröbner bases [maintainer=@palmskog]
-
Updated
Dec 30, 2023 - Coq
A Coq library to embed Impure OCaml oracles in certified Coq code
-
Updated
Feb 8, 2024 - Coq
A Coq library to embed Impure OCaml oracles in certified Coq code
-
Updated
Feb 8, 2024 - Coq
Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]
-
Updated
Aug 13, 2024 - Coq
Coq proof of Bertrand's postulate on existence of primes [maintainer=@thery]
-
Updated
Jul 15, 2024 - Coq
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
-
Updated
Aug 4, 2024 - Coq
(Terminating) hylomorphisms in Coq
-
Updated
Oct 10, 2024 - TeX
Improve this page
Add a description, image, and links to the coq-extraction topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the coq-extraction topic, visit your repo's landing page and select "manage topics."