aboutsummaryrefslogtreecommitdiffhomepage
path: root/CREDITS
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-04-14 09:05:02 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-04-14 09:05:02 +0000
commit62c152243e3c53747ae85eaad0fee664073db115 (patch)
tree59ab2606cc6d7b268d62f93c6fa71979b58cf47f /CREDITS
parent0fa88cff5bea25e13594567f2ac4a28bf07268b8 (diff)
MAJ 8.1
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8709 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CREDITS')
-rw-r--r--CREDITS181
1 files changed, 100 insertions, 81 deletions
diff --git a/CREDITS b/CREDITS
index a04c5ca68..91bdb7808 100644
--- a/CREDITS
+++ b/CREDITS
@@ -1,117 +1,136 @@
-
-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.
+The "Coq proof assistant" was jointly developed by
+
+- INRIA Formel, Coq, LogiCal, ProVal 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
+
+ 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-2004, The Coq development team,
-CNRS, INRIA and Université Paris Sud
+Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2006,
+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 :
+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)
+ developed by Pierre Corbineau (ENS Cachan, 2001)
contrib/correctness
- developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
+ developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
+contrib/dp
+ developed by Nicolas Ayache and Jean-Christophe Filliâtre (LRI, 2005-2006)
contrib/extraction
- developed by Pierre Letouzey (LRI, 2000-2004)
+ developed by Pierre Letouzey (LRI, 2000-2006)
contrib/field
- developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
+ developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
contrib/first-order
- developed by Pierre Corbineau (LRI, 2003-2004)
+ developed by Pierre Corbineau (LRI, 2003-2006)
contrib/fourier
- developed by Loïc Pottier (INRIA-Lemme, 2001)
+ developed by Loïc Pottier (INRIA-Lemme, 2001)
contrib/funind
- developed by Pierre Courtieu (INRIA-Lemme, 2003-2004)
+ developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2006)
+ and Julien Forest, Benjamin Grégoire and Gilles Barthe (INRIA-Everest, 2006)
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"
+ developed by Yves Bertot with contributions from Loïc Pottier and
+ Laurence Rideau as part of the Pcoq project (INRIA-Lemme, 1997-2006)
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)
+ developed by Pierre Crégut (France Telecom R&D, 1996)
+contrib/recdef
+ developed by Yves Bertot (INRIA-Marelle, 2005)
contrib/ring
- developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick
- Loiseleur (LRI, 1997-1999)
+ developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick
+ Loiseleur (LRI, 1997-1999)
+contrib/romega
+ developed by Pierre Crégut (France Telecom R&D, 2001-2004)
+contrib/rtauto
+ developed by Pierre Corbineau (LRI, 2005)
+contrib/setoid_ring
+ developed by Benjamin Grégoire, Assia Mahboubi (INRIA-Marelle, 2005-2006)
+ and Bruno Barras (INRIA LogiCal, 2005-2006)
+contrib/subtac
+ developed by Matthieu Sozeau (LRI, 2005-2006)
contrib/xml
- developed by Claudio Sacerdoti (Univ. Bologna, 2000-2004)
- as part of the HELM and MoWGLI project
+ developed by Claudio Sacerdoti (Univ. Bologna, 2000-2005)
+ as part of the HELM and MoWGLI projects
parsing/search.ml
- developed by Yves Bertot (INRIA-Lemme, 2000-2004)
+ mainly developed by Yves Bertot (INRIA-Lemme, 2000-2004)
theories/ZArith
- started by Pierre Crégut (France Telecom R&D, 1996)
+ started by Pierre Crégut (France Telecom R&D, 1996)
theories/IntMap
- developed by Jean Goubault-Larrecq (Dyade, 1998)
-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"
+ developed by Jean Goubault-Larrecq (Dyade, 1998)
+theories/Strings
+ developed by Laurent Théry (INRIA-Lemme, 2003)
+ide/utils
+ some files come from Maxence Guesdon's Cameleon tool
-Many discussions within the Démons team and the LogiCal project
+Many discussions within the Démons team at LRI 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
+
+ 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)
+
+ Y. Bertot, L. Pottier, L. Théry (INRIA-Lemme projects),
+ C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D),
+ P. Castéran (University Bordeaux 1),
+ The Foundations Group (Radbout University, Nijmegen, The Netherlands),
+ Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis).
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-2004)
- 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)
-
+ 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)
+ Benjamin Grégoire (INRIA, 2003-now)
+ Hugo Herbelin (INRIA, 1996-now)
+ Gérard Huet (INRIA, 1985-1997)
+ Pierre Letouzey (Paris Sud, 2000-now)
+ Pascal Manoury (INRIA, 1993)
+ Micaela Mayero (INRIA, 1997-2002)
+ Claude Marché (Paris Sud & INRIA, 2003-now)
+ Benjamin Monate (Paris Sud, 2003)
+ César Muñoz (INRIA, 1994-1995)
+ Chetan Murthy (INRIA, 1992-1994)
+ Julien Narboux (INRIA, 2005-2006)
+ Jean-Marc Notin (CNRS, 2006)
+ 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-2004)
+ Claudio Sacerdoti Coen (INRIA, 2004-2005)
+ Amokrane Saïbi (INRIA, 1993-1998)
+ Benjamin Werner (INRIA, 1989-1994)
***************************************************************************
INRIA refers to :
- Institut National de la Recherche en Informatique et Automatique
+ Institut National de la Recherche en Informatique et Automatique
CNRS refers to :
- Centre National de la Recherche Scientifique
+ Centre National de la Recherche Scientifique
Paris Sud refers to :
- Université Paris Sud
+ Université Paris Sud
ENS Lyon refers to :
- Ecole Normale Supérieure de Lyon
+ Ecole Normale Supérieure de Lyon
****************************************************************************