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-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"This is a reimplementation of the FSets/FMaps library from the standard library, using typeclasses. See tests files for usage. A new vernacular command is provided by Generate.v and the plugin to automatically generate ordered types for user-defined inductive types." |
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-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-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"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-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-hoare-tut"" |
coq-bignums"Provides BigN, BigZ, BigQ that used to be part of Coq standard library < 8.7." |
coq-search-trees"Algorithms for collecting, searching, inserting and deleting elements in binary search trees on Z" |
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-itree"A Library for Representing Recursive and Impure Programs in Coq" |
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-probhash"" |
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-lc"" |
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-hammer-tactics"" |
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-karatsuba"" |
coq-zsearch-trees"Algorithms for collecting, searching, inserting and deleting elements in binary search trees on nat" |
coq-fermat4"" |
coq-min-imports"" |
coq-plouffe"A Coq formalization of Plouffe formula" |
coq-mathcomp-solvable"" |
coq-ltac-iter"Provides tactics for performing various forms of iteration over hypotheses, hint databases, and other collections." |
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-zf"An axiomatisation of intuitionistic Zermelo-Fraenkel set theory" |
coq-plugin-utils"Utility functions for implementing Coq plugins" |
coq-mathcomp-field"" |
coq-lazy-pcf"" |
coq-goedel"" |
coq-mathcomp-real-closed"" |
coq-stdpp"" |
coq-atbr"" |
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-maple-mode"" |
coq-metacoq-template"" |
coq-io-system-ocaml"Coq system effects for extraction to OCaml" |
coq-param-pi"" |
coq-coquelicot"A Coq formalization of real analysis compatible with the standard library" |
coq-mini-compiler"" |
coq-mathcomp-sum-of-two-square"" |
coq-metacoq"" |
coq-persistent-union-find"" |
coq-constructive-geometry"Constructive Geometry following Jan von Plato." |
coq-metacoq-pcuic"" |
coq-infotheo"" |
coq-cybele"A Coq plugin for simpler proofs by reflection or OCaml certificates" |
coq-template-coq"" |
coq-algebra"Basics notions of algebra" |
coq-traversable-fincontainer"" |
coq-automata"" |
coq-reglang"" |
coq-flocq-quickchick"Flocq binary_float generators for QuickChick testing framework" |
coq-tarski-geometry"" |
coq-scev"Proofs and simplification lemmas of an algebraic theory of recurrences" |
coq-pautomata"" |
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-intuitionistic-nuprl"" |
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-elpi"" |
coq-concat"http://logical.inria.fr/~saibi/docCatV6.ps" |
coq-prfx"" |
coq-reflexive-first-order"" |
coq-geometric-algebra"Grassman Cayley and Clifford formalisations" |
coq-functional-algebra"" |
coq-miniml"" |
coq-historical-examples"" |
coq-printf"Library providing implementation of sprintf for Coq" |
coq-distributed-reference-counting"" |
coq-angles"" |
coq-buchberger"" |
coq-compcert"The CompCert C compiler" |
coq-cfgv"" |
coq-improper-integrals"" |
coq-tree-automata"" |
coq-circuits"" |
coq-ltl"" |
coq-lemma-overloading"Hoare Type Theory libraries showcasing design patterns for programming with canonical structures" |
coq-dep-map"A rudimentary library for dependent maps that contain their domain in the type." |
coq-bellantonicook"Deep embedding of Bellantoni and Cook's syntactic characterization of polytime functions" |
coq-metacoq-erasure"" |
coq-moment"Parse, manipulate and pretty-print times and dates in Coq" |
coq-topology"This library develops some of the basic concepts and results of general topology." |
coq-smc"" |
coq-jsast"A minimal JavaScript syntax tree carved out of the JsCert project" |
coq-bdds"" |
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-fpmods"A short constructive formalization of finitely presented modules" |
coq-geocoq"A formalization of foundations of geometry in Coq" |
coq-presburger"" |
coq-concurrency-proxy"A proxy to interface concurrent Coq programs with the operating system" |
coq-ceres"Library for serialization to S-expressions" |
coq-fourcolor"" |
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-graphs"*******************************************************************" |
coq-groups"An exercise on groups" |
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-pts"" |
coq-mathcomp-odd-order"" |
coq-firing-squad"" |
coq-lambda"" |
coq-coqoban"" |
coq-charge-core"A framework for embedded logics" |
coq-mathcomp-bigenough"" |
coq-coq2html"Generates HTML documentation from Coq source files. Alternative to coqdoc" |
coq-concurrency-pluto"A web server written in Coq" |
coq-classical-realizability"" |
coq-interval"A Coq tactic for proving bounds on real-valued expressions automatically" |
coq-functions-in-zfc"" |
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-additions"Addition Chains" |
coq-mathcomp-analysis"" |
coq-matrices"" |
coq-demos"" |
coq-float"A library for floating point numbers." |
coq-metacoq-translations"" |
coq-fcsl-pcm"" |
coq-mtac"Typed Tactics for Coq 8.5" |
coqide"IDE of the Coq formal proof management system" |
coq-mirror-core"A framework for computational reflection" |
coq-flocq"A floating-point formalization for the Coq system" |
coq-icharate"" |
coq-geocoq-axioms"This subpackage contains the axioms." |
coq-ssreflect"The Small Scale Reflection extension" |
coq-io-exception"Abstract your errors into exceptions" |
coq-mutual-exclusion"" |
coq-unicoq"An enhanced unification algorithm for Coq" |
coq-void"MathComp instances for the empty type (Empty_set)" |
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-cats-in-zfc"" |
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-cantor"" |
coq-lesniewski-mereology"" |
coq-zfc"" |
coq-unimath-dedekind"Aims to formalize a substantial body of mathematics using the univalent point of view" |
coq-chinese"This is a rewriting of the contribution chinese-lemma using Zarith" |
coq-higman-nw"" |
coq-stalmarck"" |
coq-propcalc"" |
coq-finger-tree"" |
coq-coqeal"" |
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-relation-extraction"" |
coq-extructures"Finite data structures with extensional reasoning" |
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-izf"" |
coq-ramsey"" |
coq-ieee754"" |
coq-tree-diameter"" |
Syndicate