Coq Package Index
coq-otway-rees"" |
coq-intuitionistic-nuprl"" |
coq-bellantonicook"Deep embedding of Bellantoni and Cook's syntactic characterization of polytime functions" |
coq-ssreflect"The Small Scale Reflection extension" |
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-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-square-matrices"" |
coq-mtac2"Mtac2: Typed Tactics for Coq" |
coq-schroeder"" |
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"This is the Coq development of the Iris Project" |
coq-reflexive-first-order"" |
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-presburger"" |
coq-relation-algebra"Relation Algebra and KAT in Coq" |
coq-procrastination"A small library for collecting side conditions and deferring their proof" |
coq-io-list"Generic functions on lists with effects" |
coq-ott"Auxiliary library for Ott, a tool for writing definitions of programming languages and calculi" |
coq-fundamental-arithmetics"http://perso.ens-lyon.fr/sebastien.briais/tools/Arith_080201.tar.gz" |
coq-ails"" |
coq-mirror-core"A framework for computational reflection" |
coq-tarski-geometry"" |
coq-group-theory"Group Theory following the book \" |
coq-minic"" |
coq-qcert"Verified compiler for data-centric languages" |
coq-idxassoc"" |
coq-mathcomp-sum-of-two-square"" |
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-historical-examples"" |
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-mutual-exclusion"" |
coq-functions-in-zfc"" |
coq-simple-io"" |
coq-quickchick"Randomized Property-Based Testing Plugin for Coq" |
coq-coqprime"Certifying prime numbers in Coq" |
coq-area-method"" |
coq-libvalidsdp"LibValidSDP" |
coq-pocklington"" |
coq-hedges"" |
coq-streams"" |
coq-random"" |
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 nat" |
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-mathcomp-finmap"" |
coq-equations"A function definition package for Coq" |
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-topology"This library develops some of the basic concepts and results of general topology." |
coq-ctltctl"" |
coq-amm11262"" |
coq-tlc"A general-purpose alternative to Coq's standard library" |
coq-demos"" |
coq-icharate"" |
coq-automata"" |
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-groups"An exercise on groups" |
coq-mtac"Typed Tactics for Coq 8.5" |
coq-semantics"" |
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-dep-map"A rudimentary library for dependent maps that contain their domain in the type." |
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-template-coq"" |
coq-gappa"A Coq tactic for discharging goals about floating-point arithmetic and 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-moment"Parse, manipulate and pretty-print times and dates in Coq" |
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." |
coq-hammer"Automation for Dependent Type Theory" |
coq-cunit"Convenience functions for unit testing in Coq" |
coq-generic-environments"" |
coq-sudoku"" |
coq-maple-mode"" |
coq-domain-theory"" |
coq-jprover"" |
coq-additions"Addition Chains" |
coq-recursive-definition"" |
coq-mathcomp-character"" |
coq-qarith"" |
coq-gc"" |
coq-higman-s"This proof is more or less the proof given by Monika Seisenberger in \" |
coq-lambek"" |
coq-coq2html"Generates HTML documentation from Coq source files. Alternative to coqdoc" |
coq-msets-extra"" |
coq-interval"A Coq tactic for proving bounds on real-valued expressions automatically" |
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 Z" |
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-zf"An axiomatisation of intuitionistic Zermelo-Fraenkel set theory" |
coq-plugin-utils"numbers, interfacing with Ltac, etc." |
coq-mathcomp-field"" |
coq-lazy-pcf"" |
coq-goedel"" |
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 in Coq" |
coq-firing-squad"" |
coq-param-pi"" |
coq-coquelicot"A Coq formalization of real analysis compatible with the standard library" |
coq-mini-compiler"" |
coq-constructive-geometry"Constructive Geometry following Jan von Plato." |
coq-finger-tree"" |
coq-cybele"A Coq plugin for simpler proofs by reflection or OCaml certificates" |
coq-cats-in-zfc"" |
coq-io-exception"Abstract your errors into exceptions" |
coq-ext-lib"tactics meant to extend the standard library." |
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-prfx"" |
coq-geometric-algebra"Grassman Cayley and Clifford formalisations" |
coq-functional-algebra"" |
coq-angles"" |
coq-buchberger"" |
coq-mathcomp-real-closed"Mathematical Components Library on real closed fields" |
coq-cfgv"" |
coq-improper-integrals"" |
coq-tree-automata"" |
coqide"IDE of the Coq formal proof management system" |
coq-ltl"" |
coq-lemma-overloading"Hoare Type Theory libraries showcasing design patterns for programming with canonical structures" |
coq-scev"Proofs and simplification lemmas of an algebraic theory of recurrences" |
coq-jordan-curve-theorem"" |
coq"Formal proof management system" |
coq-poltac"A set of tactics to deal with inequalities in Coq over N, Z and R:" |
coq-switch"" |
coq-smc"" |
coq-dpdgraph"and produce graphs" |
coq-miniml"" |
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-geocoq"A formalization of foundations of geometry in Coq" |
coq-reglang"" |
coq-jsast"A minimal JavaScript syntax tree carved out of the JsCert project" |
coq-bdds"" |
coq-euclidean-geometry"" |
coq-pigeonhole-principle"" |
coq-pts"" |
coq-graphs"*******************************************************************" |
coq-persistent-union-find"" |
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-pautomata"" |
coq-mathcomp-odd-order"" |
coq-mathcomp-bigenough"" |
coq-of-ocaml"Compile OCaml to Coq" |
coq-coqoban"" |
coq-charge-core"logics. Also includes definitions for separation algebras." |
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-menhirlib"A support library for verified Coq parsers produced by Menhir" |
coq-fcsl-pcm"" |
coq-classical-realizability"" |
coq-mathcomp-analysis"" |
coq-distributed-reference-counting"" |
coq-fairisle"" |
coq-iterable"Generic definition of iterators" |
coq-dblib"" |
coq-multiplier"Proof of a multiplier circuit" |
coq-coinductive-reals"" |
coq-tree-diameter"" |
coq-weak-up-to"" |
coq-float"A library for floating point numbers." |
coq-circuits"" |
coq-stdpp"" |
coq-fpmods"A short constructive formalization of finitely presented modules" |
coq-coqrel"Binary logical relations library for the Coq proof assistant" |
coq-pi-agm"" |
coq-flocq"A floating-point formalization for the Coq system" |
coq-matrices"" |
coq-ltac-iter"Provides tactics for performing various forms of iteration over hypotheses, hint databases, and other collections." |
coq-legacy-ring"The former implementation of the ring tactic" |
coq-concat"http://logical.inria.fr/~saibi/docCatV6.ps" |
coq-quicksort-complexity"" |
coq-unicoq"An enhanced unification algorithm for Coq" |
coq-traversable-fincontainer"" |
coq-atbr"" |
coq-list-string"Strings implemented as lists" |
coq-tortoise-hare-algorithm"" |
coq-corn"The CoRN library. A library for constructive analysis" |
coq-algebra"Basics notions of algebra" |
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-stalmarck"" |
coq-ltac2"A tactic language for Coq" |
coq-zfc"" |
coq-lesniewski-mereology"" |
coq-cantor"" |
coq-higman-nw"" |
coq-lc"" |
coq-ptsatr"" |
coq-propcalc"" |
coq-coqeal"" |
coq-lambda"" |
coq-relation-extraction"" |
coq-extructures"Finite data structures with extensional reasoning" |
coq-ipc"" |
coq-izf"" |
coq-ramsey"" |
coq-ieee754"" |
coq-chinese"OBSOLETE. See rather Zchinese-lemma that uses Z of Zarith." |
Syndicate