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.

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

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.

ppsimpl is a reflexive tactic for canonising (arithmetic) goals.

"A tool for proving OCaml programs in Separation Logic"

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

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.

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

Mtac2: Typed Tactics for Coq

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.

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

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

This is the Coq development of the Iris Project.

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

A short constructive formalization of finitely presented modules.

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.

"The Mathematical Components library"

"Paramcoq"

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

"Relation Algebra and KAT in Coq"

A small library for collecting side conditions and deferring their proof

Generic functions on lists with effects.

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

Fundamental theorems of arithmetic. http://perso.ens-lyon.fr/sebastien.briais/tools/Arith_080201.tar.gz

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

A framework for computational reflection.

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.

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.

Verified compiler for data-centric languages

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.

Compile OCaml to Coq.

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.

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

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)

"LibValidSDP"

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

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.

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.

Extraction to OCaml of system effects.

"The Mathematical Components library"

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.

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

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

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.

A tool to compare universe levels in Coq.

Simple and robust error handling functions.

A refinement framework (for algebra).

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.

"A function definition package for Coq"

Invoke SMT solvers to check goals.

"The Mathematical Components library"

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. http://www.fing.edu.uy/~cluna

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)

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

"A general-purpose alternative to Coq's standard library"

A tactic language for Coq.

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.

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. http://logical.inria.fr/~saibi/docCatV6.ps

An exercise on groups.

dblib. http://gallium.inria.fr/~fpottier/dblib/README 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. 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.

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.

Force the use of Coq 8.4 versions.

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

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

"Coq library implementing parameterized coinduction"

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

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.

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

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

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.

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.

Automation for Dependent Type Theory

Convenience functions for unit testing in Coq.

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.

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.

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.

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.

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.

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.

"The Mathematical Components library"

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

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.

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

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

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.

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.

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.

Karatsuba's Multiplication. http://r6.ca/Karatsuba/ An implementation of Karatsuba's Multiplication algorithm

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

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.

"The Mathematical Components library"

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

"A multivariate polynomial library for the Mathematical Components Library."

IDE of the Coq formal proof management system.

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.

"The Mathematical Components library"

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

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

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

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

Core framework files for Disel, a separation-style logic for compositional verification of distributed systems in 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. http://mattam.org/research/russell/fingertrees.en.html A verified generic implementation of Finger Trees

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

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.

A basic library of basic Coq datatypes, definitions, theorems, and tactics meant to extend the standard library.

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. http://www.cs.ru.nl/~hendriks/coq/prfx/ A formalisation of natural deduction for first-order logic with explicit proof terms. Read README.

"Mathematical Components Library on real closed fields"

Grassman Cayley and Clifford formalisations

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.

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

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

Formal proof management system

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

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.

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.

Generic Proofs about Alpha Equality and Substitution. http://www.nuprl.org/html/CFGVLFMTP2014/ Please read the following paper

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.

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

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.

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.

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

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

"A formalization of foundations of geometry in Coq"

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

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.

Real numbers as coinductive ternary streams. http://www.cs.ru.nl/~milad/ETrees/coinductive-field/ See the README file

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

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.

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

An implementation of bitvectors in Coq.

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

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

A verification of the alternating bit protocol expressed in CBS.

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

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.

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

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

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

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

Addition Chains.

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.

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

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 proof of the Chinese Remainder Lemma. OBSOLETE. See rather Zchinese-lemma that uses Z of Zarith.

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.

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

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

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

Binary logical relations library for the Coq proof assistant

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.

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 web server written in 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).

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.

Generic definition of iterators.

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

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.

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.

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

New Up-to Techniques for Weak Bisimulation. http://perso.ens-lyon.fr/damien.pous/upto/ 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.

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

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

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.

Coq plugin to iterate various collections

Traversable Functors are Finitary Containers. https://github.com/oconnorr/traversable-fincontainer A Coq proof that all Traversable functors are isomorphic to finitary containers.

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

A floating-point formalization for the Coq system.

Tarski's geometry. http://dpt-info.u-strasbg.fr/~narboux/tarski.html 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.

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

Force the use of Coq 8.5 versions.

Knowledge-based Dependently Typed Language (KDTL). http://www.polytech.univ-savoie.fr/index.php?id=listic-logiciels-coq&L=1 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.

Modules over monads and lambda-calculi. http://www.math.unifi.it/~/maggesi/mechanized/ 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).

An enhanced unification algorithm for Coq.

Basics notions of algebra.

A tactic for deciding Kleene algebras. http://sardes.inrialpes.fr/~braibant/atbr 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.

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.

The CoRN library. A library for constructive analysis.

The Small Scale Reflection extension.

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

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

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

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.

PTSATR. http://www.lix.polytechnique.fr/~vsiles/coq/PTSATR.html 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.

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.

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

Propositional Calculus. http://arxiv.org/abs/1503.08744 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.

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.

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

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

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

Finite data structures with extensional reasoning.

Typed Tactics for Coq 8.5

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. This library contains a non-verified implementation of binary floating-point addition and multiplication operators inspired by the IEEE-754 standard. It is today outdated. See the attached 1997 report rapport-stage-dea.ps.gz for a discussion (in French) of this work. For the state of the art at the time of updating this notice, see e.g. "Flocq: A Unified Library for Proving Floating-point Algorithms in Coq" by S. Boldo and G. Melquiond, 2011.

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