Benedikt Ahrens

According to our database, Benedikt Ahrens authored at least 40 papers between 2010 and 2025.

Collaborative distances:

• Dijkstra number of five.
• Erdős number of four.

2025

Insights from Univalent Foundations: A Case Study Using Double Categories.

Nima Rasekh, Niels van der Weide, Benedikt Ahrens, Paige Randall North

Proceedings of the 33rd EACSL Annual Conference on Computer Science Logic, 2025

2024

An Introduction to Different Approaches to Initial Semantics.

Thomas Lamiaux, Benedikt Ahrens

CoRR, 2024

Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories.

Ralph Matthes, Kobe Wullaert, Benedikt Ahrens

Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, 2024

Univalent Double Categories.

Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

Displayed Monoidal Categories for the Semantics of Linear Logic.

Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories.

Benedikt Ahrens, Peter LeFanu Lumsdaine, Paige Randall North

Proceedings of the Programming Languages and Systems - 22nd Asian Symposium, 2024

2023

Bicategorical type theory: semantics and syntax.

Benedikt Ahrens, Paige Randall North, Niels van der Weide

Math. Struct. Comput. Sci., 2023

Substitution for Non-Wellfounded Syntax with Binders.

Ralph Matthes, Kobe Wullaert, Benedikt Ahrens

CoRR, 2023

Formalizing Monoidal Categories and Actions for Syntax with Binders.

Benedikt Ahrens, Ralph Matthes, Kobe Wullaert

CoRR, 2023

2022

Category Theory for Programming.

Benedikt Ahrens, Kobe Wullaert

CoRR, 2022

Univalent foundations and the equivalence principle.

Benedikt Ahrens, Paige Randall North

CoRR, 2022

The solutions to single-variable polynomials, implemented and verified in Lean.

Nicholas Dyson, Benedikt Ahrens, Jacopo Emmenegger

CoRR, 2022

Univalent Monoidal Categories.

Kobe Wullaert, Ralph Matthes, Benedikt Ahrens

Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

Semantics for two-dimensional type theory.

Benedikt Ahrens, Paige Randall North, Niels van der Weide

Proceedings of the LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2, 2022

Implementing a category-theoretic framework for typed abstract syntax.

Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

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

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

Bicategories in univalent foundations.

Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide

Math. Struct. Comput. Sci., 2021

Presentable signatures and initial semantics.

Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi

Log. Methods Comput. Sci., 2021

The Univalence Principle.

Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis

CoRR, 2021

2020

Reduction monads and their signatures.

Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi

Proc. ACM Program. Lang., 2020

A Higher Structure Identity Principle.

Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

2019

Displayed Categories.

Benedikt Ahrens, Peter LeFanu Lumsdaine

Log. Methods Comput. Sci., 2019

Initial Semantics for Reduction Rules.

Benedikt Ahrens

Log. Methods Comput. Sci., 2019

From Signatures to Monads in UniMath.

Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

J. Autom. Reason., 2019

Modular Specification of Monads Through Higher-Order Presentations.

Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi

Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

Bicategories in Univalent Foundations.

Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide

Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

2018

Categorical structures for type theory in univalent foundations.

Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky

Log. Methods Comput. Sci., 2018

High-Level Signatures and Initial Semantics.

Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi

Proceedings of the 27th EACSL Annual Conference on Computer Science Logic, 2018

2016

Modules over relative monads for syntax and semantics.

Benedikt Ahrens

Math. Struct. Comput. Sci., 2016

Some Wellfounded Trees in UniMath - Extended Abstract.

Benedikt Ahrens, Anders Mörtberg

Proceedings of the Mathematical Software - ICMS 2016, 2016

2015

Univalent categories and the Rezk completion.

Benedikt Ahrens, Krzysztof Kapulkin, Michael Shulman

Math. Struct. Comput. Sci., 2015

Initiality for Typed Syntax and Semantics.

Benedikt Ahrens

J. Formaliz. Reason., 2015

Heterogeneous Substitution Systems Revisited.

Benedikt Ahrens, Ralph Matthes

Proceedings of the 21st International Conference on Types for Proofs and Programs, 2015

Non-Wellfounded Trees in Homotopy Type Theory.

Benedikt Ahrens, Paolo Capriotti, Régis Spadotti

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

2014

Coinitial semantics for redecoration of triangular matrices.

Benedikt Ahrens, Régis Spadotti

CoRR, 2014

Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory.

Benedikt Ahrens, Régis Spadotti

Proceedings of the 20th International Conference on Types for Proofs and Programs, 2014

2012

Extended Initiality for Typed Abstract Syntax

Benedikt Ahrens

Log. Methods Comput. Sci., 2012

2011

Initial Semantics for higher-order typed syntax in Coq.

Benedikt Ahrens, Julianna Zsido

J. Formaliz. Reason., 2011

2010

Initial Semantics for higher-order typed syntax

Benedikt Ahrens, Julianna Zsido

CoRR, 2010