Coq Package Index
coq-otway-rees"" |
coq-metacoq-checker"" |
coq-dpdgraph"and produce graphs" |
coq-ipc"" |
coq-ppsimpl"Ppsimpl is a reflexive tactic for canonising (arithmetic) goals" |
coq-cfml"A tool for proving OCaml programs in Separation Logic" |
coq-huffman"" |
coq-coq-in-coq"A formalisation of the Calculus of Construction" |
coq-axiomatic-abp"" |
coq-high-school-geometry"" |
coq-continuations"" |
coq-railroad-crossing"" |
coq-dictionaries"" |
coq-pi-calc"" |
coq-monae"" |
coq-tait"" |
coq-function-ninjas"Simple functional combinators" |
coq-coqeal-theory"The theory needed by the refinement framework library" |
coq-list-plus"More functions on lists" |
coq-alea"" |
coq-math-classes"A library of abstract interfaces for mathematical structures in Coq" |
coq-ruler-compass-geometry"" |
coq-validsdp"" |
coq-square-matrices"" |
coq-mtac2"Mtac2: Typed Tactics for Coq" |
coq-schroeder"" |
coq-extensible-records"Definitional (canonical) extensible records in Coq with string keys and arbitrary (non-dependent) types" |
coq-containers"" |
coq-rational"" |
coq-iris"Iris is a Higher-Order Concurrent Separation Logic Framework with support for interactive proofs" |
coq-geocoq-pof"This subpackage contains a model of Tarski's axioms." |
coq-founify"" |
coq-circuits"" |
coq-opam-website"Generation of a Coq website for OPAM: http://coq.io/opam/ " |
coq-constructors"An example Coq plugin, defining a tactic to get the constructors of an inductive type in a list" |
coq-regexp"" |
coq-zorns-lemma"This library develops some basic set theory. The main purpose I had in writing it was as support for the Topology library." |
coq-mathcomp-fingroup"" |
coq-paramcoq"" |
coq-tortoise-hare-algorithm"" |
coq-relation-algebra"A modular library about relation algebra, from idempotent semirings to residuated Kleene allegories, including a decision tactic for Kleene algebra with Tests (KAT)." |
coq-procrastination"A small library for collecting side conditions and deferring their proof" |
coq-io-list"Generic functions on lists with effects" |
coq-ott"" |
coq-fundamental-arithmetics"Fundamental theorems of arithmetic" |
coq-ails"" |
coq-unimath-substitution-systems"Aims to formalize a substantial body of mathematics using the univalent point of view" |
coq-quicksort-complexity"" |
coq-group-theory"Group Theory following the book \" |
coq-hierarchy-builder"" |
coq-minic"" |
coq-qcert"" |
coq-idxassoc"" |
coq-pi-agm"" |
coq-unimath-category-theory"Aims to formalize a substantial body of mathematics using the univalent point of view" |
coq-orb-stab"Finite orbit-stabilizer theorem, based on Rahbar Virk's lecture notes. A large portion of the work was a simplified version of the inclusion-exclusion principle. Requires Loic Pottier's Algebra contribution, and Jasper Stein's Linear Algebra contribution." |
coq-coinductive-examples"" |
coq-coqrel"Binary logical relations library for the Coq proof assistant" |
coq-sum-of-two-square"" |
coq-canon-bdds"" |
coq-mod-red"Fast reduction of integers by moduli up to 2^(w-1), where w is a processor's word size." |
coq-menhirlib"A support library for verified Coq parsers produced by Menhir" |
coq-of-ocaml"Compile OCaml to Coq" |
coq-simple-io"" |
coq-quickchick"QuickChick is a random property-based testing library for Coq" |
coq-chapar"" |
coq-coqprime"Certifying prime numbers in Coq" |
coq-area-method"" |
coq-metacoq-safechecker"" |
coq-libvalidsdp"" |
coq-pocklington"" |
coq-hedges"" |
coq-streams"" |
coq-random"" |
coq-io-hello-world"A Hello World program in Coq" |
coq-three-gap"This proof uses the real numbers. It is a classical proof." |
coq-mathcomp-algebra"" |
coq-lemma-overloading"" |
coq-bignums"Provides BigN, BigZ, BigQ that used to be part of Coq standard library < 8.7." |
coq-lens"Generation of lenses for record datatypes" |
coq-search-trees"" |
coq-int-map"" |
coq-nfix"This plugin provides a syntactic extension that allows one to write mutual fixpoints over nested inductives." |
coq-universe-comparator"A tool to compare universe levels in Coq" |
coq-error-handlers"Simple and robust error handling functions" |
coq-coqeal-refinements"A refinement framework (for algebra)" |
coq-libhyps" This library defines a set of tactics to manipulate hypothesis indivually or by group. In particular it allows to apply a tactic on each hypothesis of a goal, or only *new* hypothesis after some tactic. Manipulations include: automatic renaming, decomposition, extracting premisses, but define your own manipulation on (groups of) hypothesis. " |
coq-mathcomp-finmap"" |
coq-equations"A function definition package for Coq" |
coq-typing-flags"A Coq plugin to disable positivity check, guard check and termination check" |
coq-smt-check"Invoke SMT solvers to check goals" |
coq-mathcomp-ssreflect"" |
coq-ccs"" |
coq-cours-de-coq"Various simple examples of Coq proofs" |
coq-mathcomp-field-extra"" |
coq-ctltctl"" |
coq-amm11262"" |
coq-unimath-foundations"Aims to formalize a substantial body of mathematics using the univalent point of view" |
coq-tlc"" |
coq-ltac2"A tactic language for Coq" |
coq-switch"" |
coq-geocoq-elements"This subpackage contains a formalization of Euclid's proofs from Book I of the Elements." |
coq-fssec-model"Formal verification of an extension of a UNIX compatible, secure filesystem" |
coq-tree-diameter"" |
coq-weak-up-to"" |
coq-dblib"The dblib library offers facilities for working with de Bruijn indices." |
coq-semantics"" |
coq-geocoq-coinc"This subpackage contains some tactics to deal with incidence properties." |
coq-concurrency-system"Experimental library to write concurrent applications in Coq" |
coq-legacy-ring"The former implementation of the ring tactic" |
coq-io"A library for effects in Coq" |
coq-checker"The Mutilated Checkerboard" |
coq-counting"This plugin keeps the count of the size of definitions and proofs in the current Coq session." |
coq-geocoq-main"This subpackage contains the main developments from Hilbert's and Tarski's axiom systems." |
coq-gappa"round-off errors using the Gappa prover." |
coq-exact-real-arithmetic"" |
coq-ergo"This library provides a tactic that performs SMT solving (SAT + congruence closure + arithmetic)." |
coq-subst"" |
coq-fsets"" |
coq-paco"Coq library implementing parameterized coinduction" |
coq-cecoa"Implicit-complexity Coq library to prove that some programs are computable in polynomial time" |
coq-hardware"" |
coq-ptsatr"" |
coq-maths"" |
coq-abp"A verification of the alternating bit protocol expressed in CBS" |
coq-projective-geometry"" |
coq-exceptions"Pro[gramm,v]ing with continuations:A development in Coq" |
coq-lin-alg"" |
coq-compcert"The CompCert C compiler (patched for Coq 8.11 compatibility)" |
coq-hammer"Automation for Dependent Type Theory" |
coq-cunit"Convenience functions for unit testing in Coq" |
coq-generic-environments"Generic_Environments is a library which provides an abstract data type of environments, as a functor parameterized by a module defining variables, and a function which builds environments for such variables with any Type of type. Usual operations over environments are defined, along with an extensive set of basic and more advanced properties. Moreover, an implementation using lists satisfying and all the required properties is provided." |
coq-sudoku"" |
coq-poltac"A set of tactics to deal with inequalities in Coq over N, Z and R:" |
coq-domain-theory"" |
coq-io-evaluate"Generic functions to run effects" |
coq-jprover"" |
coq-pts"" |
coq-recursive-definition"" |
coq-mathcomp-character"" |
coq-qarith"" |
coq-chick-blog"A blog engine written and proven in Coq" |
coq-gc"" |
coq-higman-s"This proof is more or less the proof given by Monika Seisenberger in \" |
coq-lambek"" |
coq-multiplier"Proof of a multiplier circuit" |
coq-msets-extra"" |
coq-coinductive-reals"" |
coq-ptsf"" |
coq-graph-basics"" |
coq-string"Strings as list of characters." |
coq-bertrand"" |
coq-io-system"System effects for Coq" |
coq-squiggle-eq"" |
coq-bytestring"" |
coq-matrices"" |
coq-fermat4"" |
coq-min-imports"" |
coq-plouffe"A Coq formalization of Plouffe formula" |
coq-mathcomp-solvable"" |
coq-markov"A proof of Markov's inequality, restricted to probability spaces, based on the Wikipedia proof. Defines Lebesgue integral and associated concepts such as measurability, measure functions, and sigma algebras. Extended real numbers did not need to be defined because we are working in a probability space with measure 1. Nonconstructive; uses classic, Extensionality_Ensembles, axiomatized real numbers from Coq standard library." |
coq-kildall"" |
coq-mathcomp-multinomials"A Multivariate polynomial Library for the Mathematical Components Library" |
coq-reduction-effects"A Coq plugin to add reduction side effects to some Coq reduction strategies" |
coq-rem"A formalisation of Rem Theorem in Baire space" |
coq-pautomata"" |
coq-zf"An axiomatisation of intuitionistic Zermelo-Fraenkel set theory" |
coq-stdpp"" |
coq-plugin-utils"Utility functions for implementing Coq plugins" |
coq-atbr"" |
coq-maple-mode"" |
coq-io-system-ocaml"Coq system effects for extraction to OCaml" |
coq-hoare-tut"" |
coq-mathcomp-field"" |
coq-lazy-pcf"" |
coq-mathcomp-sum-of-two-square"" |
coq-goedel"" |
coq-metacoq"" |
coq-persistent-union-find"" |
coq-mathcomp-real-closed"" |
coq-label"'label' is a Coq plugin for referring to Propositional hypotheses by their type" |
coq-color"A library on rewriting theory and termination" |
coq-zchinese"This is a rewriting of the contribution chinese-lemma using Zarith" |
coq-disel"Core framework files for Disel, a separation-style logic for compositional verification of distributed systems" |
coq-template-coq"" |
coq-metacoq-template"" |
coq-concat"http://logical.inria.fr/~saibi/docCatV6.ps" |
coq-param-pi"" |
coq-coquelicot"A Coq formalization of real analysis compatible with the standard library" |
coq-mini-compiler"" |
coq-tarski-geometry"" |
coq-games"A library for algorithmic game theory in Ssreflect/Coq" |
coq-geocoq-axioms"This subpackage contains the axioms." |
coq-constructive-geometry"" |
coq-fcsl-pcm"" |
coq-infotheo"" |
coq-cybele"A Coq plugin for simpler proofs by reflection or OCaml certificates" |
coq-algebra"Basics notions of algebra" |
coq-intuitionistic-nuprl"" |
coq-cats-in-zfc"" |
coq-antivalence"" |
coq-reglang"" |
coq-flocq-quickchick"Flocq binary_float generators for QuickChick testing framework" |
coq-jordan-curve-theorem"Constructive formalization of the combinatorial hypermaps, characterization of the planarity, genus theorem, Euler formula, ring of faces, discrete Jordan curve theorem" |
coq-euclidean-geometry"" |
coq-lambda"" |
coq-ext-lib"A library of Coq definitions, theorems, and tactics" |
coq-paradoxes"" |
coq-descente-infinie"This is a tactic plugin for coq. The tactic helps to prove inductive lemmas by fixpoint functions. A manual for the tactic can be found on its homepage listed above." |
coq-shuffle"A full axiomatization and proof development of a non-trivial property of binary sequences, inspired from a card trick of N. Gilbreath." |
coq-higman-cf"" |
coq-additions"Addition Chains" |
coq-miniml"" |
coq-historical-examples"" |
coq-coalgebras"This contribution contains a formalisation of coalgebras, bisimulation on coalgebras, weakly final coalgebras, lambda-coiteration definition scheme (including primitive corecursion) and a version of lambda-bisimulation. The formalisation is modular. The implementation of the module types for streams and potentially infinite Peano numbers are provided using the coinductive types." |
coq-distributed-reference-counting"" |
coq-prfx"" |
coq-presburger"" |
coq-geometric-algebra"Grassman Cayley and Clifford formalisations" |
coq-functional-algebra"" |
coq-prosa"" |
coq-dep-map"A rudimentary library for dependent maps that contain their domain in the type." |
coq-metacoq-erasure"" |
coq-topology"" |
coq-angles"" |
coq-buchberger"" |
coq-scev"Proofs and simplification lemmas of an algebraic theory of recurrences" |
coq-cfgv"" |
coq-improper-integrals"" |
coq-tree-automata"" |
coq-fpmods"A short constructive formalization of finitely presented modules" |
coq-ltl"" |
coq-bellantonicook"Deep embedding of Bellantoni and Cook's syntactic characterization of polytime functions" |
coq-hott"The Homotopy Type Theory library" |
coq-moment"Parse, manipulate and pretty-print times and dates in Coq" |
coq-geocoq"A formalization of foundations of geometry in Coq" |
coq-jsast"A minimal JavaScript syntax tree carved out of the JsCert project" |
coq-bdds"" |
coq-smc"" |
coq-ceres"Library for serialization to S-expressions" |
coq-fourcolor"" |
coq-bbv"An implementation of bitvectors in Coq" |
coq-aac-tactics"This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators." |
coq-lc"" |
coq-firing-squad"" |
coq-concurrency-proxy"A proxy to interface concurrent Coq programs with the operating system" |
coq-mathcomp-bigenough"" |
coq-metacoq-pcuic"" |
coq-hammer-tactics"" |
coq-compcert-64"This package installs the 64 bit version of CompCert. For coexistence with the 32 bit version, the files are installed in: %{prefix}%/variants/compcert64/bin (ccomp and clightgen binaries) %{prefix}%/variants/compcert64/lib/compcert (C library) %{lib}%/coq/user-contrib/compcert64 (Coq library) Please note that the coq module path is compcert and not compcert64, so the files cannot be directly Required as compcert64. Instead -Q or -R options must be used to bind the compcert64 folder to the module path compcert. This is more convenient if one development uses both 32 and 64 bit versions. Otherwise all files would have to be duplicated with module paths compcert and compcert64. Please also note that the binary folder is usually not in the path." |
coq-graphs"" |
coq-elpi"" |
coq-rsa"" |
coq-euler-formula"This library formalizes the combinatorial hypermaps and their properties in a constructive way. It gives the proofs of the Genus Theorem and of the Euler Formula for the polyhedra." |
coq-groups"An exercise on groups" |
coq-mathcomp-odd-order"" |
coq-coqoban"" |
coq-coq2html"Generates HTML documentation from Coq source files. Alternative to coqdoc" |
coq-bits"" |
coq-charge-core"A framework for embedded logics" |
coq-io-exception"Abstract your errors into exceptions" |
coq-concurrency-pluto"A web server written in Coq" |
coq-interval"A Coq tactic for proving bounds on real-valued expressions automatically" |
coq-classical-realizability"" |
coq-functions-in-zfc"" |
coq-ltac-iter"Provides tactics for performing various forms of iteration over hypotheses, hint databases, and other collections." |
coq-fairisle"" |
coq-iterable"Generic definition of iterators" |
coq-unimath-ktheory"Aims to formalize a substantial body of mathematics using the univalent point of view" |
coq-reflexive-first-order"" |
coq-mathcomp-analysis"" |
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-demos"" |
coq-float"A library for floating point numbers." |
coq-metacoq-translations"" |
coq-mtac"Typed Tactics for Coq 8.5" |
coq-mutual-exclusion"" |
coq-karatsuba"" |
coq-ceramist"" |
coq-flocq"A floating-point formalization for the Coq system" |
coq-traversable-fincontainer"" |
coq-chinese"This is a rewriting of the contribution chinese-lemma using Zarith" |
coq-icharate"" |
coq-ssreflect"The Small Scale Reflection extension" |
coq-mirror-core"A framework for computational reflection" |
coq-unicoq"An enhanced unification algorithm for Coq" |
coq-coqeal"" |
coq-unimath-tactics"Aims to formalize a substantial body of mathematics using the univalent point of view" |
coq-list-string"Strings implemented as lists" |
coq-disel-examples"Example systems for Disel, a separation-style logic for compositional verification of distributed systems in Coq" |
coq-corn"The CoRN library. A library for constructive analysis" |
coq-finger-tree"" |
coq-qarith-stern-brocot"Developement of rational numbers as finite binary lists and defining field operations on them in two different ways: strict and lazy." |
coq-void"MathComp instances for the empty type (Empty_set)" |
coq-zsearch-trees"" |
coq-zfc"" |
coq-unimath-dedekind"Aims to formalize a substantial body of mathematics using the univalent point of view" |
coq-cantor"" |
coq-higman-nw"" |
coq-propcalc"" |
coq-vst"The software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program. The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context." |
coq-automata"" |
coq-stalmarck"" |
coq-lesniewski-mereology"" |
coq-relation-extraction"" |
coq-extructures"Finite data structures with extensional reasoning" |
coq-printf"Library providing implementation of sprintf for Coq" |
coq-izf"" |
coq-ramsey"" |
coq-ieee754"" |
coq-itree"A Library for Representing Recursive and Impure Programs in Coq" |
Syndicate