The Coq Proof Assistant

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.

A formalization of Predicative System F, including a computable normalization function.

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

Compute dependencies between Coq objects (definitions, theorems) and produce graphs

The Small Scale Reflection extension.

Based on the paper "Typed Assembly Language" by Greg Morrisett , TAL-0 is the design of a RISC-style typed assembly language which focuses on control-flow safety. This package provides a mechanized metatheory, particularly a machine checked proof of soundness of the TAL-0 type system as proposed by the author in section 4.2.10 of the book Advanced Topics in Types and Programming Languages.

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.

A formalisation of the Calculus of Construction.

Verification of an axiomatisation of the Alternating Bit Protocol. The Alternating Bit Protocol is expressed in an axiomatized calculi of process. Correctness is proven.

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.

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.

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.

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 )

Pi-calculus in Coq. 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.

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.

Simple functional combinators.

The theory needed by the refinement framework library.

More functions on lists.

A library of abstract interfaces for mathematical structures in Coq. We have been working on a new set of foundational interfaces for formalized constructive mathematics in Coq, heavily based on Coq's new type classes, used in a systematic way in order to achieve: * elegant and mathematically sound abstract interfaces for algebraic and numeric structures up to and including rationals (with practical use of universal algebra and category theory); * a very flexible purely predicate-based representation of algebraic structures that makes sharing, multiple inheritance, and derived inheritance, all trivial; * clean expression terms that neither refer to proofs nor require deeply nested record projections; * fluent rewriting; * easy and flexible replacement and specialization of data representations and operations with more efficient versions; * ordinary mathematical notation and overloaded names not reliant on Coq's notation scopes.

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.

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

StructTact is a Coq library of "structural tactics" as well as Coq libraries containing lemmas about lists and finite types that use the tactics library.

A Formal Library about Elliptic Curves for the Mathematical Components Library.

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.

A web server written in Coq.

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.

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

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

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.

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.

Some proofs of hardware (adder, multiplier, memory block instruction). definition and proof of a combinatorial adder, a sequential multiplier, a memory block instruction

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

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

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.

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.

Mathematical Components Library on finite groups This library contains definitions and theorems about finite groups, group quotients, group morphisms, group presentation, group action...

Presburger's algorithm. A formalization of Presburger's algorithm as stated in the initial paper by Presburger.

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

Generic functions on lists with effects.

Fundamental theorems of arithmetic.

Proof of AILS algorithm. An aircraft trajectory modeling and analysis using the AILS algorithm (Airborne Information for Lateral Spacing) to warn against possible collisions.

The Homotopy Type Theory library.

Tarski's geometry This is a formalization of geometry using a simplified version of Tarski's axiom system. The development contains a formalization of the chapters 1-8 of the book "Metamathematische Methoden in der Geometrie" by W. Schwabhäuser, W. Szmielew and A. Tarski. This includes between properties, congruence properties, midpoint, perpendicular lines, point reflection, orthogonality ... This development aims to be a low level complement for Frédérique Guilhot's development about high-school geometry. For more information see: Mechanical Theorem Proving in Tarski's geometry in the post-proceeding of ADG 2006, F. Botana and T. Recio (Eds.), LNAI 4869, pages 139-156, 2007.

Elements of Group Theory. Group Theory following the book "Group Theory" from W.R. Scott.

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.

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.

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) ===================================================

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

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.

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

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

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.

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.

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.

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.

Functions in classical ZFC. This mostly repeats Guillaume Alexandre's contribution `zf', but in classical logic and with a different proof style. We start with a simple axiomatization of some flavor of ZFC (for example Werner's implementation of ZFC should provide a model). We develop some very basic things like pairs, functions, and a little bit about natural numbers, following the standard classical path.

Certifying prime numbers in Coq

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)

The former implementation of the field tactic.

Pocklington's criterion. Pocklington's criterion for checking primality for large natural numbers. Includes a proof of Fermat's little theorem.

Persistent Union Find. Correctness proof of the Ocaml implementation of a persistent union-find data structure. See http://www.lri.fr/~filliatr/puf/ for more details.

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

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.

