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.