معرفی
Nicolas Tabareau is a researcher at Inria, France, and leads the Gallinette team (http://gallinette.inria.fr/). His work focuses on enhancing tools for formal proof verification in computer science and mathematics.
- Research Interests: Proof Assistants, Homotopy Type Theory, Semantics of Programming Languages, Category Theory
Tabareau's publications span type theory, gradual typing, and formal verification using Coq. His recent work (2025) explores gradual typing extensions and proof-irrelevant type systems. Earlier contributions (2024–2015) address OCaml extraction correctness, inductive types, and computational assumptions in proof assistants.
He actively participates in conference program committees (CPP, ICFP, POPL) and has presented at workshops (CoqPL, PriSC) and symposia (LAFI, PADL). No scientific awards or part-time affiliations are mentioned in the provided data.
