Pinned Repositories
aac-tactics
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainers=@fakusb,@palmskog]
algebra
Basics notions of algebra
analysis
Mathematical Components compliant Analysis Library
argosy
Proving crash safety for systems with layered recovery
autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
coq-hh
Hugo Herbelin's public Coq branches
cours-preuves-ordinateur
Page du cours preuves assistées par ordinateur 2021
LMFI-HoTT
opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
opam-repository
Main public package repository for OPAM, the source package manager of OCaml.
herbelin's Repositories
herbelin/cours-preuves-ordinateur
Page du cours preuves assistées par ordinateur 2021
herbelin/LMFI-HoTT
herbelin/coq-serapi
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
herbelin/analysis
Mathematical Components compliant Analysis Library
herbelin/bignums
Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library
herbelin/autosubst-ocaml
herbelin/camlp5
Preprocessor / Pretty Printer for OCaml
herbelin/category-theory
An axiom-free formalization of category theory in Coq for personal study and practical work
herbelin/ceps
Coq Enhancement Proposals
herbelin/CompCert
The CompCert formally-verified C compiler
herbelin/coq-elpi
Coq plugin embedding elpi
herbelin/Coq-Equations
A plugin for Coq to add dependent pattern-matching.
herbelin/coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
herbelin/coq-lsp
Visual Studio Code Extension and Language Server Protocol for Coq
herbelin/coq-tactician
A Seamless, Interactive Tactic Learner and Prover for Coq
herbelin/corn
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]
herbelin/fiat-crypto
Cryptographic Primitive Code Generation by Fiat
herbelin/fourcolor
Formal proof of the Four Color Theorem
herbelin/github-coq
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.
herbelin/HoTT
Homotopy type theory
herbelin/jscoq
A port of Coq to Javascript -- Run Coq in your Browser
herbelin/lablgtk
Mirror repository for https://forge.ocamlcore.org/anonscm/git/lablgtk/lablgtk.git
herbelin/math-classes
A library of abstract interfaces for mathematical structures in Coq.
herbelin/math-comp
Mathematical Components
herbelin/Mtac2
herbelin/odd-order
The formal proof of the Odd Order Theorem
herbelin/QuickChick
Randomized Property-Based Testing Plugin for Coq
herbelin/smtcoq
Communication between Coq and SAT/SMT solvers
herbelin/template-coq
Reflection library for Coq
herbelin/vscoq
A Visual Studio Code extension for Coq [maintainers=@maximedenes,@huynhtrankhanh,@thery,@Blaisorblade]