Nils Anders Danielsson
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
- Andreas Abelonce
- Eve Gengonce
- Naïm Camille Favieronce
all 5 in the filters
who talks about the same things
- Andreas Abel6 talks
- William J. Bowman13 talks
- Ondřej Lhoták11 talks
- Nicolas Tabareau14 talks
- Éric Tanter12 talks
- Aleksander Boruch-Gruszecki9 talks
| title | conference | date |
|---|---|---|
| Normalisation for First-Class Universe Levels | POPL 2026 | 2026-01-11 |
Proves normalization for a dependent type theory with first-class universe levels and derives decidable equality, decidable type-checking and canonicity; shows… | ||
| A Formalization of Opaque Definitions for a Dependent Type Theory | TyDe 2025 | 2025-10-12 |
Formal development of top-level opaque definitions is mechanized in Agda and proves that adding opacity preserves subject reduction, normalization, consistency… | ||
| A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized | ICFP 2023 | 2023-09-04 |
A graded dependent type theory is formalized in Agda (≈39,000 lines) with Π, weak/strong Σ, Nat, Empty, a universe, and a parameterized semiring‑like modality… | ||
| nothing matches | ||