From b46df5d90fd3f4a878a1804c4ee0abb5098b71d1 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 9 May 2010 14:22:56 +0000 Subject: Update of credits files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13004 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CREDITS | 71 +++++++++++++++++++++--------------------- doc/refman/RefMan-pre.tex | 79 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 115 insertions(+), 35 deletions(-) diff --git a/CREDITS b/CREDITS index 3587eec59..68009d390 100644 --- a/CREDITS +++ b/CREDITS @@ -1,12 +1,14 @@ The "Coq proof assistant" was jointly developed by -- INRIA Formel, Coq, LogiCal, ProVal, TypiCal projects (since 1985), +- INRIA Formel, Coq, LogiCal, ProVal, TypiCal, Marelle, pi.r2 projects + (starting 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. + associated to CNRS and university Paris Sud (since Sep. 1997), +- Laboratoire d'Informatique de l'Ecole Polytechnique (LIX) + associated to CNRS and Ecole Polytechnique (since Jan. 2003). +- Laboratoire PPS associated to CNRS and university Paris 7 (since Jan. 2009). All files of the "Coq proof assistant" in directories or sub-directories of @@ -14,7 +16,7 @@ All files of the "Coq proof assistant" in directories or sub-directories of 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-2008, +Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2010, The Coq development team, CNRS, INRIA and Université Paris Sud. Files from the directory doc are distributed as indicated in file doc/LICENCE. @@ -32,7 +34,7 @@ plugins/dp developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre (LRI, 2005-2008) plugins/extraction - developed by Pierre Letouzey (LRI, 2000-2004, PPS-Paris7, 2005-now) + developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now) plugins/field developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001) plugins/firstorder @@ -43,13 +45,10 @@ plugins/funind developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2008), Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008) and Yves Bertot (INRIA-Marelle, 2005-2006) -plugins/interface - developed by Yves Bertot with contributions from Loïc Pottier and - Laurence Rideau as part of the Pcoq project (INRIA-Lemme, 1997-2006); - extended by Lionel Mamane as part of the TeXMacs project (Radboud university - at Nijmegen, 2007-2008) plugins/omega developed by Pierre Crégut (France Telecom R&D, 1996) +plugins/groebner + developed by Loïc Pottier (INRIA-Marelle, 2009) plugins/ring developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick Loiseleur (LRI, 1997-1999) @@ -76,40 +75,40 @@ parsing/search.ml mainly 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) -theories/Numbers/Cyclic - developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry - (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and - Pierre Letouzey (PPS-Paris 7, 2008) theories/Strings developed by Laurent Théry (INRIA-Lemme, 2003) +theories/Numbers/Cyclic + developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and Pierre Letouzey (PPS, 2008) ide/utils some files come from Maxence Guesdon's Cameleon tool -Many discussions within the Démons team at LRI, and the -LogiCal/TypiCal projects influenced significantly the design of -components of Coq, especially with +Many discussions within the INRIA teams and labs taking part to the +development influenced the design of Coq especially with - F. Blanqui, J. Courant, P. Courtieu, J. Duprat, S. Glondu, J. Goubault, - A. Mahboubi, C. Marché, A. Miquel, B. Monate, P.-Y. Strub, B. Werner. + C. Auger, Y. Bertot, F. Blanqui, J. Courant, P. Courtieu, J. Duprat, + S. Glondu, J. Goubault, J.-P. Jouannaud, S. Lescuyer, A. Mahboubi, + C. Marché, A. Miquel, B. Monate, L. Pottier, Y. Régis-Gianas, + P.-Y. Strub, L. Théry, B. Werner -Intensive users suggested improvements of the system : +The development of Coq also significantly benefited from feedback, +suggestions or short contributions from: - Y. Bertot, L. Pottier, L. Théry (INRIA-Lemme/Marelle projects), C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D), P. Castéran (University Bordeaux 1), - The Foundations Group (Radboud University, Nijmegen, The Netherlands), + the Foundations Group (Radboud University, Nijmegen, The Netherlands), Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis), - G. Gonthier (INRIA-MSR joint lab), A. Charguéraud (INRIA-Gallium project). + F. Garillot, G. Gonthier (INRIA-MSR joint lab), + INRIA-Gallium project, + the CS dept at Yale, the CIS dept at U. Penn, + the CSE dept at Harvard, the CS dept at Princeton The following people have contributed to the development of different versions -of the Coq Proof assistant during the indicated time : +of the Coq Proof assistant during the indicated time: Bruno Barras (INRIA, 1995-now) Jacek Chrzaszcz (LRI, 1998-2003) Thierry Coquand (INRIA, 1985-1989) - Pierre Corbineau (LRI, 2003-now) + Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-now) Cristina Cornes (INRIA, 1993-1996) Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996) David Delahaye (INRIA, 1997-2002) @@ -122,15 +121,15 @@ of the Coq Proof assistant during the indicated time : Benjamin Grégoire (INRIA, 2003-now) Hugo Herbelin (INRIA, 1996-now) Gérard Huet (INRIA, 1985-1997) - Pierre Letouzey (LRI, 2000-2004 & PPS-Paris 7, 2005-now) + Pierre Letouzey (LRI, 2000-2004 & PPS, 2005-now) Evgeny Makarov (INRIA, 2007) Pascal Manoury (INRIA, 1993) Micaela Mayero (INRIA, 1997-2002) - Claude Marché (INRIA 2003-2004 & LRI, 2004-now) + Claude Marché (INRIA 2003-2004 & LRI, 2004) Benjamin Monate (LRI, 2003) César Muñoz (INRIA, 1994-1995) Chetan Murthy (INRIA, 1992-1994) - Julien Narboux (INRIA, 2005-2006) + Julien Narboux (INRIA, 2005-2006, Strasbourg, 2007-now) Jean-Marc Notin (CNRS, 2006-now) Catherine Parent-Vigouroux (ENS Lyon, 1992-1995) Patrick Loiseleur (Paris Sud, 1997-1999) @@ -146,12 +145,14 @@ of the Coq Proof assistant during the indicated time : Benjamin Werner (INRIA, 1989-1994) *************************************************************************** -INRIA refers to : +INRIA refers to: Institut National de la Recherche en Informatique et Automatique -CNRS refers to : +CNRS refers to: Centre National de la Recherche Scientifique -LRI refers to : Laboratoire de Recherche en Informatique, UMR 8623 +LRI refers to: Laboratoire de Recherche en Informatique, UMR 8623 CNRS and Université Paris-Sud -ENS Lyon refers to : +ENS Lyon refers to: Ecole Normale Supérieure de Lyon +PPS refers to: Laboratoire Preuve, Programmation, Système, UMR 7126, + CNRS and Université Paris 7 **************************************************************************** diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 736627122..8ec3c2e7f 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -691,6 +691,83 @@ Palaiseau, June 2008\\ Hugo Herbelin\\ \end{flushright} +\section*{Credits: version 8.3} + +{\Coq} version 8.3 is before all a transition version with refinements +or extensions of the existing features and libraries and a new tactic +{\tt gb} based on Hilbert's Nullstellensatz for deciding systems of +equations over rings. + +With respect to libraries, the main evolutions are due to Pierre +Letouzey with a rewriting of the library of finite sets {\tt FSets} +and a new round of evolutions in the modular development of arithmetic +(library {\tt Numbers}). The reason for making {\tt FSets} evolve is +that the computational and logical contents were quite intertwined in +the original implementation, leading in some cases to longer +computations than expected and this problem is solved in the new {\tt + MSets} implementation. As for the modular arithmetic library, it was +only dealing with the basic arithmetic operators in the former version +and its current extension adds the standard theory of the division, +min and max functions, all made available for free to any +implementation of $\mathbb{N}$, $\mathbb{Z}$ or +$\mathbb{Z}/n\mathbb{Z}$. + +The main other evolutions of the library are due to Hugo Herbelin who +made a revision of the sorting library (includingh a certified +merge-sort) and to Guillaume Melquiond who slightly revised and +cleaned up the library of reals. + +The module system evolved significantly. Besides the resolution of +some efficiency issues and a more flexible construction of module +types, Élie Soubiran brought a new model of name equivalence, the +$\Delta$-equivalence, which respects as much as possible the names +given by the users. He also designed with Pierre Letouzey a new +convenient operator \verb!<+! for nesting functor application, what +provides a light notation for inheriting the properties of cascading +modules. + +The new tactic {\tt gb} is due to Loïc Pottier. It works by computing +Gr\"obner bases what explains its name. Regarding the existing +tactics, various improvements have been done by Matthieu Sozeau, Hugo +Herbelin and Pierre Letouzey. + +Matthieu Sozeau extended and refined the type classes and {\tt + Program} features (the {\sc Russell} language). Pierre Letouzey +maintained and improved the extraction mechanism. Bruno Barras and +\'Elie Soubiran maintained the Coq checker, Julien Forest maintained +the {\tt Function} mechanism for reasoning over recursively defined +functions. Matthieu Sozeau, Hugo Herbelin and Jean-Marc Notin +maintained {\tt coqdoc}. Frédéric Besson maintained the {\sc + Micromega} plateform for deciding systems of inequalities. Pierre +Courtieu maintained the support for the Proof General Emacs +interface. Claude Marché maintained the plugin for calling external +provers ({\tt dp}). Yves Bertot made some improvements to the +libraries of lists and integers. Matthias Puech improved the search +functions. Guillaume Melquiond usefully contributed here and +there. Yann Régis-Gianas grounded the support for Unicode on a more +standard and more robust basis. + +Though invisible from outside, Arnaud Spiwack improved the general +process of management of existential variables. Pierre Letouzey and +Stéphane Glondu improved the compilation scheme of the Coq archive. +Vincent Gross provided support to CoqIDE. Jean-Marc Notin provided +support for benchmarking and archiving. + +Many users helped by reporting problems, providing patches, suggesting +improvements or making useful comments, either on the bug tracker or +on the Coq-club mailing list. This includes but not exhaustively +Cédric Auger, Arthur Charguéraud, François Garillot, Georges Gonthier, +Robin Green, Stéphane Lescuyer, Eelis van der Weegen,~... + +Though not directly related to the implementation, special thanks are +going to Yves Bertot, Pierre Castéran, Adam Chlipala, and Benjamin +Pierce for the excellent teaching materials they provided. + +\begin{flushright} +Paris, April 2010\\ +Hugo Herbelin\\ +\end{flushright} + %new Makefile %\newpage @@ -698,6 +775,8 @@ Hugo Herbelin\\ % Integration of ZArith lemmas from Sophia and Nijmegen. +% $Id$ + %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" -- cgit v1.2.3