summaryrefslogtreecommitdiff
path: root/CREDITS
diff options
context:
space:
mode:
Diffstat (limited to 'CREDITS')
-rw-r--r--CREDITS55
1 files changed, 34 insertions, 21 deletions
diff --git a/CREDITS b/CREDITS
index 93e35164..b3d563ca 100644
--- a/CREDITS
+++ b/CREDITS
@@ -1,6 +1,6 @@
The "Coq proof assistant" was jointly developed by
-- INRIA Formel, Coq, LogiCal, ProVal projects (since 1985),
+- 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)
@@ -14,7 +14,7 @@ All files of the "Coq proof assistant" in directories or sub-directories of
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-2006,
+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.
@@ -24,26 +24,30 @@ 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 and LRI, 2001-2005)
+ developed by Pierre Corbineau (ENS Cachan, 2001, LRI, 2001-2005, Radboud
+ University at Nijmegen, 2005-2008)
contrib/correctness
developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
contrib/dp
- developed by Nicolas Ayache and Jean-Christophe Filliâtre (LRI, 2005-2007)
+ developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre
+ (LRI, 2005-2008)
contrib/extraction
- developed by Pierre Letouzey (LRI, 2000-2007)
+ developed by Pierre Letouzey (LRI, 2000-2004, PPS-Paris7, 2005-now)
contrib/field
developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
-contrib/first-order
- developed by Pierre Corbineau (LRI, 2003-2005)
+contrib/firstorder
+ developed by Pierre Corbineau (LRI, 2003-2008)
contrib/fourier
developed by Loïc Pottier (INRIA-Lemme, 2001)
contrib/funind
- developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2007),
- Julien Forest (INRIA-Everest, 2006-2007)
- and Yves Bertot (INRIA-Marelle, 2005-2006).
+ 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 Loïc Pottier and
- Laurence Rideau as part of the Pcoq project (INRIA-Lemme, 1997-2006)
+ 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 Crégut (France Telecom R&D, 1996)
contrib/recdef
@@ -56,15 +60,20 @@ contrib/romega
contrib/rtauto
developed by Pierre Corbineau (LRI, 2005)
contrib/setoid_ring
- developed by Benjamin Grégoire (INRIA-Everest, 2005-2007),
- Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2007)
- and Bruno Barras (INRIA LogiCal, 2005-2007),
+ developed by Benjamin Grégoire (INRIA-Everest, 2005-2006),
+ Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006)
+ and Bruno Barras (INRIA LogiCal, 2005-2006),
contrib/subtac
- developed by Matthieu Sozeau (LRI, 2005-2007)
+ 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
-
+ 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 Frédéric 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
@@ -84,11 +93,12 @@ influenced significantly the design of Coq especially with
Intensive users suggested improvements of the system :
- Y. Bertot, L. Pottier, L. Théry (INRIA-Lemme projects),
+ Y. Bertot, L. Pottier, L. Théry (INRIA-Lemme/Marelle projects),
C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D),
P. Castéran (University Bordeaux 1),
The Foundations Group (Radboud University, Nijmegen, The Netherlands),
- Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis).
+ Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis),
+ G. Gonthier (INRIA-MSR joint lab), A. Charguéraud (INRIA-Gallium project).
The following people have contributed to the development of different versions
of the Coq Proof assistant during the indicated time :
@@ -109,10 +119,11 @@ of the Coq Proof assistant during the indicated time :
Benjamin Grégoire (INRIA, 2003-now)
Hugo Herbelin (INRIA, 1996-now)
Gérard Huet (INRIA, 1985-1997)
- Pierre Letouzey (LRI, 2000-2005 & PPS-Paris 7, 2005-now)
+ 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-2005)
+ Claude Marché (INRIA 2003-2004 & LRI, 2004-now)
Benjamin Monate (LRI, 2003)
César Muñoz (INRIA, 1994-1995)
Chetan Murthy (INRIA, 1992-1994)
@@ -124,6 +135,8 @@ of the Coq Proof assistant during the indicated time :
LRI, 1997-now)
Clément Renard (INRIA, 2001-2004)
Claudio Sacerdoti Coen (INRIA, 2004-2005)
+ Matthieu Sozeau (INRIA, 2005-now)
+ Arnaud Spiwack (INRIA, 2006-now)
Amokrane Saïbi (INRIA, 1993-1998)
Benjamin Werner (INRIA, 1989-1994)