Who did What in Coq?

Who did what in the Coq archive?

(updated for Coq 8.4)

1  The Calculus of Inductive Constructions

  • The Calculus of Constructions
    • Core type-checker: Gérard Huet and Thierry Coquand with optimizations by Chet Murthy, Bruno Barras
    • Head reduction functions: Gérard Huet, Christine Paulin, Bruno Barras
  • Conversion and reduction
    • Lazy conversion machine: Bruno Barras
    • Transparency/opacity: Bruno Barras
    • Bytecode-based conversion: Benjamin Grégoire
    • Binary-words retroknowledge: Arnaud Spiwack
  • The universe hierarchy
    • Floating universes: Gérard Huet, with contributions from Bruno Barras
    • Algebraic universes: Hugo Herbelin
  • Mutual inductive types and recursive definitions
    • Type-checking: Christine Paulin
    • Positivity condition: Christine Paulin
    • Guardness condition for fixpoints: Christine Paulin; extensions by Eduardo Gimenez, Bruno Barras, Pierre Boutillier
    • Recursively non-uniform parameters: Christine Paulin
    • Sort-polymorphism of inductive types: Hugo Herbelin
  • Local definitions: Hugo Herbelin
  • Mutual coinductive types and corecursive definitions: Eduardo Gimenez
  • Module system
    • Core system: Jacek Chrząszcz
    • Inlining: Claudio Sacerdoti Coen and Élie Soubiran
    • Module inclusion: Élie Soubiran
    • Functorial signature application: Élie Soubiran
    • Transparent name space: Élie Soubiran
    • Resolution of qualified names: Hugo Herbelin
    • Operator for nested functor application: Élie Soubiran and Pierre Letouzey
  • Minimalist stand-alone type-checker (coqchk): Bruno Barras, with extra support for modules by Élie Soubiran and Pierre Letouzey
  • Eta-conversion: Hugo Herbelin, with contributions from Stéphane Glondu, Benjamin Grégoire

2  Specification language

  • Sections: Gilles Dowek with extra contributions by Gérard Huet, Chet Murthy, Hugo Herbelin
  • The Russell specifications language, proof obligations (Program): Matthieu Sozeau
  • Type inference: Chet Murthy, with extra contributions by Bruno Barras, Hugo Herbelin, Matthieu Sozeau, Enrico Tassi
  • Pattern-matching: Hugo Herbelin on top of a first version by Cristina Cornes
  • Implicit arguments: Amokrane Saïbi, with extensions by Hugo Herbelin, Matthieu Sozeau, Pierre Boutillier
  • Synthetic Arguments command: Enrico Tassi
  • Coercions: Amokrane Saïbi
  • Records: Amokrane Saïbi with extensions by Arnaud Spiwack and Matthieu Sozeau
  • Canonical structures: Amokrane Saïbi
  • Type classes: Matthieu Sozeau
  • Functional schemes (Function, Functional Scheme, ...): Julien Forest and Pierre Courtieu (preliminary version by Yves Bertot)
  • Generation of induction schemes: Christine Paulin, Vincent Siles, Matthieu Sozeau

3  Tactics

3.1  General tactic support

  • Proof engine: Arnaud Spiwack (first version by Thierry Coquand, second version by Chet Murthy)
  • Ltac: David Delahaye, with extensions by Hugo Herbelin, Bruno Barras, ...
  • Tactic notations: Hugo Herbelin (first version by Chet Murthy)
  • Main tactic unification procedure: Chet Murthy with contributions from Hugo Herbelin and Matthieu Sozeau
  • Mathematical-style language (C-Zar): Pierre Corbineau
  • Communication with external tools (external): Hugo Herbelin
  • Proof structuring (bullets and brackets): Arnaud Spiwack

