The Coq Proof Assistant

""

"Constructive formalization of the combinatorial hypermaps, characterization of the planarity, genus theorem, Euler formula, ring of faces, discrete Jordan curve theorem"

"and produce graphs"

""

"Ppsimpl is a reflexive tactic for canonising (arithmetic) goals"

"A tool for proving OCaml programs in Separation Logic"

""

"A formalisation of the Calculus of Construction"

""

""

""

""

""

""

""

""

"Simple functional combinators"

"The theory needed by the refinement framework library"

"More functions on lists"

"A library of abstract interfaces for mathematical structures in Coq"

""

""

"Mtac2: Typed Tactics for Coq"

""

"Definitional (canonical) extensible records in Coq with string keys and arbitrary (non-dependent) types"

"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."

""

"Iris is a Higher-Order Concurrent Separation Logic for reasoning about fine-grained concurrent programs, building logical relations, and more. It features an interactive proof mode for carrying out separation logic proofs in Coq"

""

""

""

"Generation of a Coq website for OPAM: http://coq.io/opam/ "

"An example Coq plugin, defining a tactic to get the constructors of an inductive type in a list"

""

"This library develops some basic set theory. The main purpose I had in writing it was as support for the Topology library."

""

"Paramcoq"

""

"A modular library about relation algebra, from idempotent semirings to residuated Kleene allegories, including a decision tactic for Kleene algebra with Tests (KAT)."

"A small library for collecting side conditions and deferring their proof"

"Generic functions on lists with effects"

"Auxiliary library for Ott, a tool for writing definitions of programming languages and calculi"

"Fundamental theorems of arithmetic"

""

"Aims to formalize a substantial body of mathematics using the univalent point of view"

""

"Group Theory following the book \"

""

""

""

""

"Aims to formalize a substantial body of mathematics using the univalent point of view"

"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."

""

"Binary logical relations library for the Coq proof assistant"

""

""

"Fast reduction of integers by moduli up to 2^(w-1), where w is a processor's word size."

"A support library for verified Coq parsers produced by Menhir"

"Compile OCaml to Coq"

""

"QuickChick is a random property-based testing library for Coq"

""

"Certifying prime numbers in Coq"

""

"LibValidSDP"

""

""

""

""

"A Hello World program in Coq"

"This proof uses the real numbers. It is a classical proof."

""

""

"Provides BigN, BigZ, BigQ that used to be part of Coq standard library < 8.7."

"Algorithms for collecting, searching, inserting and deleting elements in binary search trees on Z"

""

"This plugin provides a syntactic extension that allows one to write mutual fixpoints over nested inductives."

"A tool to compare universe levels in Coq"

""

"A refinement framework (for algebra)"

" 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. "

""

"A function definition package for Coq"

"Invoke SMT solvers to check goals"

""

""

"Various simple examples of Coq proofs"

""

""

""

"Aims to formalize a substantial body of mathematics using the univalent point of view"

""

"A tactic language for Coq"

""

""

"Formal verification of an extension of a UNIX compatible, secure filesystem"

""

""

"The dblib library offers facilities for working with de Bruijn indices."

""

"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."

"Experimental library to write concurrent applications in Coq"

"The former implementation of the ring tactic"

"A library for effects in Coq"

"The Mutilated Checkerboard"

"This plugin keeps the count of the size of definitions and proofs in the current Coq session."

""

"round-off errors using the Gappa prover."

""

"This library provides a tactic that performs SMT solving (SAT + congruence closure + arithmetic)."

""

""

"Coq library implementing parameterized coinduction"

"Implicit-complexity Coq library to prove that some programs are computable in polynomial time"

""

""

""

"A verification of the alternating bit protocol expressed in CBS"

""

"Pro[gramm,v]ing with continuations:A development in Coq"

""

"The CompCert C compiler"

"Automation for Dependent Type Theory"

"Convenience functions for unit testing in Coq"

"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."

""

"A set of tactics to deal with inequalities in Coq over N, Z and R:"

""

"Generic functions to run effects"

""

""

""

""

