Coq Team

Project Coordinator
Matthieu Sozeau
mattam82
Inria Researcher in the Gallinette Team, Nantes, France
Co-RM: 8.2-8.5
General Maintenance, opam, Theory, Kernel, Elaboration, Unification, Typeclasses, Program, Universes, Equations, MetaCoq

Core Team

Yves Bertot
YvesBertot
Inria Researcher, Head of the Stamp Team, Sophia-Antipolis, France
Head of the Coq Consortium
Coq'Art co-author, Function, Plugin-Tutorial, Documentation, Mathematical Components
Maxime Dénès
maximedenes
Inria Engineer in the Coq Consortium, attached to the Stamp Team, Sophia-Antipolis, France
RM: 8.5, 8.6, 8.7, 8.8, 8.13
General Maintenance, CI, native_compute, Kernel, Unification, VSCoq
Emilio Jesús Gallego Arias
ejgallego
Inria Starting Researcher in the Picube Team, Paris, France
RM: 8.12
General Maintenance, Architecture, Frontend, Interfaces, Build System (dune), SerAPI, JSCoq
Gaëtan Gilbert
SkySkimmer
Inria Engineer in the Coq Consortium, attached to the Gallinette Team, Nantes, France
RM: 8.15
General Maintenance, Theory, CI, Kernel, Universes, SProp, Lean Importer
Jason Gross
JasonGross
Postdoctoral researcher at MIRI, USA
Stress Testing, Bug Reporting, Bug Minimizer, Compatibility Assurance
Hugo Herbelin
herbelin
Inria Researcher in the Picube Team, Paris, France.
Project Coordinator (2006-2016), Co-RM: 8.0-8.5
General Maintenance, Theory, Kernel, Notations, Universes, Elaboration, Unification, Standard Library, Tactics
Guillaume Melquiond
silene
Inria Researcher in the Toccata Team, Saclay, France
RM: 8.9, 8.14
General Maintenance, vm_compute, opam, Reals, Coquelicot, Flocq
Pierre-Marie Pédrot
ppedrot
Inria Researcher in the Gallinette Team, Nantes, France
RM: 8.11, 8.16
General Maintenance, Theory, Performance, Kernel, Elaboration, Universes, Ltac 1/2, Forcing
Pierre Roux
proux01
Researcher at Onera, Toulouse, France
Primitive Types, Notations
Nicolas Tabareau
tabareau
Inria Researcher, Head of the Gallinette Team, Nantes, France
ERC Coq-HoTT PI, Inria-Nomadic Labs CoqExtra
Theory, Universes, SProp
Enrico Tassi
gares
Inria Researcher in the Stamp Team, Sophia-Antipolis, France
RM: 8.13
General Maintenance, STM, SSReflect, opam, VSCoq, Mathematical Components, Coq-Elpi, Hierarchy Builder
Théo Zimmermann
Zimmi48
Associate Professor at Télécom Paris, Institut Polytechnique de Paris, France
RM: 8.7, 8.8, 8.12, 8.17, coq-community manager
Documentation, Community Management, devtools, coqbot, website

Maintainers

