Nicolas Tabareau

Registered user since Fri 25 May 2018

Name: Nicolas Tabareau

Bio: Nicolas Tabareau is a junior researcher at Inria, head of the Gallinette team ( He conducts research on programming languages and proof assistants in order to provide better tools for proofs formalization both to computer scientists and mathematicians.

Country: France

Affiliation: Inria

Personal website:

Research interests: proof assistant, (Homotopy) Type Theory, Semantics of Programming Languages, Category theory


CPP 2020Committee Member in Program Committee within the CPP 2020-track
POPL 2020Author of The Fire Triangle: How to Mix Substitutions, Dependent Elimination and Effects within the Research Papers-track
Author of Coq Coq Correct: Verification of Type Checking and Erasure for Coq, in Coq within the Research Papers-track
CPP 2019Author of Eliminating Reflection from Type Theory within the CPP 2019-track
POPL 2019Session Chair of Categories (part of Research Papers)
Committee Member in Program Committee within the Research Papers-track
Author of Definitional Proof-Irrelevance without K within the Research Papers-track
ICFP 2019Author of A Reasonably Exceptional Type Theory within the Research Papers-track
CoqPL 2018Author of Typed Template Coq within the -track
PriSC 2018Author of Foundations of Dependent Interoperability within the PriSC 2018-track
ICFP 2018Author of Equivalences for Free: Univalent Parametricity for Effective Transport within the Research Papers-track
Committee Member in External Review Committee within the Research Papers-track
CPP 2017Author of The Next 700 Syntactical models of type theory within the CPP-track
CoqPL 2017Invited speaker of Invited Talk -- Managing Logical and Computational Complexity using Program Transformations within the CoqPL 2017-track
POPL 2017ERC member in External Review Committee within the POPL-track
ICFP 2016Author of Partial Type Equivalences for Verified Dependent Interoperability within the Research Papers-track
DLS 2015Author of Gradual Certified Programming in Coq within the DLS-track