The OPAM repository for the Coq packages. Activate:

opam repo add coq-released https://coq.inria.fr/opam/released

Go to get started to start using OPAM with Coq.

Name |
Description |

coq-aac-tactics | This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators. |

coq-abp | A verification of the alternating bit protocol expressed in CBS. |

coq-additions | Addition Chains. |

coq-ails | Proof of AILS algorithm. |

coq-algebra | Basics notions of algebra. |

coq-amm11262 | Problem 11262 of The American Mathematical Monthly. |

coq-angles | Formalization of the oriented angles theory. |

coq-area-method | The Chou, Gao and Zhang area method. |

coq-atbr | A tactic for deciding Kleene algebras. |

coq-automata | Beginning of formal language theory. |

coq-axiomatic-abp | Verification of an axiomatisation of the Alternating Bit Protocol. |

coq-bbv | An implementation of bitvectors in Coq. |

coq-bdds | BDD algorithms and proofs in Coq, by reflection. |

coq-bellantonicook | Deep embedding of Bellantoni and Cook's syntactic characterization of polytime functions |

coq-bertrand | Correctness of Knuth's algorithm for prime numbers. |

coq-bignums | Bignums, the Coq library of arbitrary large numbers |

coq-buchberger | Proof of Buchberger's algorithm. |

coq-canon-bdds | Canonicity of Binary Decision Dags. |

coq-cantor | On Ordinal Notations. |

coq-cats-in-zfc | Category theory in ZFC. |

coq-ccs | Equivalence notions on labelled transitions systems. |

coq-cecoa | Implicit-complexity Coq library to prove that some programs are computable in polynomial time |

coq-cfgv | Generic Proofs about Alpha Equality and Substitution. |

coq-cfml | A tool for proving OCaml programs in Separation Logic |

coq-charge-core | A framework of typeclasses for shallow embeddings of intuitionistic |

coq-checker | The Mutilated Checkerboard. |

coq-chinese | A proof of the Chinese Remainder Lemma. |

coq-circuits | Some proofs of hardware (adder, multiplier, memory block instruction). |

coq-classical-realizability | Krivine's classical realizability. |

coq-coalgebras | Coalgebras, bisimulation and lambda-coiteration. |

coq-coinductive-examples | Some simple examples about co-inductive types and co-induction. |

coq-coinductive-reals | Real numbers as coinductive ternary streams. |

coq-color | A library on rewriting theory and termination. |

coq-compcert | The CompCert C compiler. |

coq-concat | Constructive Category Theory. |

coq-concurrency-pluto | A web server written in Coq. |

coq-concurrency-proxy | A proxy to interface concurrent Coq programs with the operating system. |

coq-concurrency-system | Experimental library to write concurrent applications in Coq. |

coq-constructive-geometry | Elements of Constructive Geometry. |

coq-constructors | An example Coq plugin, defining a tactic to get the constructors of an inductive type in a list. |

coq-containers | Containers: a typeclass-based library of finite sets/maps. |

coq-continuations | A toolkit to reason with programs raising exceptions. |

coq-coq-in-coq | A formalisation of the Calculus of Construction. |

coq-coq2html | Generates HTML documentation from Coq source files. Alternative to coqdoc. |

coq-coqeal-refinements | A refinement framework (for algebra). |

coq-coqeal-theory | The theory needed by the refinement framework library. |

coq-coqoban | Coqoban (Sokoban). |

coq-coqprime | Certifying prime numbers in Coq |

coq-coqrel | Binary logical relations library for the Coq proof assistant |

coq-coquelicot | A Coq formalization of real analysis compatible with the standard library. |

coq-corn | The CoRN library. A library for constructive analysis. |

coq-counting | Counting: a Coq plugin for measuring definitions/proofs. |

coq-cours-de-coq | Various examples of Coq proofs. |

coq-ctltctl | Computation Tree Logic for Reactive Systems and Timed Computation Tree Logic for Real Time Systems. |

coq-cunit | Convenience functions for unit testing in Coq. |

coq-cybele | A Coq plugin for simpler proofs by reflection or OCaml certificates. |

coq-dblib | dblib. |

coq-demos | Demos of some Coq tools appeared in version V6.0. |

coq-dep-map | Dependent Maps. |

coq-descente-infinie | The Descente Infinie Tactic. |

coq-dictionaries | Dictionaries (with modules). |

coq-disel | Core framework files for Disel, a separation-style logic for compositional verification of distributed systems |

coq-distributed-reference-counting | A Construction of Distributed Reference Counting. |

coq-domain-theory | Elements of Domain Theory. |

coq-dpdgraph | Compute dependencies between Coq objects (definitions, theorems) |

coq-equations | A function definition package for Coq |

coq-ergo | Ergo: a Coq plugin for reification of term with arbitrary signature. |

