Coq
215 items from coq-community/awesome-coq ★396
-
Coq tag on Proof Assistants Stack Exchange proofassistants.stackexchange.com
-
Coq Exchange: ideas and experiment reports about Coq project.inria.fr
-
Poleiro: a Coq blog by Arthur Azevedo de Amorim poleiro.info
-
Paco plv.mpi-sws.org
Library for parameterized coinduction.
-
MIT PLV blog posts on Coq plv.csail.mit.edu
-
Debian Coq packages people.debian.org
Coq-related packages available in the testing distribution of Debian.
-
opam opam.ocaml.org
Flexible and Git-friendly package manager for OCaml and Coq with multiple compiler support.
-
Mike Nahas's Coq Tutorial mdnahas.github.io
Basics of using Coq to write formal proofs.
-
The Mathematical Components book math-comp.github.io
Book oriented towards mathematically inclined users, focusing on the Mathematical Components library and the SSReflect proof language.
-
Learn X in Y minutes where X=Coq learnxinyminutes.com
Whirlwind tour of Coq as a language.
-
Coq'Art labri.fr
The first book dedicated to Coq.
-
Joachim Breitner's blog posts on Coq joachim-breitner.de
-
Iris iris-project.org
Higher-order concurrent separation logic framework.
-
Coq requirements in Common Criteria evaluations inria.hal.science
Guide on how to write readable and reviewable Coq code in high assurance applications.
-
Programs and Proofs ilyasergey.net
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.
-
Gregory Malecha's blog gmalecha.github.io
-
Program verification with types and logic gitlab.science.ru.nl
Lectures and exercise material for a course in programming language semantics, type systems and program logics, using Coq, at Radboud University Nijmegen.
-
Coq-std++ gitlab.mpi-sws.org
Extended alternative standard library for Coq.
-
lambda-rust gitlab.mpi-sws.org
Formal model of a Rust core language and type system, a logical relation for the type system, and safety proofs for some Rust libraries.
-
Prosa gitlab.mpi-sws.org
Definitions and proofs for real-time system schedulability analysis.
-
Gappa gitlab.inria.fr
Tactic for discharging goals about floating-point arithmetic and round-off errors.
-
Flocq gitlab.inria.fr
Formalization of floating-point numbers and computations.
-
Itauto gitlab.inria.fr
SMT-like tactics for combined propositional reasoning about function symbols, constructors, and arithmetic.
-
Coquelicot gitlab.inria.fr
Formalization of classical real analysis compatible with the standard library and focusing on usability.
-
CoqInterval gitlab.inria.fr
Tactics for performing proofs of inequalities on expressions of real numbers.
-
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
- next page of items loading…
