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.
-
Software Foundations softwarefoundations.cis.upenn.edu
Series of Coq-based textbooks on logic, functional programming, and foundations of programming languages, aimed at being accessible to beginners.
-
Nix nixos.org
Package manager for Linux and other Unix systems, supporting atomic upgrades and rollbacks.
-
Mathematical Components math-comp.github.io
Formalization of mathematical theories, focusing in particular on group theory.
-
Formal Reasoning About Programs adam.chlipala.net
Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose.
-
Menhir gallium.inria.fr
Parser generator that can output Coq code for verified parsers.
-
Gagallium gallium.inria.fr
-
Coq coq.inria.fr
-
Compcert C Compiler compcert.inria.fr
High-assurance compiler for almost all of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors.
-
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.
- next page of items loading…
