Coq
215 items from coq-community/awesome-coq ★396
-
CFML gitlab.inria.fr
Tool for proving properties of OCaml programs in separation logic.
-
Incremental Cycles gitlab.inria.fr
Verified OCaml implementation of an algorithm for incremental cycle detection in graphs.
-
Introduction to the Theory of Computation gitlab.com
Formalization to support an undergraduate course on the theory of computation, including languages and Turing machines.
-
Mathematical Components wiki github.com
-
Docker-Coq GitHub Action github.com
GitHub container action that can be used with Docker-Coq or Docker-MathComp.
-
proof-using-helper.py github.com
Modifies source files to include proof annotations for faster parallel proving.
-
move-vernaculars.py github.com
Lifts many vernacular commands and inner lemmas out of proof script blocks.
-
move-requires.py github.com
Moves all dependency loading statements to the top of source files.
-
minimize-requires.py github.com
Removes loading of unused dependencies.
-
inline-imports.py github.com
Creates stand-alone source files from developments by inlining the loading of all dependencies.
-
find-bug.py github.com
Automatically minimizes source files producing an error, creating small test cases for Coq bugs.
-
absolutize-imports.py github.com
Processes source files to make loading of dependencies robust against shadowing of file names.
-
Official Coq wiki github.com
-
VsCoq Legacy github.com
Backwards-compatible extension for the Visual Studio Code and VSCodium editors using Coq's legacy XML protocol.
-
Dune dune.build
Composable and opinionated build system for OCaml and Coq (former jbuilder).
-
Coq tag on Theoretical Computer Science Stack Exchange cstheory.stackexchange.com
-
Program Logics for Certified Compilers cs.princeton.edu
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.
-
Official Coq Zulip chat coq.zulipchat.com
-
Planet Coq link aggregator coq.pl-a.net
-
Official Coq standard library coq.inria.fr
-
coqdoc coq.inria.fr
Standard documentation tool that generates LaTeX or HTML files from Coq code.
-
Ltac2 coq.inria.fr
Experimental typed tactic language similar to Coq's classic Ltac language.
-
coq_makefile coq.inria.fr
Build tool distributed with Coq and based on generating a makefile.
-
CoqIDE coq.inria.fr
Standalone graphical tool for interacting with Coq.
-
Official Coq manual coq.inria.fr
-
Coq Package Index coq.inria.fr
Collection of Coq packages based on opam.
-
Coq Zulip chat archive coq.gitlab.io
-
Official Coq Discourse forum coq.discourse.group
-
Tactician coq-tactician.github.io
Interactive tool which learns from previously written tactic scripts across all the installed Coq packages and suggests the next tactic to be executed or tries to automate proof synthesis fully.
-
Coq Tactics in Plain English charlesaverill.github.io
Guide to Coq tactics with explanations and examples.
-
Foundations of Separation Logic chargueraud.org
Introduction to using separation logic to reason about sequential imperative programs in Coq.
-
Coq in a Hurry cel.archives-ouvertes.fr
Introduction to how Coq can be used to define logical concepts and functions and reason about them.
-
Lysxia's blog blog.poisson.chat
-
Certified Programming with Dependent Types adam.chlipala.net
Textbook about practical engineering with Coq which teaches advanced practical tricks and a very specific style of proof.
-
Coq-Kruskal github.com
Collection of libraries related to rose trees and Kruskal's tree theorem.