""

"This is a rewriting of the contribution chinese-lemma using Zarith"

"This proof is more or less the proof given by Monika Seisenberger in \"

""

"Proof of a multiplier circuit"

""

"A Coq tactic for proving bounds on real-valued expressions automatically"

""

""

"Strings as list of characters."

""

"System effects for Coq"

""

""

"Algorithms for collecting, searching, inserting and deleting elements in binary search trees on nat"

""

""

"A Coq formalization of Plouffe formula"

""

"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."

""

"A multivariate polynomial library for the Mathematical Components Library"

"IDE of the Coq formal proof management system"

"A formalisation of Rem Theorem in Baire space"

"An axiomatisation of intuitionistic Zermelo-Fraenkel set theory"

"Utility functions for implementing Coq plugins"

""

""

""

"'label' is a Coq plugin for referring to Propositional hypotheses by their type"

"A library on rewriting theory and termination"

"This is a rewriting of the contribution chinese-lemma using Zarith"

"Core framework files for Disel, a separation-style logic for compositional verification of distributed systems"

""

""

"A Coq formalization of real analysis compatible with the standard library"

""

"Constructive Geometry following Jan von Plato."

""

""

"A Coq plugin for simpler proofs by reflection or OCaml certificates"

""

"Abstract your errors into exceptions"

"Flocq binary_float generators for QuickChick testing framework"

"A library of Coq definitions, theorems, and tactics"

""

"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."

"A full axiomatization and proof development of a non-trivial property of binary sequences, inspired from a card trick of N. Gilbreath."

""

""

""

""

"Coq system effects for extraction to OCaml"

""

""

""

"Grassman Cayley and Clifford formalisations"

""

""

"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."

""

""

""

""

"Basics notions of algebra"

""

""

""

""

""

""

"Proofs and simplification lemmas of an algebraic theory of recurrences"

"http://logical.inria.fr/~saibi/docCatV6.ps"

"Deep embedding of Bellantoni and Cook's syntactic characterization of polytime functions"

""

"Parse, manipulate and pretty-print times and dates in Coq"

""

"A minimal JavaScript syntax tree carved out of the JsCert project"

""

"An implementation of bitvectors in Coq"

"This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators."

""

""

""

"Simple and robust error handling functions"

"A proxy to interface concurrent Coq programs with the operating system"

""

""

"*******************************************************************"

""

""

"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."

""

""

""

"Generates HTML documentation from Coq source files. Alternative to coqdoc"

""

"A framework for embedded logics"

"This library develops some of the basic concepts and results of general topology."

"A web server written in Coq"

""

""

"A short constructive formalization of finitely presented modules"

"A formalization of foundations of geometry in Coq"

""

"Generic definition of iterators"

"Aims to formalize a substantial body of mathematics using the univalent point of view"

""

"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"

""

""

"A library for floating point numbers."

""

"Provides tactics for performing various forms of iteration over hypotheses, hint databases, and other collections."

"An exercise on groups"

"Hoare Type Theory libraries showcasing design patterns for programming with canonical structures"

""

"A floating-point formalization for the Coq system"

"A Coq plugin to add reduction side effects to some Coq reduction strategies"

"A framework for computational reflection"

"Addition Chains"

""

""

"An enhanced unification algorithm for Coq"

""

"Aims to formalize a substantial body of mathematics using the univalent point of view"

"Strings implemented as lists"

"Example systems for Disel, a separation-style logic for compositional verification of distributed systems in Coq"

"The CoRN library. A library for constructive analysis"

""

"Developement of rational numbers as finite binary lists and defining field operations on them in two different ways: strict and lazy."

"Typed Tactics for Coq 8.5"

""

""

"Aims to formalize a substantial body of mathematics using the univalent point of view"

""

""

"The Small Scale Reflection extension"

"A rudimentary library for dependent maps that contain their domain in the type."

"A Library for Representing Recursive and Impure Programs in Coq"

""

""

""

"Finite data structures with extensional reasoning"

"Library providing implementation of sprintf for Coq"

""

""

""

""