Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

159 lines (144 sloc) 6.6 KB
The "Coq proof assistant" was jointly developed by
- INRIA Formel, Coq, LogiCal, ProVal, TypiCal, Marelle, pi.r2 projects
(starting 1985),
- Laboratoire de l'Informatique du Parallelisme (LIP)
associated to CNRS and ENS Lyon (Sep. 1989 to Aug. 1997),
- Laboratoire de Recherche en Informatique (LRI)
associated to CNRS and university Paris Sud (since Sep. 1997),
- Laboratoire d'Informatique de l'Ecole Polytechnique (LIX)
associated to CNRS and Ecole Polytechnique (since Jan. 2003).
- Laboratoire PPS associated to CNRS and university Paris 7 (since Jan. 2009).
All files of the "Coq proof assistant" in directories or sub-directories of
config dev ide interp kernel lib library parsing pretyping proofs
scripts states tactics test-suite theories tools toplevel
are distributed under the terms of the GNU Lesser General Public License
Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2010,
The Coq development team, CNRS, INRIA and Université Paris Sud.
Files from the directory doc are distributed as indicated in file doc/LICENCE.
The following directories contain independent contributions supported
by the Coq development team. All of them are released under the terms of
the GNU Lesser General Public License Version 2.1.
developed by Pierre Corbineau (ENS Cachan, 2001, LRI, 2001-2005, Radboud
University at Nijmegen, 2005-2008)
developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre
(LRI, 2005-2008)
developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now)
developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
developed by Pierre Corbineau (LRI, 2003-2008)
developed by Loïc Pottier (INRIA-Lemme, 2001)
developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2008),
Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008)
and Yves Bertot (INRIA-Marelle, 2005-2006)
developed by Pierre Crégut (France Telecom R&D, 1996)
developed by Loïc Pottier (INRIA-Marelle, 2009)
developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick
Loiseleur (LRI, 1997-1999)
developed by Pierre Crégut (France Telecom R&D, 2001-2004)
developed by Pierre Corbineau (LRI, 2005)
developed by Benjamin Grégoire (INRIA-Everest, 2005-2006),
Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006)
and Bruno Barras (INRIA LogiCal, 2005-2006),
developed by Matthieu Sozeau (LRI, 2005-2008)
developed by Claudio Sacerdoti (Univ. Bologna, 2000-2005)
as part of the HELM and MoWGLI projects; extension by Cezary Kaliszyk as
part of the ProofWeb project (Radbout University at Nijmegen, 2008)
developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some
extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and
interface to the csdp solver uses code from John Harrison (University
of Cambridge, 1998)
mainly developed by Yves Bertot (INRIA-Lemme, 2000-2004)
started by Pierre Crégut (France Telecom R&D, 1996)
developed by Laurent Théry (INRIA-Lemme, 2003)
developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and Pierre Letouzey (PPS, 2008)
some files come from Maxence Guesdon's Cameleon tool
Many discussions within the INRIA teams and labs taking part to the
development influenced the design of Coq especially with
C. Auger, Y. Bertot, F. Blanqui, J. Courant, P. Courtieu, J. Duprat,
S. Glondu, J. Goubault, J.-P. Jouannaud, S. Lescuyer, A. Mahboubi,
C. Marché, A. Miquel, B. Monate, L. Pottier, Y. Régis-Gianas,
P.-Y. Strub, L. Théry, B. Werner
The development of Coq also significantly benefited from feedback,
suggestions or short contributions from:
C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D),
P. Castéran (University Bordeaux 1),
the Foundations Group (Radboud University, Nijmegen, The Netherlands),
Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis),
F. Garillot, G. Gonthier (INRIA-MSR joint lab),
INRIA-Gallium project,
the CS dept at Yale, the CIS dept at U. Penn,
the CSE dept at Harvard, the CS dept at Princeton
The following people have contributed to the development of different versions
of the Coq Proof assistant during the indicated time:
Bruno Barras (INRIA, 1995-now)
Jacek Chrzaszcz (LRI, 1998-2003)
Thierry Coquand (INRIA, 1985-1989)
Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-now)
Cristina Cornes (INRIA, 1993-1996)
Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996)
David Delahaye (INRIA, 1997-2002)
Daniel de Rauglaudre (INRIA, 1996-1998)
Olivier Desmettre (INRIA, 2001-2003)
Gilles Dowek (INRIA, 1991-1994)
Amy Felty (INRIA, 1993)
Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-now)
Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998)
Benjamin Grégoire (INRIA, 2003-now)
Hugo Herbelin (INRIA, 1996-now)
Gérard Huet (INRIA, 1985-1997)
Pierre Letouzey (LRI, 2000-2004 & PPS, 2005-now)
Evgeny Makarov (INRIA, 2007)
Pascal Manoury (INRIA, 1993)
Micaela Mayero (INRIA, 1997-2002)
Claude Marché (INRIA 2003-2004 & LRI, 2004)
Benjamin Monate (LRI, 2003)
César Muñoz (INRIA, 1994-1995)
Chetan Murthy (INRIA, 1992-1994)
Julien Narboux (INRIA, 2005-2006, Strasbourg, 2007-now)
Jean-Marc Notin (CNRS, 2006-now)
Catherine Parent-Vigouroux (ENS Lyon, 1992-1995)
Patrick Loiseleur (Paris Sud, 1997-1999)
Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997,
LRI, 1997-now)
Clément Renard (INRIA, 2001-2004)
Claudio Sacerdoti Coen (INRIA, 2004-2005)
Amokrane Saïbi (INRIA, 1993-1998)
Vincent Siles (INRIA, 2007)
Élie Soubiran (INRIA, 2007-now)
Matthieu Sozeau (INRIA, 2005-now)
Arnaud Spiwack (INRIA, 2006-now)
Benjamin Werner (INRIA, 1989-1994)
INRIA refers to:
Institut National de la Recherche en Informatique et Automatique
CNRS refers to:
Centre National de la Recherche Scientifique
LRI refers to: Laboratoire de Recherche en Informatique, UMR 8623
CNRS and Université Paris-Sud
ENS Lyon refers to:
Ecole Normale Supérieure de Lyon
PPS refers to: Laboratoire Preuve, Programmation, Système, UMR 7126,
CNRS and Université Paris 7
Jump to Line
Something went wrong with that request. Please try again.