From 402bfbb2a0da64eba62cb9e7c0e8ace1330879ea Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 16 Aug 2017 13:35:30 +0200 Subject: Update CREDITS on a best-effort basis. And with help from https://github.com/coq/coq/graphs/contributors --- CREDITS | 41 ++++++++++++++++++++++++++++++----------- 1 file changed, 30 insertions(+), 11 deletions(-) (limited to 'CREDITS') diff --git a/CREDITS b/CREDITS index c6848648e..95ca5685a 100644 --- a/CREDITS +++ b/CREDITS @@ -7,7 +7,10 @@ The "Coq proof assistant" was jointly developed by 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). +- Laboratoire PPS associated to CNRS and University Paris Diderot + (Jan. 2009 - Dec. 2015). +- Institut de Recherche en Informatique Fondamentale (IRIF), + associated to CNRS and University Paris Diderot (since Jan. 2016). All files of the "Coq proof assistant" in directories or sub-directories of @@ -15,8 +18,8 @@ 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-2010, -The Coq development team, CNRS, INRIA and Université Paris Sud. +Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2017, +The Coq development team, INRIA, CNRS, LIX, LRI, PPS. Files from the directory doc are distributed as indicated in file doc/LICENCE. @@ -37,8 +40,8 @@ plugins/firstorder plugins/fourier developed by Loïc Pottier (INRIA-Lemme, 2001) plugins/funind - developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2008), - Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008) + developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2006-now), + Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008, ENSIIE, 2008-now) and Yves Bertot (INRIA-Marelle, 2005-2006) plugins/omega developed by Pierre Crégut (France Telecom R&D, 1996) @@ -60,7 +63,7 @@ plugins/ssrmatching plugins/subtac developed by Matthieu Sozeau (LRI, 2005-2008) plugins/micromega - developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some + developed by Frédéric Besson (IRISA/INRIA, 2006-now), with some extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and interface to the csdp solver uses code from John Harrison (University of Cambridge, 1998) @@ -94,32 +97,41 @@ of the Coq Proof assistant during the indicated time: Bruno Barras (INRIA, 1995-now) Yves Bertot (INRIA, 2000-now) - Pierre Boutillier (INRIA-PPS, 2010-now) + Pierre Boutillier (INRIA-PPS, 2010-2015) Xavier Clerc (INRIA, 2012-2014) + Tej Chajed (MIT, 2016-now) Jacek Chrzaszcz (LRI, 1998-2003) Thierry Coquand (INRIA, 1985-1989) Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-2011) Cristina Cornes (INRIA, 1993-1996) Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996) + Pierre Courtieu (CNAM, 2006-now) David Delahaye (INRIA, 1997-2002) Maxime Dénès (INRIA, 2013-now) - Daniel de Rauglaudre (INRIA, 1996-1998) + Daniel de Rauglaudre (INRIA, 1996-1998, 2012, 2016) Olivier Desmettre (INRIA, 2001-2003) Gilles Dowek (INRIA, 1991-1994) Amy Felty (INRIA, 1993) Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-2008) + Emilio Jesús Gallego Arias (MINES ParisTech 2015-now) + Gaetan Gilbert (INRIA-CoqHoTT 2016-now) Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998) Stéphane Glondu (INRIA-PPS, 2007-2013) Benjamin Grégoire (INRIA, 2003-2011) + Jason Gross (MIT 2013-now) Hugo Herbelin (INRIA, 1996-now) Sébastien Hinderer (INRIA, 2014) Gérard Huet (INRIA, 1985-1997) + Matej Košík (INRIA, 2015-2017) Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS, 2009-now) Patrick Loiseleur (Paris Sud, 1997-1999) Evgeny Makarov (INRIA, 2007) + Gregory Malecha (Harvard University 2013-2015, + University of California, San Diego 2016) + Cyprien Mangin (INRIA-IRIF, 2015-now) Pascal Manoury (INRIA, 1993) - Micaela Mayero (INRIA, 1997-2002) Claude Marché (INRIA, 2003-2004 & LRI, 2004) + Micaela Mayero (INRIA, 1997-2002) Guillaume Melquiond (INRIA, 2009-now) Benjamin Monate (LRI, 2003) César Muñoz (INRIA, 1994-1995) @@ -129,7 +141,8 @@ of the Coq Proof assistant during the indicated time: Catherine Parent-Vigouroux (ENS Lyon, 1992-1995) Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997, LRI, 1997-2006) - Pierre-Marie Pédrot (INRIA-PPS, 2011-now) + Pierre-Marie Pédrot (INRIA-PPS, 2011-2015, INRIA-CoqHoTT 2015-2016, + University of Ljubljana 2016-2017) Matthias Puech (INRIA-Bologna, 2008-2011) Yann Régis-Gianas (INRIA-PPS, 2009-now) Clément Renard (INRIA, 2001-2004) @@ -138,9 +151,15 @@ of the Coq Proof assistant during the indicated time: Vincent Siles (INRIA, 2007) Élie Soubiran (INRIA, 2007-2010) Matthieu Sozeau (INRIA, 2005-now) - Arnaud Spiwack (INRIA, 2006-now) + Arnaud Spiwack (INRIA-LIX-Chalmers University, 2006-2010, + INRIA, 2011-2014, MINES ParisTech 2014-2015, + Tweag/IO 2015-now) + Paul Steckler (MIT 2016-now) Enrico Tassi (INRIA, 2011-now) + Amin Timany (Katholieke Universiteit Leuven, 2017) Benjamin Werner (INRIA, 1989-1994) + Nickolai Zeldovich (MIT 2014-2016) + Théo Zimmermann (INRIA-IRIF, 2015-now) *************************************************************************** INRIA refers to: -- cgit v1.2.3