Coq Package Index
coq-otway-rees"" |
coq-intuitionistic-nuprl"" |
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-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-concurrency-pluto"A web server written in Coq" |
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-fpmods"A short constructive formalization of finitely presented modules" |
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-quicksort-complexity"" |
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-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-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-of-ocaml"Compile OCaml to Coq" |
coq-simple-io"" |
coq-fourcolor"" |
coq-chapar"" |
coq-coqprime"Certifying prime numbers in Coq" |
coq-area-method"" |
coq-libvalidsdp"LibValidSDP" |
coq-pocklington"" |
coq-persistent-union-find"" |
coq-streams"" |
coq-random"" |
coq-io-hello-world"A Hello World program in Coq" |
coq-io-system-ocaml"Extraction to OCaml of system effects" |
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-unimath-foundations"Aims to formalize a substantial body of mathematics using the univalent point of view" |
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-dblib"" |
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-concurrency-system"Experimental library to write concurrent applications in Coq" |
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-bdds"" |
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-io-evaluate"Generic functions to run effects" |
coq-jprover"" |
coq-pts"" |
coq-recursive-definition"" |
coq-mathcomp-character"" |
coq-qarith"" |
coq-mathcomp-analysis"" |
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-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-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-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"" |
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-stalmarck"" |
coq-printf"Library providing implementation of sprintf for Coq" |
coq-unimath-tactics"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-distributed-reference-counting"" |
coq-prfx"" |
coq-mathcomp-real-closed"" |
coq-geometric-algebra"Grassman Cayley and Clifford formalisations" |
coq-functional-algebra"" |
coqide"IDE of the Coq formal proof management system" |
coq-lemma-overloading"" |
coq-scev"Proofs and simplification lemmas of an algebraic theory of recurrences" |
coq"Formal proof management system" |
coq-angles"" |
coq-buchberger"" |
coq-poltac"A set of tactics to deal with inequalities in Coq over N, Z and R:" |
coq-cfgv"" |
coq-improper-integrals"" |
coq-tree-automata"" |
coq-switch"" |
coq-ltl"" |
coq-reglang"" |
coq-bellantonicook"Deep embedding of Bellantoni and Cook's syntactic characterization of polytime functions" |
coq-pigeonhole-principle"" |
coq-menhirlib"A support library for verified Coq parsers produced by Menhir" |
coq-jordan-curve-theorem"" |
coq-mathcomp-bigenough"" |
coq-smc"" |
coq-gc"" |
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-bbv"An implementation of bitvectors in Coq." |
coq-aac-tactics"" |
coq-ssreflect"The Small Scale Reflection extension" |
coq-lambda"" |
coq-jsast"A minimal JavaScript syntax tree carved out of the JsCert project" |
coq-abp"A verification of the alternating bit protocol expressed in CBS" |
coq-euclidean-geometry"" |
coq-fcsl-pcm"" |
coq-cantor"" |
coq-graphs"*******************************************************************" |
coq-quickchick"Randomized Property-Based Testing Plugin for Coq" |
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-concurrency-proxy"A proxy to interface concurrent Coq programs with the operating system" |
coq-three-gap"This proof uses the real numbers. It is a classical proof." |
coq-coqoban"" |
coq-charge-core"logics. Also includes definitions for separation algebras." |
coq-additions"Addition Chains" |
coq-coq2html"Generates HTML documentation from Coq source files. Alternative to coqdoc" |
coq-constructors"An example Coq plugin, defining a tactic to get the constructors of an inductive type in a list" |
coq-classical-realizability"" |
coq-chinese"OBSOLETE. See rather Zchinese-lemma that uses Z of Zarith." |
coq-stdpp"" |
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-coqrel"Binary logical relations library for the Coq proof assistant" |
coq-pi-agm"" |
coq-extensible-records"Definitional (canonical) extensible records in Coq with string keys and arbitrary (non-dependent) types" |
coq-coinductive-reals"" |
coq-float"A library for floating point numbers." |
coq-tree-diameter"" |
coq-legacy-ring"" |
coq-circuits"" |
coq-zsearch-trees"Algorithms for collecting, searching, inserting and deleting elements in binary search trees on Z" |
coq-weak-up-to"" |
coq-flocq"A floating-point formalization for the Coq system" |
coq-ptsatr"" |
coq-miniml"" |
coq-ltac-iter"Coq plugin to iterate various collections" |
coq-traversable-fincontainer"" |
coq-tortoise-hare-algorithm"" |
coq-unicoq"An enhanced unification algorithm for Coq" |
coq-tarski-geometry"" |
coq-atbr"" |
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-lesniewski-mereology"" |
coq-qarith-stern-brocot"" |
coq-algebra"Basics notions of algebra" |
coq-functions-in-zfc"" |
coq-zfc"" |
coq-unimath-dedekind"Aims to formalize a substantial body of mathematics using the univalent point of view" |
coq-geocoq"A formalization of foundations of geometry in Coq" |
coq-higman-nw"" |
coq-ltac2"A tactic language for Coq" |
coq-propcalc"" |
coq-hedges"" |
coq-coqeal"" |
coq-mtac"Typed Tactics for Coq 8.5" |
coq-relation-extraction"" |
coq-extructures"Finite data structures with extensional reasoning" |
coq-lc"" |
coq-izf"" |
coq-ramsey"" |
coq-ieee754"" |
coq-concat"http://logical.inria.fr/~saibi/docCatV6.ps" |
Syndicate