coq-otway-rees Otway-Rees cryptographic protocol. A description and a proof of correctness for the Otway-Rees cryptographic protocol, usually used as an example for formalisation of such protocols. author: Dominique Bolignano and Valérie Ménissier-Morain category: Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols keywords: Otway-Rees protocols cryptography versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-intuitionistic-nuprl An Impredicative Model of Nuprl's Constructive Type Theory. http://www.nuprl.org/html/Nuprl2Coq/ This library formalizes Nuprl's Constructive Type Theory (CTT) as of 2015. CTT is an extensional type theory originally inspired by Martin-Lof's extensional type theory, and that has since then been extended with several new types such as: intersection types, union types, image types, partial types, set types, quotient types, partial equivalence relation (per) types, simulation and bisimulation types, an atom type, and the "Base" type. Our formalization includes a definition of Nuprl's computation system, a definition of Howe's computational equivalence relation and a proof that it is a congruence, an impredicative definition of Nuprl's type system using Allen's PER semantics (using Prop's impredicativity, we can formalize Nuprl's infinite hierarchy of universes), definitions of most (but not all) of Nuprl's inference rules and proofs that these rules are valid w.r.t. Allen's PER semantics, and a proof of Nuprl's consistency. In addition to the standard introduction and elimination rules for Nuprl's types, we have also proved several Brouwerian rules. Our computation system also contains: (1) free choice sequences that we used to prove Bar Induction rules; (2) named exceptions and a "fresh" operator to generate fresh names, that we used to prove a continuity rule. More information can be found here: http://www.nuprl.org/html/Nuprl2Coq/ Feel free to send questions to the authors or to nuprl@cs.cornell.edu authors: Vincent Rahli Abhishek Anand Mark Bickford category: Mathematics/Logic/Type theory keywords: Nuprl Computational Type Theory Extensional Type Theory Intuitionistic Type Theory Howe's computational equivalence relation Partial Equivalence Relation (PER) semantics Consistency Continuity Bar Induction versions: 8.6.0 8.5.0 suite: released

coq-dpdgraph Compute dependencies between Coq objects (definitions, theorems) and produce graphs authors: Anne Pacalet Yves Bertot versions: 0.6.4 0.6.3 0.6.2 0.6.1 0.6 0.5.1 0.5 0.4 suite: released

coq-ipc Intuitionistic Propositional Checker. This development treats proof search in intuitionistic propositional logic, a fragment of any constructive type theory. We present new and more efficient decision procedures for intuitionistic propositional logic. They themselves are given by (non-formal) constructive proofs. We take one of them to demonstrate that constructive type theory can be used in practice to develop a real, efficient, but error-free proof searcher. This was done by formally proving the decidability of intuitionistic propositional logic in Coq; the proof searcher was automatically extracted. author: Klaus Weich categories: Mathematics/Logic/Foundations Computer Science/Decision Procedures and Certified Algorithms/Decision procedures Miscellaneous/Extracted Programs/Decision procedures keywords: intuitionistic logic proof search proof-as-programs correct-by-construction program verification program extraction versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-ppsimpl ppsimpl is a reflexive tactic for canonising (arithmetic) goals. author: Frédéric Besson category: Miscellaneous/Coq Extensions keywords: integers arithmetic automation versions: 8.8.0 1.0.0 suite: released

coq-cfml "A tool for proving OCaml programs in Separation Logic" versions: 20181201 20180525 suite: released

coq-huffman A correctness proof of Huffman algorithm. This directory contains the proof of correctness of Huffman algorithm as described in: David A. Huffman, "A Method for the Construction of Minimum-Redundancy Codes," Proc. IRE, pp. 1098-1101, September 1952. author: Laurent Théry categories: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms Miscellaneous/Extracted Programs/Combinatorics keywords: Data Compression Code Huffman Tree versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-coq-in-coq A formalisation of the Calculus of Construction. author: Bruno Barras categories: Mathematics/Logic/Type theory Miscellaneous/Extracted Programs/Type checking unification and normalization keyword: calculus of constructions versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-axiomatic-abp Verification of an axiomatisation of the Alternating Bit Protocol. The Alternating Bit Protocol is expressed in an axiomatized calculi of process. Correctness is proven. author: Jan Friso Groote category: Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols keywords: Alternating Bit Protocol Process Calculi reactive systems versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-high-school-geometry Geometry for French high-school. This library is dedicated to high-shool geometry teaching. The axiomatisation for affine euclidean space is in a non analytic setting. author: Frédérique Guilhot category: Mathematics/Geometry/General keywords: geometry teaching high-school versions: 8.6.0 1.0.0 suite: released