A Hello World program in Coq.

A Proof of the Three Gap Theorem (Steinhaus Conjecture). This proof uses the real numbers. It is a classical proof.

Mathematical Components Library on Algebra This library contains definitions and theorems about discrete (i.e. with decidable equality) algebraic structures : ring, fields, ordered fields, real fields, modules, algebras, integers, rational numbers, polynomials, matrices, vector spaces...

How to Make Ad Hoc Proof Automation Less Ad Hoc. Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through *tactics*, which are programmed in a separate language from that of the prover's base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself. We propose a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq's own type system. Our approach involves a sophisticated application of Coq's *canonical structures*, which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical *proof* of an overloaded *lemma* for a given instantiation of its parameters. We present a series of design patterns for canonical structure programming that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and we illustrate these patterns through several realistic examples drawn from Hoare Type Theory. We assume no prior knowledge of Coq and describe the relevant aspects of Coq type inference from first principles.

Coq library for synthesizing efficient correct-by-construction programs from declarative specifications.

Russell Metatheoretic Study. This development prove subject reduction of the Russell language (CC with prop, set and coercion of subset types) using the TPOSR machinery. This includes an equivalence of judgmental and definitional presentations of the system.

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.

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.

Mathematical Components Library on real closed fields This library contains definitions and theorems about real closed fields, with a construction of the real closure and the algebraic closure (including a proof of the fundamental theorem of algebra). It also contains a proof of decidability of the first order theory of real closed field, through quantifier elimination.

KDTL. LesniewskiMereology is a Coq library created by R. Dapoigny and P. Barlatier whose purpose is to implement the alternative to Set Theory of Stanislaw Lesniewski. It is part of an on-going project using the Coq language and called KDTL (Knowledge-based Dependently Typed Language) to build an alternative to Description Logics. The developed theory is close to the analysis of Denis Mieville (1984) in his book "Un developpement des systemes logiques de Stanislaw Lesniewski". It is a theoretical construct which relies on three dependent levels, logic (a.k.a. Protothetic), the Lesniewski Ontologie (LO) and mereology. Each level incorporates a minimal collection of axioms, protothetic and ontologic definitions and a set of theorems together with their intuitionist proofs.

A verified system transformer for serialization of Verdi systems using the Cheerios library.

A refinement framework (for algebra).

Finite sets, finite maps, finitely supported functions. This library is under developpment and 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. Multisets are still experimental. There also an embryo of generic order and set libary... very experimental.

A plugin for Coq to add dependent pattern-matching.

[PORTING IN PROGRESS] Mostly automated verification of higher-order programs with higher-order separation logic, with a small trusted code base. Note that somet things are still broken with 8.6, and this is primarily for benchmarking/compatibility testing purposes, at the moment.

Invoke SMT solvers to check goals.

Small Scale Reflection This library includes the small scale reflection proof language extension and the minimal set of libraries to take advantage of it. This includes libraries on lists (seq), boolean and boolean predicates, natural numbers and types with decidable equality, finite types, finite sets, finite functions, finite graphs, basic arithmetics and prime numbers, big operators

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.

Various examples of Coq proofs. Various simple examples of Coq proofs

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

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.

Problem 11262 of The American Mathematical Monthly. Formalisation of Tonny Hurkens' proof of the problem 11262 of The American Mathematical Monthly 113(10), Dec. 2006 (see the README files)

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

A general-purpose library.

Demos of some Coq tools appeared in version V6.0. Example of sorting algorithms defined using the Cases (pattern-matching) construction. Demo of the decision tactic Tauto for intuitionistic propositional calculus. Demo of the AutoRewrite tactic. Demo of the Prolog tactic applied to the compilation of miniML programs.

Icharate: A logical Toolkit for Multimodal Categorial Grammars. 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.

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.

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

Constructive Category Theory.

An exercise on groups.

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

A survey of semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, to. abstract interpretation. 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.

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.

Experimental library to write concurrent applications in Coq.

