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
|
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 (sept.89-sept.97),
Laboratoire de Recherche en Informatique (LRI)
associated to CNRS and Paris 11 (since sept. 97).
All files of the "Coq proof assistant" in directories or sub-directories of
config contrib dev doc kernel lib library parsing pretyping
proofs scripts syntax tactics test-suite theories tools toplevel
are distributed under the terms of the GNU Lesser General Public License
Version 2.1 (see file LICENSE).
The current version V7 is a new implementation started in september 1999.
J-C. Filliâtre designed the architecture of the new system, a
new represention of environments and wrote a new kernel for
type-checking terms (LRI)
H. Herbelin introduced a new structure of terms with local
definitions. He introduced ``qualified'' names, wrote a new
pattern-matching compilation algorithm and designed an
algebraic structure for universes (INRIA)
D. Delahaye introduced a new language for tactics (INRIA)
B. Barras improved the reduction strategy for lazy evaluation (INRIA)
P. Letouzey redesigned the extraction mechanism from proofs
to functional programs (LRI)
The following directories contain independant contributions supported
by the Coq development team for the new architecture :
contrib/correctness
developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
contrib/extraction
developed by Pierre Letouzey (LRI, 2000-2001)
contrib/field
developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
contrib/fourier
developed by Loic Pottier (INRIA-Lemme, 2001)
contrib/interface
developed by Yves Bertot (INRIA-Lemme, 1997)
contrib/omega
developed by Pierre Cregut (France Telecom R&D, 1996)
contrib/romega
developed by Pierre Cregut (France Telecom R&D, 2001)
contrib/ring
developed by Samuel Boutin (INRIA-Coq, 1996)
and Patrick Loiseleur (LRI, 1997-1999)
contrib/xml
developed by Claudio Sacerdotti (Univ. Bologna, 2000-2001)
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 HUANG Guan-Shieng (LRI, 2001-2002)
parsing/search.ml
developed by Yves Bertot (INRIA-Lemme, 2000)
Many discussions within the Démons team and the LogiCal project
influenced significantly the design of Coq especially with
J. Chrzaszcz, 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)
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)
Thierry Coquand (INRIA, 1985-1989)
Cristina Cornes, (INRIA, 1993-1996)
Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996)
David Delahaye, (INRIA, 1997-now)
Daniel de Rauglaudre, (INRIA, 1996-1998)
Olivier Desmettre (INRIA, 2001-now)
Gilles Dowek, (INRIA, 1991-1994)
Amy Felty, (INRIA, 1993)
Jean-Christophe Filliâtre, (ENS Lyon, 1994-1997) (Paris 11,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-now)
César Muñoz, (INRIA, 1994-1995)
Chetan Murthy, (INRIA, 1992-1994)
Catherine Parent-Vigouroux, (ENS Lyon 1992-1995)
Patrick Loiseleur, (Paris 11, 1997-1999)
Christine Paulin-Mohring, (INRIA, 1985-1989) (ENS Lyon, 1989-1997)
(Paris 11, 1997-now)
Clément Renard, (INRIA, 2001-now)
Amokrane Saïbi, (INRIA, 1993-1998)
Benjamin Werner, (INRIA, 1989-1994)
***************************************************************************
INRIA refers to :
Institute National de la Recherche en Informatique et Automatique
CNRS refers to :
Centre National de la Recherche Scientifique
Paris 11 refers to :
Universite Paris Sud
ENS Lyon refers to :
Ecole Normale Superieure de Lyon
****************************************************************************
|
