Benedikt Ahrens
where else to find them
what they talk about
where they keep going back
- CPP2 editions2022–2024
all 4 in the filters
on a stage with
all 9 in the filters
who talks about the same things
- Andreas Abel6 talks
- Vlad Patryshev11 talks
- Ambroise Lafont3 talks
- Andrei Popescu5 talks
- Nicolas Tabareau14 talks
- James McKinna2 talks
| title | conference | date |
|---|---|---|
| From Semantics to Syntax: A Type Theory for Comprehension Categories | POPL 2026 | 2026-01-11 |
Defines a syntax CCT that internalizes the previously unused vertical morphisms of comprehension categories and proves that any comprehension category with the… | ||
| 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… | ||
| Displayed Monoidal Categories for the Semantics of Linear Logic | CPP 2024 | 2024-01-15 |
Formalized a reusable library of monoidal-category constructions in UniMath using new displayed monoidal categories that let complicated monoidal structures be… | ||
| Univalent Double Categories | CPP 2024 | 2024-01-15 |
Formalization builds two equivalent definitions of double categories: an unfolded explicit version and a structured version using two-sided displayed… | ||
| Formalizing Monoidal Categories and Actions for Syntax with Binders | CoqPL 2023 | 2023-01-21 |
Mechanization of syntax with binders uses Coq + UniMath to formalize semantic signatures, initial algebras, monad-like substitution and the notion of strength… | ||
| Implementing a category-theoretic framework for typed abstract syntax | CPP 2022 | 2022-01-17 |
Mechanized extension of the UniMath/Coq framework produces simply‑typed syntax from signatures by generalizing signatures to non‑endofunctors, extending the… | ||
| nothing matches | ||