Demos of some Coq tools appeared in version V6.0. Example of sorting algorithms defined using the Cases (pattern-matching) construction. Demo of the decision tactic Tauto for intuitionistic propositional calculus. Demo of the AutoRewrite tactic. Demo of the Prolog tactic applied to the compilation of miniML programs.

A library for effects in Coq.

The Mutilated Checkerboard.

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.

A quoting library for Coq.

A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover.

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

Ergo: a Coq plugin for reification of term with arbitrary signature. This library provides a tactic that performs SMT solving (SAT + congruence closure + arithmetic).

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, ...).

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.

Parameterized Coinduction Paco is a Coq library implementing parameterized coinduction. Parameterized coinduction is a technique for defining coinductive predicates (i.e., in Prop), using which one can perform coinductive proofs in a more compositional and incremental fashion than with standard Tarski-style constructions. The Paco library provides a tactic called "pcofix", replacing Coq's primitive cofix and avoiding its syntactic guardedness checking of proof terms. We have found that pcofix yields clear performance and usability benefits, even on simple examples.

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.

A formalization of geometry in Coq based on Tarski's axiom system

Basic mathematics. Basic mathematics (gcd, primality, etc.) from French ``Mathematiques Superieures'' (first year of preparation to high schools)

A verification of the alternating bit protocol expressed in CBS.

A library used to prove algorithms working on OCaml native integers using representations with SSReflect's finite sets.

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.

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

Linear Algebra. A development of some preliminary linear algebra based on Chapter 1 of "Linear Algebra" by Friedberg, Insel and Spence

The CompCert C compiler.

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

Convenience functions for unit testing in Coq.

Generic_Environments. Generic_Environments is a library which provides an abstract data type of environments, as a functor parameterized by a module defining variables, and a function which builds environments for such variables with any Type of type. Usual operations over environments are defined, along with an extensive set of basic and more advanced properties. Moreover, an implementation using lists satisfying and all the required properties is provided.

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

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.

Elements of Domain Theory. Domain theory as devised by Scott and Plotkin and following Kahn and Plotkin paper on Concrete Domains

Generic functions to run effects.

Mostly automated synthesis of correct-by-construction programs.

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.

Addition Chains.

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.

Mathematical Components Library on character theory This library contains definitions and theorems about group representations, characters and class functions.

A Library for Rational Numbers (QArith). This contribution is a proposition of a library formalizing rational number in Coq.

A proof of the Chinese Remainder Lemma. This is a rewriting of the contribution chinese-lemma using Zarith

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

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

Proof of a multiplier circuit.

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

Real numbers as coinductive ternary streams. See the README file

Explicit Convertibility Proofs in Pure Type Systems. Formalization of the proof that PTS and PTS with explicit convertibility proofs (PTSf) are equivalent.

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.

Definition of strings in Coq. Strings as list of characters.

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

System effects for Coq.

A series of auxiliary tactics for Coq. These tactics won't change the proof environment but just give internal information of Coq. These tactics are very useful when you're developing an ML plugin. Up to now, these tactics are available: - print_term: print the CiC term - print_term_constant: print the target term of CONST term - print_goal: print the CiC term of goal - print_hyps: print the CiC terms of hypotheses

A formalization of Howe's Squiggle equality Howe, Douglas J. “Equality in Lazy Computation Systems.” In LICS, 198–203, 1989.

Karatsuba's Multiplication. An implementation of Karatsuba's Multiplication algorithm

Binary Search Trees. Algorithms for collecting, searching, inserting and deleting elements in binary search trees on nat

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.

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.

A Coq formalization of Plouffe formula.

Mathematical Components Library on finite groups (II) This library contains more definitions and theorems about finite groups.

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.

Application of the Generic kildall's Data Flow Analysis Algorithm to a Type and Shape Static Analyses of Bytecode. 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.

A Multinomial Library for the Mathematical Components Library.

Verdi Raft is a verified implementation of the Raft distributed consensus protocol in Coq.

Rem Theorem in Baire space. A formalisation of Rem Theorem in Baire space

An axiomatisation of intuitionistic Zermelo-Fraenkel set theory.

