-
Stars19
-
Rank 1,127,987 (Top 23 %)
-
Language Coq
-
License
Other -
Created over 4 years ago
-
Updated 2 months ago
Reviews
There are no reviews yet. Be the first to send feedback to the community and the maintainers!
Repository Details
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
More Repositories
1
vscoq
A Visual Studio Code extension for Coq [maintainers=@rtetley,@maximedenes,@huynhtrankhanh,@thery,@Blaisorblade]OCaml
310
2
awesome-coq
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainers=@anton-trunov,@palmskog]
279
3
math-classes
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters]
Coq
157
4
fourcolor
Formal proof of the Four Color Theorem [maintainer=@ybertot]
Coq
148
5
coq-ext-lib
A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
Coq
124
6
corn
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]
Coq
107
7
coq-art
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
Coq
104
8
coq-dpdgraph
Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
Coq
83
9
manifesto
Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
68
10
coqeal
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Coq
64
11
hydra-battles
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
Coq
59
12
coq-100-theorems
Statements of famous theorems proven in Coq [maintainer=@jmadiot]HTML
52
13
autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
Coq
48
14
topology
General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
Coq
45
15
paramcoq
Coq plugin for parametricity [maintainer=@proux01]
Coq
44
16
semantics
A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]
Coq
42
17
parseque
Total Parser Combinators in Coq [maintainer=@womeier]
Coq
41
18
reglang
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
Coq
41
19
coqdocjs
Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]JavaScript
36
20
docker-coq
Docker images of the Coq proof assistant (see also: https://github.com/coq-community/docker-coq-action) [maintainers=@erikmd,@himito]Dockerfile
36
21
chapar
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
Coq
32
22
coqffi
Automatically generates Coq FFI bindings to OCaml libraries [maintainer=@lthms]OCaml
31
23
coq-nix-toolbox
Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]Nix
31
24
graph-theory
Graph Theory [maintainers=@chdoc,@damien-pous]
Coq
29
25
aac-tactics
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]OCaml
29
26
goedel
Archived since the contents have been moved to the Hydras & Co. repository
Coq
28
27
dblib
Coq library for working with de Bruijn indices [maintainer=@KevOrr]
Coq
27
28
lemma-overloading
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
Coq
26
29
coq-program-verification-template
Template project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]
Coq
26
30
gaia
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
Coq
25
31
alea
Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
Coq
24
32
atbr
Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]
Coq
22
33
bits
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
Coq
22
34
bignums
Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
Coq
22
35
coqoban
Sokoban (in Coq) [maintainer=@erikmd]
Coq
21
36
sudoku
A certified Sudoku solver in Coq [maintainers=@siraben,@thery]
Coq
20
37
hoare-tut
A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]
Coq
19
38
HighSchoolGeometry
Geometry in Coq for French high school [maintainer=@thery]
Coq
16
39
coq-plugin-template
Template project for Coq plugins using the Dune build system, showcasing some advanced features [maintainer=@ejgallego]OCaml
16
40
metaprogramming-rosetta-stone
A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=@yforster]
Coq
16
41
coqtail-math
Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis. [maintainer=@jmadiot]
Coq
14
42
huffman
Correctness proof of the Huffman coding algorithm in Coq [maintainer=@palmskog]
Coq
14
43
regexp-Brzozowski
Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]
Coq
12
44
qarith-stern-brocot
Binary rational numbers in Coq [maintainer=@herbelin]
Coq
12
45
templates
Templates for configuration files and scripts useful for maintaining Coq projects [maintainers=@palmskog,@Zimmi48]
Mustache
12
46
docker-coq-action
GitHub Action using Docker-Coq [maintainers=@erikmd,@Zimmi48]Shell
12
47
trocq
A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]
Coq
12
48
tarjan
Coq formalization of algorithms due to Tarjan and Kosaraju for finding strongly connected graph components using Mathematical Components and SSReflect [maintainers=@CohenCyril,@palmskog]
Coq
11
49
coq-mmaps
Modular Finite Maps over Ordered Types in Coq [maintainers=@letouzey,@palmskog]
Coq
8
50
comp-dec-modal
Completeness and Decidability of Modal Logic Calculi [maintainer=@chdoc]
Coq
8
51
buchberger
Verified implementation in Coq of Buchberger's algorithm for computing Gröbner bases [maintainer=@palmskog]
Coq
8
52
proviola
Tool for reanimation of Coq proofs [maintainer=@JasonGross]Python
7
53
notation-gallery
Examples showing best practices for using Coq notations and custom entries [maintainer=@bcpierce00]
Coq
7
54
zorns-lemma
Archived since the contents have been moved to the topology repository
Coq
6
55
reduction-effects
A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]
Makefile
6
56
coq-performance-tests
A library of Coq source files testing for performance regressions on Coq [maintainer=@JasonGross]
Coq
6
57
generic-environments
Coq library that provides an abstract data type for environments [maintainer=@aerabi]
Coq
6
58
docker-base
Parent image for Docker images of the Coq proof assistant [maintainers=@erikmd,@himito]Dockerfile
4
59
almost-full
Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination [maintainer=@palmskog]
Coq
3
60
jmlcoq
Coq definition of JML and a verified runtime assertion checker [maintainer=@palmskog]
Coq
3
61
bertrand
Coq proof of Bertrand's postulate on existence of primes [maintainer=@thery]
Coq
3
62
run-coq-bug-minimizer
Repository for triggering runs of the Coq bug minimizer using GitHub Actions [maintainer=@JasonGross]Shell
2
63
pocklington
Pocklington's criterion for primality in Coq [maintainer=@Casteran]
Coq
2
64
stalmarck
Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]
Coq
1
65
exact-real-arithmetic
Exact Real Arithmetic [maintainers=@ybertot,@magaud]
Coq
1