Coq
215 items from coq-community/awesome-coq ★396
-
coq-haskell github.com
Library smoothing the transition to Coq for Haskell users.
-
SMTCoq github.com
Tool that checks proof witnesses coming from external SAT and SMT solvers.
-
Math Classes github.com
Abstract interfaces for mathematical structures based on type classes.
-
Lectures on Software Foundations github.com
Material on the Software Foundations series of textbooks, including a series of YouTube videos.
-
Fiat github.com
Mostly automated synthesis of correct-by-construction programs.
-
Formalised Undecidable Problems github.com
Library of undecidable problems and reductions between them.
-
SerAPI github.com
Tools and OCaml library for (de)serialization of Coq code to and from JSON and S-expressions.
-
ExtLib github.com
Collection of theories and plugins that may be useful in other Coq developments.
-
Coq'Art Exercises and Tutorials github.com
Coq code and exercises from the Coq'Art book, including additional tutorials.
-
ConCert github.com
Framework for smart contract testing and verification featuring a code extraction pipeline to several smart contract languages.
-
Modeling and Proving in Computational Type Theory github.com
Book covering topics in computational logic using Coq, including foundations, canonical case studies, and practical programming.
-
WasmCert-Coq github.com
Formalization in Coq of the WebAssembly (aka Wasm) 1.0 specification.
-
Ceramist github.com
Verified hash-based approximate membership structures such as Bloom filters.
-
RISC-V Specification in Coq github.com
Definition of the RISC-V processor instruction set architecture and extensions.
-
CoRN github.com
Library of constructive real analysis and algebra.
-
Hierarchy Builder github.com
Collection of commands for declaring Coq hierarchies based on packed classes.
-
coq-dpdgraph github.com
Tool for building dependency graphs between Coq objects.
-
hs-to-coq github.com
Converter from Haskell code to equivalent Coq code.
-
Jupyter kernel for Coq github.com
Coq support for the Jupyter Notebook web environment.
-
SSProve github.com
Framework for modular cryptographic proofs based on the Mathematical Components library.
-
Hoare Type Theory github.com
A shallow embedding of sequential separation logic formulated as a type theory.
-
Hydras & Co. github.com
Continuously in-progress book and library on Kirby and Paris' hydra battles and other entertaining formalized mathematics in Coq, including a proof of the Gödel-Rosser first incompleteness theorem.
-
Metalib github.com
Library for programming language metatheory using locally nameless variable binding representations.
-
Monae github.com
Monadic effects and equational reasoning.
-
Infotheo github.com
Formalization of information theory and linear error-correcting codes.
-
CoqEAL github.com
Framework to ease change of data representations in proofs.
-
Coq-community package maintenance project github.com
-
Mechanized Semantics github.com
Companion Coq sources for a course on programming language semantics at Collège de France.
-
Name the Biggest Number github.com
Repository for submitting proven contenders for the title of biggest number in Coq.
-
100 famous theorems proved using Coq github.com
-
Unicoq github.com
Plugin that replaces the existing unification algorithm with an enhanced one.
-
Q*cert github.com
Platform for implementing and verifying query compilers.
-
Mtac2 github.com
Plugin adding typed tactics for backward reasoning.
-
PyCoq github.com
Set of bindings and libraries for interacting with Coq from inside Python 3.
-
Coq Nix Toolbox github.com
Nix helper scripts to automate local builds and continuous integration for Coq.
-
FCF github.com
Framework for proofs of cryptography.
-
FreeSpec github.com
Framework for modularly verifying programs with effects and effect handlers.
-
Waterproof proof language github.com
Plugin providing a language for writing proof scripts in a style that resembles non-mechanized mathematical proof.
-
Relation Algebra github.com
Modular formalization of algebras with heterogeneous binary relations as models.
-
Finmap github.com
Extension of Mathematical Components with finite maps, sets, and multisets.
-
Functional Algorithms Verified in SSReflect github.com
Purely functional verified implementations of algorithms for searching, sorting, and other fundamental problems.
-
Coq record update github.com
Library which provides a generic way to update Coq record fields.
-
coq-tools github.com
Scripts for manipulating Coq developments.
-
Regular Language Representations github.com
Translations between different definitions of regular languages, including regular expressions and automata.
-
Program Logics github.com
Companion Coq sources for a course on program logics at Collège de France.
-
Graph Theory github.com
Formalized graph theory results.
-
CoqPrime github.com
Library for certifying primality using Pocklington and Elliptic Curve certificates.
-
Waterproof editor github.com
Educational environment for writing mathematical proofs in interactive notebooks.
-
Paramcoq github.com
Plugin to generate parametricity translations of Coq terms.
-
TLC github.com
Non-constructive alternative to Coq's standard library.
- next page of items loading…
