Nicolas Tabareau

Registered user since Fri 25 May 2018

Name:Nicolas Tabareau

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.

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


POPL 2023 Committee Member in Program Committee within the POPL-track
Author of Impredicative Observational Equality within the POPL-track
ICFP 2022 Author of A Reasonably Gradual Type Theory within the ICFP Papers and Events-track
ML 2022 Author of Extraction to OCaml from Coq: Operational Correctness Verified in Coq within the ML-track
POPL 2022 Author of Observational Equality: Now for Good within the POPL-track
Panelist of Panel 1: proof assistants for PL and math within the Virtual Workshop-track
POPL 2021 Author of The Taming of the Rew: A Type Theory with Computational Assumptions within the POPL-track
CPP 2021 Author of Gradualizing the Calculus of Inductive Constructions within the Lightning Talks-track
ICFP 2020 Committee Member in External Review Committee within the ICFP Program-track
CPP 2020 Committee Member in Program Committee within the CPP 2020-track
POPL 2020 Author of The Fire Triangle: How to Mix Substitution, 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
ICFP 2019 Author of A Reasonably Exceptional Type Theory within the Research Papers-track
POPL 2019 Session 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
CPP 2019 Author of Eliminating Reflection from Type Theory within the CPP 2019-track
ICFP 2018 Author 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
CoqPL 2018 Author of Typed Template Coq within the -track
PriSC 2018 Author of Foundations of Dependent Interoperability within the PriSC 2018-track
POPL 2017 ERC member in External Review Committee within the POPL-track
CoqPL 2017 Invited Speaker of Invited Talk -- Managing Logical and Computational Complexity using Program Transformations within the CoqPL 2017-track
CPP 2017 Author of The Next 700 Syntactical models of type theory within the CPP-track
ICFP 2016 Author of Partial Type Equivalences for Verified Dependent Interoperability within the Research Papers-track
DLS 2015 Author of Gradual Certified Programming in Coq within the DLS-track