CREDITS

The "Coq proof assistant" was jointly developed by
- INRIA Formel, Coq, LogiCal, ProVal, TypiCal, Marelle,
  pi.r2, Ascola, Galinette 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 Diderot
  (Jan. 2009 - Dec. 2015 when it was merged into IRIF).
- Institut de Recherche en Informatique Fondamentale (IRIF),
  associated to CNRS and University Paris Diderot (since Jan. 2016).
- And many contributors from various institutions.

All files but the material of the reference manual are distributed
under the term of the GNU Lesser General Public License Version 2.1.

The material of the reference manual is distributed under the terms of
the Open Publication License v1.0 or above, 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.

plugins/cc
  developed by Pierre Corbineau (ENS Cachan, 2001, LRI, 2001-2005, Radboud
  University at Nijmegen, 2005-2008, Grenoble 1, 2010-2014)
plugins/extraction
  developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now)
plugins/firstorder
  developed by Pierre Corbineau (LRI, 2003-2008)
plugins/funind
  developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2006-now),
  Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008, ENSIIE, 2008-now)
  and Yves Bertot (INRIA-Marelle, 2005-2006)
plugins/micromega
  developed by Frédéric Besson (IRISA/INRIA, 2006-now), 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)
plugins/nsatz
  developed by Loïc Pottier (INRIA-Marelle, 2009-2011)
plugins/omega
  developed by Pierre Crégut (France Telecom R&D, 1996)
plugins/rtauto
  developed by Pierre Corbineau (LRI, 2005)
plugins/ring
  developed by Benjamin Grégoire (INRIA-Everest, 2005-2006),
  Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006)
  and Bruno Barras (INRIA LogiCal, 2005-2006),
plugins/ssr
  developed by Georges Gonthier (Microsoft Research - Inria Joint Centre, 2007-2013, Inria, 2013-now),
  Assia Mahboubi and Enrico Tassi (Inria, 2011-now).
plugins/ssrmatching
  developed by Georges Gonthier (Microsoft Research - Inria Joint Centre, 2007-2011, Inria, 2013-now),
  and Enrico Tassi (Inria-Marelle, 2011-now)
theories/ZArith
  started by Pierre Crégut (France Telecom R&D, 1996)
theories/Strings
  developed by Laurent Théry (INRIA-Lemme, 2003)
theories/Numbers/Cyclic
  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)
ide/utils
  some files come from Maxence Guesdon's Cameleon tool

The development of Coq significantly benefited from feedback,
suggestions or short contributions from the following non exhaustive
list of persons and groups:

  C. Alvarado, C. Auger, F. Blanqui, P. Castéran, C. Cohen,
  J. Courant, J. Duprat, F. Garillot, G. Gonthier, J. Goubault,
  J.-P. Jouannaud, S. Lescuyer, A. Miquel, J.-F. Monin, P.-Y. Strub
  the Foundations Group (Radboud University, Nijmegen, The Netherlands),
  Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis),
  L. Lee (https://orcid.org/0000-0002-7128-9257, 2018),
  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 CS dept at MIT
  as well as a lot of users on coq-club, coqdev, coq-bugs

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)
  Yves Bertot (INRIA, 2000-now)
  Pierre Boutillier (INRIA-PPS, 2010-2015)
  Xavier Clerc (INRIA, 2012-2014)
  Tej Chajed (MIT, 2016-now)
  Jacek Chrzaszcz (LRI, 1998-2003)
  Thierry Coquand (INRIA, 1985-1989)
  Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-2011)
  Cristina Cornes (INRIA, 1993-1996)
  Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996)
  Pierre Courtieu (CNAM, 2006-now)
  David Delahaye (INRIA, 1997-2002)
  Maxime Dénès (INRIA, 2013-now)
  Daniel de Rauglaudre (INRIA, 1996-1998, 2012, 2016)
  Olivier Desmettre (INRIA, 2001-2003)
  Gilles Dowek (INRIA, 1991-1994)
  Jim Fehrle (2018-now)
  Amy Felty (INRIA, 1993)
  Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-2008)
  Emilio Jesús Gallego Arias (MINES ParisTech 2015-now)
  Gaetan Gilbert (INRIA-Galinette, 2016-now)
  Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998)
  Stéphane Glondu (INRIA-PPS, 2007-2013)
  Benjamin Grégoire (INRIA, 2003-2011)
  Jason Gross (MIT 2013-now)
  Hugo Herbelin (INRIA, 1996-now)
  Sébastien Hinderer (INRIA, 2014)
  Gérard Huet (INRIA, 1985-1997)
  Konstantinos Kallas (U. Penn, 2019)
  Matej Košík (INRIA, 2015-2017)
  Leonidas Lampropoulos (University of Pennsylvania, 2018)
  Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008,
                   INRIA-PPS then IRIF, 2009-2018)
  Yao Li (ORCID: https://orcid.org/0000-0001-8720-883X,
          University of Pennsylvania, 2018)
  Yishuai Li (ORCID: https://orcid.org/0000-0002-5728-5903
              U. Penn, 2018-2019)
  Patrick Loiseleur (Paris Sud, 1997-1999)
  Andreas Lynge (Aarhus University, 2019)
  Evgeny Makarov (INRIA, 2007)
  Gregory Malecha (Harvard University 2013-2015,
                   University of California, San Diego 2016)
  Cyprien Mangin (INRIA-PPS then IRIF, 2015-now)
  Pascal Manoury (INRIA, 1993)
  Claude Marché (INRIA, 2003-2004 & LRI, 2004)
  Micaela Mayero (INRIA, 1997-2002)
  Guillaume Melquiond (INRIA, 2009-now)
  Benjamin Monate (LRI, 2003)
  César Muñoz (INRIA, 1994-1995)
  Chetan Murthy (INRIA, 1992-1994)
  Julien Narboux (INRIA, 2005-2006, Strasbourg, 2007-2011)
  Jean-Marc Notin (CNRS, 2006-now)
  Catherine Parent-Vigouroux (ENS Lyon, 1992-1995)
  Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997,
                            LRI, 1997-2006)
  Pierre-Marie Pédrot (INRIA-PPS, 2011-2015, INRIA-Ascola, 2015-2016,
                       University of Ljubljana, 2016-2017,
                       MPI-SWS, 2017-2018, INRIA 2018-now)
  Clément Pit-Claudel (MIT, 2015-now)
  Matthias Puech (INRIA-Bologna, 2008-2011)
  Yann Régis-Gianas (INRIA-PPS then IRIF, 2009-2016)
  Clément Renard (INRIA, 2001-2004)
  Talia Ringer (University of Washington, 2019)
  Claudio Sacerdoti Coen (INRIA, 2004-2005)
  Amokrane Saïbi (INRIA, 1993-1998)
  Vincent Semeria (2018-now)
  Vincent Siles (INRIA, 2007)
  Élie Soubiran (INRIA, 2007-2010)
  Matthieu Sozeau (INRIA, 2005-now)
  Arnaud Spiwack (INRIA-LIX-Chalmers University, 2006-2010,
                  INRIA, 2011-2014, MINES ParisTech 2014-2015,
                  Tweag/IO 2015-now)
  Paul Steckler (MIT 2016-2018)
  Enrico Tassi (INRIA, 2011-now)
  Amin Timany (Katholieke Universiteit Leuven, 2017)
  Benjamin Werner (INRIA, 1989-1994)
  Nickolai Zeldovich (MIT 2014-2016)
  Théo Zimmermann (ORCID: https://orcid.org/0000-0002-3580-8806,
                   INRIA-PPS then IRIF, 2015-now)

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