362 packages 1891 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 Coq plugin providing 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-addition-chains Exponentiation algorithms following addition chains
coq-additions Addition Chains
coq-ails Proof of AILS algorithm
coq-alea Coq library for reasoning on randomized algorithms
coq-algebra Basics notions of algebra
coq-algorand A verified model of the Algorand consensus protocol in Coq
coq-almost-full Almost-full relations in Coq for proving termination
coq-amm11262 Problem 11262 of The American Mathematical Monthly
coq-angles Formalization of the oriented angles theory
coq-antivalence A Coq plugin to generate type-inequality axioms for inductive definitions
coq-approx-models Rigorous approximations with a posteriori verified operations
coq-area-method The Chou, Gao and Zhang area method
coq-atbr Coq library and tactic for deciding Kleene algebras
coq-automata Beginning of formal language theory
coq-autosubst Coq library for parallel de Bruijn substitutions
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-bits A bit vector library
coq-buchberger Verified implementation in Coq of Buchberger's algorithm for computing Gröbner bases
coq-bytestring A simple string library built around byte instead of Ascii
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-ceramist Coq library for reasoning about probabilistic algorithms
coq-ceres Library for serialization to S-expressions
coq-cfgv Generic Proofs about Alpha Equality and Substitution
coq-cfml A tool for proving OCaml programs in Separation Logic
coq-chapar A framework for verification of causal consistency for distributed key-value stores and their clients in Coq
coq-charge-core A framework of typeclasses for shallow embeddings of intuitionistic
coq-checker The Mutilated Checkerboard
coq-chick-blog A blog engine written and proven in Coq
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-coinduction A library and plugin for doing proofs by (enhanced) coinduction
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-comp-dec-modal Constructive proofs of soundness and completeness for K, K*, CTL, PDL, and PDL with converse
coq-compcert The CompCert C compiler (64 bit)
coq-compcert-32 The CompCert C compiler (32 bit)
coq-compcert-64 The CompCert C compiler (64 bit, using coq-platform supplied version of Flocq)
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 CoqEAL - The Coq Effective Algebra Library
coq-coqeal-refinements A refinement framework (for algebra)
coq-coqeal-theory The theory needed by the CoqEAL refinement framework library
coq-coqffi Tool for generating Coq FFI bindings to OCaml libraries
coq-coqoban Coqoban (Sokoban in Coq)
coq-coqprime Certifying prime numbers in Coq
coq-coqrel Binary logical relations library for the Coq proof assistant
coq-coqtail Library of mathematical theorems and tools proved inside the Coq
coq-coquelicot A Coq formalization of real analysis compatible with the standard library
coq-corn The Coq Constructive Repository at Nijmegen
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-deriving Generic instances of MathComp classes
coq-descente-infinie The Descente Infinie Tactic
coq-dictionaries Dictionaries (with modules)
coq-dijkstra A Verified Implementation of Dijkstra's Algorithm
coq-disel Core framework files for Disel, a separation-style logic for compositional verification of distributed systems in Coq
coq-disel-examples Example systems for Disel, a separation-style logic for compositional verification of distributed systems in Coq
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) and produce graphs
coq-elpi Elpi extension language for Coq
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 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-extructures Finite sets, maps, and other 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 formalization of floating-point arithmetic for the Coq system
coq-flocq-quickchick Flocq binary_float generators for QuickChick testing framework
coq-founify Correctness and extraction of the unification algorithm
coq-fourcolor Mechanization of the Four Color Theorem
coq-fpmods A short constructive formalization of finitely presented modules
coq-free-groups Free Groups
coq-freespec-core A framework for implementing and certifying impure computations in Coq
coq-freespec-exec A framework for implementing and certifying impure computations in Coq
coq-freespec-ffi A framework for implementing and certifying impure computations in Coq
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-gaia Implementation of books from Bourbaki's Elements of Mathematics in Coq
coq-games A library for algorithmic game theory in Ssreflect/Coq
coq-gappa A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover
coq-gc Formal Verification of an Incremental Garbage Collector
coq-generic-environments Generic Environments is a library that provides an abstract data type for environments
coq-geocoq A formalization of foundations of geometry in Coq
coq-geocoq-axioms A formalization of foundations of geometry in Coq
coq-geocoq-coinc A formalization of foundations of geometry in Coq
coq-geocoq-elements A formalization of foundations of geometry in Coq
coq-geocoq-main A formalization of foundations of geometry in Coq
coq-geocoq-pof A formalization of foundations of geometry in Coq
coq-geometric-algebra Grassman Cayley and Clifford formalisations
coq-giskard Verified model of the Giskard consensus protocol in Coq
coq-goedel Coq proof of the Gödel-Rosser 1st incompleteness theorem
coq-graph-basics a Coq toolkit for graph theory
coq-graph-theory Graph theory results in Coq and MathComp
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 General-purpose automated reasoning hammer tool for Coq
coq-hammer-tactics Reconstruction tactics for the hammer for Coq
coq-hardware Verification and synthesis of hardware linear arithmetic structures
coq-hedges Some properties of hedges used by hedged bisimulation
coq-hierarchy-builder High level commands to declare and evolve a hierarchy based on packed classes
coq-hierarchy-builder-shim Shim package for HB
coq-high-school-geometry Geometry in Coq 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-hott The Homotopy Type Theory library
coq-http HTTP in Coq
coq-huffman Coq proof of the correctness of the Huffman coding algorithm
coq-hydra-battles Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq
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-infotheo Discrete probabilities and information theory for Coq
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 Framework with support for interactive proofs
coq-iris-heap-lang HeapLang is the canonical example language for Iris
coq-iris-string-ident Add support for Gallina names in intro patterns to the Iris Proof Mode
coq-itauto 'itauto' is a reflexive SAT solver parameterised by a leaf tactic
coq-iterable Generic definition of iterators
coq-itree A Library for Representing Recursive and Impure Programs in Coq
coq-itree-io Run interaction trees in IO
coq-izf Intuitionistic Zermelo-Fraenkel Set Theory in Coq
coq-jmlcoq Coq definition of the JML specification language and a verified runtime assertion checker for JML
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 Libraries demonstrating design patterns for programming and proving with canonical structures in Coq
coq-lens Generation of lenses for record datatypes
coq-lesniewski-mereology Knowledge-based Dependently Typed Language (KDTL)
coq-libhyps Hypotheses manipulation library
coq-library-undecidability A Coq Library of Undecidability Proofs
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 Access hint databases from tactics
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-abel Abel - Ruffini's theorem
coq-mathcomp-algebra Mathematical Components Library on Algebra
coq-mathcomp-analysis An analysis library for mathematical components
coq-mathcomp-bigenough A small library to do epsilon - N reasonning
coq-mathcomp-character Mathematical Components Library on character theory
coq-mathcomp-dioid Dioid
coq-mathcomp-field Mathematical Components Library on Fields
coq-mathcomp-field-extra Extra Mathematical Components Library on Fields
coq-mathcomp-fingroup Mathematical Components Library on finite groups
coq-mathcomp-finmap Finite sets, finite maps, finitely supported functions
coq-mathcomp-multinomials A Multivariate polynomial Library for the Mathematical Components Library
coq-mathcomp-odd-order The formal proof of the Feit-Thompson theorem
coq-mathcomp-real-closed Mathematical Components Library on real closed fields
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-mathcomp-zify Micromega tactics for Mathematical Components
coq-maths Basic mathematics
coq-matrices Ring properties for square matrices
coq-menhirlib A support library for verified Coq parsers produced by Menhir
coq-metacoq A meta-programming framework for Coq
coq-metacoq-checker Specification of Coq's type theory and reference checker implementation
coq-metacoq-erasure Implementation and verification of an erasure procedure for Coq
coq-metacoq-pcuic A type system equivalent to Coq's and its metatheory
coq-metacoq-safechecker Implementation and verification of safe conversion and typechecking algorithms for Coq
coq-metacoq-template A quoting and unquoting library for Coq in Coq
coq-metacoq-translations Translations built on top of MetaCoq
coq-mi-cho-coq A specification of Michelson in Coq to prove properties about smart contracts in Tezos
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-monae Monads and equational reasoning 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-native Package flag enabling coq's native-compiler flag
coq-nfix Nfix: a Coq extension for fixpoints on nested inductives
coq-of-ocaml Compile a subset of OCaml to Coq
coq-ollibs OL libraries
coq-opam-website Generation of a Coq website for OPAM: http://coq.io/opam/
coq-orb-stab Finite orbit-stabilizer theorem
coq-ordinal Ordinal Numbers in Coq
coq-ott Auxiliary Coq library for Ott, a tool for writing definitions of programming languages and calculi
coq-otway-rees Otway-Rees cryptographic protocol
coq-paco Coq library implementing 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 Plugin for generating parametricity statements to perform refinement proofs
coq-parsec Monadic parser combinator library in Coq
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, e.g. building natural
coq-pocklington Pocklington's criterion in Coq
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-printf Implementation of sprintf for Coq
coq-procrastination A small library for collecting side conditions and deferring their proof
coq-projective-geometry Projective Geometry
coq-propcalc Propositional Calculus
coq-prosa A Foundation for Formally Proven Schedulability Analysis
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 Randomized Property-Based Testing Plugin 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-record-update Generic support for updating record fields in Coq
coq-recursive-definition ML-like recursive definitions
coq-reduction-effects A Coq plugin to add reduction side effects to some Coq reduction strategies
coq-reflexive-first-order Reflexive first-order proof interpreter
coq-regexp Regular Expression
coq-reglang Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp
coq-relation-algebra Relation Algebra and KAT in Coq
coq-relation-extraction Functions extraction from inductive relations
coq-rem Rem Theorem in Baire space
coq-robot Formal Foundations for Modeling Robot Manipulators
coq-rsa Correctness of RSA algorithm
coq-ruler-compass-geometry Ruler and compass geometry axiomatization
coq-scev Proofs and simplification lemmas of an algebraic theory of recurrences
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 Serialization library and protocol for machine 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-smpl Smpl: An Extensible Tactic for Coq
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 Correctness proof of Stålmarck's algorithm in Coq
coq-stalmarck-tactic Coq tactic and verified tool for proving tautologies using Stålmarck's algorithm
coq-stdpp std++ is an extended "Standard Library" for Coq
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 language
coq-tactician Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq
coq-tactician-dummy A dummy implementation of Tactician
coq-tactician-stdlib Recompiles Coq's standard libary with Tactician's instrumentation loaded
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 TLC: A Library for Classical Coq
coq-topology General topology in Coq
coq-tortoise-hare-algorithm Tortoise and the hare algorithm
coq-traversable-fincontainer Traversable Functors are Finitary Containers
coq-tree-automata Tree automatas
coq-tree-calculus A Coq library for tree calculus
coq-tree-diameter Diameter of a binary tree
coq-type-infer A formal verification of algorithm W
coq-typing-flags A Coq plugin to disable positivity check, guard check and termination check
coq-unicoq An enhanced unification algorithm for Coq
coq-unimath Library of Univalent Mathematics
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-validsdp ValidSDP
coq-void MathComp instances for the empty type (Empty_set)
coq-vst Verified Software Toolchain
coq-vst-32 Verified Software Toolchain
coq-vst-64 Verified Software Toolchain
coq-waterproof Waterproof library
coq-weak-up-to New Up-to Techniques for Weak Bisimulation
coq-yalla Yalla library
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 This library develops some basic set theory in Coq
coq-zsearch-trees Binary Search Trees