Fréderic Besson
fbesson
Inria Researcher in the Celtique Team, Rennes, France
Decision Procedures
Ana de Almeida Borges
ana-borges
PhD student at the University of Barcelona, Spain
Signed primitive integers
Ali Caglayan
alizter
Master student at the University of Gothenburg, Sweden
CoqIDE, CI, Numbers
Tej Chajed
tchajed
Postdoctoral researcher at VMware Research
Ltac 2
Guillaume Claret
clarus
Coq Engineer at Formal Land, Paris, France
Opam, coq-io, opam-bench
Cyril Cohen
CohenCyril
Inria Researcher in the Stamp Team, Sophia-Antipolis, France
Opam, Nix, Mathematical Components, Hierarchy Builder
Pierre Corbineau
PierreCorbineau
Associate Professor at VERIMAG, Grenoble, France
Decision Procedures (firstorder, cc, rtauto)
Pierre Courtieu
Matafou
Associate Professor at CNAM, Paris, France
Function, Proof-General
Andres Erbsen
andres-erbsen
Graduate student at MIT, Boston, USA
Standard Library
Jim Fehrle
Jim Fehrle
jfehrle
Software Engineer in Menlo Park, CA, USA
Documentation, Proof diffs, Ltac debugger
Julien Forest
forestjulien
Associate Professor at ENSIEE/CNAM, Evry/Paris, France
Function
Georges Gonthier
Georges Gonthier
ggonthier
Inria Advanced Researcher in Saclay, France
SSReflect, Mathematical Components, Notations
Paolo G. Giarrusso
blaisorblade
Formal Methods Engineer at Bedrock Systems, Inc., Berlin, Germany
VsCoq
Benjamin Grégoire
bgregoir
Inria Researcher in the Stamp Team, Sophia-Antipolis, France
Ring, vm_compute
Huỳnh Trần Khanh
huynhtrankhanh
Student
VsCoq
Vincent Laporte
vbgl
Inria Researcher in the Pesto Team, Nancy, France
RM: 8.10
Nix, micromega
Olivier Laurent
olaure01
CNRS Researcher in the Plume Team, Lyon, France
Standard library
Assia Mahboubi
amahboubi
Inria Researcher in the Gallinette Team, Nantes, France
Ring, SSReflect, Mathematical Components
Kenji Maillard
kyod
Inria Researcher in the Gallinette Team, Nantes, France
Ltac2
Érik Martin-Dorel
erikmd
Associate Professor at IRIT, Toulouse University, France
Primitive Types, Docker, Proof-General
Karl Palmskog
palmskog
Researcher at the KTH Royal Institute of Technology, Stockholm, Sweden
Coq-community manager
coq-community, opam, website, SerAPI, Roosterize
Clément Pit-Claudel
cpitclaudel
Assistant Professor at EPFL, Lausanne, Switzerland
Documentation, Alectryon, SerAPI, Proof-General, Company-Coq
Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
pi8027
Inria Research Engineer in the Gallinette Team, Nantes, France
Coercions, Extraction, Mathematical Components, Hierarchy Builder
Vincent Semeria
Vincent Semeria
VincentSe
Expert Software Developer at Finastra, Paris, France
Reals
Michael Soegtrop
Michael Soegtrop
MSoegtropIMC
Coq Platform, Standard Library
Arnaud Spiwack
aspiwack
Senior Architect at Tweag, Paris, France
Proof Engine, vm_compute
Laurent Théry
Laurent Théry
thery
Inria Researcher in the Stamp Team, Sophia-Antipolis, France
Standard Library, Mathematical Components, VsCoq
Anton Trunov
Anton Trunov
anton-trunov
Research Engineer at Zilliqa Research, Saint Petersburg, Russia
Standard Library, Build Tools
Li-Yao Xia
Lysxia
Postdoctoral researcher at the University of Edinburgh, Scotland, UK
coqdoc

Past Core Team Members

Thierry Coquand
Professor at the University of Gothenburg, Sweden
Creator (1984), V1-V5
Architecture, Theory, Kernel, Tactics, Proof Engine
Gérard Huet
Inria Emeritus Researcher, Paris, France
Creator and Head of the Project (1984-1995), V1-V5
Architecture, Theory, Kernel, Universes, Elaboration, Proof Engine
Gilles Dowek
Inria Researcher, Head of the Deducteam Team, Gif-sur-Yvette, France
V4.3-V4.11
Sections, Unification
Christine Paulin-Mohring
Professor at the University of Paris-Saclay, France
V4.4-V8, Head of the Project (1995-2006)
Theory, Inductive Types, Kernel, Tactics, Automation
Chetan R. Murthy
Independent Computer Scientist, San Francisco, CA, USA
V5 Architect (1993)
Architecture, Proof Engine, Extensibility
Eduardo Giménez
Operating Officer at ICT4V, Montevideo, Uruguay
V6-7
Theory, (Co)-Inductive types and Guard Checking, Tactics
Jean-Christophe Filliâtre
backtracking
Senior CNRS Researcher, Saclay, France
V5, V6, V7 Architect (1999), V8
General Maintenance, Architecture, Kernel, Tactics, Extraction, Modules, Documentation, Syntax, CoqIDE
Bruno Barras
barras
Inria Researcher in the Deducteam Team, Gif-sur-Yvette, France
V6-V8.4, Co-RM: V8.0-V8.5
General Maintenance, Theory, Architecture, Kernel, Reduction/Conversion, Tactics, Elaboration, Checker, Decision Procedures, Syntax, Coq In Coq
Benjamin Werner
Inria Researcher at École Polytechnique, Palaiseau, France
Theory, Inductive Types, Proof Irrelevance
David Delahaye
delahayd
Professor at the University of Montpellier, France
V6, V7
Search, Autorewrite, Ltac 1 Developer
Pierre Letouzey
letouzey
Associate Professor at IRIF, Paris, France
V7-V8.9, Co-RM: V8.0-V8.5
General Maintenance, Theory, Packaging, Extraction, Tactics, Standard Library (Sets, Number Hierarchy)
Benjamin Monate
monate
Founder & CTO at TrustInSoft, Paris, France
V8
CoqIDE Developer