coq-error-handlers | Simple and robust error handling functions. |

coq-euclidean-geometry | Basis of the Euclid's plane geometry. |

coq-euler-formula | Hypermaps, Genus Theorem and Euler Formula. |

coq-exact-real-arithmetic | Exact Real Arithmetic. |

coq-exceptions | Pro[gramm,v]ing with continuations:A development in Coq. |

coq-ext-lib | A basic library of basic Coq datatypes, definitions, theorems, and |

coq-extensible-records | Definitional (canonical) extensible records in Coq with string keys and arbitrary (non-dependent) types. |

coq-extructures | Finite data structures with extensional reasoning. |

coq-fairisle | Proof of the Fairisle 4x4 Switch Element. |

coq-fcsl-pcm | Partial Commutative Monoids |

coq-fermat4 | Diophantus' 20th Problem and Fermat's Last Theorem for n = 4. |

coq-finger-tree | Dependent Finger Trees. |

coq-firing-squad | Firing Squad Synchronization Problem. |

coq-float | Library for floating point numbers. |

coq-flocq | A floating-point formalization for the Coq system. |

coq-force-84 | Force the use of Coq 8.4 versions. |

coq-force-85 | Force the use of Coq 8.5 versions. |

coq-founify | Correctness and extraction of the unification algorithm. |

coq-fpmods | A short constructive formalization of finitely presented modules. |

coq-free-groups | Free Groups. |

coq-fsets | Finite Sets overs Ordered Types. |

coq-fssec-model | Formal verification of an extension of a UNIX compatible, secure filesystem. |

coq-function-ninjas | Simple functional combinators. |

coq-functional-algebra | This package provides a Coq formalization of abstract algebra using |

coq-functions-in-zfc | Functions in classical ZFC. |

coq-fundamental-arithmetics | Fundamental theorems of arithmetic. |

coq-gappa | A Coq tactic for discharging goals about floating-point arithmetic and |

coq-gc | Formal Verification of an Incremental Garbage Collector. |

coq-generic-environments | Generic_Environments. |

coq-geocoq | A formalization of foundations of geometry in Coq. |

coq-geometric-algebra | Grassman Cayley and Clifford formalisations |

coq-goedel | The Gödel-Rosser 1st incompleteness theorem. |

coq-graph-basics | a Coq toolkit for graph theory. |

coq-graphs | Satisfiability of inequality constraints and detection of cycles with negative weight in graphs. |

coq-group-theory | Elements of Group Theory. |

coq-groups | An exercise on groups. |

coq-hammer | Automation for Dependent Type Theory |

coq-hardware | Verification and synthesis of hardware linear arithmetic structures. |

coq-hedges | Some properties of hedges used by hedged bisimulation. |

coq-high-school-geometry | Geometry for French high-school. |

coq-higman-cf | A direct constructive proof of Higman's Lemma. |

coq-higman-nw | A program from an A-translated impredicative proof of Higman's Lemma. |

coq-higman-s | Higman's lemma on an unrestricted alphabet. |

coq-historical-examples | Historical examples developed in the (pure) Calculus of Constructions. |

coq-hoare-tut | A Tutorial on Reflecting in Coq the generation of Hoare proof obligations. |

coq-huffman | A correctness proof of Huffman algorithm. |

coq-icharate | Icharate: A logical Toolkit for Multimodal Categorial Grammars. |

coq-idxassoc | Associative Arrays. |

coq-ieee754 | A formalisation of the IEEE754 norm on floating-point arithmetic. |

coq-improper-integrals | Additions to the coquelicot library for handling improper integrals |

coq-int-map | Maps indexed by binary integers : IntMap. |

coq-interval | A Coq tactic for proving bounds on real-valued expressions automatically. |

coq-intuitionistic-nuprl | An Impredicative Model of Nuprl's Constructive Type Theory. |

coq-io | A library for effects in Coq. |

coq-io-evaluate | Generic functions to run effects. |

coq-io-exception | Abstract your errors into exceptions. |

coq-io-hello-world | A Hello World program in Coq. |

coq-io-list | Generic functions on lists with effects. |

coq-io-system | System effects for Coq. |

coq-io-system-ocaml | Extraction to OCaml of system effects. |

coq-ipc | Intuitionistic Propositional Checker. |

coq-iris | This is the Coq development of the Iris Project. |

coq-iterable | Generic definition of iterators. |

coq-izf | Intuitionistic Zermelo-Fraenkel Set Theory in Coq. |

coq-jordan-curve-theorem | Hypermaps, planarity and discrete Jordan curve theorem. |

coq-jprover | A theorem prover for first-order intuitionistic logic. |

coq-jsast | A minimal JavaScript syntax tree carved out of the JsCert project. |

coq-karatsuba | Karatsuba's Multiplication. |