Utility functions for implementing Coq plugins, e.g. building natural numbers, interfacing with Ltac, etc.

Mathematical Components Library on Fields This library contains definitions and theorems about field extensions, galois theory, algebraic numbers, cyclotomic polynomials...

Subject Reduction for Lazy-PCF. An Operational Semantics of Lazy Evaluation and a Proof of Subject Reduction

The Gödel-Rosser 1st incompleteness theorem. A proof that any first order theory extending NN (which is PA without induction) that is complete is inconsistent

A library on rewriting theory and termination.

A proof of the Chinese Remainder Lemma. This is a rewriting of the contribution chinese-lemma using Zarith.

A tool to check proof witnesses coming from external SAT and SMT solvers and to call SAT and SMT solvers from Coq.

Firing Squad Synchronization Problem. This contribution is a formal verification of a solution of the firing squad synchronization problem.

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.

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

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)

Elements of Constructive Geometry. Constructive Geometry following Jan von Plato.

Dependent Finger Trees. A verified generic implementation of Finger Trees

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

Odd Order Theorem This library contains the complete formal proof of the Odd Order Theorem (aka Feit Thompson Theorem). The file stripped_odd_order_theorem.v contains a proof of a self contained statement of the odd order.

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.

Abstract your errors into exceptions.

Cheerios is a Coq library for serialization.

A library of Coq definitions, theorems, and tactics.

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

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.

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.

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.

Proof Reflection in Coq. A formalisation of natural deduction for first-order logic with explicit proof terms. Read README.

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

Formal proof management system.

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.

Binary logical relations library for the Coq proof assistant

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.

Proof of Buchberger's algorithm. A machine-checked implementation of Buchberger's. It computes the Grobner basis associated to a polynomial ideal.

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.

IDE of the Coq formal proof management system.

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

Tree automatas. provides tree automatas algorithms in Coq (merge, intersection, vacuity test, deletion of empty states, coaccessiblity test, deletion of non coaccessible states)

Extraction to OCaml of system effects.

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.

A framework for computational reflection.

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

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

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

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

Some properties of hedges used by hedged bisimulation. These properties are in section 6.1 of the paper "On Bisimulations for the Spi-Calculus" by J. Borgström and U. Nestmann. However, we consider here an extended message language.

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

The mathematical underpinnings of reliable software.

Cryptographic Primitive Code Generation in Fiat.

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.

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

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.

COQ Theorems, Abstractions and Implementations (bachelor-Level).

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.

Coq plugin to iterate various collections

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

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

Mathematical Components.

Satisfiability of inequality constraints and detection of cycles with negative weight in graphs. *******************************************************************

Generic Proofs about Alpha Equality and Substitution. Please read the following paper

Correctness of RSA algorithm. This directory contains the proof of correctness of RSA algorithm. It contains a proof of Fermat's little theorem

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.

