From b46df5d90fd3f4a878a1804c4ee0abb5098b71d1 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 9 May 2010 14:22:56 +0000 Subject: Update of credits files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13004 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CREDITS | 71 +++++++++++++++++++++++++++++++++-------------------------------- 1 file changed, 36 insertions(+), 35 deletions(-) (limited to 'CREDITS') diff --git a/CREDITS b/CREDITS index 3587eec59..68009d390 100644 --- a/CREDITS +++ b/CREDITS @@ -1,12 +1,14 @@ The "Coq proof assistant" was jointly developed by -- INRIA Formel, Coq, LogiCal, ProVal, TypiCal projects (since 1985), +- 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 Paris Sud (since Sep. 1997), -- Laboratoire d'Informatique de l'Ecole Polytechnique (since Jan. 2003) - associated to CNRS and Ecole Polytechnique. + 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 7 (since Jan. 2009). All files of the "Coq proof assistant" in directories or sub-directories of @@ -14,7 +16,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-2008, +Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2010, The Coq development team, CNRS, INRIA and Université Paris Sud. Files from the directory doc are distributed as indicated in file doc/LICENCE. @@ -32,7 +34,7 @@ plugins/dp developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre (LRI, 2005-2008) plugins/extraction - developed by Pierre Letouzey (LRI, 2000-2004, PPS-Paris7, 2005-now) + developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now) plugins/field developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001) plugins/firstorder @@ -43,13 +45,10 @@ plugins/funind 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) -plugins/interface - developed by Yves Bertot with contributions from Loïc Pottier and - 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) plugins/omega developed by Pierre Crégut (France Telecom R&D, 1996) +plugins/groebner + developed by Loïc Pottier (INRIA-Marelle, 2009) plugins/ring developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick Loiseleur (LRI, 1997-1999) @@ -76,40 +75,40 @@ parsing/search.ml mainly developed by Yves Bertot (INRIA-Lemme, 2000-2004) theories/ZArith started by Pierre Crégut (France Telecom R&D, 1996) -theories/IntMap - developed by Jean Goubault-Larrecq (Dyade, 1998) -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-Paris 7, 2008) 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 -Many discussions within the Démons team at LRI, and the -LogiCal/TypiCal projects influenced significantly the design of -components of Coq, especially with +Many discussions within the INRIA teams and labs taking part to the +development influenced the design of Coq especially with - F. Blanqui, J. Courant, P. Courtieu, J. Duprat, S. Glondu, J. Goubault, - A. Mahboubi, C. Marché, A. Miquel, B. Monate, P.-Y. Strub, B. Werner. + C. Auger, Y. Bertot, F. Blanqui, J. Courant, P. Courtieu, J. Duprat, + S. Glondu, J. Goubault, J.-P. Jouannaud, S. Lescuyer, A. Mahboubi, + C. Marché, A. Miquel, B. Monate, L. Pottier, Y. Régis-Gianas, + P.-Y. Strub, L. Théry, B. Werner -Intensive users suggested improvements of the system : +The development of Coq also significantly benefited from feedback, +suggestions or short contributions from: - 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), + the Foundations Group (Radboud University, Nijmegen, The Netherlands), Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis), - G. Gonthier (INRIA-MSR joint lab), A. Charguéraud (INRIA-Gallium project). + F. Garillot, G. Gonthier (INRIA-MSR joint lab), + 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 following people have contributed to the development of different versions -of the Coq Proof assistant during the indicated time : +of the Coq Proof assistant during the indicated time: Bruno Barras (INRIA, 1995-now) Jacek Chrzaszcz (LRI, 1998-2003) Thierry Coquand (INRIA, 1985-1989) - Pierre Corbineau (LRI, 2003-now) + Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-now) Cristina Cornes (INRIA, 1993-1996) Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996) David Delahaye (INRIA, 1997-2002) @@ -122,15 +121,15 @@ 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-2004 & PPS-Paris 7, 2005-now) + Pierre Letouzey (LRI, 2000-2004 & PPS, 2005-now) Evgeny Makarov (INRIA, 2007) Pascal Manoury (INRIA, 1993) Micaela Mayero (INRIA, 1997-2002) - Claude Marché (INRIA 2003-2004 & LRI, 2004-now) + Claude Marché (INRIA 2003-2004 & LRI, 2004) Benjamin Monate (LRI, 2003) César Muñoz (INRIA, 1994-1995) Chetan Murthy (INRIA, 1992-1994) - Julien Narboux (INRIA, 2005-2006) + Julien Narboux (INRIA, 2005-2006, Strasbourg, 2007-now) Jean-Marc Notin (CNRS, 2006-now) Catherine Parent-Vigouroux (ENS Lyon, 1992-1995) Patrick Loiseleur (Paris Sud, 1997-1999) @@ -146,12 +145,14 @@ of the Coq Proof assistant during the indicated time : Benjamin Werner (INRIA, 1989-1994) *************************************************************************** -INRIA refers to : +INRIA refers to: Institut National de la Recherche en Informatique et Automatique -CNRS refers to : +CNRS refers to: Centre National de la Recherche Scientifique -LRI refers to : Laboratoire de Recherche en Informatique, UMR 8623 +LRI refers to: Laboratoire de Recherche en Informatique, UMR 8623 CNRS and Université Paris-Sud -ENS Lyon refers to : +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 **************************************************************************** -- cgit v1.2.3