63
97
164
Mentions
@
|
Stars | Project | Description |
---|---|---|---|
36 | 1,767 | The CompCert formally-verified C compiler | |
11 | 1,477 | Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️ | |
4 | 1,218 | A Coq library for Homotopy Type Theory | |
2 | 914 | This coq library aims to formalize a substantial body of mathematics using the univalent point of view. | |
22 | 804 | A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers. | |
10 | 690 | Cryptographic Primitive Code Generation by Fiat | |
1 | 548 | Mathematical Components | |
9 | 390 | Sail RISC-V model | |
2 | 370 | A Learning Environment for Theorem Proving with the Coq proof assistant | |
5 | 286 | My personal repository of formally verified mathematics. | |
1 | 223 | Language for high-assurance and high-speed cryptography | |
1 | 211 | A function definition package for Coq | |
1 | 191 | A Library for Representing Recursive and Impure Programs in Coq | |
1 | 181 | Mathematical Components compliant Analysis Library | |
1 | 177 | An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework | |
2 | 150 | Formal proof of the Four Color Theorem [maintainer=@ybertot] | |
1 | 145 | Mostly Automated Synthesis of Correct-by-Construction Programs | |
1 | 139 | Advent of Code 2018, in Coq! (https://adventofcode.com/2018) | |
2 | 139 | A Platform for High-Level Parametric Hardware Specification and its Modular Verification | |
2 | 128 | A core language for rule-based hardware design 🦑 |
Popular Coq Topics
Latest Mentions
Latest mentioned Coq repos
Stars | Project |
---|---|
2 | Coq-BB5 |
390 | sail-riscv |
235 | hacspec |
0 | type-experiments |
1,477 | stalin-sort |
1,767 | CompCert |
139 | kami |
6 | bfcoq |
1,218 | Coq-HoTT |
370 | CoqGym |
286 | proofs |
99 | riscv-coq |
804 | magmide |
914 | UniMath |
690 | fiat-crypto |
181 | analysis |
548 | math-comp |
5 | finite |
150 | fourcolor |
28 | coq-simple-io |
Latest Discoveries
Latest discovered Coq repos
Stars | Project |
---|---|
2 | Coq-BB5 |
0 | type-experiments |
6 | bfcoq |
99 | riscv-coq |
181 | analysis |
548 | math-comp |
5 | finite |
914 | UniMath |
0 | recross-coq |
12 | regexp-Brzozowski |
70 | Schools |
0 | traversable-fincontainer |
223 | jasmin |
9 | diffgeo |
24 | cps |
31 | aneris |
286 | proofs |
48 | rupicola |
2 | strong-induction |
59 | name-the-biggest-number |
Recently updated posts
-
Proving with Coq the 5th Busy Beaver number, BB(5)=47,176,870
-
Bertie – A minimal, high-assurance implementation of TLS 1.3 written in hacspec
-
Stalin Sort Algorithm
-
So you think you know C?
-
Kami: A Platform for Hardware Specification and Verification