Inria ERC

Nicolas Tabareau
Inria Researcher (CR1)
Head of the Gallinette team



Current Projects

  • ERC Starting Grant CoqHoTT (PI, 2015-2020)
  • GECO associate team / CSEC Conicyt project (Chile) (2018-2020)

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.


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


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

I may be available @ IMT Atlantique or @ University of Nantes
If you want to be sure to find me there, it is better to contact me first by email.

My email :