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) theories/IntMap developed by Jean Goubault-Larrecq (Dyade, 1998) 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-2004) 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 ****************************************************************************