From 20755ea50bd68b5ac431dba59ab628bfceed7aeb Mon Sep 17 00:00:00 2001 From: mohring Date: Mon, 15 Mar 2004 14:27:41 +0000 Subject: Mise a jour CREDITS en vue copyright git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5490 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CREDITS | 53 ++++++++++++++++++++++++++--------------------------- 1 file changed, 26 insertions(+), 27 deletions(-) (limited to 'CREDITS') diff --git a/CREDITS b/CREDITS index ad186afb3..beb9dabbe 100644 --- a/CREDITS +++ b/CREDITS @@ -4,58 +4,55 @@ The "Coq proof assistant" was developed conjointly by Laboratoire de l'Informatique du Parallelisme (LIP) associated to CNRS and ENS Lyon (sept.89-sept.97), Laboratoire de Recherche en Informatique (LRI) - associated to CNRS and Paris 11 (since sept. 97). + associated to CNRS and Paris Sud (since sept. 97), + Laboratoire d'Informatique de l'Ecole Polytechnique (since jan 03) + associated to CNRS and Ecole Polytechnique. All files of the "Coq proof assistant" in directories or sub-directories of config contrib dev doc kernel lib library parsing pretyping proofs scripts syntax 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 -The current version V7 is a new implementation started in september 1999. - J-C. Filliâtre designed the architecture of the new system, a -new represention of environments and wrote a new kernel for -type-checking terms (LRI) - H. Herbelin introduced a new structure of terms with local -definitions. He introduced ``qualified'' names, wrote a new -pattern-matching compilation algorithm and designed an -algebraic structure for universes (INRIA) - D. Delahaye introduced a new language for tactics (INRIA) - B. Barras improved the reduction strategy for lazy evaluation (INRIA) - P. Letouzey redesigned the extraction mechanism from proofs -to functional programs (LRI) The following directories contain independant contributions supported -by the Coq development team for the new architecture : +by the Coq development team : contrib/correctness developed by Jean-Christophe Filliâtre (LRI, 1999-2001) contrib/extraction developed by Pierre Letouzey (LRI, 2000-2001) contrib/field developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001) +contrib/first-order + developed by Pierre Corbineau (Paris Sud, 2003-2004) contrib/fourier developed by Loic Pottier (INRIA-Lemme, 2001) +contrib/funind + developed by P. Courtieu (INRIA-Lemme, 2003-2004) contrib/interface developed by Yves Bertot (INRIA-Lemme, 1997) +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) contrib/omega - developed by Pierre Cregut (France Telecom R&D, 1996) + developed by Pierre Crégut (France Telecom R&D, 1996) contrib/romega - developed by Pierre Cregut (France Telecom R&D, 2001) + 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 Sacerdotti (Univ. Bologna, 2000-2001) -contrib/jprover - The author of JProver is Stephan Schmitt , - and is integrated into MetaPRL by Aleksey Nogin - and then into Coq by HUANG Guan-Shieng (LRI, 2001-2002) + parsing/search.ml developed by Yves Bertot (INRIA-Lemme, 2000) Many discussions within the Démons team and the LogiCal project influenced significantly the design of Coq especially with -J. Chrzaszcz, J. Courant, P. Courtieu, J. Duprat, J. Goubault, +J. Courant, P. Courtieu, J. Duprat, J. Goubault, A. Miquel, C. Marché, B. Monate, B. Werner Intensive users suggested improvements of the system : @@ -66,27 +63,29 @@ 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-now) + David Delahaye, (INRIA, 1997-2001) Daniel de Rauglaudre, (INRIA, 1996-1998) - Olivier Desmettre (INRIA, 2001-now) + Olivier Desmettre (INRIA, 2001-2002) Gilles Dowek, (INRIA, 1991-1994) Amy Felty, (INRIA, 1993) - Jean-Christophe Filliâtre, (ENS Lyon, 1994-1997) (Paris 11,1997-now) + 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-now) + 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 11, 1997-1999) + Patrick Loiseleur, (Paris Sud, 1997-1999) Christine Paulin-Mohring, (INRIA, 1985-1989) (ENS Lyon, 1989-1997) - (Paris 11, 1997-now) + (Paris Sud, 1997-now) Clément Renard, (INRIA, 2001-now) Amokrane Saïbi, (INRIA, 1993-1998) Benjamin Werner, (INRIA, 1989-1994) @@ -97,7 +96,7 @@ INRIA refers to : Institute National de la Recherche en Informatique et Automatique CNRS refers to : Centre National de la Recherche Scientifique -Paris 11 refers to : +Paris Sud refers to : Universite Paris Sud ENS Lyon refers to : Ecole Normale Superieure de Lyon -- cgit v1.2.3