Coq
Showing 36 of 121 projects
A Coq library providing verified translations between automata, regular expressions, and WS1S logic for regular languages.
A Coq library formalizing graph theory results, including Menger's Theorem, Hall's Marriage Theorem, and Wagner's Theorem.
An educational environment for writing mathematical proofs in interactive notebooks, now available as a VS Code extension.
A deprecated Coq plugin for generating parametricity statements and proofs from Coq definitions.
Coq formalization of program logics (Hoare logic, separation logic, concurrent separation logic) for verifying imperative and concurrent programs.
A Coq library for certifying primality using Pocklington and Elliptic Curve certificates, with efficient modular arithmetic.
Docker images for Coq proof assistant versions 8.4 to 8.20, based on Debian Slim with opam 2.x.
Provides ring, field, lra, nra, and psatz tactics for the Mathematical Components library in Coq.
A Rocq/Coq library providing formal definitions and mechanically verified proofs for rewriting theory, λ-calculus, and termination analysis.
A Coq plugin providing tactics for rewriting universally quantified equations modulo associativity and commutativity.
A formal verification of the Feit-Thompson theorem (Odd Order Theorem) using the Coq proof assistant and Mathematical Components library.
A Coq library formalizing Partial Commutative Monoids (PCMs) for separation logic-based program verification.
A library providing a purely functional IO monad for Coq, enabling direct implementation of IO programs with OCaml bindings.
Generates locally nameless definitions and infrastructure lemmas for Coq from Ott language specifications.
Mutation analysis tool for Coq verification projects to detect incomplete specifications.
A Coq formalization of Bourbaki's Elements of Mathematics, covering set theory and number theory using the Mathematical Components library.
An HTML documentation generator for Coq source files with proof script folding capabilities.
A unified Coq library for bit vectors used across multiple MIT research projects.
Extends Coq's zify tactic to support Mathematical Components library definitions for arithmetic solving.
A Coq library providing lemmas and tactics for reasoning about lists and binary relations.
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq's Hoare Type Theory.
A formal Coq development of the Tower of Hanoi problem with generalized frameworks and proofs.
A Coq library for formal verification of randomized algorithms using a monadic probability distribution interpretation.
A Coq library providing enhanced coinductive proof methods based on the 'companion' concept from coinduction theory.
A Coq implementation of Sokoban, the Japanese warehouse keeper puzzle game.
A Coq library providing arbitrarily large integer and rational numbers (BigN, BigZ, BigQ) for formal verification.
A Rocq library providing stable mergesort algorithms with formal correctness proofs using relational parametricity.
A Coq library providing tactics and tacticals for hypothesis manipulation during proofs.
A neural network-based tool that suggests lemma names for Coq verification projects by analyzing serialized statements and elaborated terms.
A formal verification of the 2048 game implemented in the Coq proof assistant.
Generates Coq boilerplate code for handling binders, renaming, and substitutions in formal language metatheory.
A Coq library for formal verification of graph-manipulating C programs, compatible with CompCert and VST.
Coq formalization and correctness proofs of Tarjan's and Kosaraju's algorithms for finding strongly connected components in graphs.
A certified Sudoku solver implemented in Coq using a formalized Davis-Putnam procedure.
A generic goal preprocessing tool for proof automation tactics in Coq.
Templates for generating configuration files and boilerplate for Coq projects, including CI setup and documentation.
Related Tags
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.