rhetenor/awesome-awesomeness
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

update lists

Browse Source
This commit is contained in:
Jonas Zeunert
2025-07-18 22:22:32 +02:00
parent 55bed3b4a1
commit 5916c5c074
3078 changed files with 331679 additions and 357255 deletions
Download Patch File Download Diff File Expand all files Collapse all files

95
html/coq.html
View File

@@ -95,8 +95,8 @@ text editor Emacs.</li>
href="https://github.com/ProofGeneral/opam-switch-mode">opam-switch-mode</a>
- IDE extension for Proof General to locally change or reset the opam
switch from a menu or using a command.</li>
<li><a href="https://github.com/ejgallego/jscoq">jsCoq</a> - Port of Coq
to JavaScript, which enables running Coq projects in a browser.</li>
<li><a href="https://github.com/jscoq/jscoq">jsCoq</a> - Port of Coq to
JavaScript, which enables running Coq projects in a browser.</li>
<li><a href="https://github.com/EugeneLoy/coq_jupyter">Jupyter kernel
for Coq</a> - Coq support for the Jupyter Notebook web environment.</li>
<li><a href="https://github.com/coq-community/vscoq">VsCoq</a> -
@@ -127,6 +127,9 @@ rewriting theory, lambda-calculus and termination, with sub-libraries on
common data structures extending the Coq standard library.</li>
<li><a href="https://github.com/jwiegley/coq-haskell">coq-haskell</a> -
Library smoothing the transition to Coq for Haskell users.</li>
<li><a href="https://github.com/DmxLarchey/Coq-Kruskal">Coq-Kruskal</a>
- Collection of libraries related to rose trees and Kruskal’s tree
theorem.</li>
<li><a
href="https://gitlab.inria.fr/coqinterval/interval/">CoqInterval</a> -
Tactics for performing proofs of inequalities on expressions of real
@@ -222,13 +225,11 @@ support.</li>
<li><a href="https://github.com/coq-community/aac-tactics">AAC
Tactics</a> - Tactics for rewriting universally quantified equations,
modulo associativity and commutativity of some operator.</li>
<li><a href="https://github.com/damien-pous/coinduction">Coinduction</a>
- Plugin for doing proofs by enhanced coinduction.</li>
<li><a href="https://github.com/LPCIC/coq-elpi">Coq-Elpi</a> - Extension
framework based on λProlog providing an extensive API to implement
commands and tactics.</li>
<li><a href="https://github.com/impermeable/coq-waterproof">Waterproof
proof language</a> - Plugin providing a language for writing proof
scripts in a style that resembles non-mechanized mathematical
proof.</li>
<li><a href="https://github.com/lukaszcz/coqhammer">CoqHammer</a> -
General-purpose automated reasoning hammer tool that combines learning
from previous proofs with the translation of problems to automated
@@ -265,6 +266,10 @@ across all the installed Coq packages and suggests the next tactic to be
executed or tries to automate proof synthesis fully.</li>
<li><a href="https://github.com/unicoq/unicoq">Unicoq</a> - Plugin that
replaces the existing unification algorithm with an enhanced one.</li>
<li><a href="https://github.com/impermeable/coq-waterproof">Waterproof
proof language</a> - Plugin providing a language for writing proof
scripts in a style that resembles non-mechanized mathematical
proof.</li>
</ul>
<h3 id="puzzles-and-games">Puzzles and Games</h3>
<ul>
@@ -294,7 +299,8 @@ the 2048 sliding tile game.</li>
<li><a href="https://github.com/cpitclaudel/alectryon">Alectryon</a> -
Collection of tools for writing technical documents that mix Coq code
and prose.</li>
<li><a href="https://github.com/uds-psl/autosubst2">Autosubst 2</a> -
<li><a
href="https://github.com/uds-psl/autosubst-ocaml">Autosubst-ocaml</a> -
Tool that generates Coq code for handling binders in syntax, such as for
renaming and substitutions.</li>
<li><a href="https://gitlab.inria.fr/charguer/cfml2">CFML</a> - Tool for
@@ -364,8 +370,8 @@ bindings and libraries for interacting with Coq from inside Python
href="https://github.com/EngineeringSoftware/roosterize">Roosterize</a>
- Tool for suggesting lemma names in Coq projects.</li>
<li><a href="https://github.com/rems-project/sail">Sail</a> - Tool for
specifying instruction set architecture semantics of processors and
generating Coq definitions.</li>
specifying instruction set architecture (ISA) semantics of processors
and generating Coq definitions.</li>
<li><a href="https://github.com/ejgallego/coq-serapi">SerAPI</a> - Tools
and OCaml library for (de)serialization of Coq code to and from JSON and
S-expressions.</li>
@@ -438,6 +444,9 @@ efficient code for the PowerPC, ARM, RISC-V and x86 processors.</li>
<li><a href="https://github.com/certichain/ceramist">Ceramist</a> -
Verified hash-based approximate membership structures such as Bloom
filters.</li>
<li><a href="https://github.com/CertiCoq/certicoq">CertiCoq</a> -
Verified compiler from Gallina, the internal language of Coq, down to
CompCert’s Clight language.</li>
<li><a href="https://github.com/mit-plv/fiat-crypto">Fiat-Crypto</a> -
Cryptographic primitive code generation.</li>
<li><a href="https://github.com/clayrat/fav-ssr">Functional Algorithms
@@ -464,6 +473,9 @@ analysis.</li>
<li><a href="https://github.com/mit-plv/riscv-coq">RISC-V Specification
in Coq</a> - Definition of the RISC-V processor instruction set
architecture and extensions.</li>
<li><a href="https://github.com/pi8027/stablesort">Stable sort
algorithms in Coq</a> - Generic and modular proofs of correctness,
including stability, of mergesort functions.</li>
<li><a href="https://github.com/math-comp/tarjan">Tarjan and
Kosaraju</a> - Verified implementations of algorithms for topological
sorting and finding strongly connected components in finite graphs.</li>
@@ -489,7 +501,7 @@ forum</a></li>
<li><a href="https://sympa.inria.fr/sympa/arc/coq-club">Official
Coq-Club mailing list</a></li>
<li><a href="https://github.com/coq/coq/wiki">Official Coq wiki</a></li>
<li><a href="https://twitter.com/CoqLang">Official Coq Twitter</a></li>
<li><a href="https://x.com/CoqLang">Official Coq X/Twitter</a></li>
<li><a href="https://coq.gitlab.io/zulip-archive/">Coq Zulip chat
archive</a></li>
<li><a href="https://www.reddit.com/r/Coq/">Coq subreddit</a></li>
@@ -503,15 +515,13 @@ href="https://proofassistants.stackexchange.com/questions/tagged/coq">Coq
tag on Proof Assistants Stack Exchange</a></li>
<li><a href="https://zenodo.org/search?q=keywords%3A%22Coq%22">Coq
keyword on Zenodo</a></li>
<li><a href="https://github.com/coq-community/manifesto">coq-community
<li><a href="https://github.com/coq-community/manifesto">Coq-community
package maintenance project</a></li>
<li><a href="https://github.com/math-comp/math-comp/wiki">Mathematical
Components wiki</a></li>
<li><a href="https://github.com/coq-community/coq-100-theorems">100
famous theorems proved using Coq</a></li>
<li><a href="https://coq.pl-a.net">Planet Coq link aggregator</a></li>
<li><a href="https://sherlocoq.sirref.org">Sherlocoq code
search</a></li>
</ul>
<h3 id="blogs">Blogs</h3>
<ul>
@@ -540,7 +550,34 @@ The first book dedicated to Coq.</li>
<li><a href="https://softwarefoundations.cis.upenn.edu">Software
Foundations</a> - Series of Coq-based textbooks on logic, functional
programming, and foundations of programming languages, aimed at being
accessible to beginners.</li>
accessible to beginners.
<ul>
<li><a
href="https://softwarefoundations.cis.upenn.edu/lf-current/index.html">Volume
1: Logical Foundations</a> - Introduction to functional programming,
basic concepts of logic, and computer-assisted theorem proving.</li>
<li><a
href="https://softwarefoundations.cis.upenn.edu/plf-current/index.html">Volume
2: Programming Language Foundations</a> - Introduction to the theory of
programming languages, including operational semantics, Hoare logic, and
static type systems.</li>
<li><a
href="https://softwarefoundations.cis.upenn.edu/vfa-current/index.html">Volume
3: Verified Functional Algorithms</a> - Demonstration of how a variety
of fundamental data structures can be specified and verified.</li>
<li><a
href="https://softwarefoundations.cis.upenn.edu/qc-current/index.html">Volume
4: QuickChick</a> - Introduction to tools for combining randomized
property-based testing with formal specification and proof.</li>
<li><a
href="https://softwarefoundations.cis.upenn.edu/vc-current/index.html">Volume
5: Verifiable C</a> - An extended tutorial on specifying and verifying C
programs using the Verified Software Toolchain.</li>
<li><a
href="https://softwarefoundations.cis.upenn.edu/slf-current/index.html">Volume
6: Separation Logic Foundations</a> - An introduction to separation
logic and how to build program verification tools on top of it.</li>
</ul></li>
<li><a href="http://adam.chlipala.net/cpdt/">Certified Programming with
Dependent Types</a> - Textbook about practical engineering with Coq
which teaches advanced practical tricks and a very specific style of
@@ -560,9 +597,11 @@ 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.</li>
<li><a href="http://iste.co.uk/book.php?id=1238">Computer Arithmetic and
Formal Proofs</a> - Book that describes how to formally specify and
verify floating-point algorithms in Coq using the Flocq library.</li>
<li><a
href="https://www.sciencedirect.com/book/9781785481123/computer-arithmetic-and-formal-proofs">Computer
Arithmetic and Formal Proofs</a> - Book that describes how to formally
specify and verify floating-point algorithms in Coq using the Flocq
library.</li>
<li><a href="https://math-comp.github.io/mcb/">The Mathematical
Components book</a> - Book oriented towards mathematically inclined
users, focusing on the Mathematical Components library and the SSReflect
@@ -579,6 +618,11 @@ theorem.</li>
</ul>
<h3 id="course-material">Course Material</h3>
<ul>
<li><a
href="https://staff.aist.go.jp/reynald.affeldt/documents/karate-coq.pdf">An
Introduction to MathComp-Analysis</a> - Lecture notes on getting started
with the Mathematical Components library and using it for classical
reasoning and real analysis.</li>
<li><a href="https://chargueraud.org/teach/verif/">Foundations of
Separation Logic</a> - Introduction to using separation logic to reason
about sequential imperative programs in Coq.</li>
@@ -602,6 +646,11 @@ language semantics at Collège de France.</li>
Logics</a> - Companion Coq sources for a course on program logics at
Collège de France.</li>
<li><a
href="https://gitlab.science.ru.nl/program-verification/course-2023-2024">Program
verification with types and logic</a> - Lectures and exercise material
for a course in programming language semantics, type systems and program
logics, using Coq, at Radboud University Nijmegen.</li>
<li><a
href="https://team.inria.fr/stamp/proofs-and-reliable-programming-using-coq-2022/">Proofs
and Reliable Programming using Coq</a> - Introduction to developing and
verifying programs with Coq.</li>
@@ -617,6 +666,11 @@ concepts and functions and reason about them.</li>
<li><a href="https://inria.hal.science/hal-04452421">Coq requirements in
Common Criteria evaluations</a> - Guide on how to write readable and
reviewable Coq code in high assurance applications.</li>
<li><a href="https://charlesaverill.github.io/ctpe/">Coq Tactics in
Plain English</a> - Guide to Coq tactics with explanations and
examples.</li>
<li><a href="https://learnxinyminutes.com/docs/coq/">Learn X in Y
minutes where X=Coq</a> - Whirlwind tour of Coq as a language.</li>
<li><a href="https://github.com/coq-community/lemma-overloading">Lemma
Overloading</a> - Demonstration of design patterns for programming and
proving with canonical structures.</li>
@@ -626,6 +680,9 @@ tutorials.</li>
<li><a href="https://mdnahas.github.io/doc/nahas_tutorial.html">Mike
Nahas’s Coq Tutorial</a> - Basics of using Coq to write formal
proofs.</li>
<li><a href="https://github.com/tchajed/coq-tricks">Tricks in Coq</a> -
Tips, tricks, and features that are hard to discover.</li>
<li><a href="https://github.com/coq-community/coq-tricks">Tricks in
Coq</a> - Tips, tricks, and features in Coq that are hard to
discover.</li>
</ul>
<p><a href="https://github.com/coq-community/awesome-coq">coq.md
Github</a></p>