236 packages 340 versions

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 AAC tactics.
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-bdds BDD algorithms and proofs in Coq, by reflection.
coq-bertrand Correctness of Knuth's algorithm for prime 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-cfgv Generic Proofs about Alpha Equality and Substitution.
coq-charge-core A framework for embedded logics.
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-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 Demos of some Coq tools appeared in version V6.0.
coq-descente-infinie The Descente Infinie Tactic.
coq-dictionaries Dictionaries (with modules).
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 plugin for Coq to add dependent pattern-matching.
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 library of Coq definitions, theorems, and tactics.
coq-extensible-records Definitional (canonical) extensible records in Coq with string keys and arbitrary (non-dependent) types.
coq-fairisle Proof of the Fairisle 4x4 Switch Element .
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 This small contribution is a formalization of van der Waerden's proof of the construction of a free group on a set of generators, as the reduced words where a letter is a generator or its formal inverse.
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-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-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-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-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 Iris is a Higher-Order Concurrent Separation Logic for reasoning about fine-grained concurrent programs, building logical relations, and more. It features an interactive proof mode for carrying out separation logic proofs in Coq.
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-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-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-lesniewski-mereology KDTL.
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-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-math-comp Mathematical Components.
coq-mathcomp-algebra Mathematical Components Library on Algebra
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-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-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-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-otway-rees Otway-Rees cryptographic protocol.
coq-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-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-plouffe A Coq formalization of Plouffe formula.
coq-plugin-utils Utility functions for implementing Coq plugins
coq-pocklington Pocklington's criterion.
coq-presburger Presburger's algorithm.
coq-prfx Proof Reflection in Coq.
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-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-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-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.
coq-shell Simplified OPAM shell for Coq
coq-shuffle Gilbreath's card trick.
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 A formalization of Howe's Squiggle equality
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-tait A normalization proof a la Tait for simply-typed lambda-calculus.
coq-tarski-geometry Tarski's geometry
coq-template-coq A quoting library for Coq.
coq-three-gap A Proof of the Three Gap Theorem (Steinhaus Conjecture).
coq-tlc A general-purpose library.
coq-toolbox A series of auxiliary tactics for Coq.
coq-topology General Topology.
coq-tortoise-hare-algorithm Tortoise and the hare algorithm.
coq-traversable-fincontainer A Coq proof that all Traversable functors are isomorphic to 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-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.