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 (http://gallinette.inria.fr/). 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:http://tabareau.fr

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

Contributions

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