Coq
215 items from coq-community/awesome-coq ★396
-
opam-switch-mode github.com
IDE extension for Proof General to locally change or reset the opam switch from a menu or using a command.
-
Docker-Coq github.com
Docker images for many versions of Coq.
-
Algebra Tactics github.com
Ring and field tactics for Mathematical Components.
-
Odd Order Theorem github.com
Formal proof of the Odd Order Theorem, a landmark result of finite group theory.
-
CoLoR github.com
Library on rewriting theory, lambda-calculus and termination, with sub-libraries on common data structures extending the Coq standard library.
-
AAC Tactics github.com
Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator.
-
FCSL-PCM github.com
Formalization of partial commutative monoids as used in verification of pointer-manipulating programs.
-
Simple IO github.com
Input/output monad with user-definable primitive operations.
-
VCFloat github.com
Framework for verifying C programs with floating-point computations.
-
lngen github.com
Tool for generating locally nameless Coq definitions and proofs.
-
coq2html github.com
Alternative HTML documentation generator for Coq.
-
Mczify github.com
Library enabling Micromega arithmetic solvers to work when using Mathematical Components number definitions.
-
mCoq github.com
Mutation analysis tool for Coq projects.
-
Hahn github.com
Library for reasoning on lists and binary relations.
-
Bedrock Bit Vectors github.com
Library for reasoning on fixed precision machine words.
-
Gaia github.com
Implementation of books from Bourbaki's Elements of Mathematics, including set theory and number theory.
-
Coinduction github.com
Plugin for doing proofs by enhanced coinduction.
-
Lemma Overloading github.com
Demonstration of design patterns for programming and proving with canonical structures.
-
Hanoi github.com
The Tower of Hanoi puzzle in Coq, including generalizations and theorems about configurations.
-
Stable sort algorithms in Coq github.com
Generic and modular proofs of correctness, including stability, of mergesort functions.
-
ALEA github.com
Library for reasoning on randomized algorithms.
-
Bignums github.com
Library of arbitrarily large numbers.
-
Coqoban github.com
Coq implementation of Sokoban, the Japanese warehouse keepers' game.
-
LibHyps github.com
Library of Ltac tactics to manage and manipulate hypotheses in proofs.
-
Autosubst-ocaml github.com
Tool that generates Coq code for handling binders in syntax, such as for renaming and substitutions.
-
T2048 github.com
Coq version of the 2048 sliding tile game.
-
Roosterize github.com
Tool for suggesting lemma names in Coq projects.
-
CertiGraph github.com
Library for reasoning about directed graphs and their embedding in separation logic.
-
Sudoku github.com
Formalization and solver of the Sudoku number-placement puzzle in Coq.
-
Tarjan and Kosaraju github.com
Verified implementations of algorithms for topological sorting and finding strongly connected components in finite graphs.
-
Trakt github.com
Generic goal preprocessing tool for proof automation tactics.
-
coq-community Templates github.com
Templates for generating configuration files for Coq projects.
-
MathComp Tutorial Materials github.com
Source code for Mathematical Components tutorials.
-
Coqtail Math github.com
Library of mathematical results ranging from arithmetic to real and complex analysis.
-
Completeness and Decidability of Modal Logic Calculi github.com
Soundness, completeness, and decidability for the logics K, K*, CTL, and PDL.
-
coq-scripts github.com
Scripts for dealing with Coq files, including tabulating proof times.
-
Floating-Point Numbers and Formal Proof github.com
Introductory course on Coq real numbers and floating-point numbers from the Flocq library.
-
Natural Number Game github.com
Coq version of the natural number game developed for the Lean prover.
-
MathComp School github.com
Coq sources for lessons and exercises that introduce the SSReflect proof language and the Mathematical Components library.
-
Docker-MathComp github.com
Docker images for many combinations of versions of Coq and the Mathematical Components library.
-
Mini-Rubik github.com
Coq formalization and solver of the 2x2x2 version of the Rubik's Cube puzzle.
-
MathComp Extra github.com
Extra material for the Mathematical Components library, including the AKS primality test and RSA encryption and decryption.
-
Tree Sitter Rocq github.com
Partial Rocq tree-sitter grammar useful for syntax highlighting in text editors like Helix, but not recommended for full parsing of Rocq code.
-
Puiseuxth github.com
Proof of Puiseux's theorem and computation of roots of polynomials of Puiseux's series.
-
Rocqnavi github.com
Fork of coq2html that adds indexes, clickable notations, Markdown and LaTeX formatting in comments, and more.
-
Coq-Kruskal github.com
Collection of libraries related to rose trees and Kruskal's tree theorem.
