1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157
|
The "Coq proof assistant" was jointly developed by
- INRIA Formel, Coq, LogiCal, ProVal, TypiCal projects (since 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 Paris Sud (since Sep. 1997),
- Laboratoire d'Informatique de l'Ecole Polytechnique (since Jan. 2003)
associated to CNRS and Ecole Polytechnique.
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-2008,
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.
contrib/cc
developed by Pierre Corbineau (ENS Cachan, 2001, LRI, 2001-2005, Radboud
University at Nijmegen, 2005-2008)
contrib/correctness
developed by Jean-Christophe Fillitre (LRI, 1999-2001)
contrib/dp
developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Fillitre
(LRI, 2005-2008)
contrib/extraction
developed by Pierre Letouzey (LRI, 2000-2004, PPS-Paris7, 2005-now)
contrib/field
developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
contrib/firstorder
developed by Pierre Corbineau (LRI, 2003-2008)
contrib/fourier
developed by Loc Pottier (INRIA-Lemme, 2001)
contrib/funind
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)
contrib/interface
developed by Yves Bertot with contributions from Loc Pottier and
Laurence Rideau as part of the Pcoq project (INRIA-Lemme, 1997-2006);
extended by Lionel Mamane as part of the TeXMacs project (Radboud university
at Nijmegen, 2007-2008)
contrib/omega
developed by Pierre Crgut (France Telecom R&D, 1996)
contrib/ring
developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick
Loiseleur (LRI, 1997-1999)
contrib/romega
developed by Pierre Crgut (France Telecom R&D, 2001-2004)
contrib/rtauto
developed by Pierre Corbineau (LRI, 2005)
contrib/setoid_ring
developed by Benjamin Grgoire (INRIA-Everest, 2005-2006),
Assia Mahboubi, Laurent Thry (INRIA-Marelle, 2006)
and Bruno Barras (INRIA LogiCal, 2005-2006),
contrib/subtac
developed by Matthieu Sozeau (LRI, 2005-2008)
contrib/xml
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)
contrib/micromega
developed by Frdric 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)
parsing/search.ml
mainly developed by Yves Bertot (INRIA-Lemme, 2000-2004)
theories/ZArith
started by Pierre Crgut (France Telecom R&D, 1996)
theories/IntMap
developed by Jean Goubault-Larrecq (Dyade, 1998)
theories/Numbers/Cyclic
developed by Benjamin Grgoire (INRIA-Everest, 2007), Laurent Thry
(INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and
Pierre Letouzey (PPS-Paris 7, 2008)
theories/Strings
developed by Laurent Thry (INRIA-Lemme, 2003)
ide/utils
some files come from Maxence Guesdon's Cameleon tool
Many discussions within the Dmons team at LRI, and the
LogiCal/TypiCal projects influenced significantly the design of
components of Coq, especially with
F. Blanqui, J. Courant, P. Courtieu, J. Duprat, S. Glondu, J. Goubault,
A. Mahboubi, C. March, A. Miquel, B. Monate, P.-Y. Strub, B. Werner.
Intensive users suggested improvements of the system :
Y. Bertot, L. Pottier, L. Thry (INRIA-Lemme/Marelle projects),
C. Alvarado, P. Crgut, J.-F. Monin (France Telecom R&D),
P. Castran (University Bordeaux 1),
The Foundations Group (Radboud University, Nijmegen, The Netherlands),
Laboratoire J.-A. Dieudonn (University of Nice-Sophia Antipolis),
G. Gonthier (INRIA-MSR joint lab), A. Charguraud (INRIA-Gallium project).
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-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 Fillitre (ENS Lyon, 1994-1997, LRI, 1997-now)
Eduardo Gimnez (ENS Lyon, 1993-1996, INRIA, 1997-1998)
Benjamin Grgoire (INRIA, 2003-now)
Hugo Herbelin (INRIA, 1996-now)
Grard Huet (INRIA, 1985-1997)
Pierre Letouzey (LRI, 2000-2004 & PPS-Paris 7, 2005-now)
Evgeny Makarov (INRIA, 2007)
Pascal Manoury (INRIA, 1993)
Micaela Mayero (INRIA, 1997-2002)
Claude March (INRIA 2003-2004 & LRI, 2004-now)
Benjamin Monate (LRI, 2003)
Csar Muoz (INRIA, 1994-1995)
Chetan Murthy (INRIA, 1992-1994)
Julien Narboux (INRIA, 2005-2006)
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)
Clment Renard (INRIA, 2001-2004)
Claudio Sacerdoti Coen (INRIA, 2004-2005)
Amokrane Sabi (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 Suprieure de Lyon
****************************************************************************
|