Top 50 Awesome List

coq-community/awesome-coq

Programming Languages  15 days ago  113
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainers=@anton-trunov,@palmskog]
View byDAY/WEEK/README
View on Github

Oct 10th

Resources

Tutorials and Hints

  • Hydras, Ordinals & Co.stars16 - Variations on Kirby and Paris' hydra battles and other entertaining math in Coq, including documentation and exercises.
  • Projects

    Libraries

  • Algebra Tacticsstars16 - Ring and field tactics for Mathematical Components.
  • Projects

    Verified Software

  • Prosa - Definitions and proofs for real-time system schedulability analysis.
  • Oct 5th

    Projects

    Libraries

  • CoLoRstars23 - Library on rewriting theory, lambda-calculus and termination, with sub-libraries on common data structures extending the Coq standard library.
  • Flocq - Formalization of floating-point numbers and computations.
  • Bedrock Bit Vectorsstars25 - Library for reasoning on fixed precision machine words.
  • Projects

    Tools

  • coq-dpdgraphstars66 - Tool for building dependency graphs between Coq objects.
  • Aug 25th

    Projects

    Tools

  • coq-toolsstars30 - Scripts for manipulating Coq developments.
    • find-bug.py - Automatically minimizes source files producing an error, creating small test cases for Coq bugs.
    • absolutize-imports.py - Processes source files to make loading of dependencies robust against shadowing of file names.
    • inline-imports.py - Creates stand-alone source files from developments by inlining the loading of all dependencies.
    • minimize-requires.py - Removes loading of unused dependencies.
    • move-requires.py - Moves all dependency loading statements to the top of source files.
    • move-vernaculars.py - Lifts many vernacular commands and inner lemmas out of proof script blocks.
    • proof-using-helper.py - Modifies source files to include proof annotations for faster parallel proving.
  • Aug 24th

    Resources

    Course Material

  • Proofs and reliable programming using Coq - Introduction to developing and verifying programs with Coq.
  • Aug 21st

    Resources

    Books

  • Modeling and Proving in Computational Type Theorystars16 - Book covering topics in computational logic using Coq, including foundations, canonical case studies, and practical programming.
  • Projects

    Frameworks

  • Hybrid - System for reasoning using higher-order abstract syntax representations of object logics.
  • FreeSpecstars45 - Framework for modularly verifying programs with effects and effect handlers.
  • Projects

    Libraries

  • Mczifystars15 - Library enabling Micromega arithmetic solvers to work when using Mathematical Components number definitions.
  • Projects

    Tools

  • coqdoc - Standard documentation tool that generates LaTeX or HTML files from Coq code.
  • Aug 15th

    Projects

    Plugins

  • Coq-Elpistars66 - Extension framework based on λProlog providing an extensive API to implement commands and tactics.
  • Aug 13th

    Projects

    Tools

  • SerAPIstars100 - Tools and OCaml library for (de)serialization of Coq code to and from JSON and S-expressions.
  • Resources

    Course Material

  • Introduction to Computational Logic - Introduction to basic logic principles, constructive type theory, and interactive theorem proving with Coq.
  • Aug 12th

    Resources

    Tutorials and Hints

  • Coq requirements in Common Criteria evaluations - Guide on how to write readable and reviewable Coq code in high assurance applications.
  • Projects

    Tools

  • Autosubst 2stars7 - Tool that generates Coq code for handling binders in syntax, such as for renaming and substitutions.
  • coq-scriptsstars3 - Scripts for dealing with Coq files, including tabulating proof times.
  • Projects

    Package and Build Management

  • Coq Nix Toolboxstars9 - Nix helper scripts to automate local builds and continuous integration for Coq.
  • Projects

    Frameworks

  • Q*certstars47 - Platform for implementing and verifying query compilers.
  • Projects

    Libraries

  • Bignumsstars19 - Library of arbitrarily large numbers.
  • Projects

    Verified Software

  • RISC-V Specification in Coqstars67 - Definition of the RISC-V processor instruction set architecture and extensions.
  • Vélus - Verified compiler for a Lustre/Scade-like dataflow synchronous language.
  • Aug 10th

    Projects

    Type Theory and Mathematics

  • Goedelstars16 - Constructive proof of the Gödel-Rosser incompleteness theorem.
  • Projects

    Package and Build Management

  • Coq platformstars60 - Curated collection of packages to support Coq use in industry, education, and research.
  • coq-community Templatesstars8 - Templates for generating configuration files for Coq projects.
  • Docker-Coq GitHub Action - GitHub container action that can be used with Docker-Coq or Docker-MathComp.
  • Projects

    Verified Software

  • Ceramiststars113 - Verified hash-based approximate membership structures such as Bloom filters.
  • Resources

    Tutorials and Hints

  • MathComp Tutorial Materialsstars8 - Source code for Mathematical Components tutorials.
  • Projects

    Tools

  • Alectryonstars129 - Collection of tools for writing technical documents that mix Coq code and prose.
  • Dec 6th, 2020

    Projects

    Package and Build Management

  • Nix Coq packages - Collection of Coq-related packages for Nix.
  • Nov 23rd, 2020

    Projects

    User Interfaces

  • VSCoqstars161 - Extension for the Visual Studio Code editor.
  • Projects

    Libraries

  • Simple IOstars20 - Input/output monad with user-definable primitive operations.
  • Projects

    Package and Build Management

  • coq_makefile - Build tool distributed with Coq and based on generating a makefile.
  • Projects

    Tools

  • hs-to-coqstars42 - Converter from Haskell code to equivalent Coq code.
  • Roosterizestars13 - Tool for suggesting lemma names in Coq projects.
  • Oct 20th, 2020

    Projects

    Frameworks

  • FCFstars36 - Framework for proofs of cryptography.
  • Projects

    Tools

  • Ottstars211 - Tool for writing definitions of programming languages and calculi that can be translated to Coq.
  • Projects

    Type Theory and Mathematics

  • Coqtail Mathstars11 - Library of mathematical results ranging from arithmetic to real and complex analysis.
  • Resources

    Blogs

  • PLClub Blog
  • Thomas Letan's blog posts on Coq
  • Sep 10th, 2020

    Projects

    Libraries

  • TLCstars15 - Non-constructive alternative to Coq's standard library.
  • Projects

    Tools

  • coq2htmlstars23 - Alternative HTML documentation generator for Coq.
  • Projects

    Type Theory and Mathematics

  • Completeness and Decidability of Modal Logic Calculistars3 - Soundness, completeness, and decidability for the logics K, K*, CTL, and PDL.
  • CoqPrimestars15 - Library for certifying primality using Pocklington and Elliptic Curve certificates.
  • Finmapstars39 - Extension of Mathematical Components with finite maps, sets, and multisets.
  • Gaiastars10 - Implementation of books from Bourbaki's Elements of Mathematics, including set theory and number theory.
  • Resources

    Community

  • Planet Coq link aggregator
  • Resources

    Books

  • Program Logics for Certified Compilers - Book that explains how to construct program logics using separation logic, accompanied by a formal model in Coq which is applied to the Clight programming language and other examples.
  • Resources

    Course Material

  • Foundations of Separation Logic - Introduction to using separation logic to reason about sequential imperative programs in Coq.
  • Aug 19th, 2020

    Projects

    Type Theory and Mathematics

  • Puiseuxthstars3 - Proof of Puiseux's theorem and computation of roots of polynomials of Puiseux's series.
  • Resources

    Community

  • Official Coq standard library
  • Resources

    Blogs

  • MIT PLV blog posts on Coq
  • May 31st, 2020

    Projects

    Libraries

  • Coq record updatestars30 - Library which provides a generic way to update Coq record fields.
  • Projects

    Package and Build Management

  • Dune - Composable and opinionated build system for Coq and OCaml (former jbuilder).
  • Projects

    Plugins

  • Hierarchy Builderstars51 - Collection of commands for declaring Coq hierarchies based on packed classes.
  • Projects

    Type Theory and Mathematics

  • Graph Theorystars16 - Formalized graph theory results.
  • Resources

    Community

  • Official Coq Zulip chat
  • Mar 20th, 2020

    Projects

    Verified Software

  • Incremental Cycles - Verified OCaml implementation of an algorithm for incremental cycle detection in graphs.
  • Resources

    Community

  • Official Coq manual
  • Feb 26th, 2020

    Projects

    Libraries

  • Monaestars54 - Monadic effects and equational reasoning.
  • Projects

    Package and Build Management

  • Docker-MathCompstars4 - Docker images for many combinations of versions of Coq and the Mathematical Components library.
  • Projects

    Type Theory and Mathematics

  • Infotheostars47 - Formalization of information theory and linear error-correcting codes.
  • Resources

    Books

  • The Mathematical Components book - Book oriented towards mathematically inclined users, focusing on the Mathematical Components library and the SSReflect proof language.
  • Resources

    Tutorials and Hints

  • Coq'Art Exercises and Tutorialsstars48 - Coq code and exercises from the Coq'Art book, including additional tutorials.
  • Feb 24th, 2020

    Projects

    Libraries

  • Formalised Undecidable Problemsstars65 - Library of undecidable problems and reductions between them.
  • Regular Language Representationsstars25 - Translations between different definitions of regular languages, including regular expressions and automata.
  • Projects

    Plugins

  • Ltac2 - Experimental typed tactic language similar to Coq's classic Ltac language.
  • Feb 20th, 2020

    Projects

    Package and Build Management

  • Nix - Package manager for Linux and other Unix systems, supporting atomic upgrades and rollbacks.
  • OPAM - Flexible and Git-friendly package manager for OCaml with multiple compiler support.
  • Projects

    Tools

  • CFML - Tool for proving properties of OCaml programs in separation logic.
  • Feb 7th, 2020

    Projects

    Libraries

  • ALEAstars19 - Library for reasoning on randomized algorithms.
  • Hahnstars24 - Library for reasoning on lists and binary relations.
  • Projects

    Tools

  • Cosettestars549 - Automated solver for reasoning about SQL query equivalences.
  • Resources

    Community

  • Official Coq wiki
  • Official Coq Twitter
  • Coq tag on Stack Overflow
  • Coq tag on Theoretical Computer Science Stack Exchange
  • Resources

    Blogs

  • Coq Exchange: ideas and experiment reports about Coq
  • Guillaume Claret's Coq blog
  • Joachim Breitner's blog posts on Coq
  • Poleiro: a Coq blog by Arthur Azevedo de Amorim
  • Ralf Jung's blog posts on Coq
  • Jan 19th, 2020

    Projects

    Package and Build Management

  • Coq Package Index - OPAM-based collection of Coq packages.
  • Docker-Coqstars26 - Docker images for many versions of Coq.
  • Resources

    Books

  • Coq'Art - The first book dedicated to Coq.
  • Software Foundations - Series of Coq-based textbooks on logic, functional programming, and foundations of programming languages, aimed at being accessible to beginners.
  • Certified Programming with Dependent Types - Textbook about practical engineering with Coq which teaches advanced practical tricks and a very specific style of proof.
  • Formal Reasoning About Programs - Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose.
  • Programs and Proofs - Book that gives a brief and practically-oriented introduction to interactive proofs in Coq which emphasizes the computational nature of inductive reasoning about decidable propositions via a small set of primitives from the SSReflect proof language.
  • Computer Arithmetic and Formal Proofs - Book that describes how to formally specify and verify floating-point algorithms in Coq using the Flocq library.
  • Projects

    Frameworks

  • CoqEALstars54 - Framework to ease change of data representations in proofs.
  • Projects

    Libraries

  • Metalibstars55 - Library for programming language metatheory using locally nameless variable binding representations.
  • Projects

    Tools

  • lngenstars27 - Tool for generating locally nameless Coq definitions and proofs.
  • mCoqstars18 - Mutation analysis tool for Coq projects.
  • Jan 18th, 2020

    Projects

    User Interfaces

  • Proof General - Generic interface for proof assistants based on the extensible, customizable text editor Emacs.
  • Jupyter kernel for Coqstars55 - Coq support for the Jupyter Notebook web environment.
  • Jan 14th, 2020

    Projects

    Type Theory and Mathematics

  • Analysisstars104 - Library for classical real analysis compatible with Mathematical Components.
  • Coquelicot - Formalization of classical real analysis compatible with the standard library and focusing on usability.
  • Jan 13th, 2020

    Projects

    Type Theory and Mathematics

  • Category Theory in Coqstars593 - Axiom-free formalization of category theory.
  • Mathematical Components - Formalization of mathematical theories, focusing in particular on group theory.
  • Resources

    Tutorials and Hints

  • Coq in a Hurry - Introduction to how Coq can be used to define logical concepts and functions and reason about them.
  • CodeWars' Coq kata - Online proving challenges.
  • Lemma Overloadingstars22 - Demonstration of design patterns for programming and proving with canonical structures.
  • Mike Nahas's Coq Tutorial - Basics of using Coq to write formal proofs.
  • Tricks in Coqstars333 - Tips, tricks, and features that are hard to discover.
  • Projects

    Libraries

  • coq-haskellstars141 - Library smoothing the transition to Coq for Haskell users.
  • Projects

    Plugins

  • SMTCoqstars98 - Tool that checks proof witnesses coming from external SAT and SMT solvers.
  • AAC Tacticsstars21 - Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator.
  • Gappa - Tactic for discharging goals about floating-point arithmetic and round-off errors.
  • Mtac2stars45 - Plugin adding typed tactics for backward reasoning.
  • Projects

    Verified Software

  • JSCertstars187 - Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter.
  • Projects

    Tools

  • Menhir - Parser generator that can output Coq code for verified parsers.
  • Resources

    Community

  • Mathematical Components wiki
  • Jan 12th, 2020

    Projects

    Libraries

  • FCSL-PCMstars18 - Formalization of partial commutative monoids as used in verification of pointer-manipulating programs.
  • ExtLibstars106 - Collection of theories and plugins that may be useful in other Coq developments.
  • Paco - Library for parameterized coinduction.
  • Relation Algebrastars30 - Modular formalization of algebras with heterogeneous binary relations as models.
  • Projects

    Plugins

  • Unicoqstars37 - Plugin that replaces the existing unification algorithm with an enhanced one.
  • CoqHammerstars165 - General-purpose automated reasoning hammer tool that combines learning from previous proofs with the translation of problems to automated provers and the reconstruction of found proofs.
  • MetaCoqstars220 - Project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins.
  • Projects

    Type Theory and Mathematics

  • Four Color Theoremstars99 - Formal proof of the Four Color Theorem, a landmark result of graph theory.
  • GeoCoqstars134 - Formalization of geometry based on Tarski's axiom system.
  • Homotopy Type Theorystars1k - Development of homotopy-theoretic ideas.
  • Math Classesstars139 - Abstract interfaces for mathematical structures based on type classes.
  • Odd Order Theoremstars15 - Formal proof of the Odd Order Theorem, a landmark result of finite group theory.
  • UniMathstars716 - Library which aims to formalize a substantial body of mathematics using the univalent point of view.
  • Projects

    Verified Software

  • Fiat-Cryptostars423 - Cryptographic primitive code generation.
  • lambda-rust - Formal model of a Rust core language and type system, a logical relation for the type system, and safety proofs for some Rust libraries.
  • Jan 10th, 2020

    Projects

    Plugins

  • Paramcoqstars36 - Plugin to generate parametricity translations of Coq terms.
  • Equationsstars166 - Function definition package for Coq.
  • QuickChickstars192 - Plugin for randomized property-based testing.
  • Projects

    Type Theory and Mathematics

  • CoRNstars99 - Library of constructive real analysis and algebra.
  • Projects

    Frameworks

  • Fiatstars123 - Mostly automated synthesis of correct-by-construction programs.
  • Iris - Higher-order concurrent separation logic framework.
  • Verdistars507 - Framework for formally verifying distributed systems implementations.
  • VST - Toolchain for verifying C code inside Coq in a higher-order concurrent, impredicative separation logic that is sound w.r.t. the Clight language of the CompCert compiler.
  • Projects

    User Interfaces

  • CoqIDE - Standalone graphical tool for interacting with Coq.
  • Coqtailstars135 - Interface for Coq based on the Vim text editor.
  • Company-Coqstars307 - IDE extensions for Proof General's Coq mode.
  • jsCoqstars415 - Port of Coq to JavaScript, which enables running Coq projects in a browser.
  • Projects

    Libraries

  • Coq-std++ - Extended alternative standard library for Coq.
  • Projects

    Tools

  • CoqOfOCamlstars149 - Tool for generating idiomatic Coq from OCaml code.
  • Projects

    Verified Software

  • CompCert - High-assurance compiler for almost all of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors.
  • Verdi Raftstars151 - Implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework.
  • Resources

    Community

  • Coq subreddit
  • Official Coq website
  • Official Coq Discourse forum
  • Official Coq-Club mailing list
  • Jan 9th, 2020

    Last Checked At: 2021-10-25T03:42:56.945Z
    Previous
    desiderantes/awesome-vala
    Next
    vlang/awesome-v

    About

    Track your favorite github awesome repo, not just star it. trackawesomelist.com provides website, newsletter, RSS for tracking the popular awesome list by daily and weekly.
    Contact us: [email protected]
    Track Awesome List - Track your favorite Github awesome repos, not just star them | Product Hunt

    Subscribe

    Subscribe to our weekly newsletter to receive the awesome updates! We never send spam and you can unsubscribe instantly with one click. Here's past issues.

    Links

    Follow us on TwitterSubscribe us on TelegramSubmit awesome list repoNewsletterDonateSitemap