File: CREDITS

package info (click to toggle)
coq 8.0pl2-2
  • links: PTS
  • area: main
  • in suites: sarge
  • size: 14,228 kB
  • ctags: 17,685
  • sloc: ml: 97,070; makefile: 1,255; sh: 738; lisp: 456; awk: 15
file content (115 lines) | stat: -rw-r--r-- 4,570 bytes parent folder | download | duplicates (2)
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

The "Coq proof assistant" was developed conjointly by 
	INRIA Formel-Coq-LogiCal 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 doc interp kernel lib library parsing pretyping proofs
	scripts syntax tactics test-suite theories tools toplevel translate
are distributed under the terms of the GNU Lesser General Public License 
Version 2.1 (see file LICENSE).
These files are COPYRIGHT 1999-2004, The Coq development team, 
CNRS, INRIA and Universit� Paris Sud


The following directories contain independent contributions supported 
by the Coq development team :
contrib/cc
	developed by Pierre Corbineau (ENS Cachan, 2001)
contrib/correctness
	developed by Jean-Christophe Filli�tre (LRI, 1999-2001)
contrib/extraction
	developed by Pierre Letouzey (LRI, 2000-2004)
contrib/field
	developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
contrib/first-order 
	developed by Pierre Corbineau (LRI, 2003-2004)
contrib/fourier
	developed by Lo�c Pottier (INRIA-Lemme, 2001)
contrib/funind
	developed by Pierre Courtieu (INRIA-Lemme, 2003-2004)
contrib/interface
	developed by Yves Bertot with contributions from Lo�c Pottier and
	Laurence Rideau as part of the Pcoq project (INRIA-Lemme, 1997-2004)
contrib/jprover
	The author of JProver is Stephan Schmitt <schmitts@spmail.slu.edu>,
	and is integrated into MetaPRL by Aleksey Nogin <nogin@cs.cornell.edu>
	and then into Coq by Guan-Shieng Huang (LRI, 2001-2002)
	original files from Stephan Schmitt are "GPL"
contrib/omega
	developed by Pierre Cr�gut (France Telecom R&D, 1996)
contrib/romega
	developed by Pierre Cr�gut (France Telecom R&D, 2001-2004)
contrib/ring
	developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick 
	Loiseleur (LRI, 1997-1999)
contrib/xml
	developed by Claudio Sacerdoti (Univ. Bologna, 2000-2004) 
	as part of the HELM and MoWGLI project

parsing/search.ml
	developed by Yves Bertot (INRIA-Lemme, 2000-2004)
theories/ZArith
	started by Pierre Cr�gut (France Telecom R&D, 1996)
ide/
	developed by Benjamin Monate (LRI, 2003) with contributions 
	from Claude March� (INRIA, 2003-2004); some files from ide/utils 
	come from Maxence Guesdon's Cameleon project and are "GPL"

Many discussions within the D�mons team and the LogiCal project
influenced significantly the design of Coq especially with
J. Courant, P. Courtieu, J. Duprat, J. Goubault,
A. Miquel, C. March�, B. Monate, B. Werner

Intensive users suggested improvements of the system : 
Y. Bertot, L. Pottier, L. Th�ry (INRIA-Lemme project) 
C. Alvarado, P. Cr�gut, J.-F. Monin (France Telecom R&D)
P. Cast�ran (Universit� Bordeaux 1)

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 (Paris Sud, 1998-2003)
	Thierry Coquand (INRIA, 1985-1989)
	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, Paris Sud, 1997-now)
	Eduardo Gim�nez (ENS Lyon, 1993-1996, INRIA, 1997-1998)
	Hugo Herbelin (INRIA, 1996-now)
	G�rard Huet (INRIA, 1985-1997)
	Pierre Letouzey (LRI, 2000-now)
	Pascal Manoury (INRIA, 1993)
	Micaela Mayero (INRIA, 1997-2002)
	Claude March� (Paris Sud & INRIA, 2003-now)
	C�sar Mu�oz (INRIA, 1994-1995)
	Chetan Murthy (INRIA, 1992-1994)
	Catherine Parent-Vigouroux (ENS Lyon, 1992-1995)
	Patrick Loiseleur (Paris Sud, 1997-1999)
	Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997, 
				  Paris Sud, 1997-now)
	Cl�ment Renard (INRIA, 2001-now)
	Amokrane Sa�bi (INRIA, 1993-1998)
	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
Paris Sud refers to :
	Universit� Paris Sud
ENS Lyon refers to :
	Ecole Normale Sup�rieure de Lyon
****************************************************************************