From a71201a2a46e98b68d98bf584a677e993838abee Mon Sep 17 00:00:00 2001 From: mohring Date: Fri, 21 Sep 2001 11:29:11 +0000 Subject: Mise a jour git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2042 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CREDITS | 50 +++++++++++++++++++++++++++++++++----------------- 1 file changed, 33 insertions(+), 17 deletions(-) (limited to 'CREDITS') diff --git a/CREDITS b/CREDITS index affa2f30d..fde4b2b98 100644 --- a/CREDITS +++ b/CREDITS @@ -13,30 +13,45 @@ are distributed under the terms of the GNU Lesser General Public License Version 2.1 (see file LICENSE). 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 and redesigned -the translation from the high-level language of Coq to the internal representation (INRIA) + 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 and redesigned the translation from the high-level +language of Coq to the internal representation (INRIA) D. Delahaye introduced a new language for tactics (INRIA) B. Barras improved the reduction strategy for lazy evaluation (INRIA) -The development was coordinated by C. Paulin (LRI). + P. Letouzey redesigned the extraction mechanism from proofs +to functional programs The following directories contain independant contributions supported by the Coq development team for the new architecture : +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/fourier + developed by Loic Pottier (INRIA-Lemme, 2001) +contrib/interface + developed by Yves Bertot (INRIA-Lemme, 1997) contrib/omega developed by Pierre Cregut (France Telecom R&D, 1996) +contrib/romega + developed by Pierre Cregut (France Telecom R&D, 2001) contrib/ring - developed by Samuel Boutin (INRIA, 1996) + developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick Loiseleur (LRI, 1997-1999) contrib/xml developed by Claudio Sacerdotti (Univ. Bologna, 2000-2001) parsing/search.ml - developed by Yves Bertot (INRIA, 2000) + 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, A. Miquel, C. Marché, -M. Mayero, B. Monate, B. Werner +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, +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) @@ -45,26 +60,27 @@ C. Alvarado, P. Cr The following people have contributed to the development of different versions of the Coq Proof assistant during the indicated time : - Bruno Barras, (INRIA, 1995-2000) + Bruno Barras, (INRIA, 1995-now) Thierry Coquand (INRIA, 1985-1989) Cristina Cornes, (INRIA, 1993-1996) Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996) - David Delahaye, (INRIA, 1997-2000) + David Delahaye, (INRIA, 1997-now) Daniel de Rauglaudre, (INRIA, 1996-1998) Gilles Dowek, (INRIA, 1991-1994) Amy Felty, (INRIA, 1993) - Jean-Christophe Filliâtre, (ENS Lyon, 1994-1997) (Paris 11,1997-2000) + Jean-Christophe Filliâtre, (ENS Lyon, 1994-1997) (Paris 11,1997-now) Eduardo Giménez, (ENS Lyon, 1993-1996, INRIA, 1997-1998) - Hugo Herbelin, (INRIA, 1996-2000) + Hugo Herbelin, (INRIA, 1996-now) Gérard Huet, (INRIA, 1985-1997) + Pierre Letouzey (LRI, 2000-now) Pascal Manoury, (INRIA, 1993) - Micaela Mayero (INRIA, 1997-2000) + Micaela Mayero (INRIA, 1997-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) Christine Paulin-Mohring, (INRIA, 1985-1989) (ENS Lyon, 1989-1997) - (Paris 11, 1997-2001) + (Paris 11, 1997-now) Amokrane Saïbi, (INRIA, 1993-1998) Benjamin Werner, (INRIA, 1989-1994) -- cgit v1.2.3