3.2  Predefined tactics

  • Basic tactics (intro, apply, assumption, exact): Thierry Coquand, with further collective extensions
  • Reduction tactics: Christine Paulin (simpl), Bruno Barras (cbv, lazy), with contributions from Hugo Herbelin, Enrico Tassi, ...
  • Tacticals: Thierry Coquand, Chet Murthy, Eduardo Gimenez, ...; new versions of info and Show Script by Pierre Letouzey; timeout by Pierre Letouzey
  • Induction: Christine Paulin (elim, case), Hugo Herbelin (induction, destruct
  • Refinement (refine): Jean-Christophe Filliâtre
  • Introduction patterns: Eduardo Gimenez with collective extensions
  • Forward reasoning: Hugo Herbelin (assert, apply in), Pierre Letouzey (specialize, initial version by Amy Felty)
  • Rewriting tactics (rewrite): basic version by Christine Paulin, extensions by Jean-Christophe Filliâtre and Pierre Letouzey
  • Tactics about equivalence properties (reflexivity, symmetry, transitivity): Christine Paulin (?),
  • Equality tactics (injection/discriminate): Cristina Cornes
  • Inversion tactics (inversion): Cristina Cornes, Chet Murthy
  • Setoid rewriting: Matthieu Sozeau (first version by Clément Renard, second version by Claudio Sacerdoti Coen), contributions from Nicolas Tabareau
  • Decision of equality: Eduardo Gimenez
  • Basic Ltac-level tactics: Pierre Letouzey, Matthieu Sozeau, Evgeny Makarov
  • Tactics about existential variables: Clément Renard, Pierre Corbineau, Stéphane Glondu, Arnaud Spiwack, ...

3.3  General automation tactics

  • Resolution (auto, trivial): Christine Paulin with extensions from Chet Murthy, Eduardo Gimenez, Patrick Loiseleur (hint bases), Matthieu Sozeau
  • Resolution with existential variables (eauto): Chet Murthy, Jean-Christophe Filliâtre, with extensions from Matthieu Sozeau
  • Automatic rewriting (autorewrite): David Delahaye

3.4  Domain-specific decision tactics

  • Congruence closure (cc): Pierre Corbineau
  • Decision of first-order logic (firstorder): Pierre Corbineau
  • Simplification of polynomial fractions (field): Laurent Théry and Benjamin Grégoire (first version by David Delahaye and Micaela Mayero)
  • Simplification of polynomial expressions (ring): Assia Mahboubi, Bruno Barras and Benjamin Grégoire (first version by Samuel Boutin, second version by Patrick Loiseleur)
  • Decision of systems of polynomial equations: Loïc Pottier (nsatz)
  • Decision of systems of linear inequations: Frédéric Besson (psatzl); Loïc Pottier (fourier)
  • Decision of systems of linear inequations over integers: Frédéric Besson (lia); Pierre Crégut (omega and romega)
  • (Partial) decision of systems of polynomical inequations (sos, psatz): Frédéric Besson, with generalization over arbitrary rings by Evgeny Makarov; uses HOL-Light interface to csdp by John Harrisson
  • Decision/simplification of intuitionistic propositional logic: David Delahaye (tauto, intuition, first version by Cesar Muñoz, second version by Chet Murthy), with contributions from Judicaël Courant; Pierre Corbineau (rtauto)
  • Decision/simplification of intuition first-order logic: Pierre Corbineau (firstorder)

4  Extra tools

  • Program extraction: Pierre Letouzey (first implementation by Benjamin Werner, second by Jean-Christophe Filliâtre)
  • Export of context to external communication tools (dp): Nicolas Ayache and Jean-Christophe Filliâtre, with contributions by Claude Marché
  • Export of terms and environments to XML format: Claudio Sacerdoti Coen, with extensions from Cezary Kaliszyk

5  Environment management

  • Separate compilation: initiated by Chet Murthy
  • Import/Export: initiated by Chet Murthy
  • Options management: Hugo Herbelin with contributions by Arnaud Spiwack
  • Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu
  • Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech
  • Whelp suppport: Hugo Herbelin

6  Parsing and printing

  • General parsing support: Chet Murthy, Bruno Barras, Daniel de Rauglaudre
  • General printing support: Chet Murthy, Jean-Christophe Filliâtre
  • Lexing: Daniel de Rauglaudre
  • Support for UTF-8: Hugo Herbelin, with contributions from Alexandre Miquel and Yann Régis-Gianas
  • Numerical notations: Hugo Herbelin, Patrick Loiseleur, Micaela Mayero
  • String notations: Hugo Herbelin
  • New “V8” syntax: Bruno Barras, Hugo Herbelin with contributions by Olivier Desmettre
  • Abbreviations: Chet Murthy
  • Notations: Chet Murthy, Hugo Herbelin

7  Libraries

  • Init: collective (initiated by Christine Paulin and Gérard Huet)
  • Arith: collective (initiated by Christine Paulin)
  • ZArith: collective (initiated by Pierre Crégut)
  • Bool: collective (initiated by Christine Paulin)
  • NArith: Hugo Herbelin, Pierre Letouzey, Evgeny Makarov (out of initial contibution by Pierre Crégut)
  • Lists: Pierre Letouzey, Jean-Marc Notin (initiated by Christine Paulin)
  • Vectors: Pierre Boutillier
  • Reals: Micaela Mayero (axiomatization and main properties), Olivier Desmettre (convergence, derivability, integrals, trigonometric functions), contributions from Russell O’Connor, Cezary Kaliszyk, Guillaume Melquiond, Yves Bertot, Guillaume Allais
  • Relations: Bruno Barras, Cristina Cornes with contributions from Pierre Castéran
  • Wellfounded: Bruno Barras, Cristina Cornes
  • FSets: Pierre Letouzey, from initial work with Jean-Christophe Filliâtre, decision tactic for FSets by Aaron Bohannon, red-black trees by Andrew Appel and Pierre Letouzey
  • MSets: Pierre Letouzey
  • Logic: Christine Paulin, Hugo Herbelin, Bruno Barras
  • Numbers: Evgeny Makarov (abstractions), Laurent Théry and Benjamin Grégoire (big numbers), Arnaud Spiwack and Pierre Letouzey (word-based arithmetic), further extensions by Pierre Letouzey; integration of Arith and ZArith to Numbers by Pierre Letouzey
  • Classes: Matthieu Sozeau
  • QArith: Pierre Letouzey, with contributions from Russell O’Connor
  • Setoid: Matthieu Sozeau (first version by Clément Renard, second version by Claudio Sacerdoti Coen)
  • Sets: Gilles Kahn and Gérard Huet
  • Sorting: Gérard Huet with revisions by Hugo Herbelin
  • Strings: Laurent Théry
  • Program: Matthieu Sozeau
  • Unicode: Claude Marché

8  Commands

  • Batch compiler (coqc): Chet Murthy (?)
  • Compilation dependency calculator (coqdep): Jean-Christophe Filliâtre
  • Statistic tool (coqwc): Jean-Christophe Filliâtre
  • Simple html presentation tool (gallina) (deprecated): Jean-Christophe Filliâtre
  • Auto-maker (coq_makefile): Jean-Christophe Filliâtre, with contributions from Judicaël Courant, updated by Pierre Boutillier
  • LaTeX presentation tool (coq-tex): Jean-Christophe Filliâtre
  • Multi-purpose presentation tool (coqdoc): Jean-Christophe Filliâtre with extensions from Matthieu Sozeau, Jean-Marc Notin, Hugo Herbelin and contributions from Adam Chlipala
  • Interactive toplevel (coqtop): Jean-Christophe Filliâtre (?)
  • Custom toplevel builder (coqmktop): Jean-Christophe Filliâtre (?)

9  Graphical interfaces

  • Support for PCoq: Yves Bertot with contributions by Laurence Rideau and Loïc Pottier; additional support for TmEgg by Lionel Mamane
  • Support for Proof General: Pierre Courtieu with contributions from Arnaud Spiwack
  • CoqIDE: Benjamin Monate with contributions from Jean-Christophe Filliâtre, Claude Marché, Pierre Letouzey, Julien Narboux, Hugo Herbelin, Pierre Corbineau, Pierre Boutillier, Pierre-Marie Pédrot; processus-based communication protocol by Vincent Gross with contributions from Pierre Letouzey, Pierre Boutillier, Pierre-Marie Pédrot; backtracking revised by Pierre Letouzey; uses the Cameleon library by Maxence Guesdon;

10  Architecture

  • Functional-kernel-based architecture: Jean-Christophe Filliâtre
  • Extensible objects and summaries: Chet Murthy
  • Hash-consing: Bruno Barras
  • Error locations: Jean-Christophe Filliâtre, Bruno Barras, Hugo Herbelin, with contributions from Arnaud Spiwack
  • Existential variables engine: Chet Murthy with revisions by Bruno Barras and Arnaud Spiwack and extensions by Clément Renard and Hugo Herbelin

11  Development tools

  • Makefile’s: Chet Murthy, Jean-Christophe Filliâtre, Judicaël Courant, Lionel Mamane, Pierre Corbineau, Pierre Letouzey with contributions from Stéphane Glondu, Hugo Herbelin, ...
  • Debugging: Jean-Christophe Filliâtre with contributions from Jacek Chrząszcz, Hugo Herbelin, Bruno Barras, ...
  • ML quotations: David Delahaye and Daniel de Rauglaudre
  • ML tactic and vernacular extensions: Hugo Herbelin (first version by Chet Murthy)
  • Test suite: collective content, initiated by Jean-Christophe Filliâtre with further extensions by Hugo Herbelin, Jean-Marc Notin

12  Maintenance and system engineering

  • General bug support: Gérard Huet, Christine Paulin, Chet Murthy, Jean-Christophe Filliâtre, Hugo Herbelin, Bruno Barras, Pierre Letouzey with contributions at some time from Benjamin Werner, Jean-Marc Notin, Pierre Boutillier, ...
  • Team coordination: Gérard Huet, Christine Paulin, Hugo Herbelin, with various other contributions
  • Packaging tools: Henri Laulhere, David Delahaye, Julien Narboux, Pierre Letouzey, Enrico Tassi (Windows); Damien Doligez, Hugo Herbelin, Pierre Boutillier (MacOS); Jean-Christophe Filliâtre, Judicaël Courant, Hugo Herbelin, Stéphane Glondu (Linux)

13  Documentation

  • Reference Manual: collective, layout by Patrick Loiseleur, Claude Marché (former User’s Guide in 1991 by Gilles Dowek, Amy Felty, Hugo Herbelin, Gérard Huet, Christine Paulin, Benjamin Werner; initial documentation in 1989 by Thierry Coquand, Gilles Dowek, Gérard Huet, Christine Paulin),
  • Basic tutorial: Gérard Huet, Gilles Kahn, Christine Paulin
  • Tutorial on recursive types: Eduardo Gimenez with updates by Pierre Castéran
  • FAQ: Hugo Herbelin, Julien Narboux, Florent Kirchner

14  Features discontinued by lack of support

  • Searching modulo isomorphism: David Delahaye
  • Explanation of proofs in pseudo-natural language: Yann Coscoy

For probable oversights or accidental errors, please report to Hugo . Herbelin @ inria . fr