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
•11•33•29•7•Updated Nov 28, 2024Nov 28, 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•111•8•1•Updated Nov 28, 2024Nov 28, 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 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
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
•46•129•16•2•Updated Nov 26, 2024Nov 26, 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
•20•168•0•3•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
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 Nov 1, 2024Nov 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 Nov 1, 2024Nov 1, 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 Oct 31, 2024Oct 31, 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
templates
Public
Templates for configuration files and scripts useful for maintaining Coq projects [maintainers=@palmskog,@Zimmi48]
continuous-integration mustache-templates coq
Mustache
•
The Unlicense
•8•13•22•5•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•18•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•52•4•1•Updated Sep 17, 2024Sep 17, 2024
paramcoq
Public
Coq plugin for parametricity [maintainer=@proux01]
coq-plugin parametricity docker-coq-action coq-ci coq-platform coq
Coq
•
Other
•24•44•6•2•Updated Sep 17, 2024Sep 17, 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 Sep 10, 2024Sep 10, 2024
coqeal
Public
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
coq refinement mathcomp coq-ci coq-platform mathcomp-ci
Coq
•
Other
•17•66•6•3•Updated Aug 19, 2024Aug 19, 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•504•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•320•5•0•Updated Aug 11, 2024Aug 11, 2024
comp-dec-modal
Public
Completeness and Decidability of Modal Logic Calculi [maintainer=@chdoc]
coq ctl pdl mathcomp modal-logics
Coq
•
Other
•2•8•1•0•Updated Aug 11, 2024Aug 11, 2024
gaia
Public
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
coq set-theory ssreflect mathcomp docker-coq-action bourbaki mathcomp-ci
Coq
•
MIT License
•7•29•0•0•Updated Aug 11, 2024Aug 11, 2024