coq-kildall | Application of the Generic kildall's Data Flow Analysis Algorithm to a Type and Shape Static Analyses of Bytecode. |

coq-label | 'label' is a Coq plugin for referring to Propositional hypotheses by their type |

coq-lambda | Residual Theory in Lambda-Calculus. |

coq-lambek | A Coq Toolkit for Lambek Calculus. |

coq-lazy-pcf | Subject Reduction for Lazy-PCF. |

coq-lc | Modules over monads and lambda-calculi. |

coq-legacy-ring | The former implementation of the ring tactic. |

coq-lemma-overloading | Hoare Type Theory libraries showcasing design patterns for programming with canonical structures |

coq-lesniewski-mereology | Knowledge-based Dependently Typed Language (KDTL). |

coq-libvalidsdp | LibValidSDP |

coq-lin-alg | Linear Algebra. |

coq-list-plus | More functions on lists. |

coq-list-string | Strings implemented as lists. |

coq-ltac-iter | Coq plugin to iterate various collections |

coq-ltac2 | A tactic language for Coq. |

coq-ltl | Linear Temporal Logic. |

coq-maple-mode | A Maple Mode for Coq. |

coq-markov | Markov's inequality. |

coq-math-classes | A library of abstract interfaces for mathematical structures in Coq. |

coq-mathcomp-algebra | Mathematical Components Library on Algebra |

coq-mathcomp-bigenough | A small library to do epsilon - N reasonning. |

coq-mathcomp-character | Mathematical Components Library on character theory |

coq-mathcomp-field | Mathematical Components Library on Fields |

coq-mathcomp-fingroup | Mathematical Components Library on finite groups |

coq-mathcomp-finmap | Finite sets, finite maps, finitely supported functions, orders. |

coq-mathcomp-multinomials | A Multinomial Library for the Mathematical Components Library. |

coq-mathcomp-odd-order | The formal proof of the Feit-Thompson theorem. |

coq-mathcomp-solvable | Mathematical Components Library on finite groups (II) |

coq-mathcomp-ssreflect | Small Scale Reflection |

coq-mathcomp-sum-of-two-square | A proof of Fermat's theorem on sum of two squares. It is the proof that uses gaussian integers. This is done in ssreflect. It contains two file : |

coq-maths | Basic mathematics. |

coq-matrices | Ring properties for square matrices. |

coq-menhirlib | A support library for verified Coq parsers produced by Menhir |

coq-min-imports | This script will try to remove unnecessary module imports from Coq |

coq-mini-compiler | Correctness of a tiny compiler for arithmetic expressions. |

coq-minic | Semantics of a subset of the C language. |

coq-miniml | Correctness of the compilation of Mini-ML into the Categorical Abstract Machine. |

coq-mirror-core | A framework for computational reflection. |

coq-mod-red | Efficient Reduction of Large Integers by Small Moduli. |

coq-moment | Parse, manipulate and pretty-print times and dates in Coq. |

coq-msets-extra | Extensions of MSets for Efficient Execution |

coq-mtac | Typed Tactics for Coq 8.5 |

coq-mtac2 | Mtac2: Typed Tactics for Coq |

coq-multiplier | Proof of a multiplier circuit. |

coq-mutual-exclusion | A certification of Peterson's algorithm for managing mutual exclusion. |

coq-nfix | Nfix: a Coq extension for fixpoints on nested inductives. |

coq-of-ocaml | Compile OCaml to Coq. |

coq-opam-website | Generation of a Coq website for OPAM: http://coq.io/opam/ . |

coq-orb-stab | Finite orbit-stabilizer theorem. |

coq-ott | Auxiliary library for Ott, a tool for writing definitions of programming languages and calculi |

coq-otway-rees | Otway-Rees cryptographic protocol. |

coq-paco | Paco: Parameterized Coinduction. |

coq-paradoxes | Paradoxes in Set Theory and Type Theory. |

coq-param-pi | Coding of a typed monadic pi-calculus using parameters for free names. |

coq-paramcoq | Paramcoq |

coq-pautomata | Parameterized automata. |

coq-persistent-union-find | Persistent Union Find. |

coq-pi-agm | Computing thousands or millions of digits of PI with arithmetic-geometric means |

coq-pi-calc | Pi-calculus in Coq. |

coq-pigeonhole-principle | This library provides a stand-alone proof of the Pigeonhole |

coq-plouffe | A Coq formalization of Plouffe formula. |

coq-plugin-utils | Utility functions for implementing Coq plugins, e.g. building natural |

coq-pocklington | Pocklington's criterion. |

coq-poltac | A set of tactics to deal with inequalities in Coq over N, Z and R: |

coq-ppsimpl | ppsimpl is a reflexive tactic for canonising (arithmetic) goals. |

coq-presburger | Presburger's algorithm. |

coq-prfx | Proof Reflection in Coq. |

