Coq OPAM
Disclaimer
This website shows what can be done with the Coq.io framework.
The official index of Coq packages is at coq.inria.fr/opam/www.
352 packages 1820 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-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-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 of Buchberger's algorithm for computing Gröbner bases in Coq |
| 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-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 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-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-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-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-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 | Proof of Stålmarck's algorithm in Coq |
| 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-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-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 |
| coq-zsearch-trees | Binary Search Trees |