From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- CREDITS | 115 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 115 insertions(+) create mode 100644 CREDITS (limited to 'CREDITS') diff --git a/CREDITS b/CREDITS new file mode 100644 index 00000000..12cd8e65 --- /dev/null +++ b/CREDITS @@ -0,0 +1,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 , + and is integrated into MetaPRL by Aleksey Nogin + 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 +**************************************************************************** -- cgit v1.2.3