# Coq

Tricks in Coq is nice read.

## Links

- Coq Docs
- UniMath - Coq library aims to formalize a substantial body of mathematics using the univalent point of view.
- Mathematical Components - Libraries of formalized mathematics developed using the Coq proof assistant. (GitHub)
- Mathematical Components book (Code)
- Mathematical Components compliant Analysis Library
- QuickChick - Randomized Property-Based Testing Plugin for Coq.
- CoqHammer - Automated Reasoning Hammer Tool for Coq.
- coq-ext-lib - Library of Coq definitions, theorems, and tactics.
- Tricks in Coq - Some tips, tricks, and features in Coq that are hard to discover.
- MetaCoq - Metaprogramming in Coq.
- Convert Haskell source code to Coq source code
- Fiat - Deductive Synthesis of Abstract Data Types in a Proof Assistant.
- Advent of Code 2018 in Coq (HN)
- Equations - Function definition package for Coq.
- Proofs - Selection of formal developments in Coq.
- My hobby: proof engineering (2017)
- Programs and Proofs - Lecture notes for a short course on proving/programming in Coq via SSReflect.
- CoqGym - Learning Environment for Theorem Proving with the Coq proof assistant.
- Kami - DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness.
- PeaCoq - Web-based front-end to the Coq proof assistant.
- Kami - Platform for High-Level Parametric Hardware Specification and its Modular Verification.
- Lean versus Coq: The cultural chasm
- Awesome Coq
- Awesome Coq 2
- coq-of-ocaml - Import OCaml programs to Coq.
- Poleiro - Blog about Coq. (Code)
- Coq'Art - Coq code and exercises from the Coq'Art book.
- Interaction Trees - Representing Recursive and Impure Programs in Coq (2020)
- Formal Reasoning About Programs - In-progress, open-source book by Adam Chlipala simultaneously introducing the Coq proof assistant and techniques for proving correctness of programs. (HN) (Web) (MIT course)
- GeoCoq - Formalization of geometry in Coq.
- Formalizing text editors in Coq (2020) (HN)
- Monadic equational reasoning in Coq
- Coq Enhancement Proposals
- A Study of Clight and its Semantics
- Implementing and Certifying a Web Server in Coq (2020)
- Rewriting in Coq
- FreeSpec - Framework for implementing, certifying, and executing impure computations in Coq.
- How hard can you believe in your logic? (2020)
- CoqPrime - Prime numbers for Coq.
- coqffi - Automatically generates Coq FFI bindings to OCaml libraries.
- Coqtail - Library of mathematical theorems and tools proved inside the Coq proof assistant.
- Interaction Trees - Library for Representing Recursive and Impure Programs in Coq.
- Coq/SSReflect Library for Elliptic Curves
- Alectryon - Library to process Coq snippets embedded in documents, showing goals and messages for each Coq sentence.
- Cerise - Formalisation of a capability machine and principles for reasoning about security properties.
- coq-procrastination - Small Coq library for collecting side conditions and deferring their proof.
- Finite maps - Finite sets, finite maps, multisets and generic sets.
- Alectryon - Collection of tools for writing technical documents that mix Coq code and prose.
- Certified semantics for relational programming workout
- 100 famous theorems proved using Coq (Code)
- codegen plugin for Coq
- Coq record update library - Automatically provides a generic way to update record fields.
- HELIX - Formally verified operator language and rewriting engine for high-performance computing.
- Bits - Formalization of bitset operations in Coq with a corresponding axiomatization and extraction to OCaml native integers.
- Coq formalization of information theory and linear error correcting codes
- jsCoq - Use Coq in Your Browser. (Code)
- Translating My Z3 Tutorial to Coq (2021)
- CoqPL: Verifying a compiler through equational means (2021)
- Formalization of the Calculus of Constructions in Coq
- Coq Library of Undecidability Proofs
- Perennial - Verifying concurrent crash-safe systems.
- Coq Platform - Multi platform setup for Coq, Coq libraries and tools.
- Whitehead and Russell’s Principia rewritten in Coq (Code) (HN)
- Algebra Tactics - Experimental reflexive tactics for ring and field expressions.
- Coq encoding of ZFC and formalization of the textbook Elements of Set Theory
- Free Theorems from Separation Logic Specifications
- Example of Coq Plugin using Dune - Contains a template for writing a Coq plugin using the Dune build system.
- Extensional Structures - Finite sets and maps for Coq with extensional equality.
- SSProve - Foundational framework for modular cryptographic proofs in Coq.
- Eliminating Reflection from Type Theory - Coq formalisation of a translation from (an) extensional type theory to (a) weak type theory.
- Mechanized semantics: the Coq development
- PyCoq - Access Coq from Python.
- Mechanization of a noninterference proof via a type system for a simple imperative language with a small-step semantics in Coq
- Coq library formalizes dependent type theory in the style of Per Martin-Löf
- Hanoi tower in Coq
- W-in-Coq - Coq formalization of Damas-Milner type system and its algorithm W.
- coq-bonsai - Generate a fresh bonsai in your terminal. Written in Coq.
- Coq-Combi - Algebraic Combinatorics in Coq.
- Toy Hoare Logic Formalization for IMP
- Reasoning about the garden of forking paths (2021) (Coq Code)
- Formalization of the basic actuarial mathematics using Coq
- Sniper - Coq plugin that provides a new Coq tactic, snipe, that provides general proof automation.
- SMTCoq - Communication between Coq and SAT/SMT solvers.
- TLC - Library for Classical Coq.
- Formalization of some elementary mathematical theories in Coq
- Stable sort algorithms in Coq
- CertiCoq - Compiler for Gallina, the specification language of the Coq proof assistant.
- Tealeaves - Coq library for proving theorems about syntax abstractly.
- Connectivity Graphs Coq Development
- Hemiola - Coq framework to support structural design and proof of hardware cache-coherence protocols.
- Mczify - Micromega tactics for Mathematical Components.
- Hierarchy Builder - High level commands to declare a hierarchy based on packed classes.
- Coq Package Index - Archive for all Coq related OPAM packages organized in various repositories. (Code)
- Formalizing Dawn in Coq (2021)
- Semantics - Survey of semantics styles in Coq.
- vstyle - Style guide for Coq. (Docs)
- AAC Tactics - Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators.
- Vermillion - LL(1) parser generator verified in Coq.
- Coq Domains
- Proof in Coq of the Gödel-Rosser 1st incompleteness theorem
- Coq-Elpi - Coq plugin embedding Elpi.
- Cheat Sheet for Coq (Code)
- Apery - Formal proof of the irrationality of zeta(3), the Apéry constant.
- Ordinal Numbers in Coq
- Coq development of A Promising Semantics for Relaxed-Memory Concurrency
- Coq Developments for Linear Types
- coq-ext-lib - Collection of theories and plugins that may be useful in other Coq developments.
- Math Classes - Library of abstract interfaces for mathematical structures in Coq.
- C-CoRN - Coq Repository at Nijmegen.
- ch2o - Aims at formalizing novel features of the ISO C11 standard of the C programming language.
- ATBR - Coq library and tactic for deciding Kleene algebras.
- Multinomials - Multivariate polynomial Library for the Mathematical Components Library.
- Efficient Extensional Binary Tries (2021) (Code)
- UniCoq - Enhanced unification algorithm for Coq.
- Phase Semantics - Some Coq formalizations of Linear Logic.
- CertiGraph - Library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.
- Coinduction - Library for doing proofs by (enhanced) coinduction.
- Tactical - Library of Coq proof automation.
- Huffman - Correctness proof of the Huffman coding algorithm in Coq.
- Nuprl's type theory in Coq
- Trakt - Generic goal preprocessing tool for proof automation tactics in Coq.
- metalib - Penn Locally Nameless Metatheory Library.
- Scripts associated to tutorials for mathcomp
- Ergo - Language for Smart Legal Contracts. (Web)
- Bonak - Research project that formalizes semi-cubical types in Coq.
- Imp: Simple Imperative Programs
- Monadic Coq Compiler - Alternative Coq compiler, by extraction to C++17. Written in Haskell.
- Noq - Simple expression transformer that is not Coq. (Dev Stream)
- Falso - Proof of false in Coq. (HN)
- ChickBlog - Blog engine written and proven in Coq.
- Practical Aspects of Monadic Equational Reasoning in Coq (2022)
- Making Weak Memory Models Fair using Coq
- Relation Algebra for Coq
- Mathematics of Rigid Body Transformationss using Coq and MathComp
- Country-Fried Coq: Overly- Formalized Nonstandard Arithmetic (2022)
- Hydras & Co - Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises).
- Mechanized Theory of Event Structures
- Few Coq typeclasses
- Mtac2 - Typed tactic language for Coq. (Paper)
- Autosubst - Library for the Coq proof assistant which provides automation for formalizing syntactic theories with variable binders.
- Argosy - Verifying layered storage systems with recovery refinement.
- Coq Performance Tests - Library of Coq source files testing for performance regressions on Coq.
- xmonad in Coq
- mCoq - Mutation analysis tool for Coq verification projects.
- bedrock2 - Work-in-progress language and compiler for verified low-level programming.
- Useful scripts for dealing with Coq files
- Coq Universe - Aim to provide a composed build of all active Coq developments in existence.
- Formal proof of the Odd Order Theorem in Coq
- Paramcoq - Coq plugin providing commands for generating parametricity statements.
- Gaia - Implementation of books from Bourbaki's Elements of Mathematics in Coq.
- Rupicola - Relation compilation for performance-critical applications.
- Coherence space semantics for linear logic in Coq
- Computability in Constructive Type Theory in Coq
- Deriving - Generic instances for Coq inductive types.
- Coq LSP - Language Server Protocol for Coq.
- CoqBan - Allows you to directly execute your Coq code uploaded to Gist.
- coq-switch
- Coqoban - Coq implementation of Sokoban, the Japanese warehouse keepers' game.
- Lustre compiler in Coq
- Choice Trees - itree-like data-structure to additionally support internal non-determinism.
- Automatik - Library of formalized graph and automata based algorithms.
- LibHyps - Coq library providing tactics to deal with hypothesis.
- CoqEAL - Coq Effective Algebra Library.
- IO - Library for effects in Coq.
- Bidirectional Programming with Monadic Profunctors
- CoLoR - Coq library on rewriting theory and termination.
- Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq (2022)
- Goose - Converts a small subset of Go to Coq.
- simp_lang - Simple programming language that we instantiate Iris with.
- PUMPKIN Pi - Plugin for automatic discovery of and lifting across equivalences between types in Coq.
- SerAPI - Machine-Friendly, Data-Centric Serialization for Coq.
- Natural Number Game Solutions in Coq
- Commutative algebra in Coq/SSReflect
- Ceres - Coq library for serialization to S-expressions.
- Coq HTTP - HTTP specification in Coq, testable and verifiable.
- Parsec - Monadic parser combinator library in Coq.
- Purely functional IO for Coq
- File Synchroniser - File synchroniser specification in Coq.
- Proof of the Church-Rosser theorem using locally nameless representation in Coq
- Clutch - Higher-order probabilistic relational separation logic with support for asynchronous probabilistic couplings.
- mech.v - Coq/Mathematical Components library for mechanism design.
- CoqCP - Formally verified competitive programming code.
- WiSE - Formally verified symbolic bug-finder for imperative programs.