coq-community

All

74 repositories

coq-nix-toolbox
Public
Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
coq nix
Nix
•
MIT License
•12•34•29•11•Updated Dec 21, 2024Dec 21, 2024
docker-rocq
Public
Docker images of the Rocq Prover (see also: https://github.com/coq-community/docker-coq-action) [maintainers=@erikmd,@himito]
Dockerfile
•
MIT License
•0•0•0•0•Updated Dec 19, 2024Dec 19, 2024
docker-coq
Public
Docker images of the Coq proof assistant (see also: https://github.com/coq-community/docker-coq-action) [maintainers=@erikmd,@himito]
ci coq opam docker-coq dockerfile docker-image
Dockerfile
•
BSD 3-Clause "New" or "Revised" License
•3•37•5•0•Updated Dec 19, 2024Dec 19, 2024
paramcoq
Public
Coq plugin for parametricity [maintainer=@proux01]
coq-plugin parametricity docker-coq-action coq-ci coq-platform coq
Coq
•
Other
•24•45•6•2•Updated Dec 19, 2024Dec 19, 2024
coq-dpdgraph
Public
Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
dependency-analysis dependency-graph docker-coq-action coq-ci coq-platform coq
Coq
•
GNU Lesser General Public License v2.1
•28•87•8•8•Updated Dec 18, 2024Dec 18, 2024
coqeal
Public
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
coq refinement mathcomp coq-ci coq-platform mathcomp-ci
Coq
•
Other
•17•67•6•3•Updated Dec 15, 2024Dec 15, 2024
templates
Public
Templates for configuration files and scripts useful for maintaining Coq projects [maintainers=@liyishuai,@palmskog,@Zimmi48]
continuous-integration coq mustache-templates
Mustache
•
The Unlicense
•9•13•22•3•Updated Dec 13, 2024Dec 13, 2024
coq-ext-lib
Public
A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
library programming coq coq-ci coq-platform
Coq
•
BSD 2-Clause "Simplified" License
•47•129•16•1•Updated Dec 9, 2024Dec 9, 2024
bignums
Public
Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
large-numbers coq-plugin docker-coq-action coq-ci coq-platform coq
Coq
•
GNU Lesser General Public License v2.1
•22•22•1•2•Updated Dec 8, 2024Dec 8, 2024
coq-performance-tests-plots-history
Public
Maintaining plot history for coq-community/coq-performance-tests gh-pages branch [maintainer=@JasonGross]
0•0•1•0•Updated Dec 1, 2024Dec 1, 2024
coq-performance-tests
Public
A library of Coq source files testing for performance regressions on Coq [maintainer=@JasonGross]
testing performance coq
Coq
•
MIT License
•7•7•1•3•Updated Dec 1, 2024Dec 1, 2024
graph-theory
Public
Graph Theory [maintainers=@chdoc,@damien-pous]
coq graph-theory mathcomp docker-coq-action mathcomp-ci
Coq
•4•35•2•1•Updated Nov 30, 2024Nov 30, 2024
corn
Public
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
coq coq-library real-number coq-ci coq-platform
Coq
•
GNU General Public License v2.0
•45•112•9•1•Updated Nov 28, 2024Nov 28, 2024
docker-base
Public
Parent image for Docker images of the Coq proof assistant [maintainers=@erikmd,@himito]
coq docker-coq
Dockerfile
•
BSD 3-Clause "New" or "Revised" License
•4•4•0•0•Updated Nov 27, 2024Nov 27, 2024
fav-ssr
Public
Functional Algorithms Verified in SSReflect [maintainer=@clayrat]
avl-tree coq huffman-coding quadtree binomial-heap ssreflect 2-3-tree leftist-heap mathcomp redblack-tree
Coq
•
MIT License
•7•45•13•1•Updated Nov 17, 2024Nov 17, 2024
apery
Public
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
ssreflect mathcomp coq
Coq
•
Other
•7•19•5•1•Updated Nov 16, 2024Nov 16, 2024
run-coq-bug-minimizer
Public
Repository for triggering runs of the Coq bug minimizer using GitHub Actions [maintainer=@JasonGross]
Shell
•
MIT License
•0•2•8•0•Updated Nov 16, 2024Nov 16, 2024
fourcolor
Public
Formal proof of the Four Color Theorem [maintainer=@ybertot]
ssreflect four-color-theorem mathcomp coq-ci coq
Coq
•
Other
•22•175•0•4•Updated Nov 15, 2024Nov 15, 2024
lemma-overloading
Public
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
automation coq typeclasses ssreflect paper-artifacts canonical-structures mathcomp
Coq
•
Other
•6•26•3•0•Updated Nov 13, 2024Nov 13, 2024
math-classes
Public
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
coq mathematics typeclasses coq-library coq-ci coq-platform
Coq
•
MIT License
•43•162•10•2•Updated Nov 3, 2024Nov 3, 2024
aac-tactics
Public
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
coq-plugin coq-tactic docker-coq-action nix-action coq-ci coq-platform coq
OCaml
•
Other
•21•29•3•2•Updated Nov 1, 2024Nov 1, 2024
reduction-effects
Public
A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]
coq side-effects coq-plugin coq-ci
Makefile
•
Mozilla Public License 2.0
•6•6•4•0•Updated Oct 30, 2024Oct 30, 2024
atbr
Public
Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]
coq coq-plugin coq-tactic kleene-algebra coq-ci
Coq
•
Other
•5•23•0•1•Updated Oct 21, 2024Oct 21, 2024
topology
Public
General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
topology coq-library coq
Coq
•
Other
•10•47•9•4•Updated Oct 19, 2024Oct 19, 2024
trocq
Public
A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]
coq parametricity
Coq
•
GNU Lesser General Public License v3.0
•3•19•15•5•Updated Oct 18, 2024Oct 18, 2024
vscoq-legacy
Public
Legacy Visual Studio Code extension for Coq [maintainers=@huynhtrankhanh,@thery,@Blaisorblade]
TypeScript
•
MIT License
•0•1•4•0•Updated Oct 10, 2024Oct 10, 2024
autosubst
Public
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
variable-binding ssreflect debruijn-indices mathcomp coq-ci coq
Coq
•
MIT License
•14•53•4•1•Updated Sep 17, 2024Sep 17, 2024
stalmarck
Public
Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]
coq tautology coq-plugin tautology-checking coq-extraction docker-coq-action nix-action coq-ci
Coq
•
GNU Lesser General Public License v2.1
•3•1•0•1•Updated Aug 13, 2024Aug 13, 2024
coq-tricks
Public
Tricks you wish the Coq manual told you [maintainer=@tchajed]
coq
Coq
•
MIT License
•22•506•5•0•Updated Aug 13, 2024Aug 13, 2024
awesome-coq
Public
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]
awesome coq resources awesome-list
Creative Commons Zero v1.0 Universal
•20•327•5•0•Updated Aug 11, 2024Aug 11, 2024