Thomas Lamiaux
where else to find them
what they talk about
where they keep going back
no series more than once — all 3 in the filters
on a stage with
- Ambroise Lafontonce
- Anders Mörtbergonce
- Axel Ljungströmonce
all 7 in the filters
who talks about the same things
nobody close enough yet
| 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… | ||
| 2-Functoriality of Initial Semantics, and Applications | ICFP 2025 | 2025-10-12 |
Shows that initial semantics, when parametrized by the monoidal category of contexts, is 2-functorial: a monoidal functor or adjunction between base categories… | ||
| Computing Cohomology Rings in Cubical Agda | CPP 2023 | 2023-01-16 |
Claims a first fully mechanized, constructive definition of cohomology rings implemented in Cubical Agda, with concrete computations for spheres and the Klein… | ||
| nothing matches | ||