Initial Semantics for higher-order typed syntax - Benedikt Ahrens; Julianna Zsido (CoRR, 2010)

Initial Semantics for higher-order typed syntax in Coq. - Benedikt Ahrens; Julianna Zsido (J. Formaliz. Reason., 2011)

Extended Initiality for Typed Abstract Syntax - Benedikt Ahrens (Log. Methods Comput. Sci., 2012)

Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory. - Benedikt Ahrens; Régis Spadotti (TYPES, 2014)

Coinitial semantics for redecoration of triangular matrices. - Benedikt Ahrens; Régis Spadotti (CoRR, 2014)

Non-Wellfounded Trees in Homotopy Type Theory. - Benedikt Ahrens; Paolo Capriotti; Régis Spadotti (TLCA, 2015)

Heterogeneous Substitution Systems Revisited. - Benedikt Ahrens; Ralph Matthes (TYPES, 2015)

Initiality for Typed Syntax and Semantics. - Benedikt Ahrens (J. Formaliz. Reason., 2015)

Univalent categories and the Rezk completion. - Benedikt Ahrens; Krzysztof Kapulkin; Michael Shulman (Math. Struct. Comput. Sci., 2015)

Some Wellfounded Trees in UniMath - Extended Abstract. - Benedikt Ahrens; Anders Mörtberg (ICMS, 2016)

Modules over relative monads for syntax and semantics. - Benedikt Ahrens (Math. Struct. Comput. Sci., 2016)

High-Level Signatures and Initial Semantics. - Benedikt Ahrens; André Hirschowitz; Ambroise Lafont; Marco Maggesi (CSL, 2018)

Categorical structures for type theory in univalent foundations. - Benedikt Ahrens; Peter LeFanu Lumsdaine; Vladimir Voevodsky (Log. Methods Comput. Sci., 2018)

Bicategories in Univalent Foundations. - Benedikt Ahrens; Dan Frumin; Marco Maggesi; Niels van der Weide (FSCD, 2019)

Modular Specification of Monads Through Higher-Order Presentations. - Benedikt Ahrens; André Hirschowitz; Ambroise Lafont; Marco Maggesi (FSCD, 2019)

From Signatures to Monads in UniMath. - Benedikt Ahrens; Ralph Matthes; Anders Mörtberg (J. Autom. Reason., 2019)

Initial Semantics for Reduction Rules. - Benedikt Ahrens (Log. Methods Comput. Sci., 2019)

Displayed Categories. - Benedikt Ahrens; Peter LeFanu Lumsdaine (Log. Methods Comput. Sci., 2019)

A Higher Structure Identity Principle. - Benedikt Ahrens; Paige Randall North; Michael Shulman; Dimitris Tsementzis (LICS, 2020)

Reduction monads and their signatures. - Benedikt Ahrens; André Hirschowitz; Ambroise Lafont; Marco Maggesi (Proc. ACM Program. Lang., 2020)

The Univalence Principle. - Benedikt Ahrens; Paige Randall North; Michael Shulman; Dimitris Tsementzis (CoRR, 2021)

Presentable signatures and initial semantics. - Benedikt Ahrens; André Hirschowitz; Ambroise Lafont; Marco Maggesi (Log. Methods Comput. Sci., 2021)

Bicategories in univalent foundations. - Benedikt Ahrens; Dan Frumin; Marco Maggesi; Niccolò Veltri; Niels van der Weide (Math. Struct. Comput. Sci., 2021)

Preface to the MSCS Issue 31.1 (2021) Homotopy Type Theory and Univalent Foundations. - Benedikt Ahrens; Simon Huber; Anders Mörtberg (Math. Struct. Comput. Sci., 2021)

Preface to the MSCS Issue 31.1 (2021) Homotopy Type Theory and Univalent Foundations - Part II. - Benedikt Ahrens; Simon Huber; Anders Mörtberg (Math. Struct. Comput. Sci., 2021)

Implementing a category-theoretic framework for typed abstract syntax. - Benedikt Ahrens; Ralph Matthes; Anders Mörtberg (CPP, 2022)

Semantics for two-dimensional type theory. - Benedikt Ahrens; Paige Randall North; Niels van der Weide (LICS, 2022)

Univalent Monoidal Categories. - Kobe Wullaert; Ralph Matthes; Benedikt Ahrens (TYPES, 2022)

The solutions to single-variable polynomials, implemented and verified in Lean. - Nicholas Dyson; Benedikt Ahrens; Jacopo Emmenegger (CoRR, 2022)

Univalent foundations and the equivalence principle. - Benedikt Ahrens; Paige Randall North (CoRR, 2022)

Category Theory for Programming. - Benedikt Ahrens; Kobe Wullaert (CoRR, 2022)

Formalizing Monoidal Categories and Actions for Syntax with Binders. - Benedikt Ahrens; Ralph Matthes; Kobe Wullaert (CoRR, 2023)

Substitution for Non-Wellfounded Syntax with Binders. - Ralph Matthes; Kobe Wullaert; Benedikt Ahrens (CoRR, 2023)

Bicategorical type theory: semantics and syntax. - Benedikt Ahrens; Paige Randall North; Niels van der Weide (Math. Struct. Comput. Sci., 2023)

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. - Benedikt Ahrens; Peter LeFanu Lumsdaine; Paige Randall North (APLAS, 2024)

Displayed Monoidal Categories for the Semantics of Linear Logic. - Benedikt Ahrens; Ralph Matthes; Niels van der Weide; Kobe Wullaert (CPP, 2024)

Univalent Double Categories. - Niels van der Weide; Nima Rasekh; Benedikt Ahrens; Paige Randall North (CPP, 2024)

Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories. - Ralph Matthes; Kobe Wullaert; Benedikt Ahrens (FSCD, 2024)

An Introduction to Different Approaches to Initial Semantics. - Thomas Lamiaux; Benedikt Ahrens (CoRR, 2024)

Insights from Univalent Foundations: A Case Study Using Double Categories. - Nima Rasekh; Niels van der Weide; Benedikt Ahrens; Paige Randall North (CSL, 2025)

Algebraic Presentations of Type Dependency. - Benedikt Ahrens; Jacopo Emmenegger; Paige Randall North; Egbert Rijke (Log. Methods Comput. Sci., 2025)

A Unified Framework for Initial Semantics. - Thomas Lamiaux; Benedikt Ahrens (CoRR, 2025)

2-Functoriality of Initial Semantics, and Applications. - Benedikt Ahrens; Ambroise Lafont; Thomas Lamiaux (CoRR, 2025)

A Type Theory for Comprehension Categories with Applications to Subtyping. - Niyousha Najmaei; Niels van der Weide; Benedikt Ahrens; Paige Randall North (CoRR, 2025)

Scott's Representation Theorem and the Univalent Karoubi Envelope. - Arnoud van der Leer; Kobe Wullaert; Benedikt Ahrens (CoRR, 2025)