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 Bedrock Systems, 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