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 pi.r2 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
General Maintenance, Theory, CI, Kernel, Universes, SProp, Lean Importer
Jason Gross
JasonGross
MIT PhD, MA, USA
Stress Testing, Bug Reporting, Bug Minimizer, Compatibility Assurance
Hugo Herbelin
herbelin
Inria Researcher in the pi.r2 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
General Maintenance, Theory, Performance, Kernel, Elaboration, Universes, Ltac 1/2, Forcing
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
Post-Doctoral Researcher in the pi.r2 Team, Paris, France
RM: 8.7, 8.8, 8.12, coq-community manager
Documentation, Community Management, devtools, coqbot, website

Maintainers

Fréderic Besson
fbesson
Inria Researcher in the Celtique Team, Rennes, France
Decision Procedures
Guillaume Claret
clarus
Coq Engineer at Nomadic Labs, Paris, France
opam, coq-io
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
Jim Fehrle
Jim Fehrle
jfehrle
Software Engineer in Menlo Park, CA, USA
Documentation, Proof diffs, Ltac debugger
Julien Forest
forestjulien
Associate Professor at the ENSIEE/CNAM, Evry/Paris, France
Function
Georges Gonthier
Georges Gonthier
ggonthier
Inria Advanced Researcher in Saclay, France
SSReflect, Mathematical Components, Notations
Benjamin Grégoire
bgregoir
Inria Researcher in the Stamp Team, Sophia-Antipolis, France
Ring, vm_compute
Vincent Laporte
vbgl
Inria Researcher in the Pesto Team, Nancy, France
RM: 8.10
Nix, micromega
Assia Mahboubi
amahboubi
Inria Researcher in the Gallinette Team, Nantes, France
Ring, SSReflect, Mathematical Components
É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
PhD Student at MIT, MA, USA
Documentation, Alectryon, SerAPI, Proof-General, Company-Coq
Pierre Roux
proux01
Researcher at Onera, Toulouse, France
Primitive Types
Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
pi8027
PhD Student at the University of Tsukuba, Japan
Coercions, Extraction, Mathematical Components, Hierarchy Builder
Vincent Semeria
Vincent Semeria
VincentSe
Expert Software Developer at Finastra, Paris, France
Reals
Arnaud Spiwack
aspiwack
Senior Architect at Tweag, Paris, France
Proof Engine, vm_compute
Michael Soegtrop
Michael Soegtrop
MSoegtropIMC
Coq Platform, Standard Library
Laurent Théry
Laurent Théry
thery
Inria Researcher in the Stamp Team, Sophia-Antipolis, France
Standard Library, Mathematical Components
Anton Trunov
Anton Trunov
anton-trunov
Research Engineer at Zilliqa Research, Saint Petersburg, Russia
Standard Library, Build Tools
Li-Yao Xia
Lysxia
PhD Student at the University of Pennsylvania, PA, USA
coqdoc

Members at Large

Nicolas Tabareau
tabareau
Inria Researcher, Head of the Gallinette Team, Nantes, France
ERC Coq-HoTT PI, Inria-Nomadic Labs CoqExtra
Theory, Universes, SProp

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 Orsay, 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