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
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
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 Diderot
(Jan. 2009 - Dec. 2015).
- Institut de Recherche en Informatique Fondamentale (IRIF),
associated to CNRS and University Paris Diderot (since Jan. 2016).
All files of the "Coq proof assistant" in directories or sub-directories of
config dev ide interp intf 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-2017,
The Coq development team, INRIA, CNRS, LIX, LRI, PPS.
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.
plugins/cc
developed by Pierre Corbineau (ENS Cachan, 2001, LRI, 2001-2005, Radboud
University at Nijmegen, 2005-2008, Grenoble 1, 2010-2014)
plugins/decl_mode
developed by Pierre Corbineau (Radboud University at Nijmegen, 2005-2008,
Grenoble 1, 2009-2011)
plugins/extraction
developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now)
plugins/firstorder
developed by Pierre Corbineau (LRI, 2003-2008)
plugins/fourier
developed by Loïc Pottier (INRIA-Lemme, 2001)
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/omega
developed by Pierre Crégut (France Telecom R&D, 1996)
plugins/nsatz
developed by Loïc Pottier (INRIA-Marelle, 2009-2011)
plugins/quote
developed by Patrick Loiseleur (LRI, 1997-1999)
plugins/romega
developed by Pierre Crégut (France Telecom R&D, 2001-2004)
plugins/rtauto
developed by Pierre Corbineau (LRI, 2005)
plugins/setoid_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/ssrmatching
developed by Georges Gonthier (Microsoft Research - Inria Joint Centre, 2007-2011),
and Enrico Tassi (Inria-Marelle, 2011-now)
plugins/subtac
developed by Matthieu Sozeau (LRI, 2005-2008)
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)
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),
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)
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-CoqHoTT 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)
Matej Košík (INRIA, 2015-2017)
Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS, 2009-now)
Patrick Loiseleur (Paris Sud, 1997-1999)
Evgeny Makarov (INRIA, 2007)
Gregory Malecha (Harvard University 2013-2015,
University of California, San Diego 2016)
Cyprien Mangin (INRIA-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-CoqHoTT 2015-2016,
University of Ljubljana 2016-2017)
Matthias Puech (INRIA-Bologna, 2008-2011)
Yann Régis-Gianas (INRIA-PPS, 2009-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-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-now)
Enrico Tassi (INRIA, 2011-now)
Amin Timany (Katholieke Universiteit Leuven, 2017)
Benjamin Werner (INRIA, 1989-1994)
Nickolai Zeldovich (MIT 2014-2016)
Théo Zimmermann (INRIA-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
****************************************************************************
|
