Coq
Showing 13 of 121 projects
A Coq library of formally verified mathematical theorems and tools covering arithmetic, real analysis, and complex analysis.
Proof scripts and materials for tutorials on the Mathematical Components library and small-scale reflection in Coq.
Machine-checked constructive proofs of soundness, completeness, and decidability for modal logics K, K*, CTL, and PDL.
A collection of utility scripts for working with Coq proof assistant files, including parsing, analysis, and automation tools.
An Emacs minor mode for selecting and switching between OCaml opam switches via menu or command.
An introductory course on formal verification of floating-point numbers and real numbers using the Coq proof assistant and Flocq library.
A Coq reimplementation of the Natural Number Game, providing interactive theorem proving exercises for learning mathematical proofs.
Coq lessons and exercises introducing the SSReflect proof language and Mathematical Components library.
Docker images providing stable versions of the Mathematical Components library for the Coq proof assistant.
A collection of formalized mathematical theories and algorithms extending the Mathematical Components library for Coq.
A certified solver for the 2x2 Rubik's Cube, formally verified in Coq.
An HTML documentation generator for Rocq source files with proof folding, cross-referencing, and Markdown support.
A modular Coq library providing constructive, axiom-free proofs of Kruskal's Tree Theorem and related results using almost full relations.
Related Tags
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.