Benedikt Ahrens

69 papers A* 2B 12C 1Journal 49Unranked 5
YearRankTypeTitle / Venue / Authors
2026 J jnl
From Semantics to Syntax: A Type Theory for Comprehension Categories.
Proc. ACM Program. Lang.
Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, Paige Randall North
2025 J jnl
2-Functoriality of Initial Semantics, and Applications.
CoRR
Benedikt Ahrens, Ambroise Lafont, Thomas Lamiaux
2025 J jnl
2-Functoriality of Initial Semantics, and Applications.
Proc. ACM Program. Lang.
Benedikt Ahrens, Ambroise Lafont, Thomas Lamiaux
2025 J jnl
A Type Theory for Comprehension Categories with Applications to Subtyping.
CoRR
Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, Paige Randall North
2025 J jnl
A Unified Framework for Initial Semantics.
CoRR
Thomas Lamiaux, Benedikt Ahrens
2025 J jnl
Algebraic Presentations of Type Dependency.
Log. Methods Comput. Sci.
Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North, Egbert Rijke
2025 B conf
Insights from Univalent Foundations: A Case Study Using Double Categories.
CSL
Nima Rasekh, Niels van der Weide, Benedikt Ahrens, Paige Randall North
2025 B conf
Scott's Representation Theorem and the Univalent Karoubi Envelope.
ITP
Arnoud van der Leer, Kobe Wullaert, Benedikt Ahrens
2025 J jnl
Scott's Representation Theorem and the Univalent Karoubi Envelope.
CoRR
Arnoud van der Leer, Kobe Wullaert, Benedikt Ahrens
2024 J jnl
An Introduction to Different Approaches to Initial Semantics.
CoRR
Thomas Lamiaux, Benedikt Ahrens
2024 B conf
Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories.
APLAS
Benedikt Ahrens, Peter LeFanu Lumsdaine, Paige Randall North
2024 J jnl
Comparing semantic frameworks for dependently-sorted algebraic theories.
CoRR
Benedikt Ahrens, Peter LeFanu Lumsdaine, Paige Randall North
2024 B conf
Displayed Monoidal Categories for the Semantics of Linear Logic.
CPP
Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert
2024 B conf
Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories.
FSCD
Ralph Matthes, Kobe Wullaert, Benedikt Ahrens
2024 B conf
Univalent Double Categories.
CPP
Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North
2023 J jnl
Bicategorical type theory: semantics and syntax.
Math. Struct. Comput. Sci.
Benedikt Ahrens, Paige Randall North, Niels van der Weide
2023 J jnl
Formalizing Monoidal Categories and Actions for Syntax with Binders.
CoRR
Benedikt Ahrens, Ralph Matthes, Kobe Wullaert
2023 J jnl
Substitution for Non-Wellfounded Syntax with Binders.
CoRR
Ralph Matthes, Kobe Wullaert, Benedikt Ahrens
2023 J jnl
Univalent Double Categories.
CoRR
Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North
2022 J jnl
Category Theory for Programming.
CoRR
Benedikt Ahrens, Kobe Wullaert
2022 B conf
Implementing a category-theoretic framework for typed abstract syntax.
CPP
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
2022 A* conf
Semantics for two-dimensional type theory.
LICS
Benedikt Ahrens, Paige Randall North, Niels van der Weide
2022 J jnl
Semantics for two-dimensional type theory.
CoRR
Benedikt Ahrens, Paige Randall North, Niels van der Weide
2022 J jnl
The solutions to single-variable polynomials, implemented and verified in Lean.
CoRR
Nicholas Dyson, Benedikt Ahrens, Jacopo Emmenegger
2022 — conf
Univalent Monoidal Categories.
TYPES
Kobe Wullaert, Ralph Matthes, Benedikt Ahrens
2022 J jnl
Univalent Monoidal Categories.
CoRR
Kobe Wullaert, Ralph Matthes, Benedikt Ahrens
2022 J jnl
Univalent foundations and the equivalence principle.
CoRR
Benedikt Ahrens, Paige Randall North
2021 J jnl
Bicategories in univalent foundations.
Math. Struct. Comput. Sci.
Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide
2021 J jnl
Implementing a Category-Theoretic Framework for Typed Abstract Syntax.
CoRR
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
2021 J jnl
Preface to the MSCS Issue 31.1 (2021) Homotopy Type Theory and Univalent Foundations - Part II.
Math. Struct. Comput. Sci.
Benedikt Ahrens, Simon Huber, Anders Mörtberg
2021 J jnl
Preface to the MSCS Issue 31.1 (2021) Homotopy Type Theory and Univalent Foundations.
Math. Struct. Comput. Sci.
Benedikt Ahrens, Simon Huber, Anders Mörtberg
2021 J jnl
Presentable signatures and initial semantics.
Log. Methods Comput. Sci.
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2021 J jnl
The Univalence Principle.
CoRR
Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis
2020 A* conf
A Higher Structure Identity Principle.
LICS
Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis
2020 J jnl
A Higher Structure Identity Principle.
CoRR
Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis
2020 J jnl
Reduction monads and their signatures.
Proc. ACM Program. Lang.
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2019 B conf
Bicategories in Univalent Foundations.
FSCD
Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide
2019 J jnl
Bicategories in Univalent Foundations.
CoRR
Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide
2019 J jnl
Displayed Categories.
Log. Methods Comput. Sci.
Benedikt Ahrens, Peter LeFanu Lumsdaine
2019 J jnl
From Signatures to Monads in UniMath.
J. Autom. Reason.
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
2019 J jnl
Initial Semantics for Reduction Rules.
Log. Methods Comput. Sci.
Benedikt Ahrens
2019 B conf
Modular Specification of Monads Through Higher-Order Presentations.
FSCD
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2019 J jnl
Modular specification of monads through higher-order presentations.
CoRR
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2019 J jnl
Reduction Monads and Their Signatures.
CoRR
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2018 J jnl
Categorical structures for type theory in univalent foundations.
Log. Methods Comput. Sci.
Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky
2018 B conf
High-Level Signatures and Initial Semantics.
CSL
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2018 J jnl
High-level signatures and initial semantics.
CoRR
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
2017 B conf
Categorical Structures for Type Theory in Univalent Foundations.
CSL
Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky
2017 J jnl
Categorical structures for type theory in univalent foundations.
CoRR
Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky
2017 B conf
Displayed Categories.
FSCD
Benedikt Ahrens, Peter LeFanu Lumsdaine
2016 J jnl
From signatures to monads in UniMath.
CoRR
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
2016 J jnl
Heterogeneous substitution systems revisited.
CoRR
Benedikt Ahrens, Ralph Matthes
2016 J jnl
Modules over relative monads for syntax and semantics.
Math. Struct. Comput. Sci.
Benedikt Ahrens
2016 — conf
Some Wellfounded Trees in UniMath - Extended Abstract.
ICMS
Benedikt Ahrens, Anders Mörtberg
2015 — conf
Heterogeneous Substitution Systems Revisited.
TYPES
Benedikt Ahrens, Ralph Matthes
2015 J jnl
Initiality for Typed Syntax and Semantics.
J. Formaliz. Reason.
Benedikt Ahrens
2015 — conf
Non-Wellfounded Trees in Homotopy Type Theory.
TLCA
Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
2015 J jnl
Non-wellfounded trees in Homotopy Type Theory.
CoRR
Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
2015 J jnl
Univalent categories and the Rezk completion.
Math. Struct. Comput. Sci.
Benedikt Ahrens, Krzysztof Kapulkin, Michael Shulman
2014 J jnl
Coinitial semantics for redecoration of triangular matrices.
CoRR
Benedikt Ahrens, Régis Spadotti
2014 — conf
Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory.
TYPES
Benedikt Ahrens, Régis Spadotti
2012 J jnl
Extended Initiality for Typed Abstract Syntax
Log. Methods Comput. Sci.
Benedikt Ahrens
2012 J jnl
Initial Semantics for Reduction Rules
CoRR
Benedikt Ahrens
2012 J jnl
Initiality for Typed Syntax and Semantics
CoRR
Benedikt Ahrens
2012 J jnl
Initiality for Typed Syntax and Semantics
CoRR
Benedikt Ahrens
2012 C conf
Initiality for Typed Syntax and Semantics.
WoLLIC
Benedikt Ahrens
2011 J jnl
Initial Semantics for higher-order typed syntax in Coq.
J. Formaliz. Reason.
Benedikt Ahrens, Julianna Zsido
2011 J jnl
Modules over relative monads for syntax and semantics
CoRR
Benedikt Ahrens
2010 J jnl
Initial Semantics for higher-order typed syntax
CoRR
Benedikt Ahrens, Julianna Zsido