-
Stars26
-
Rank 902,487 (Top 19 %)
-
Language Coq
-
License
Other -
Created over 3 years ago
-
Updated 11 months ago
Reviews
There are no reviews yet. Be the first to send feedback to the community and the maintainers!
Repository Details
Template project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]
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
gaia
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
Coq
25
30
alea
Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
Coq
24
31
atbr
Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]
Coq
22
32
bits
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
Coq
22
33
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
34
coqoban
Sokoban (in Coq) [maintainer=@erikmd]
Coq
21
35
sudoku
A certified Sudoku solver in Coq [maintainers=@siraben,@thery]
Coq
20
36
apery
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
Coq
19
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