Coq Team
Coordinators

YvesBertot
Inria Researcher, Head of the Stamp Team, Sophia-Antipolis, France
Head of the Coq Consortium and the Liber Abaci project
Coq'Art co-author, Function, Plugin-Tutorial, Documentation,
Mathematical Components

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

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

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
, websiteCore Team

ejgallego
Inria Starting Researcher in the Picube Team, Paris, France
RM: 8.12
General Maintenance, Architecture, Frontend, Interfaces, Build System (dune), SerAPI, JSCoq

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

JasonGross
Postdoctoral researcher at MIRI, USA
Stress Testing, Bug Reporting, Bug Minimizer, Compatibility Assurance

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

silene
Inria Researcher in the Toccata Team, Saclay, France
RM: 8.9, 8.14, 8.20
General Maintenance,
vm_compute
, opam, Reals, Coquelicot, Flocq
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

gares
Inria Researcher in the Stamp Team, Sophia-Antipolis, France
RM: 8.13, 8.19
General Maintenance, STM, SSReflect, opam, VSCoq, Mathematical Components, Coq-Elpi, Hierarchy Builder
Maintainers

ana-borges
PhD student at the University of Barcelona, Spain
Signed primitive integers

CohenCyril
Inria Researcher in the Stamp Team, Sophia-Antipolis, France
Opam, Nix, Mathematical Components, Hierarchy Builder

PierreCorbineau
Associate Professor at VERIMAG, Grenoble, France
Decision Procedures (firstorder, cc, rtauto)

Jim Fehrle
jfehrle
Software Engineer in Menlo Park, CA, USA
Documentation, Proof diffs, Ltac debugger

Georges Gonthier
ggonthier
Inria Advanced Researcher in Saclay, France
SSReflect, Mathematical Components, Notations

blaisorblade
Formal Methods Engineer at BlueRock Security, Inc., Berlin, Germany
VsCoq

bgregoir
Inria Researcher in the Stamp Team, Sophia-Antipolis, France
Ring,
vm_compute

amahboubi
Inria Researcher in the Gallinette Team, Nantes, France
Ring, SSReflect, Mathematical Components

erikmd
Associate Professor at IRIT, Toulouse University, France
Primitive Types, Docker, Proof-General

palmskog
Researcher at the KTH Royal Institute of Technology, Stockholm, Sweden
Coq-community manager
coq-community, opam, website, SerAPI, Roosterize

cpitclaudel
Assistant Professor at EPFL, Lausanne, Switzerland
Documentation, Alectryon, SerAPI, Proof-General, Company-Coq

Kazuhiko Sakaguchi
pi8027
Inria Research Engineer in the Gallinette Team, Nantes, France
Coercions, Extraction, Mathematical Components, Hierarchy Builder

Vincent Semeria
VincentSe
Expert Software Developer at Finastra, Paris, France
Reals

Michael Soegtrop
MSoegtropIMC
Coq Platform, Standard Library

Laurent Théry
thery
Inria Researcher in the Stamp Team, Sophia-Antipolis, France
Standard Library, Mathematical Components, VsCoq

Anton Trunov
anton-trunov
Research Engineer at Zilliqa Research, Saint Petersburg, Russia
Standard Library, Build Tools
Past Core Team Members

Professor at the University of Gothenburg, Sweden
Creator (1984), V1-V5
Architecture, Theory, Kernel, Tactics, Proof Engine

Inria Emeritus Researcher, Paris, France
Creator and Head of the Project (1984-1995), V1-V5
Architecture, Theory, Kernel, Universes, Elaboration, Proof Engine

Inria Researcher, Head of the Deducteam Team, Gif-sur-Yvette, France
V4.3-V4.11
Sections, Unification

Professor at the University of Paris-Saclay, France
V4.4-V8, Head of the Project (1995-2006)
Theory, Inductive Types, Kernel, Tactics, Automation

Independent Computer Scientist, San Francisco, CA, USA
V5 Architect (1993)
Architecture, Proof Engine, Extensibility

Operating Officer at ICT4V, Montevideo, Uruguay
V6-7
Theory, (Co)-Inductive types and Guard Checking, Tactics

backtracking
Senior CNRS Researcher, Saclay, France
V5, V6, V7 Architect (1999), V8
General Maintenance, Architecture, Kernel, Tactics, Extraction, Modules, Documentation, Syntax, CoqIDE

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

Inria Researcher at École Polytechnique, Palaiseau, France
Theory, Inductive Types, Proof Irrelevance

delahayd
Professor at the University of Montpellier, France
V6, V7
Search, Autorewrite, Ltac 1 Developer

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)

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