coq-procrastination | A small library for collecting side conditions and deferring their proof |

coq-projective-geometry | Projective Geometry. |

coq-propcalc | Propositional Calculus. |

coq-pts | A formalisation of Pure Type Systems. |

coq-ptsatr | PTSATR. |

coq-ptsf | Explicit Convertibility Proofs in Pure Type Systems. |

coq-qarith | A Library for Rational Numbers (QArith). |

coq-qarith-stern-brocot | Binary Rational Numbers. |

coq-qcert | Verified compiler for data-centric languages |

coq-quickchick | QuickChick is a random property-based testing library for Coq. |

coq-quicksort-complexity | Proofs of Quicksort's worst- and average-case complexity. |

coq-railroad-crossing | The Railroad Crossing Example. |

coq-ramsey | Ramsey Theory. |

coq-random | Interpretation of random programs. |

coq-rational | A definition of rational numbers. |

coq-recursive-definition | ML-like recursive definitions. |

coq-reflexive-first-order | Reflexive first-order proof interpreter. |

coq-regexp | Regular Expression. |

coq-reglang | Regular Language Representations in the Constructive Type Theory of Coq |

coq-relation-algebra | Relation Algebra and KAT. |

coq-relation-extraction | Functions extraction from inductive relations. |

coq-rem | Rem Theorem in Baire space. |

coq-rsa | Correctness of RSA algorithm. |

coq-ruler-compass-geometry | Ruler and compass geometry axiomatization. |

coq-scev | Scalar evolution is an algebraic theory of recurrences. It has found |

coq-schroeder | The Theorem of Schroeder-Bernstein. |

coq-search-trees | Binary Search Trees. |

coq-semantics | A survey of semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation. |

coq-serapi | Sexp Protocol for machine-based interaction with the Coq Proof Assistant. |

coq-shell | Simplified OPAM shell for Coq |

coq-shuffle | Gilbreath's card trick. |

coq-simple-io | IO monad for Coq |

coq-smc | BDD based symbolic model checker for the modal mu-calculus. |

coq-smt-check | Invoke SMT solvers to check goals. |

coq-square-matrices | From Fast Exponentiation to Square Matrices. |

coq-squiggle-eq | An abstract formalization of variable bindings (both named and de-bruijn), |

coq-ssreflect | The Small Scale Reflection extension. |

coq-stalmarck | Proof of Stalmarck's algorithm. |

coq-stdpp | This project contains an extended "Standard Library" for Coq called coq-std++. |

coq-streams | Specification of Eratosthene Sieve. |

coq-string | Definition of strings in Coq. |

coq-subst | The confluence of Hardin-Lévy lambda-sigma-lift-calcul. |

coq-sudoku | A certified Sudoku solver. |

coq-sum-of-two-square | Numbers equal to the sum of two square numbers. |

coq-switch | A plugin to implement functionality similar to `switch` statement in C |

coq-tait | A normalization proof a la Tait for simply-typed lambda-calculus. |

coq-tarski-geometry | Tarski's geometry. |

coq-template-coq | A quoting and unquoting library for Coq in Coq. |

coq-three-gap | A Proof of the Three Gap Theorem (Steinhaus Conjecture). |

coq-tlc | A general-purpose alternative to Coq's standard library. |

coq-topology | General Topology. |

coq-tortoise-hare-algorithm | Tortoise and the hare algorithm. |

coq-traversable-fincontainer | Traversable Functors are Finitary Containers. |

coq-tree-automata | Tree automatas. |

coq-tree-diameter | Diameter of a binary tree. |

coq-unicoq | An enhanced unification algorithm for Coq. |

coq-unimath-category-theory | Aims to formalize a substantial body of mathematics using the univalent point of view. |

coq-unimath-dedekind | Aims to formalize a substantial body of mathematics using the univalent point of view. |

coq-unimath-foundations | Aims to formalize a substantial body of mathematics using the univalent point of view. |

coq-unimath-ktheory | Aims to formalize a substantial body of mathematics using the univalent point of view. |

coq-unimath-substitution-systems | Aims to formalize a substantial body of mathematics using the univalent point of view. |

coq-unimath-tactics | Aims to formalize a substantial body of mathematics using the univalent point of view. |

coq-universe-comparator | A tool to compare universe levels in Coq. |

coq-vst | Verified Software Toolchain |

coq-weak-up-to | New Up-to Techniques for Weak Bisimulation. |

coq-zchinese | A proof of the Chinese Remainder Lemma. |

coq-zf | An axiomatisation of intuitionistic Zermelo-Fraenkel set theory. |

coq-zfc | An encoding of Zermelo-Fraenkel Set Theory in Coq. |

coq-zorns-lemma | Zorn's Lemma. |

coq-zsearch-trees | Binary Search Trees. |