Nicolas Tabareau
Inria Senior Researcher
Head of the Gallinette team



Current Projects

  • CoqExtra (PI, 2020-2024), founded by Nomadic Labs.

What I'm interested in

  • Proof Assistant (Coq)
  • (Homotopy) Type Theory
  • Category theory
  • Semantics for low level languages
  • Cognitive Science
  • Aspect Oriented Programming


Here is a list of softwares/developments I have co-developed:
  • Forcing for Coq - An extension of Coq that integrates forcing. It enables in particular to use general inductive types with Coq.
  • Aspect JoCaml - A distributed aspect calculus based on JoCaml.
  • Strid - A string diagram generator.

PhD Students

Here is a list of my past/current PhD students.


Here is a list of my past/current post-docs and engineers.
  • Benedikt Ahrens: (2015-2017) Now assistant professor at Delft University of Technology, The Netherlands, and Birmingham Fellow.
  • Pierre-Marie Pédrot: (2016-2018) Now Inria Research Scientist, Gallinette team, Nantes.
  • Danil Annenkov: (2017-2018) Now Senior Scientist at Concordium.
  • Pierre Vial: (2018-2019) Now Software Engineer at Formal Land.
  • Maxime Lucas: (2018-2019) Now Software Engineer at SYSNAV.
  • Simon Boulier: (2018-2019) Now working on a biodynamic farming project.
  • Kenji Maillard (2020-2022): Now Inria Starting Faculty Position, Gallinette team, Nantes.
  • Yannick Forster: (2021-2023) Marie Skłodowska-Curie fellow, Now Inria Research Scientist, Cambium team, Paris.
  • Kazuhiko Sakaguchi: (2022-now) Working on correct extraction from Coq to Ocaml.
  • Koen Jacobs: (2022-now) Working on gradual type systems.


PhD thesis

"Modalités de ressource et contrôle en logique tensorielle", Université Denis Diderot - Paris VII (03/12/2008), Paul-André Melliès (Dir.)


The manuscrit of my HDR is available here


  • Rosemont/Demassieux PhD thesis award in applied and fundamental mathematics from La Chancellerie des Universités de Paris, 2009
  • Second Gilles Kahn PhD thesis award from the Société des Personnels Enseignants et Chercheurs en Informatique de France (specif), 2009


Where to contact me

My Office Address: 11-213
Campus de la Faculté des Sciences
2 Chem. de la Houssinière
44300 Nantes

My email :