Nicolas Tabareau
where else to find them
website:http://tabareau.fr
github:tabareau
what they talk about
all 5 in the filters
where they keep going back
all 6 in the filters
on a stage with
all 21 in the filters
who talks about the same things
- Éric Tanter12 talks
- Kenji Maillard11 talks
- Théo Winterhalter14 talks
- Matthieu Sozeau14 talks
- Loïc Pujet6 talks
- Ondřej Lhoták11 talks
| title | conference | date |
|---|---|---|
| Nested Inductive Types for Rocq and Lean | RocqPL 2026 | 2026-01-17 |
Nested nested inductive types like RoseTree now get a syntactic check that classifies well behaved cases and rejects ones that rely on reduction tricks… | ||
| Business Meeting | CPP 2026 | 2026-01-12 |
Conference sees 178 registrations, the highest yet; program runs from 75 submissions with 27 accepted (about 36%), up from 51 last year. Review process uses a… | ||
| Bounded Sort Polymorphism with Elimination Constraints | POPL 2026 | 2026-01-11 |
Extends sort polymorphism with elimination constraints that record which sorts may eliminate into which, implements the system in the Rocq prover, and proves… | ||
| Incremental Certified Programming | OOPSLA 2025 | 2025-10-16 |
Claims a formal framework that makes specifications monotone over partial programs by defining a completion refinement relation and a notion of completeness… | ||
| Robust Dynamic Embedding for Gradual Typing | ICFP 2025 | 2025-10-12 |
Defines Robust Dynamic Embedding as a new adequacy criterion: if a dynamic component semantically satisfies a static type then its embedding ascribed to that… | ||
| Business Meeting | CPP 2025 | 2025-01-20 |
About 51 papers are submitted and 20 accepted this year, reviewed by 32 PC members with 26 external reviewers and two months for reviews and rebuttals; reviews… | ||
| All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants | POPL 2025 | 2025-01-19 |
Adds a principled sort quantifier that generalizes Prop, Type, and SProp and is implemented in Coq with a new sort-polymorphic prelude that replaces duplicated… | ||
| Verified Extraction from Coq to OCaml | PLDI 2024 | 2024-06-24 |
A verified extraction pipeline implemented in Coq proves that programs over first‑order inductive data types extracted from Coq safely interoperate with OCaml… | ||
| Impredicative Observational Equality | POPL 2023 | 2023-01-15 |
Extends observational TTobs with an impredicative universe of definitionally proof‑irrelevant types and implements transport via a type‑casting/observational… | ||
| A Reasonably Gradual Type Theory | ICFP 2022 | 2022-09-11 |
Presents GRIP, an extension of CastCIC that is normalizing and a conservative extension of CIC, and that internalizes precision so graduality can be proven for… | ||
| Proof Assistants for PL and Math | POPL 2022 Virtual Workshop | 2022-01-27 |
Panel reports active, practical work: large libraries (Lean + mathlib, ~700k LOC) and successful formalizations (including the four‑color style project and… | ||
| Observational Equality: Now for Good | POPL 2022 | 2022-01-16 |
TTobs extends MLTT with a proof-irrelevant universe and an observational equality that satisfies function and propositional extensionality plus UIP while… | ||
| The Taming of the Rew: A Type Theory with Computational Assumptions | POPL 2021 | 2021-01-17 |
Rewriting Type Theory lets users add user-defined rewrite rules as computational assumptions that the type checker applies automatically, not as… | ||
| The Taming of the Rew: A Type Theory with Computational Assumptions | POPL 2021 | 2021-01-17 |
Adds Rewriting Type Theory to dependently typed systems so user-supplied rewrite rules run automatically during typechecking instead of requiring explicit… | ||
| nothing matches | ||