From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- CREDITS | 183 ++++++++++++++++++++++++++++++++++++---------------------------- 1 file changed, 102 insertions(+), 81 deletions(-) (limited to 'CREDITS') diff --git a/CREDITS b/CREDITS index 12cd8e65..0bc6ee56 100644 --- a/CREDITS +++ b/CREDITS @@ -1,115 +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 and LRI, 2001-2005) 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-2005) 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 , - 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" + 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) -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" + started by Pierre Crégut (France Telecom R&D, 1996) +theories/IntMap + 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-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) - + Bruno Barras (INRIA, 1995-now) + Jacek Chrzaszcz (LRI, 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, LRI, 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 (LRI, 2000-2005 & PPS-Paris 7, 2005-now) + Pascal Manoury (INRIA, 1993) + Micaela Mayero (INRIA, 1997-2002) + Claude Marché (INRIA 2003-2004 & LRI, 2004-now) + Benjamin Monate (LRI, 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, + LRI, 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 -Paris Sud refers to : - Université Paris Sud + Centre National de la Recherche Scientifique +LRI refers to : Laboratoire de Recherche en Informatique, UMR 8623 + CNRS and Université Paris-Sud ENS Lyon refers to : - Ecole Normale Supérieure de Lyon + Ecole Normale Supérieure de Lyon **************************************************************************** -- cgit v1.2.3