Théo Zimmermann's Projects
org-level github configuration
This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators.
Mathematical Components compliant Analysis Library
A tactic for deciding Kleene algebras
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainers=@anton-trunov,@palmskog]
Formal proof in Coq of Banach-Tarski paradox (in development)
Correctness of Knuth's algorithm for prime numbers
Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library
A (Coq Development Team) bot written in OCaml
Bugzilla bug reports to GitHub Issue Tracker convertor
An axiom-free formalization of category theory in Coq for personal study and practical work
Coq Enhancement Proposals
Limit to one pusher thanks to certified-origin GitHub status check
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
Coq library on rewriting theory and termination
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
Coq plugin embedding elpi
A function definition package for Coq
A conda-smithy repository for coq.
A binder environment relying on Conda to install Coq and the coq_jupyter kernel.
Visual Studio Code Extension and Language Server Protocol for Coq
Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
Preliminary / experimental version of the Coq platform discussed in the coq-dev maling list.
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Statement of theorems proven in Coq