Modules over monads and lambda-calculi. We define a notion of module over a monad and use it to propose a new definition (or semantics) for abstract syntax (with binding constructions). Using our notion of module, we build a category of `exponential' monads, which can be understood as the category of lambda-calculi, and prove that it has an initial object (the pure untyped lambda-calculus).

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

A certified Sudoku solver. A formalisation of Sudoku in Coq. It implements a naive Davis-Putnam procedure to solve sudokus.

Correctness of the compilation of Mini-ML into the Categorical Abstract Machine. A formalisation of Mini-ML and of the Categorical Abstract Machine (C.A.M) in natural semantics. It also contains the definition of the translation from Mini-ML to the CAM and the proof that this translation is correct

A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers.

A framework of typeclasses for shallow embeddings of intuitionistic logics. Also includes definitions for separation algebras.

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.

Binary Search Trees. Algorithms for collecting, searching, inserting and deleting elements in binary search trees on Z

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.

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.

A Construction of Distributed Reference Counting. This library contains the constructive proof of correctness of several variants of a distributed reference counting algorithm.

A tool to compare universe levels in Coq.

Proof of the Fairisle 4x4 Switch Element . 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.

Generic definition of iterators.

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

A short constructive formalization of finitely presented modules.

Force the use of Coq 8.5 versions.

Force the use of Coq 8.4 versions.

Simple and robust error handling functions.

Library for floating point numbers. A library for floating point numbers.

Tortoise and the hare algorithm. Correctness proof of Floyd's cycle-finding algorithm, also known as the "tortoise and the hare"-algorithm. See http://en.wikipedia.org/wiki/Floyd's_cycle-finding_algorithm

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.

Compile OCaml to Coq.

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

Bignums, the Coq library of arbitrary large numbers Provides BigN, BigZ, BigQ that used to be part of Coq standard library < 8.7.

A floating-point formalization for the Coq system.

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

Verdi is a framework for verification of implementations of distributed systems in Coq.

InfSeqExt is a collection of Coq libraries for reasoning inductively and coinductively on infinite sequences, using modal operators similar to those in linear temporal logic (LTL).

A programming language for topology and probability in Coq.

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.

An enhanced unification algorithm for Coq.

Propositional Calculus Formalization of basic theorems about classical propositional logic. The main theorems are (1) the soundness and completeness of natural deduction calculus, (2) the equivalence between natural deduction calculus, Hilbert systems and sequent calculus and (3) cut elimination for sequent calculus. Keywords: propositional calculus, classical logic, completeness, natural deduction, sequent calculus, cut elimination.

A tactic for deciding Kleene algebras. This library provides algebraic tools for working with binary relations. The main tactic we provide is a reflexive tactic for solving (in)equations in an arbitrary Kleene algebra. The decision procedure goes through standard finite automata constructions, that we formalized.

Strings implemented as lists.

Basics notions of algebra.

Constructive Coq Repository at Nijmegen. The Constructive Coq Repository at Nijmegen, C-CoRN, aims at building a computer based library of constructive mathematics, formalized in the theorem prover Coq. It includes the following parts: * Algebraic Hierarchy o An axiomatic formalization of the most common algebraic structures, including setoids, monoids, groups, rings, fields, ordered fields, rings of polynomials, real and complex numbers * Model of the Real Numbers o Construction of a concrete real number structure satisfying the previously defined axioms * Fundamental Theorem of Algebra o A proof that every non-constant polynomial on the complex plane has at least one root * Real Calculus o A collection of elementary results on real analysis, including continuity, differentiability, integration, Taylor's theorem and the Fundamental Theorem of Calculus

A Coq proof that all Traversable functors are isomorphic to finitary containers.

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

New Up-to Techniques for Weak Bisimulation. This contribution is the formalisation of a paper that appeared in Proc. of ICALP 2005: "Up-to Techniques for Weak Bisimulation". First we define a framework for defining up-to techniques for weak bisimulation in a modular way. Then we prove the correctness of some new up-to techniques, based on termination guarantees. Notably, a generalisation of Newman's Lemma to commutation results is established.

On Ordinal Notations . This contribution contains data structures for ordinals less than Gamma0 under Cantor and Veblen normal forms. Well-foundedness is established thanks to RPO with status for generic terms. This contribution also includes termination proofs of Hydra battles and Goodstein sequences as well as a computation of the length of the Goodstein sequence starting from 4 in base 2. This work is supported by INRIA-Futurs (Logical project-team), CNRS and the French ANR via the A3PAT project (http://www3.iie.cnam.fr/~urbain/a3pat/).

An encoding of Zermelo-Fraenkel Set Theory in Coq. The encoding of Zermelo-Fraenkel Set Theory is largely inspired by Peter Aczel's work dating back to the eighties. A type Ens is defined, which represents sets. Two predicates IN and EQ stand for membership and extensional equality between sets. The axioms of ZFC are then proved and thus appear as theorems in the development. A main motivation for this work is the comparison of the respective expressive power of Coq and ZFC. A non-computational type-theoretical axiom of choice is necessary to prove the replacement schemata and the set-theoretical AC. The main difference between this work and Peter Aczel's is that propositions are defined on the impredicative level Prop. Since the definition of Ens is, however, still unchanged, I also added most of Peter Aczel's definition. The main advantage of Aczel's approach is a more constructive vision of the existential quantifier (which gives the set-theoretical axiom of choice for free).

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

Residual Theory in Lambda-Calculus. We present the complete development in Gallina of the residual theory of beta-reduction in pure lambda-calculus. The main result is the Prism Theorem, and its corollary Lévy's Cube Lemma, a strong form of the parallel-moves lemma, itself a key step towards the confluence theorem and its usual corollaries (Church-Rosser, uniqueness of normal forms).

A program from an A-translated impredicative proof of Higman's Lemma. The file Higman.v formalizes an A-translated version of Nash-Williams impredicative and classical proof of Higman's lemma for a two-letter alphabet. A constructive and impredicative program can be extracted from the proof.

PTSATR. Formalization of the proof that PTS and PTS with judgmental equality (PTSe) are equivalent. With this equivalence, we are able to derive all the meta-theory of PTSe, like Pi-injectivity or Subject Reduction.

Some Coq formalizations of Linear Logic.

# grobner A fornalisation of Grobner basis in ssreflect. It contains one file grobner.v It defines. From mathcomp Require Import all_ssreflect all_algebra. From SsrMultinomials Require Import ssrcomplements poset freeg mpoly. From mathcomp.contrib.grobner Require Import grobner. (* p belongs to the ideal generated by L *) Check ideal. ideal = fun (R : ringType) (n : nat) (L : seq {mpoly R[n]}) (p : {mpoly R[n]}) => exists t, p = \sum_(i < size L) t`_i * L`_i (* it is decidable *) Check idealfP. idealfP : forall (R : fieldType) (n : nat) (p : {mpoly R[n]}) (l : seq {mpoly R[n]}), reflect (ideal l p) (idealf l p)

Proof of Stalmarck's algorithm. A two-level approach to prove tautology using Stalmarck's algorithm.

A Tutorial on Reflecting in Coq the generation of Hoare proof obligations. 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.

Functions extraction from inductive relations. This plugin introduces a new set of extraction commands that generates functional code form inductive specifications.

Coqoban (Sokoban). A Coq implementation of Sokoban, the Japanese warehouse keepers' game

Mtac as a Plugin: Typed Tactics for Coq .

Intuitionistic Zermelo-Fraenkel Set Theory in Coq. This development contains the set-as-pointed-graph interpretation of Intuitionistic Zermelo Frankel set theory in system F_omega.2++ (F_omega + one extra universe + intuitionistic choice operator), which is described in chapter 9 of the author's PhD thesis (for IZ) and in the author's CSL'03 paper (for the extension IZ -> IZF).

Ramsey Theory. For dimension one, the Infinite Ramsey Theorem states that, for any subset A of the natural numbers nat, either A or nat\A is infinite. This special case of the Pigeon Hole Principle is classically equivalent to: if A and B are both co-finite, then so is their intersection. None of these principles is constructively valid. In [VB] the notion of an almost full set is introduced, classically equivalent to co-finiteness, for which closure under finite intersection can be proved constructively. A is almost full if for every (strictly) increasing sequence f: nat -> nat there exists an x in nat such that f(x) in A. The notion of almost full and its closure under finite intersection are generalized to all finite dimensions, yielding constructive Ramsey Theorems. The proofs for dimension two and higher essentially use Brouwer's Bar Theorem. In the proof development below we strengthen the notion of almost full for dimension one in the following sense. A: nat -> Prop is called Y-full if for every (strictly) increasing sequence f: nat -> nat we have (A (f (Y f))). Here of course Y : (nat -> nat) -> nat. Given YA-full A and YB-full B we construct X from YA and YB such that the intersection of A and B is X-full. This is essentially [VB, Th. 5.4], but now it can be done without using axioms, using only inductive types. The generalization to higher dimensions will be much more difficult and is not pursued here.

A formalisation of the IEEE754 norm on floating-point arithmetic. The IEEE754 norm was born in 1985 and is now used in all microprocessors. Here is a full formalistion in Coq of this norm, including denormalized numbers, infinite values and NaNs.

The former implementation of the ring tactic.