Pierre-Marie Pédrot
where else to find them
no profile links on file
what they talk about
where they keep going back
no series more than once — all 2 in the filters
on a stage with
all 9 in the filters
who talks about the same things
- Kenji Maillard11 talks
- Matthieu Sozeau14 talks
- Nicolas Tabareau14 talks
- Éric Tanter12 talks
- Théo Winterhalter14 talks
- Lionel Parreaux19 talks
| title | conference | date |
|---|---|---|
| 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… | ||
| Martin-Löf à la Coq | CPP 2024 | 2024-01-15 |
A Coq formalization of Martin-Löf Type Theory (MLTT) that mechanizes its metatheory and proves decidability of conversion and of type checking using… | ||
| nothing matches | ||