Loïc Pujet
where else to find them
what they talk about
where they keep going back
on a stage with
all 6 in the filters
who talks about the same things
- Nicolas Tabareau14 talks
- Stephanie Weirich14 talks
- Ondřej Lhoták11 talks
- Lionel Parreaux19 talks
- Jason Z. S. Hu6 talks
- Andreas Abel6 talks
| title | conference | date |
|---|---|---|
| Type Theory in Type Theory using a Strictified Syntax | ICFP 2025 | 2025-10-12 |
They build an isomorphic, substitution strictified initial CwF that encodes substitutions as meta-level functions so all substitution equations become… | ||
| 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… | ||
| 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… | ||
| 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… | ||
| Cubical Synthetic Homotopy Theory | CPP 2020 | 2020-01-20 |
Claims that computational univalence holds and higher inductive types give genuine computation are backed by a Cubical Agda development that redoes standard… | ||
| nothing matches | ||