coq-continuations A toolkit to reason with programs raising exceptions. We show a way of developing correct functionnal programs raising exceptions. This is made possible using a Continuation Passing Style translation, see the contribution "exceptions" from P. Casteran at Bordeaux. Things are made easier and more modular using some general definitions. author: Jean-François Monin categories: Computer Science/Semantics and Compilation/Semantics Miscellaneous/Extracted Programs/Combinatorics keywords: exceptions monads continuations cps versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-railroad-crossing The Railroad Crossing Example. This library present the specification and verification of one real time system: the Railroad Crossing Problem, which has been proposed as a benchmark for the comparison of real-time formalisms. We specify the system using timed automatas (timed graphs) with discrete time and we prove invariants, the system safety property and the NonZeno property, using the logics CTL and TCTL. author: Carlos Daniel Luna [http://www.fing.edu.uy/~cluna] category: Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols keywords: CTL TCTL Real Time Systems Timed Automatas Safety Concurrency Properties Invariants NonZeno Discrete Time. versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-dictionaries Dictionaries (with modules). This file contains a specification for dictionaries, and an implementation using binary search trees. Coq's module system, with module types and functors, is heavily used. It can be considered as a certified version of an example proposed by Paulson in Standard ML. A detailed description (in French) can be found in the chapter 11 of The Coq'Art, the book written by Yves Bertot and Pierre Castéran (please follow the link http://coq.inria.fr/doc-eng.html) author: Pierre Castéran categories: Computer Science/Data Types and Data Structures Miscellaneous/Extracted Programs/Data structures keyword: modules functors search-trees versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-pi-calc Pi-calculus in Coq. http://www.dimi.uniud.it/~scagnett/pi-calculus.html This is a HOAS-based encoding of the pi-calculus (as originally conceived by Milner, Parrow and Walker in "A Calculus of Mobile Processes" Parts I-II, Information and Computation n. 100) together with the formal verification of a large part of the metatheory of Strong Late Bisimilarity. author: Ivan Scagnetto category: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keywords: process algebras pi-calculus concurrency formal verification higher order syntax versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-tait A normalization proof a la Tait for simply-typed lambda-calculus. This is a formalization of Berger's TLCA'93 paper, with complete proofs of the axioms and an extraction of a normalization program close to N.B.E. authors: Pierre Letouzey Helmut Schwichtenberg categories: Mathematics/Logic/Type theory Computer Science/Lambda Calculi Miscellaneous/Extracted Programs/Type checking unification and normalization keywords: Normalization Lambda-calculus Extraction Tait proof normalization by evalution type theory versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-function-ninjas Simple functional combinators. author: Guillaume Claret version: 1.0.0 suite: released

coq-coqeal-theory The theory needed by the refinement framework library. version: 0.9.1 suite: released

coq-list-plus More functions on lists. author: Guillaume Claret versions: 1.1.0 1.0.0 suite: released

coq-math-classes A library of abstract interfaces for mathematical structures in Coq. authors: Eelis van der Weegen Bas Spitters Robbert Krebbers versions: 8.8.1 1.0.7 1.0.6 1.0.5 1.0.4 1.0.3 suite: released

coq-ruler-compass-geometry Ruler and compass geometry axiomatization. This library contains an axiomatization of the ruler and compass euclidian geometry. Files A1 to A6 contain the axioms and the basic constructions. The other files build the proof that this axiomatization induces the whole plane geometry except the continuity axiom. For that the proofs of the Hilbert's axioms conclude this work in the files E1 to E5. author: Jean Duprat category: Mathematics/Geometry/General keywords: geometry plane geometry ruler and compass geometry Euclidian geometry Hilbert's axioms versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-square-matrices From Fast Exponentiation to Square Matrices. This development is a formalization of Chris Okasaki's article ``From Fast Exponentiation to Square Matrices: An Adventure in Types'' author: Jean-Christophe Filliâtre category: Mathematics/Algebra keywords: exponentiation vectors matrices polymorphic recursion nested datatypes versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-mtac2 Mtac2: Typed Tactics for Coq authors: Beta Ziliani Jan-Oliver Kaiser Robbert Krebbers Yann Régis-Gianas Derek Dreyer versions: 1.1+8.9 1.1+8.8 1.0.1+8.8 1.0.0+8.7 suite: released

coq-schroeder The Theorem of Schroeder-Bernstein. Fraenkel's proof of Schroeder-Bernstein theorem on decidable sets is formalized in a constructive variant of set theory based on stratified universes (the one defined in the Ensemble library). The informal proof can be found for instance in "Axiomatic Set Theory" from P. Suppes. author: Hugo herbelin category: Mathematics/Logic/Set theory keywords: Schroeder-Bernstein Set Theory versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-extensible-records Definitional (canonical) extensible records in Coq with string keys and arbitrary (non-dependent) types. author: Gregory Malecha versions: 1.2.0 1.1.0 1.0.0 suite: released

coq-containers Containers: a typeclass-based library of finite sets/maps. 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. author: Stéphane Lescuyer category: Computer Science/Data Types and Data Structures keywords: data structures type classes versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-rational A definition of rational numbers. Definition of integers as the usual symetric completion of a semi-group and of rational numbers as the product of integers and strictly positive integers quotiented by the usual relation. This implementation assumes two sets of axioms allowing to define quotient types and subset types. These sets of axioms should be proved coherent by mixing up the deliverable model and the setoid model (both are presented in Martin Hofmann' thesis). author: Samuel Boutin category: Mathematics/Arithmetic and Number Theory/Rational numbers keywords: Integers rational numbers quotient types subset types versions: 8.6.0 8.5.0 suite: released

coq-iris This is the Coq development of the Iris Project. versions: 3.1.0 3.0.0 suite: released

coq-reflexive-first-order Reflexive first-order proof interpreter. This contribution is a package which can be used to interpret firstorder proofs provided by an external theorem prover, using computationnal reflexion. author: Pierre Corbineau category: Miscellaneous/Coq Extensions keywords: computationnal reflection interpretation first-order logic equational reasoning versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-founify Correctness and extraction of the unification algorithm. A notion of terms based on symbols without fixed arities is defined and an extended unification problem is proved solvable on these terms. An algorithm, close from Robinson algorithm, can be extracted from the proof. author: Jocelyne Rouyer categories: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms Miscellaneous/Extracted Programs/Type checking unification and normalization keywords: First-order Unification Robinson versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-circuits Some proofs of hardware (adder, multiplier, memory block instruction). definition and proof of a combinatorial adder, a sequential multiplier, a memory block instruction author: Laurent Arditi category: Computer Science/Architecture keyword: hardware verification versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-opam-website Generation of a Coq website for OPAM: http://coq.io/opam/ . author: Guillaume Claret versions: 1.4.0 1.3.2 1.3.1 1.3.0 1.2.1 1.2.0 1.1.0 1.0.0 suite: released

coq-fpmods A short constructive formalization of finitely presented modules. version: 0.2.0 suite: released

coq-regexp Regular Expression. The Library RegExp is a Coq library for regular expression. The implementation is based on the Janusz Brzozowski's algorithm ("Derivatives of Regular Expressions", Journal of the ACM 1964). The RegExp library satisfies the axioms of Kleene Algebra. The proofs are shown in the library. author: Takashi Miyamoto category: Computer Science/Formal Languages Theory and Automata keywords: Regular Expression Kleene Algebra versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-zorns-lemma Zorn's Lemma. This library develops some basic set theory. The main purpose I had in writing it was as support for the Topology library. author: Daniel Schepler category: Mathematics/Logic/Set theory keywords: set theory cardinals ordinals finite countable quotients well orders Zorn's lemma versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-mathcomp-fingroup "The Mathematical Components library" authors: Jeremy Avigad Andrea Asperti Stephane Le Roux Yves Bertot Laurence Rideau Enrico Tassi Ioana Pasca Georges Gonthier Sidi Ould Biha Cyril Cohen Francois Garillot Alexey Solovyev Russell O'Connor Laurent Théry Assia Mahboubi keywords: finite groups small scale reflection mathematical components odd order theorem versions: 1.7.0 1.6.4 1.6.2 1.6.1 1.6 suite: released

coq-paramcoq "Paramcoq" authors: Chantal Keller (Inria, École polytechnique) Marc Lasson (ÉNS de Lyon) Abhishek Anand Pierre Roux Emilio Jesús Gallego Arias Cyril Cohen Matthieu Sozeau categories: paramcoq Miscellaneous/Coq Extensions keywords: paramcoq parametricity ocaml module versions: 1.1.1+coq8.9 1.1.1+coq8.8 1.1.1+coq8.7 1.1.0 1.0.9 1.0.6 1.0.5 suite: released

coq-presburger Presburger's algorithm. A formalization of Presburger's algorithm as stated in the initial paper by Presburger. author: Laurent Théry categories: Mathematics/Logic/Foundations Mathematics/Arithmetic and Number Theory/Miscellaneous Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keywords: Integers Arithmetic Decision Procedure Presburger versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-relation-algebra "Relation Algebra and KAT in Coq" authors: Damien Pous Christian Doczkal category: Mathematics/Algebra keywords: relation algebra kleene algebra with tests kat allegories residuated structures automata regular expressions matrices versions: 1.7.1 1.7 1.6 1.5 1.4 1.3 suite: released

coq-procrastination A small library for collecting side conditions and deferring their proof author: Armaël Guéneau versions: 1.2 1.1 1.0 suite: released

coq-io-list Generic functions on lists with effects. author: Guillaume Claret versions: 1.1.0 1.0.0 suite: released

coq-ott Auxiliary library for Ott, a tool for writing definitions of programming languages and calculi authors: Peter Sewell Francesco Zappa Nardelli Scott Owens category: Computer Science/Semantics and Compilation/Semantics keyword: abstract syntax versions: 0.28 0.27 0.26 suite: released

coq-fundamental-arithmetics Fundamental theorems of arithmetic. http://perso.ens-lyon.fr/sebastien.briais/tools/Arith_080201.tar.gz author: Sébastien Briais category: Mathematics/Arithmetic and Number Theory/Miscellaneous keywords: arithmetic number theory versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-ails Proof of AILS algorithm. An aircraft trajectory modeling and analysis using the AILS algorithm (Airborne Information for Lateral Spacing) to warn against possible collisions. author: Olivier Desmettre category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keywords: ails aircraft trajectory conflict collision versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-mirror-core A framework for computational reflection. author: Gregory Malecha versions: 1.0.2 1.0.1 1.0.0 suite: released

coq-quicksort-complexity Proofs of Quicksort's worst- and average-case complexity. The development contains: - a set of monads and monad transformers for measuring a (possibly nondeterministic) algorithm's use of designated operations; - monadically expressed deterministic and nondeterministic implementations of Quicksort; - proofs of these implementations' worst- and average case complexity. Most of the development is documented in the TYPES 2008 paper "A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq", available at the homepage. author: Eelis category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keywords: quicksort complexity average-case versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-group-theory Elements of Group Theory. Group Theory following the book "Group Theory" from W.R. Scott. author: Gilles Kahn category: Mathematics/Algebra keyword: Group Theory versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-minic Semantics of a subset of the C language. This contribution defines the denotational semantics of MiniC, a sub-set of the C language. This sub-set is sufficiently large to contain any program generated by lustre2C. The denotation function describing the semantics of a MiniC program actually provides an interpreter for the program. author: Eduardo Giménez and Emmanuel Ledinot category: Computer Science/Semantics and Compilation/Semantics keywords: denotational semantics compilation versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-qcert Verified compiler for data-centric languages authors: Josh Auerbach Martin Hirzel Louis Mandel Avi Shinnar Jerome Simeon versions: 1.2.0 1.1.0 1.0.9 1.0.7 1.0.6 1.0.5 1.0.4 suite: released

coq-idxassoc Associative Arrays. We define the associative array (key -> value associations) datatype as list of couples, providing definitions of standards operations such as adding, deleting. We introduce predicates for membership of a key and of couples. Finally we define a search operator ("find") which returns the value associated with a key or the "none" option (see file Option.v which should be part of this contribution) on failure. Lemmas we prove about these concepts were motivated by our needs at the moment we created this file. We hope they'll suit your needs too but anyway, feel free to communicate any wish or remark. authors: Dominique Quatravaux François-René Ridaux Gérald Macinenti category: Computer Science/Data Types and Data Structures keywords: associative arrays search operator data structures versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-mathcomp-sum-of-two-square A proof of Fermat's theorem on sum of two squares. It is the proof that uses gaussian integers. This is done in ssreflect. It contains two file : gauss_int.v : the definition of gaussian integers fermat2.v : the proof of Fermat's theorem The final statement reads: =================================================== From mathcomp Require Import all_ssreflect. From mathcomp.contrib.sum_of_two_square Require Import gauss_int fermat2. Check sum2stest. sum2stest : forall n : nat, reflect (forall p : nat, prime p -> odd p -> p %| n -> odd (logn p n) -> p %% 4 = 1) (n \is a sum_of_two_square) =================================================== versions: 1.0.1 1.0.0 suite: released

coq-unimath-category-theory Aims to formalize a substantial body of mathematics using the univalent point of view. author: The UniMath Development Team version: 0.1.0 suite: released

coq-orb-stab Finite orbit-stabilizer theorem. 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. author: Robert Kam category: Mathematics/Algebra keywords: orbit stabilizer inclusion-exclusion versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-coinductive-examples Some simple examples about co-inductive types and co-induction. This directory containts some simple examples about the use of co-inductive types in Coq. Directory ARITH is about non-standard arithmetic. Directory STREAMS contains examples about schemes, including an application of the translation method presented in Eduardo Giménez's article ``Codifying guarded definitions with recursive schemes'' (LNCS no. 996). author: Eduardo Giménez category: Miscellaneous/Coq Use Examples keywords: co-inductive types co-induction versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-historical-examples Historical examples developed in the (pure) Calculus of Constructions. This is a collection of historical examples developed in system CoC that implemented Coquand's Calculus of Constructions. Newman.v and Tarski.v originate in version 1.10, Manna.v and Format.v are from version 4.3. Their evolution to the Calculus of Inductive Constructions (up to Coq V6.3) are in MannaCIC.v and FormatCIC.v. (Collection by Hugo Herbelin.) authors: Gérard Huet Christine Paulin category: Miscellaneous/Coq Use Examples keywords: Newman's lemma Tarski's fixpoint theorem line formatting binary-search paradigm square root approximation Calculus of Constructions history of Coq versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-sum-of-two-square Numbers equal to the sum of two square numbers. A proof that a number n can be written as the sum of two square numbers if and only if each prime factor p of n that is equal to 3 modulo 4 has its exponent in the decomposition of n that is even. author: Laurent Thery category: Mathematics/Arithmetic and Number Theory/Number theory keyword: number theory versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-canon-bdds Canonicity of Binary Decision Dags. A proof of unicity and canonicity of Binary Decision Trees and Binary Decision Dags. This contrib contains also a development on finite sets. author: Emmanuel Ledinot categories: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures Miscellaneous/Extracted Programs/Decision procedures keywords: BDD BDT Finite Sets Model-Checking binary decision diagrams versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-mod-red Efficient Reduction of Large Integers by Small Moduli. Fast reduction of integers by moduli up to 2^(w-1), where w is a processor's word size. author: Luc Rutten category: Mathematics/Arithmetic and Number Theory/Miscellaneous keywords: Algorithms Performance Computer Arithmetic Modular Reduction Optimization versions: 8.7.0 8.6.0 8.5.0 suite: released

coq-mutual-exclusion A certification of Peterson's algorithm for managing mutual exclusion. This is a proof of certification of Peterson's algorithm for managing mutual exclusion. The case of two processes is treated in the directory called ``binary'' (see the README file in this directory). The case of n processes will be available soon. author: Eduardo Giménez categories: Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols Miscellaneous/Extracted Programs/Automata and protocols keywords: mutual exclusion concurrency Peterson's algorithm co-inductive types co-induction versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-of-ocaml Compile OCaml to Coq. author: Guillaume Claret versions: 1.2.1 1.1.0 1.0.0 suite: released

coq-simple-io IO monad for Coq This library provides tools to implement IO programs directly in Coq, in a similar style to Haskell. Facilities for formal verification are not included. IO is defined as a parameter with a purely functional interface in Coq, to be extracted to OCaml. Some wrappers for the basic types and functions in the OCaml Pervasives module are provided. Users are free to define their own APIs on top of this IO type. keywords: extraction effects versions: 1.0.0 0.2 0.1 suite: released

coq-quickchick QuickChick is a random property-based testing library for Coq. authors: Leonidas Lampropoulos Zoe Paraskevopoulou Maxime Denes Catalin Hritcu Benjamin Pierce Arthur Azevedo de Amorim Antal Spector-Zabusky Li-Yao Xia Yishuai Li versions: 1.0.2 1.0.1 1.0.0 suite: released

coq-coqprime Certifying prime numbers in Coq author: Laurent Théry versions: 1.0.3 1.0.2 1.0.1 1.0.0 suite: released

coq-area-method The Chou, Gao and Zhang area method. This contribution is the implementation of the Chou, Gao and Zhang's area method decision procedure for euclidean plane geometry. This development contains a partial formalization of the book "Machine Proofs in Geometry, Automated Production of Readable Proofs for Geometry Theorems" by Chou, Gao and Zhang. The examples shown automatically (there are more than 100 examples) includes the Ceva, Desargues, Menelaus, Pascal, Centroïd, Pappus, Gauss line, Euler line, Napoleon theorems. Changelog 2.1 : remove some not needed assumptions in some elimination lemmas (2010) 2.0 : extension implementation to Euclidean geometry (2009-2010) 1.0 : first implementation for affine geometry (2004) author: Julien Narboux keywords: geometry Chou Gao Zhang area method decision procedure automatic theorem proving versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-libvalidsdp "LibValidSDP" authors: Pierre Roux Érik Martin-Dorel categories: libValidSDP Miscellaneous/Coq Extensions keywords: libValidSDP ValidSDP floating-point arithmetic Cholesky decomposition version: 0.5 suite: released

coq-pocklington Pocklington's criterion. Pocklington's criterion for checking primality for large natural numbers. Includes a proof of Fermat's little theorem. authors: Olga Caprotti Martijn Oostdijk category: Mathematics/Arithmetic and Number Theory/Number theory keywords: pocklington number theory prime numbers primality fermat's little theorem versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-persistent-union-find Persistent Union Find. http://www.lri.fr/~filliatr/puf/ Correctness proof of the Ocaml implementation of a persistent union-find data structure. See http://www.lri.fr/~filliatr/puf/ for more details. author: Jean-Christophe Filliâtre category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keywords: program verification union-find data structures Tarjan versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-streams Specification of Eratosthene Sieve. Proof of Eratosthene Sieve formalised using streams encoded as greatest fixpoints. See paper: @InProceedings{LePa94, author = "F. Leclerc and C. Paulin-Mohring", title = "Programming with Streams in {Coq}. A case study : The Sieve of Eratosthenes", editor = "H. Barendregt and T. Nipkow", volume = 806, series = "LNCS", booktitle = "{Types for Proofs and Programs, Types' 93}", year = 1994, publisher = "Springer-Verlag" } author: François Leclerc, Christine Paulin-Mohring category: Mathematics/Arithmetic and Number Theory/Number theory keywords: Streams Eratosthene Sieve prime numbers number theory primality versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-random Interpretation of random programs. This contribution is a modelisation of random programs as measures in Coq. It started in 2004 in the context of the AVERROES project (http://www-verimag.imag.fr/AVERROES/). It is based on comon work with Philippe Audebaud (ENS Lyon). It was last updated in february 2007. It contains the following elements - an axiomatisation of the interval [0,1] and derived properties (files Ubase.v and Uprop.v); - a definition of measures on a type A as functions of type (A->[0,1])->[0,1] enjoying special stability properties (files Monads.v and Probas.v); proofs that these constructions have a monadic structure; - an interpretation of programs of type A as measures, in particular a fixpoint construction; the definition of an axiomatic semantic for deriving judgements such as ``the probability of an expression e to evaluate to a result satisfying property q belongs to an interval [p,q]'' (file Prog.v); - Proof of probabilistic termination of a linear random walk (file Iterflip.v); - Proof of a program implementing a bernoulli distribution (Proba(bernouilli(p)=true)=p) using a coin flip and the derived binomial law (Proba(binomial p n=k)=C(n,k)p^k(1-p)^{n-k}) (file Bernoulli.v); - Proof of estimation of the combination of two random executions (file Choice.v) - Proof of partial termination of parameterized random walk (file Ycart.v) - Definition of a measure on traces from a mesure on transitions steps (file Nelist.v, Transitions.v) The document random.pdf contains a short introduction to the library associated to the Gallina source code of the library. author: Christine Paulin category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keywords: randomized algorithms monads probability versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-io-hello-world A Hello World program in Coq. author: Guillaume Claret versions: 1.1.0 1.0.0 suite: released

coq-io-system-ocaml Extraction to OCaml of system effects. author: Guillaume Claret versions: 2.3.0 2.2.0 2.1.0 2.0.0 suite: released

coq-mathcomp-algebra "The Mathematical Components library" authors: Jeremy Avigad Andrea Asperti Stephane Le Roux Yves Bertot Laurence Rideau Enrico Tassi Ioana Pasca Georges Gonthier Sidi Ould Biha Cyril Cohen Francois Garillot Alexey Solovyev Russell O'Connor Laurent Théry Assia Mahboubi keywords: algebra small scale reflection mathematical components odd order theorem versions: 1.7.0 1.6.4 1.6.2 1.6.1 1.6 suite: released

coq-hoare-tut A Tutorial on Reflecting in Coq the generation of Hoare proof obligations. http://www-verimag.imag.fr/~boulme/HOARE_LOGIC_TUTORIAL/ This work is both an introduction to Hoare logic and a demo illustrating Coq nice features. It formalizes the generation of PO (proof obligations) in a Hoare logic for a very basic imperative programming language. It proves the soundness and the completeness of the PO generation both in partial and total correctness. At last, it examplifies on a very simple example (a GCD computation) how the PO generation can simplify concrete proofs. Coq is indeed able to compute PO on concrete programs: we say here that the generation of proof obligations is reflected in Coq. Technically, the PO generation is here performed through Dijkstra's weakest-precondition calculus. author: Sylvain Boulmé categories: Mathematics/Logic/See also Computer Science/Semantics and Compilation/Semantics keywords: Hoare logic imperative program weakest precondition reflection versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-bignums Bignums, the Coq library of arbitrary large numbers Provides BigN, BigZ, BigQ that used to be part of Coq standard library < 8.7. authors: Laurent Théry Benjamin Grégoire Arnaud Spiwack Evgeny Makarov Pierre Letouzey categories: Miscellaneous/Coq Extensions Mathematics/Arithmetic and Number Theory/Number theory Mathematics/Arithmetic and Number Theory/Rational numbers keywords: integer numbers rational numbers arithmetic arbitrary-precision versions: 8.9.0 8.8.0 8.7.0 8.6.0 suite: released

coq-search-trees Binary Search Trees. Algorithms for collecting, searching, inserting and deleting elements in binary search trees on nat author: Pierre Castéran categories: Computer Science/Data Types and Data Structures Miscellaneous/Extracted Programs/Data structures keyword: binary search trees versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-int-map Maps indexed by binary integers : IntMap. This library contains a data structure for finite sets implemented by an efficient structure of map (trees indexed by binary integers). It was initially developed by Jean Goubault. This user contribution used to be part of Coq Standard Library. It is now considered to be obsolete and subsumed by the new FSets/FMap library. IntMap can be now seen as a particular implementation of FMapInterface, see file FMapIntMap. author: Jean Goubault category: Computer Science/Data Types and Data Structures keywords: finite sets maps binary integers efficient data structures data structures versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-nfix Nfix: a Coq extension for fixpoints on nested inductives. This plugin provides a syntactic extension that allows one to write mutual fixpoints over nested inductives. author: Stéphane Lescuyer category: Miscellaneous/Coq Extensions keyword: mutual fixpoint functions versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-universe-comparator A tool to compare universe levels in Coq. author: Amin Timany versions: 1.1.0 1.0.1 suite: released

coq-error-handlers Simple and robust error handling functions. author: Guillaume Claret versions: 1.2.0 1.1.1 1.1.0 1.0.0 suite: released

coq-coqeal-refinements A refinement framework (for algebra). version: 0.9.1 suite: released

coq-mathcomp-finmap Finite sets, finite maps, finitely supported functions, orders. This library is an extension of mathematical component in order to support finite sets and finite maps on choicetypes (rather that finite types). This includes support for functions with finite support and multisets. The library also contains a generic order and set libary, which will be used to subsume notations for finite sets, eventually. author: Cyril Cohen keywords: finmap finset multiset order versions: 1.1.0 1.0.0 suite: released

coq-equations A function definition package for Coq Equations is a function definition plugin for Coq, that allows the definition of functions by dependent pattern-matching and well-founded, mutual or nested structural recursion and compiles them into core terms. It automatically derives the clauses equations, the graph of the function and its associated elimination principle. authors: Matthieu Sozeau Cyprien Mangin versions: 1.2~beta+8.9 1.2~beta+8.8 1.1+8.8 1.0+8.8 1.0+8.7 1.0 1.0~beta2+8.7 1.0~beta2 1.0~beta 0.9~beta2 suite: released

coq-smt-check Invoke SMT solvers to check goals. versions: 2.0.0 1.0.0 suite: released

coq-mathcomp-ssreflect "The Mathematical Components library" authors: Jeremy Avigad Andrea Asperti Stephane Le Roux Yves Bertot Laurence Rideau Enrico Tassi Ioana Pasca Georges Gonthier Sidi Ould Biha Cyril Cohen Francois Garillot Alexey Solovyev Russell O'Connor Laurent Théry Assia Mahboubi keywords: small scale reflection mathematical components odd order theorem versions: 1.7.0 1.6.4 1.6.2 1.6.1 1.6 suite: released

coq-ccs Equivalence notions on labelled transitions systems. We give the specification of three different notions of equivalence classically defined on labelled transitions systems underlying the theories of process algebra (and particularly CCS). The fundamentals properties of these equivalence notions are proven. author: Solange Coupet-Grimal category: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keywords: Labelled Transitions Systems Process Algebra Calculus of Concurrent Process (CCS) versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-cours-de-coq Various examples of Coq proofs. Various simple examples of Coq proofs authors: Frédéric Prost Gilles Kahn category: Miscellaneous/Coq Use Examples keywords: Coq examples versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-topology General Topology. This library develops some of the basic concepts and results of general topology. author: Daniel Schepler category: Mathematics/Real Calculus and Topology keywords: topology filters nets metric spaces real analysis Urysohn's lemma Tietze extension theorem versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-ctltctl Computation Tree Logic for Reactive Systems and Timed Computation Tree Logic for Real Time Systems. This library formalises two logics for reasoning about reactive systems (CTL) and real time systems (TCTL) represents using timed automatas (timed graphs) with discrete time. http://www.fing.edu.uy/~cluna author: Carlos Daniel Luna category: Mathematics/Logic/Modal logic keywords: CTL TCTL real time systems reactive systems temporal logic timed automatas timed graphs discrete time modal logic versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-amm11262 Problem 11262 of The American Mathematical Monthly. http://www.cs.ru.nl/~milad/AMM11262 Formalisation of Tonny Hurkens' proof of the problem 11262 of The American Mathematical Monthly 113(10), Dec. 2006 (see the README files) authors: Milad Niqui (Coq files) Tonny Hurkens (paper proof) keyword: american mathematical monthly problem 11262 versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-unimath-foundations Aims to formalize a substantial body of mathematics using the univalent point of view. author: The UniMath Development Team version: 0.1.0 suite: released

coq-tlc "A general-purpose alternative to Coq's standard library" author: Arthur Charguéraud versions: 20181116 20180316 20171206 20171128 20161010 suite: released

coq-ltac2 A tactic language for Coq. version: 0.1-8.7 suite: released

coq-icharate Icharate: A logical Toolkit for Multimodal Categorial Grammars. http://www.labri.fr/perso/anoun/Icharate The logical toolkit ICHARATE is built upon a formalization of multimodal categorial grammars in Coq proof assistant. This toolkit aims at facilitating the study of these complicated formalisms by allowing users to build interactively the syntactic derivations of different sentences, compute their semantic interpretations and also prove universal properties of entire classes of grammars using a collection of already established derived rules. Several tactics are defined to ease the interaction with users. authors: Houda Anoun Pierre Casteran category: Computer Science/Formal Languages Theory and Automata keywords: Multimodal Categorial Grammars Syntax/Semantics Interface Higher Order Logic Meta-Linguistics versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-automata Beginning of formal language theory. This library formalises the beginning of formal language theory: finite automata and rational languages, context-free grammars and push-down automata. authors: Judicaël Courant Jean-Christophe Filliâtre category: Computer Science/Formal Languages Theory and Automata keywords: formal language theory finite automatas push-down automatas rational langages kleene versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-fssec-model Formal verification of an extension of a UNIX compatible, secure filesystem. author: Maximiliano Cristiá category: Computer Science/Operating Systems keywords: security filesystem UNIX MLS access control versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-concat Constructive Category Theory. http://logical.inria.fr/~saibi/docCatV6.ps author: Amokrane Saïbi category: Mathematics/Category Theory keyword: category theory versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-groups An exercise on groups. author: Pierre Castéran category: Miscellaneous/Coq Use Examples keyword: group theory versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-dblib dblib. http://gallium.inria.fr/~fpottier/dblib/README The dblib library offers facilities for working with de Bruijn indices. author: Francois Pottier category: Computer Science/Lambda Calculi keywords: abstract syntax binders de Bruijn indices shift lift substitution versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-semantics A survey of semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation. ftp://ftp-sop.inria.fr/marelle/Yves.Bertot/semantics_survey.tgz This is a survey of programming language semantics styles for a miniature example of a programming language, with their encoding in Coq, the proofs of equivalence of different styles, and the proof of soundess of tools obtained from axiomatic semantics or abstract interpretation. The tools can be run inside Coq, thus making them available for proof by reflection, and the code can also be extracted and connected to a yacc-based parser, thanks to the use of a functor parameterized by a module type of strings. A hand-written parser is also provided in Coq, but there are no proofs associated. author: Yves Bertot category: Computer Science/Semantics and Compilation/Semantics keywords: natural semantics denotational semantics axiomatic semantics Hoare logic Dijkstra weakest pre-condition calculus abstract interpretation intervals versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-coalgebras Coalgebras, bisimulation and lambda-coiteration. 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. author: Milad Niqui category: Mathematics/Category Theory keywords: coalgebra bisimulation weakly final coiteration coinductive versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-concurrency-system Experimental library to write concurrent applications in Coq. author: Guillaume Claret versions: 1.1.0 1.0.0 suite: released

coq-force-84 Force the use of Coq 8.4 versions. version: 1.0.0 suite: released

coq-io A library for effects in Coq. author: Guillaume Claret versions: 3.3.0 3.2.0 3.1.0 3.0.0 2.1.0 2.0.0 suite: released

coq-checker The Mutilated Checkerboard. author: Gérard Huet category: Miscellaneous/Logical Puzzles and Entertainment keywords: checker dominos puzzles versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-counting Counting: a Coq plugin for measuring definitions/proofs. This plugin keeps the count of the size of definitions and proofs in the current Coq session. author: Stéphane Lescuyer category: Miscellaneous/Coq Extensions keyword: statistics versions: 8.6.0 8.5.0 suite: released

coq-template-coq A quoting and unquoting library for Coq in Coq. Template Coq is a quoting library for Coq. It takes Coq terms and constructs a representation of their syntax tree as a Coq inductive data type. The representation is based on the kernel's term representation. In addition to a complete reification and denotation of CIC terms, Template Coq includes: - Reification of the environment structures, for constant and inductive declarations. - Denotation of terms and global declarations - A monad for manipulating global declarations, calling the type checker, and inserting them in the global environment, in the style of MetaCoq/MTac. - A partial type-checker for the Calculus of Inductive Constructions, runnable as a plugin. - Example plugins built on top of this. authors: Abhishek Anand Simon Boulier Cyril Cohen Gregory Malecha Matthieu Sozeau Nicolas Tabareau versions: 2.1~beta3 2.1~beta 2.0~beta 1.1.0~beta3 1.1.0~beta2 1.0.0~beta2 suite: released

coq-gappa A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover. author: Guillaume Melquiond category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keywords: floating point arithmetic interval arithmetic decision procedure versions: 1.4.0 1.3.4 1.3.3 1.3.2 1.2.1 suite: released

coq-exact-real-arithmetic Exact Real Arithmetic. This contribution contains a proof of correctness of some exact real arithmetic algorithms from the PhD thesis of Valérie Ménissier-Morain author: Jérôme Creci category: Mathematics/Arithmetic and Number Theory/Real numbers keywords: correctness real numbers arithmetic versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-ergo Ergo: a Coq plugin for reification of term with arbitrary signature. This library provides a tactic that performs SMT solving (SAT + congruence closure + arithmetic). author: Stéphane Lescuyer category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keywords: reflexive decision procedure satisfiability modulo theories versions: 8.6.0 8.5.0 suite: released

coq-subst The confluence of Hardin-Lévy lambda-sigma-lift-calcul. The confluence of Hardin-Lévy lambda-sigma-lift-calcul is proven. By the way, several standard definition and results about rewriting systems are proven (Newman's lemma, Yokouchi's lemma, ...). author: Amokrane Saïbi category: Computer Science/Lambda Calculi keywords: lambda-sigma-lift-calculus explicit substitution Newman's lemma Yokouchi's lemma confluence rewriting versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-fsets Finite Sets overs Ordered Types. This contribution contains several implementations of finite sets over arbitrary ordered types using functors. Currently, there are 3 implementations: sorted lists, red-black trees and AVLs. authors: Pierre Letouzey Jean-Christophe Filliâtre categories: Computer Science/Data Types and Data Structures Miscellaneous/Extracted Programs/Data structures keywords: Finite Sets Sorted lists Balanced trees Red-black trees AVL Functors data structures versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-paco "Coq library implementing parameterized coinduction" authors: Chung-Kil Hur Georg Neis Derek Dreyer Viktor Vafeiadis categories: Programming Languages/Formal Definitions and Theory Mathematical Logic and Foramal Languages/Mathematical Logic keywords: coinduction simulation parameterized greatest fixed point versions: 2.0.2 2.0.1 2.0.0 1.2.9 1.2.8 suite: released

coq-cecoa Implicit-complexity Coq library to prove that some programs are computable in polynomial time authors: Hugo Férée Samuel Hym Micaela Mayero Jean-Yves Moyen David Nowak category: CS/Algo/Complexity keywords: implicit complexity polynomial time rewriting version: 1.0.0 suite: released

coq-hardware Verification and synthesis of hardware linear arithmetic structures. Verification and synthesis of hardware linear arithmetic structures. Example of a left-to-right comparator. Three approaches are tackled : - the usual verification of a circuit, consisting in proving that the description satisfies the specification, - the synthesis of a circuit from its specification using the Coq extractor, - the same approach as above but using the Program tactic. author: Solange Coupet-Grimal & Line Jakubiec categories: Computer Science/Architecture Miscellaneous/Extracted Programs/Hardware keywords: hardware verification comparator circuit versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-moment Parse, manipulate and pretty-print times and dates in Coq. author: Guillaume Claret version: 1.0.0 suite: released

coq-maths Basic mathematics. Basic mathematics (gcd, primality, etc.) from French ``Mathematiques Superieures'' (first year of preparation to high schools) author: Jean-Christophe Filliâtre category: Mathematics/Arithmetic and Number Theory/Number theory keyword: mathematics versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-bdds BDD algorithms and proofs in Coq, by reflection. Provides BDD algorithms running under Coq. (BDD are Binary Decision Diagrams.) Allows one to do classical validity checking by reflection in Coq using BDDs, can also be used to get certified BDD algorithms by extraction. First step towards actual symbolic model-checkers in Coq. See file README for operation. author: Kumar Neeraj Verma categories: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures Miscellaneous/Extracted Programs/Decision procedures keywords: BDD binary decision diagrams classical logic propositional logic validity satisfiability model-checking reflection versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-projective-geometry Projective Geometry. This contributions contains elements of formalization of projective geometry. In the plane: Two axiom systems are shown equivalent. We prove some results about the decidability of the the incidence and equality predicates. The classic notion of duality between points and lines is formalized thanks to a functor. The notion of 'flat' is defined and flats are characterized. Fano's plane, the smallest projective plane is defined. We show that Fano's plane is desarguesian. In the space: We prove Desargues' theorem. authors: Nicolas Magaud Julien Narboux Pascal Schreck category: Mathematics/Geometry/General keywords: geometry projective fano homogeneous coordinates model flat rank desargues moulton versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-exceptions Pro[gramm,v]ing with continuations:A development in Coq. author: Pierre Castéran category: Computer Science/Semantics and Compilation/Semantics keywords: exceptions continuations versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-lin-alg Linear Algebra. A development of some preliminary linear algebra based on Chapter 1 of "Linear Algebra" by Friedberg, Insel and Spence author: Jasper Stein category: Mathematics/Algebra keyword: linear algebra versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-compcert The CompCert C compiler. versions: 3.3.0 3.2.0 3.1.0 3.0.1 3.0.0 2.7.1 2.6.0 2.5.0 2.4.0 2.3.2 2.0.0 suite: released

coq-hammer Automation for Dependent Type Theory authors: Lukasz Czajka Cezary Kaliszyk Burak Ekici category: Miscellaneous/Coq Extensions keywords: automation hammer versions: 1.1+8.9 1.1+8.8 1.0.9+8.8.1 1.0.9+8.8.0 1.0.8+8.7 1.0.3 suite: released

coq-cunit Convenience functions for unit testing in Coq. author: Guillaume Claret version: 1.0.0 suite: released

coq-generic-environments Generic_Environments. http://lacl.u-pec.fr/polonowski/Develop/Generic_Env/gen-env.html 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. author: Emmanuel Polonowski category: Mathematics/Logic/Type theory keywords: generic environments typing type theory versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-sudoku A certified Sudoku solver. ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/Sudoku.zip A formalisation of Sudoku in Coq. It implements a naive Davis-Putnam procedure to solve sudokus. author: Laurent Théry category: Miscellaneous/Logical Puzzles and Entertainment keywords: sudoku puzzles Davis-Putnam versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-maple-mode A Maple Mode for Coq. This contribution is an interface between Coq and Maple. In particular, this exports the functions simplify/factor/expand/normal giving the corresponding tactics Simplify/Factor/Expand/Normal. The manipulations carried out by these tactics are proved thanks to the tactic Field. These tactics can be also used as functions by means of the Eval ... In command. authors: David Delahaye Micaela Mayero category: Miscellaneous/Coq Extensions keywords: Maple simplification field tactic versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-domain-theory Elements of Domain Theory. Domain theory as devised by Scott and Plotkin and following Kahn and Plotkin paper on Concrete Domains author: Gilles Kahn category: Computer Science/Lambda Calculi keyword: Concrete Domains versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-io-evaluate Generic functions to run effects. author: Guillaume Claret version: 1.0.0 suite: released

coq-jprover A theorem prover for first-order intuitionistic logic. JProver is a theorem prover for first-order intuitionistic logic. It is originally implemented by Stephan Schmitt and then integrated into MetaPRL by Aleksey Nogin. After this, Huang Guan-Shieng extracted the necessary ML-codes from MetaPRL and then adapted it to Coq. author: Huang Guan-Shieng category: Miscellaneous/Coq Extensions and Computer Science/Decision Procedures keywords: Decision procedures First-order logic Intuitionistic logic Theorem proving Proof search versions: 8.6.0 8.5.0 suite: released

coq-pts A formalisation of Pure Type Systems. This contrib is a formalization of Pure Type Systems. It includes most of the basic metatheoretical properties: weakening, substitution, subject-reduction, decidability of type-checking (for strongly normalizing PTSs). Strengtheningis not proven here. The kernel of a very simple proof checker is automatically generated from the proofs. A small interface allows interacting with this kernel, making up a standalone proof system. The Makefile has a special target "html" that produces html files from the sources and main.html that gives a short overview. author: Bruno Barras category: Computer Science/Lambda Calculi keywords: calculus of constructions coq PTS pure type systems metatheory versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-recursive-definition ML-like recursive definitions. This module provides a facility to define recursive functions in an ML-like style, giving a fixpoint equation, a variant and a well-founded relation. A pure function is then generated, together with a theorem giving the fixpoint equation. THIS IS MAINLY A TEST CONTRIB, BEFORE INTEGRATION IN COQ. authors: Antonia Balaa Yves Bertot category: Miscellaneous/Coq Extensions keywords: recursive functions well founded recursion well foundedness versions: 8.6.0 8.5.0 suite: released

coq-mathcomp-character "The Mathematical Components library" authors: Jeremy Avigad Andrea Asperti Stephane Le Roux Yves Bertot Laurence Rideau Enrico Tassi Ioana Pasca Georges Gonthier Sidi Ould Biha Cyril Cohen Francois Garillot Alexey Solovyev Russell O'Connor Laurent Théry Assia Mahboubi keywords: algebra character small scale reflection mathematical components odd order theorem versions: 1.7.0 1.6.4 1.6.2 1.6.1 1.6 suite: released

coq-qarith A Library for Rational Numbers (QArith). This contribution is a proposition of a library formalizing rational number in Coq. author: Pierre Letouzey categories: Mathematics/Arithmetic and Number Theory/Rational numbers Miscellaneous/Extracted Programs/Arithmetic keywords: Q Arithmetic Rational numbers Setoid Ring versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-gc Formal Verification of an Incremental Garbage Collector. We specify an incremental garbage collection algorithm and we give a formal proof of its correctness. The algorithm is represented as an infinite transition system and we establish safety and liveness properties. This work relies on an axiomatization of LTL and is based on a co-inductive representation of programs executions. Although motivated by integrating the dynamic memory management to the Java Card platform, this study applies more generally to real-time embedded systems and to devices with virtually infinite memory. author: Solange Coupet-Grimal and Catherine Nouvet category: Computer Science/Semantics and Compilation/Compilation keywords: Linear temporal logic finite sets co-induction garbage collection versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-higman-s Higman's lemma on an unrestricted alphabet. This proof is more or less the proof given by Monika Seisenberger in "An Inductive Version of Nash-Williams' Minimal-Bad-Sequence Argument for Higman's Lemma". author: William Delobel category: Mathematics/Combinatorics and Graph Theory keywords: Higman's lemma well quasi-ordering versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-lambek A Coq Toolkit for Lambek Calculus. This library contains some definitions concerning Lambek calculus. Three formalisations of this calculus are proposed, and also some certified functions which translate derivations from one formalism to another. Several derived properties are proved and also some meta-theorems. Users can define their own lexicons and use the defined tactics to prove the derivation of sentences in a particular system (L, NL, LP, NLP ...) authors: Houda Anoun Pierre Castéran category: Computer Science/Formal Languages Theory and Automata keywords: Computational linguistic categorial grammar Lambek calculus... versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-multiplier Proof of a multiplier circuit. author: Christine Paulin categories: Computer Science/Architecture Miscellaneous/Extracted Programs/Hardware keywords: hardware verification circuit versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-msets-extra Extensions of MSets for Efficient Execution Coq's MSet library provides various, reasonably efficient finite set implementations. Nevertheless, FireEye was struggling with performance issues. This library contains extensions to Coq's MSet library that helped the FireEye Formal Methods team (formal-methods@fireeye.com), solve these performance issues. There are - Fold With Abort efficient folding with possibility to start late and stop early - Interval Sets a memory efficient representation of sets of numbers - Unsorted Lists with Duplicates authors: FireEye Formal Methods Team Thomas Tuerk categories: Computer Science/Data Types and Data Structures Miscellaneous/Extracted Programs/Data structures keywords: finite sets fold with abort extracting efficient code data structures versions: 1.1.0 1.0.0 suite: released

coq-interval A Coq tactic for proving bounds on real-valued expressions automatically. author: Guillaume Melquiond categories: Mathematics/Real Calculus and Topology Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keywords: interval arithmetic decision procedure floating point arithmetic reflexive tactic taylor models versions: 3.4.0 3.3.0 3.2.0 3.1.1 2.2.1 2.2.0 2.1.0 2.0.0 1.1.0 suite: released

coq-ptsf Explicit Convertibility Proofs in Pure Type Systems. http://www.andrew.cmu.edu/user/fpv/ptsf/ Formalization of the proof that PTS and PTS with explicit convertibility proofs (PTSf) are equivalent. authors: Floris van Doorn Herman Geuvers Freek Wiedijk category: Mathematics/Logic/Type theory keywords: pure type systems judgmental equality explicit equality proofs proof relevance versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-graph-basics a Coq toolkit for graph theory. This library offers inductive definitions of basics in graph theory. The goal is to offer the possibility to write proofs and programs on graphs in the same formalism : the Coq language. It now contains : vertices, arcs, edges, degrees, graphs, directed graphs, paths, acyclic graphs, connected graphs and tree. author: Jean Duprat category: Mathematics/Combinatorics and Graph Theory keywords: graph theory Curry-Howard's isomorphism inductive definitions versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-string Definition of strings in Coq. Strings as list of characters. author: Laurent Théry category: Miscellaneous/Coq Extensions keywords: string ascii character versions: 8.6.0 8.5.0 suite: released

coq-bertrand Correctness of Knuth's algorithm for prime numbers. A proof of correctness of the algorithm as described in `The Art of Computer Programming: Fundamental Algorithms' by Knuth, pages 147-149 author: Laurent Théry categories: Mathematics/Arithmetic and Number Theory/Number theory Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs based on external tools Miscellaneous/Extracted Programs/Arithmetic keywords: Knuth's algorithm prime numbers Bertrand's postulate versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-io-system System effects for Coq. author: Guillaume Claret versions: 2.4.0 2.3.0 2.2.0 2.1.0 2.0.0 suite: released

coq-squiggle-eq An abstract formalization of variable bindings (both named and de-bruijn), based on ideas in the following paper: Howe, Douglas J. “Equality in Lazy Computation Systems.” In LICS, 198–203, 1989. authors: Abhishek Anand Vincent Rahli versions: 1.0.4 1.0.3 1.0.2 1.0.1 suite: released

coq-karatsuba Karatsuba's Multiplication. http://r6.ca/Karatsuba/ An implementation of Karatsuba's Multiplication algorithm author: Russell O'Connor category: Mathematics/Arithmetic and Number Theory/Number theory keywords: karatsuba multiplication binary ring versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-matrices Ring properties for square matrices. This contribution contains an operational formalization of square matrices. (m,n)-Matrices are represented as vectors of length n. Each vector (a row) is itself a vector whose length is m. Vectors are actually implemented as dependent lists. We define basic operations for this datatype (addition, product, neutral elements O_n and I_n). We then prove the ring properties for these operations. The development uses Coq modules to specify the interface (the ring structure properties) as a signature. This development deals with dependent types and partial functions. Most of the functions are defined by dependent case analysis and some functions such as getting a column require the use of preconditions (to check whether we are within the bounds of the matrix). author: Nicolas Magaud category: Mathematics/Algebra keywords: matrices vectors linear algebra Coq modules versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-fermat4 Diophantus' 20th Problem and Fermat's Last Theorem for n = 4. This contribution presents the formalization of Fermat's proofs of Diophantus' 20th Problem and Fermat's Last Theorem for n = 4. The proofs are completed using Fermat's "wonderful" method of infinite descent. authors: David Delahaye Micaela Mayero category: Mathematics/Arithmetic and Number Theory/Number theory keywords: Diophantus Fermat Arithmetic Infinite Descent versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-min-imports This script will try to remove unnecessary module imports from Coq sources. It examines modules listed in "Require Import" statements one by one and tries to recompile to see if their removal would cause compilation errors. author: Vadim Zaliva category: Miscellaneous/Coq Extensions versions: 1.0.2 1.0.1 1.0.0 suite: released

coq-plouffe A Coq formalization of Plouffe formula. versions: 1.4.0 1.3.0 1.2.1 1.2.0 1.1.0 1.0.0 suite: released

coq-mathcomp-solvable "The Mathematical Components library" authors: Jeremy Avigad Andrea Asperti Stephane Le Roux Yves Bertot Laurence Rideau Enrico Tassi Ioana Pasca Georges Gonthier Sidi Ould Biha Cyril Cohen Francois Garillot Alexey Solovyev Russell O'Connor Laurent Théry Assia Mahboubi keywords: finite groups Feit Thompson theorem small scale reflection mathematical components odd order theorem versions: 1.7.0 1.6.4 1.6.2 1.6.1 1.6 suite: released

coq-markov Markov's inequality. 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. author: Robert Kam category: Mathematics/Real Calculus and Topology keywords: probability theory markov lebesgue integral measures sigma algebras measurability borel versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-kildall Application of the Generic kildall's Data Flow Analysis Algorithm to a Type and Shape Static Analyses of Bytecode. http://www.lif-sud.univ-mrs.fr/Rapports/24-2005.html This Library provides a generic data flow analysis algorithm and a proof of its correctness. This algorithm is then used to perform type and shape analysis at bytecode level on a first order functionnal language. authors: Solange Coupet-Grimal William Delobel category: Computer Science/Semantics and Compilation/Semantics keywords: Kildall data flow analysis bytecode verification versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-mathcomp-multinomials "A multivariate polynomial library for the Mathematical Components Library." author: Pierre-Yves Strub categories: Math/Algebra/Multinomials Math/Algebra/Monoid algebra keywords: multinomials monoid algebra versions: 1.1 1.0 suite: released

coqide IDE of the Coq formal proof management system. versions: 8.9.0 8.8.2 suite: released

coq-rem Rem Theorem in Baire space. A formalisation of Rem Theorem in Baire space author: Henk Barendregt category: Mathematics/Real Calculus and Topology keywords: Rem Theorem Baire space versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-zf An axiomatisation of intuitionistic Zermelo-Fraenkel set theory. author: Guillaume Alexandre category: Mathematics/Logic/Set theory keywords: Set Theory Zermelo-Fraenkel versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-plugin-utils Utility functions for implementing Coq plugins, e.g. building natural numbers, interfacing with Ltac, etc. versions: 1.3.0 1.2.0 1.1.0 suite: released

coq-mathcomp-field "The Mathematical Components library" authors: Jeremy Avigad Andrea Asperti Stephane Le Roux Yves Bertot Laurence Rideau Enrico Tassi Ioana Pasca Georges Gonthier Sidi Ould Biha Cyril Cohen Francois Garillot Alexey Solovyev Russell O'Connor Laurent Théry Assia Mahboubi keywords: algebra field small scale reflection mathematical components odd order theorem versions: 1.7.0 1.6.4 1.6.2 1.6.1 1.6 suite: released

coq-lazy-pcf Subject Reduction for Lazy-PCF. http://www.cs.bell-labs.com/~felty/abstracts/ppcoq.html An Operational Semantics of Lazy Evaluation and a Proof of Subject Reduction authors: Amy Felty Jill Seaman category: Computer Science/Lambda Calculi keywords: functional programming lazy evaluation operational semantics type soundness normal forms versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-goedel The Gödel-Rosser 1st incompleteness theorem. http://r6.ca/goedel1.html A proof that any first order theory extending NN (which is PA without induction) that is complete is inconsistent author: Russell O'Connor category: Mathematics/Logic/Foundations keyword: Goedel Rosser Incompleteness Logic Hilbert versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-label 'label' is a Coq plugin for referring to Propositional hypotheses by their type authors: Pierre-Évariste Dagand Théo Zimmermann Pierre-Marie Pédrot version: 1.0.0 suite: released

coq-color A library on rewriting theory and termination. authors: Frédéric Blanqui Adam Koprowski Sébastien Hinderer Pierre-Yves Strub Sidi Ould Biha Solange Coupet-Grimal William Delobel Hans Zantema Stéphane Leroux Léo Ducas Johannes Waldmann Qiand Wang Lianyi Zhang Sorin Stratulat categories: Computer Science/Algorithms/Correctness proofs of algorithms Computer Science/Data Types and Data Structures Computer Science/Lambda Calculi Mathematics/Algebra Mathematics/Combinatorics and Graph Theory Mathematics/Logic/Type theory Miscellaneous/Extracted Programs/Type checking unification and normalization keywords: rewriting termination lambda calculus list multiset polynom vectors matrices FSet FMap term context substitution universal algebra varyadic term string alpha-equivalence de bruijn indices simple types matching unification relation ordering quasi-ordering lexicographic ordering ring semiring well-founded noetherian finitely branching dependent choice infinite sequences non-termination loop graph path transitive closure strongly connected component topological ordering rpo horpo dependency pair dependency graph semantic labeling reducibility Girard fixpoint theorem Tarski pigeon-hole principle Ramsey theorem versions: 1.6.0 1.5.0 1.4.0 1.3.0 1.2.0 1.1.0 1.0.0 suite: released

coq-zchinese A proof of the Chinese Remainder Lemma. This is a rewriting of the contribution chinese-lemma using Zarith author: Valérie Ménissier-Morain categories: Mathematics/Arithmetic and Number Theory/Number theory Miscellaneous/Extracted Programs/Arithmetic keywords: number theory chinese remainder primality prime numbers versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-disel Core framework files for Disel, a separation-style logic for compositional verification of distributed systems in Coq authors: Ilya Sergey James R. Wilcox category: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keywords: program verification separation logic distributed algorithms versions: 2.1 2.0 suite: released

coq-firing-squad Firing Squad Synchronization Problem. This contribution is a formal verification of a solution of the firing squad synchronization problem. author: Jean Duprat categories: Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols Miscellaneous/Extracted Programs/Automata and protocols keywords: concurrency synchronization finite-state machines versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-param-pi Coding of a typed monadic pi-calculus using parameters for free names. This development contains the specification for a monadic pi-calculus using the same coding method for names than J. Mc Kinna and R. Pollack used for PTS in LEGO: "Some Lambda Calculus and Type Theory Formalized". The basic, monadic calculus encoded here has a type system restraining the direction of communication for processes' names. A number of lemmas usefull for doing proofs on that coding are included, and subject reduction properties for each kind of transition is made as an example of actually using the coding to mechanize proofs on the pi-calculus. author: Loïc Henry-Gréard category: Computer Science/Lambda Calculi keyword: Pi-Calculus versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-coquelicot A Coq formalization of real analysis compatible with the standard library. authors: Sylvie Boldo Catherine Lelay Guillaume Melquiond category: Mathematics/Real Calculus and Topology keywords: real analysis topology filters metric spaces versions: 3.0.2 2.1.2 2.1.1 2.1.0 2.0.1 suite: released

coq-mini-compiler Correctness of a tiny compiler for arithmetic expressions. Tutorial correctness proof of a tiny compiler from simple arithmetic expressions (constants, variables and additions) to simple assembly-like code (one accumulator, infinitly many registers and addition) author: Jean-Christophe Filliâtre category: Computer Science/Semantics and Compilation/Compilation keywords: compilation correctness arithmetic versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-constructive-geometry Elements of Constructive Geometry. Constructive Geometry following Jan von Plato. author: Gilles Kahn category: Mathematics/Geometry/General keywords: Constructive mathematics Geometry versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-finger-tree Dependent Finger Trees. http://mattam.org/research/russell/fingertrees.en.html A verified generic implementation of Finger Trees author: Matthieu Sozeau category: Computer Science/Data Types and Data Structures keywords: data structures dependent types Finger Trees versions: 8.7.0 8.6.0 8.5.0 suite: released

coq-cybele A Coq plugin for simpler proofs by reflection or OCaml certificates. author: Guillaume Claret version: 1.3.0 suite: released

coq-cats-in-zfc Category theory in ZFC. In a ZFC-like environment augmented by reference to the ambient type theory, we develop some basic set theory, ordinals, cardinals and transfinite induction, and category theory including functors, natural transformations, limits and colimits, functor categories, and the theorem that functor_cat a b has (co)limits if b does. author: Carlos Simpson categories: Mathematics/Logic/Set theory Mathematics/Category Theory keywords: set theory ordinal cardinal category theory functor natural transformation limit colimit versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-io-exception Abstract your errors into exceptions. author: Guillaume Claret versions: 1.1.0 1.0.0 suite: released

coq-ext-lib A basic library of basic Coq datatypes, definitions, theorems, and tactics meant to extend the standard library. author: Gregory Malecha versions: 0.10.1 0.10.0 0.9.8 0.9.7 0.9.6 0.9.5 0.9.4 0.9.3 0.9.2 0.9.1 0.9.0 0.9.0~beta3 suite: released

coq-paradoxes Paradoxes in Set Theory and Type Theory. A formalisation of Burali-Forti paradox in system U (the existence of an ordinal of ordinals is inconsistent), of Diaconescu paradox (axiom of choice implies excluded-middle), of Reynolds paradox (there is no set-theoretic model of system F) and Hurkens paradox in system U (adapted by H. Geuvers to show the inconsistency of Excluded-Middle in impredicative-Set Calculus of Inductive Constructions). authors: Bruno Barras Thierry Coquand Hugo Herbelin Benjamin Werner category: Mathematics/Logic/Foundations keywords: Reynolds paradox Burali-Forti paradox Diaconescu paradox set theory system U inconsistency Hurkens paradox versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-descente-infinie The Descente Infinie Tactic. 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. authors: Razvan Voicu Li Mengran category: Miscellaneous/Coq Extensions keywords: Induction Descente Infinie versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-shuffle Gilbreath's card trick. A full axiomatization and proof development of a non-trivial property of binary sequences, inspired from a card trick of N. Gilbreath. author: Gérard Huet category: Miscellaneous/Logical Puzzles and Entertainment keywords: Gilbreath's card trick binary sequences versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-higman-cf A direct constructive proof of Higman's Lemma. This development formalizes in Coq the Coquand-Friedlender proof of Higman's lemma for a two-letter alphabet. An efficient program can be extracted from the proof. author: Stefan Berghofer categories: Mathematics/Combinatorics and Graph Theory Miscellaneous/Extracted Programs/Combinatorics keywords: Higman's Lemma Extraction versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-prfx Proof Reflection in Coq. http://www.cs.ru.nl/~hendriks/coq/prfx/ A formalisation of natural deduction for first-order logic with explicit proof terms. Read README. author: Dimitri Hendriks category: Mathematics/Logic/Foundations keywords: first-order logic natural deduction reflection proof terms de bruijn indices permutative conversions versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-mathcomp-real-closed "Mathematical Components Library on real closed fields" authors: Cyril Cohen Assia Mahboubi keywords: real closed field small scale reflection mathematical components version: 1.0.1 suite: released

coq-geometric-algebra Grassman Cayley and Clifford formalisations version: 0.8.8 suite: released

coq-functional-algebra This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs. This module is unique in that it eschews the tactic-oriented style of traditional Coq developments. As pointed out by others, programs written in that style are brittle, hard to read, and generally inefficient. While tactic driven development is useful for sketching out proofs, these disadvantages should dissuade us from publising proofs in this form. In this library, I provide a worked example of using Gallina directly and demonstrate both the feasibility of this approach and its advantages in terms of clarity, maintainability, and compile-time efficiency. In addition, this module includes two expression simplifiers. The first, defined in monoid_expr.v simplifies monoid expressions. The second, defined in group_expr.v simplifies group expressions. These functions allow us to automate many of the steps involved in proving algebraic theorems directly in Gallina, and represent an alternative to relying on tactics such as auto, omega, etc. For more information about this package, please read its Readme file, which can be found here: https://github.com/llee454/functional-algebra. author: Larry D. Lee Jr. category: Miscellaneous/Coq Extensions keywords: algebra abstract algebra version: 1.0.2 suite: released

coq-lemma-overloading Hoare Type Theory libraries showcasing design patterns for programming with canonical structures authors: Georges Gonthier Beta Ziliani Aleksandar Nanevski Derek Dreyer category: Computer Science/Data Types and Data Structures keywords: canonical structures proof automation hoare type theory lemma overloading version: 8.8.0 suite: released

coq-scev "Proofs and simplification lemmas of an algebraic theory of recurrences" author: Siddharth Bhat category: Miscellaneous/Coq Extensions keyword: math version: 1.0.1 suite: released

coq Formal proof management system versions: 8.9.0 8.8.2 suite: released

coq-poltac A set of tactics to deal with inequalities in Coq over N, Z and R: author: Laurent Théry version: 0.8.8 suite: released

coq-angles Formalization of the oriented angles theory. The basis of the contribution is a formalization of the theory of oriented angles of non-zero vectors. Then, we prove some classical plane geometry theorems: the theorem which gives a necessary and sufficient condition so that four points are cocyclic, the one which shows that the reflected points with respect to the sides of a triangle orthocenter are on its circumscribed circle, the Simson's theorem and the Napoleon's theorem. The reader can refer to the associated research report (http://www-sop.inria.fr/lemme/FGRR.ps) and the README file of the contribution. author: Frédérique Guilhot category: Mathematics/Geometry/General keywords: Pcoq geometry plane geometry oriented angles versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-buchberger Proof of Buchberger's algorithm. A machine-checked implementation of Buchberger's. It computes the Grobner basis associated to a polynomial ideal. authors: Laurent Théry Henrik Persson categories: Mathematics/Algebra Miscellaneous/Extracted Programs/Combinatorics keywords: Grobner basis polynomial ideal Buchberger's algorithm versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-switch A plugin to implement functionality similar to `switch` statement in C language. It allows easier dispatch on several constant values of a type with decidable equality. Given a type, boolean equality predicate, and list of choices, it will generate (using TemplateCoq) an inductive type with constructors, one for each of the choices, and a function mapping values to this type. author: Vadim Zaliva category: Miscellaneous/Coq Extensions version: 1.0.0 suite: released

coq-cfgv Generic Proofs about Alpha Equality and Substitution. http://www.nuprl.org/html/CFGVLFMTP2014/ Please read the following paper authors: Abhishek Vincent Rahli category: Computer Science/Lambda Calculi keywords: generic programming variable bindings context free grammars substitution alpha equality equivariance versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-improper-integrals Additions to the coquelicot library for handling improper integrals This package contains a few theorems whose use case was discovered when making experiments, for instance in the pi-agm package. These theorems should probably integrated in coquelicot in the long run, but having this package makes them easily available while waiting for any necessary cleanup and discussion to happen. author: Yves Bertot category: Mathematics/Real Calculus and Topology keyword: real analysis version: 0.1.0 suite: released

coq-tree-automata Tree automatas. provides tree automatas algorithms in Coq (merge, intersection, vacuity test, deletion of empty states, coaccessiblity test, deletion of non coaccessible states) author: Xavier Rival [http://www.eleves.ens.fr/home/rival] category: Computer Science/Formal Languages Theory and Automata keywords: tree automatas bottom up reflexion terms versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-reglang Regular Language Representations in the Constructive Type Theory of Coq We verify translations between different representations of regular languages: various forms of automata (deterministic, nondeterministic, one-way, two-way), regular expressions, and the logic WS1S. We also show various decidability results and closure properties. authors: Christian Doczkal Gert Smolka category: Computer Science/Formal Languages Theory and Automata keywords: regular languages regular expressions finite automata two-way automata monadic second-order logic version: 1 suite: released

coq-ltl Linear Temporal Logic. This contribution contains a shallow embedding of Linear Temporal Logic (LTL) based on a co-inductive representation of program executions. Temporal operators are implemented as inductive (respectively co-inductive) types when they are least (respectively greatest) fixpoints. Several general lemmas, that correspond to LTL rules, are proved. author: Solange Coupet-Grimal category: Mathematics/Logic/Modal logic keywords: temporal logic infinite transition systems co-induction versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-bellantonicook Deep embedding of Bellantoni and Cook's syntactic characterization of polytime functions authors: Sylvain Heraud David Nowak category: CS/Algo/Complexity keywords: implicit complexity polynomial time version: 1.0.0 suite: released

coq-pigeonhole-principle This library provides a stand-alone proof of the Pigeonhole principle. The Pigeonhole principle is a fundamental theorem that is used widely in Computer Science and Combinatorics, it asserts that if you put n things into m containers, and n > m, then at least one of the containers contains more than one thing. For more information about this proof, Please read its Readme file, which can be found here: https://github.com/llee454/pigeons author: Larry D. Lee Jr. category: Math/Combinatorics and Graph Theory keywords: pigeon-hole principle mathematics versions: 1.0.4 1.0.3 suite: released

coq-geocoq "A formalization of foundations of geometry in Coq" authors: Michael Beeson Gabriel Braun Pierre Boutry Charly Gries Julien Narboux category: Mathematics/Geometry/General keywords: geometry neutral geometry euclidean geometry foundations Tarski Hilbert Euclid Pappus Desargues Elements parallel postulates versions: 2.3.0 2.2.1 2.2.0 2.1.0 2.0.0 1.1.0 1.0.1 suite: released

coq-jordan-curve-theorem Hypermaps, planarity and discrete Jordan curve theorem. http://dpt-info.u-strasbg.fr/~jfd/Downloads/JORDAN_Contrib_Coq.tar.gz Constructive formalization of the combinatorial hypermaps, characterization of the planarity, genus theorem, Euler formula, ring of faces, discrete Jordan curve theorem author: Jean-François Dufourd category: Mathematics/Geometry/General keywords: combinatorial hypermaps genus planarity Euler formula Discrete Jordan Curve Theorem versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-mathcomp-bigenough A small library to do epsilon - N reasonning. The package contains a package to reasoning with big enough objects (mostly natural numbers). This package is essentially for backward compatibility purposes as `bigenough` will be subsumed by the near tactics. The formalization is based on the Mathematical Components library. author: Cyril Cohen keywords: bigenough asymptotic reasonning small scale reflection mathematical components version: 1.0.0 suite: released

coq-coinductive-reals Real numbers as coinductive ternary streams. http://www.cs.ru.nl/~milad/ETrees/coinductive-field/ See the README file author: Milad Niqui category: Mathematics/Arithmetic and Number Theory/Real numbers keywords: real numbers co-inductive types co-recursion exact arithmetic versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-smc BDD based symbolic model checker for the modal mu-calculus. Provides BDD algorithms, a symbolic model checker for the modal mu-calculus based on it, together with a garbage collector author: Kumar Neeraj Verma category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keywords: BDD binary decision diagrams classical logic propositional logic garbage collection modal mu-calculus model checking symbolic model checking reflection versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-vst Verified Software Toolchain 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. authors: Andrew W. Appel Lennart Beringer Sandrine Blazy Qinxiang Cao Santiago Cuellar Robert Dockins Josiah Dodds Nick Giannarakis Samuel Gruetter Aquinas Hobor Jean-Marie Madiot version: 2.2 suite: released

coq-menhirlib "A support library for verified Coq parsers produced by Menhir" versions: 20180827 20180530 suite: released

coq-bbv An implementation of bitvectors in Coq. authors: Tej Chajed Haogang Chen Adam Chlipala Joonwon Choi Andres Erbsen Jason Gross Samuel Gruetter Frans Kaashoek Alex Konradi Gregory Malecha Duckki Oe Murali Vijayaraghavan Nickolai Zeldovich Daniel Ziegler version: 1.0 suite: released

coq-aac-tactics This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators. authors: Damien Pous Thomas Braibant Fabian Kunze category: Miscellaneous/Coq Extensions keywords: reflexive tactic rewriting rewriting modulo associativity and commutativity rewriting modulo ac decision procedure versions: 8.8.0 8.6.1 8.5.1 8.5.0 suite: released

coq-jsast A minimal JavaScript syntax tree carved out of the JsCert project. author: Jerome Simeon versions: 1.0.8 1.0.7 suite: released

coq-abp A verification of the alternating bit protocol expressed in CBS. author: Eduardo Giménez category: Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols keywords: alternating bit protocol process calculi reactive systems co-inductive types co-induction versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-euclidean-geometry Basis of the Euclid's plane geometry. This is a more recent version of the basis of Euclid's plane geometry, the previous version was the contribution intitled RulerCompassGeometry. The plane geometry is defined as a set of points, with two predicates : Clokwise for the orientation and Equidistant for the metric and three constructors, Ruler for the lines, Compass for the circles and Intersection for the points. For using it, we suggest to compile the files the name of which begin by a capital letter and a number from A1 to N7 in the lexicographic order and to keep modifiable the files of tacics (from Tactic1 to Tactic4) and the files of examples (Hilbert and Bolyai). author: Jean Duprat category: Mathematics/Geometry/General keywords: plane geometry Euclid ruler and compass versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-fcsl-pcm Partial Commutative Monoids The PCM library provides a formalisation of Partial Commutative Monoids (PCMs), a common algebraic structure used in separation logic for verification of pointer-manipulating sequential and concurrent programs. The library provides lemmas for mechanised and automated reasoning about PCMs in the abstract, but also supports concrete common PCM instances, such as heaps, histories and mutexes. This library relies on extensionality axioms: propositional and functional extentionality. author: Aleksandar Nanevski keywords: separation logic partial commutative monoid version: 1.0.0 suite: released

coq-pautomata Parameterized automata. This contribution is a modelisation in Coq of the p-automata designed in the CALIFE project (http://www.loria.fr/calife). It contains an axiomatisation of time, the definition of a p-automaton, the definition of binary and arbitrary synchronisation of a family of p-automaton, the semantics of a p-automaton as a labelled transition system. The description of the ABR algorithm as a p-automaton is also given. This work is reported in : P. Castéran, E. Freund, C. Paulin and D. Rouillard ``Bibliothèques Coq et Isabelle-HOL pour les systèmes de transitions et les p-automates'' author: Emmanuel Freund & Christine Paulin category: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keywords: p-automata ABR PGM time versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-concurrency-proxy A proxy to interface concurrent Coq programs with the operating system. author: Guillaume Claret version: 1.0.0 suite: released

coq-three-gap A Proof of the Three Gap Theorem (Steinhaus Conjecture). This proof uses the real numbers. It is a classical proof. author: Micaela Mayero categories: Mathematics/Geometry/See also Mathematics/Arithmetic and Number Theory/Miscellaneous keywords: Real Numbers Steinhaus Three Gap Theorem versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-graphs Satisfiability of inequality constraints and detection of cycles with negative weight in graphs. ******************************************************************* author: Jean Goubault categories: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures Miscellaneous/Extracted Programs/Combinatorics keywords: graphs graph theory cycle detection paths constraints inequalities reflection versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-additions Addition Chains. author: Pierre Castéran categories: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms Miscellaneous/Extracted Programs/Arithmetic keyword: addition chains versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-rsa Correctness of RSA algorithm. This directory contains the proof of correctness of RSA algorithm. It contains a proof of Fermat's little theorem authors: Jose C. Almeida Laurent Théry category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keywords: RSA Chinese remainder Fermat's little theorem versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-euler-formula Hypermaps, Genus Theorem and 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. author: Jean-François Dufourd category: Mathematics/Geometry/See also keywords: polyhedron hypermap genus Euler formula assisted proofs versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-coq2html Generates HTML documentation from Coq source files. Alternative to coqdoc. versions: 1.1 1.0 suite: released

coq-mathcomp-odd-order The formal proof of the Feit-Thompson theorem. From mathcomp Require Import all_ssreflect all_fingroup all_solvable PFsection14. Check Feit_Thompson. : forall (gT : finGroupType) (G : {group gT}), odd #|G| -> solvable G From mathcomp Require Import all_ssreflect all_fingroup all_solvable stripped_odd_order_theorem. Check stripped_Odd_Order. : forall (T : Type) (mul : T -> T -> T) (one : T) (inv : T -> T) (G : T -> Type) (n : natural), group_axioms T mul one inv -> group T mul one inv G -> finite_of_order T G n -> odd n -> solvable_group T mul one inv G authors: Jeremy Avigad Andrea Asperti Stephane Le Roux Yves Bertot Laurence Rideau Enrico Tassi Ioana Pasca Georges Gonthier Sidi Ould Biha Cyril Cohen Francois Garillot Alexey Solovyev Russell O'Connor Laurent Théry Assia Mahboubi keywords: finite groups Feit Thompson theorem small scale reflection mathematical components odd order theorem versions: 1.7.0 1.6.2 1.6.1 suite: released

coq-chinese A proof of the Chinese Remainder Lemma. OBSOLETE. See rather Zchinese-lemma that uses Z of Zarith. author: Valérie Ménissier-Morain category: Mathematics/Arithmetic and Number Theory/Number theory keywords: number theory chinese remainder primality prime numbers versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-stdpp This project contains an extended "Standard Library" for Coq called coq-std++. The key features of this library are as follows: - It provides a great number of definitions and lemmas for common data structures such as lists, finite maps, finite sets, and finite multisets. - It uses type classes for common notations (like `∅`, `∪`, and Haskell-style monad notations) so that these can be overloaded for different data structures. - It uses type classes to keep track of common properties of types, like it having decidable equality or being countable or finite. - Most data structures are represented in canonical ways so that Leibniz equality can be used as much as possible (for example, for maps we have `m1 = m2` iff `∀ i, m1 !! i = m2 !! i`). On top of that, the library provides setoid instances for most types and operations. - It provides various tactics for common tasks, like an ssreflect inspired `done` tactic for finishing trivial goals, a simple breadth-first solver `naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper` for proving compatibility of functions with respect to relations, and a solver `set_solver` for goals involving set operations. - It is entirely dependency- and axiom-free. versions: 1.1.0 1.0.0 suite: released

coq-coqoban Coqoban (Sokoban). A Coq implementation of Sokoban, the Japanese warehouse keepers' game author: Jasper Stein category: Miscellaneous/Logical Puzzles and Entertainment keywords: Sokoban puzzles versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-charge-core A framework of typeclasses for shallow embeddings of intuitionistic logics. Also includes definitions for separation algebras. authors: Jesper Bengtson Gregory Malecha versions: 1.2.0 1.1.0 1.0.1 1.0.0 suite: released

coq-distributed-reference-counting A Construction of Distributed Reference Counting. This library contains the constructive proof of correctness of several variants of a distributed reference counting algorithm. author: Luc Moreau, Jean Duprat categories: Computer Science/Semantics and Compilation/Compilation Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols keywords: garbage collection distributed algorithms versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-coqrel Binary logical relations library for the Coq proof assistant author: Jérémie Koenig category: Mathematics/Logic/Type theory keyword: relations version: 0.1.0 suite: released

coq-pi-agm Computing thousands or millions of digits of PI with arithmetic-geometric means This is a proof of correctness for two algorithms to compute PI to high precision using arithmetic-geometric means. A first file contains the calculus-based proofs for an abstract view of the algorithm, where all numbers are real numbers. A second file describes how to approximate all computations using large integers. Other files describe the second algorithm which is close to the one used in mpfr, for instance. The whole development can be used to produce mathematically proved and formally verified approximations of PI. author: Yves Bertot category: Mathematics/Real Calculus and Topology keywords: real analysis pi versions: 1.2.3 1.2.2 1.2.1 1.2.0 1.1.0 1.0.0 suite: released

coq-classical-realizability Krivine's classical realizability. The aim of this Coq library is to provide a framework for checking proofs in Krivine's classical realizability for second-order Peano arithmetic. It is designed to be as extensible as the original theory by Krivine and to support on-the-fly extensions by new instructions with their evaluation rules. author: Lionel Rieg category: Mathematics/Logic/Foundations keywords: classical realizability Krivine's realizability primitive datatype non determinism quote axiom of countable choice real numbers versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-concurrency-pluto A web server written in Coq. author: Guillaume Claret versions: 1.1.0 1.0.0 suite: released

coq-tree-diameter Diameter of a binary tree. This contribution contains the verification of a divide-and-conquer algorithm to compute the diameter of a binary tree (the maxmimal distance between two nodes in the tree). author: Jean-Christophe Filliâtre category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keywords: program verification trees paths graphs distance diameter versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-fairisle Proof of the Fairisle 4x4 Switch Element. http://www.dil.univ-mrs.fr/~jakubiec/fairisle.tar.gz This library contains the development of general definitions dedicated to the verification of sequential synchronous devices (based on Moore and Mealy automata) and the formal verification of the Fairisle 4x4 Switch Element. authors: Solange Coupet-Grimal Line Jakubiec-Jamet category: Computer Science/Architecture keywords: circuits automata co-induction dependent types. versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-iterable Generic definition of iterators. author: Guillaume Claret version: 1.0.0 suite: released

coq-unimath-ktheory Aims to formalize a substantial body of mathematics using the univalent point of view. author: The UniMath Development Team version: 0.1.0 suite: released

coq-free-groups 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. author: Daniel Schepler category: Mathematics/Algebra keyword: free group versions: 8.8.0 8.7.0 8.6.0 8.5.0 suite: released

coq-legacy-ring The former implementation of the ring tactic. Tactics to decide equality and simplify polynomial expressions over an arbitrary commutative ring. This generalizes a previous tactics by Samuel Boutin. author: Patrick Loiseleur versions: 8.6.0 8.5.0 suite: released

coq-zsearch-trees Binary Search Trees. Algorithms for collecting, searching, inserting and deleting elements in binary search trees on Z author: Pierre Castéran categories: Computer Science/Data Types and Data Structures Miscellaneous