72 citations · 159 across the 26 of their papers we have counts for
29 papers
Verification of a DPLL Transition System in Rocq
Julia Dijkstra, Benedikt Ahrens
We present a formal verification of an abstract transition-system presentation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure in the Rocq proof assistant. Following Nieuwen…
Rzk: a Proof Assistant for Synthetic -Categories
Nikolai Kudasov, Violetta Sim, Benedikt Ahrens
Homotopy type theory (HoTT) is a type theory that allows for synthetic reasoning about -groupoids. Several proof assistants (such as Rocq and Agda) implement variants of Ho…
Substitution for Non-Wellfounded Syntax with Binders through Monoidal Categories
Ralph Matthes, Kobe Wullaert, Benedikt Ahrens
We describe a generic construction of non-wellfounded syntax involving variable binding and its monadic substitution operation. Our construction of the syntax and its substitution…
Formalizing Monoidal Categories and Actions for Syntax with Binders
Benedikt Ahrens, Ralph Matthes, Kobe Wullaert
We discuss some aspects of our work on the mechanization of syntax and semantics in the UniMath library, based on the proof assistant Coq. We focus on experiences where Coq (as a t…
Univalent Monoidal Categories
Kobe Wullaert, Ralph Matthes, Benedikt Ahrens
Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories an…
Category Theory for Programming
Benedikt Ahrens, Kobe Wullaert
In these lecture notes, we give a brief introduction to some elements of category theory. The choice of topics is guided by applications to functional programming. Firstly, we stud…
Univalent foundations and the equivalence principle
Benedikt Ahrens, Paige Randall North
In this paper, we explore the 'equivalence principle' (EP): roughly, statements about mathematical objects should be invariant under an appropriate notion of equivalence for the ki…
Bicategorical type theory: semantics and syntax
Benedikt Ahrens, Paige Randall North, Niels van der Weide
We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is…
The solutions to single-variable polynomials, implemented and verified in Lean
Nicholas Dyson, Benedikt Ahrens, Jacopo Emmenegger
In this work, we describe our experience in learning the use of a computer proof assistant - specifically, Lean - from scratch, through proving formulae for the solutions of polyno…
Implementing a Category-Theoretic Framework for Typed Abstract Syntax
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
In previous work ("From signatures to monads in UniMath"), we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library bas…
Algebraic Presentations of Type Dependency
Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North +1
C-systems were defined by Cartmell as the algebraic structures that correspond exactly to generalised algebraic theories. B-systems were defined by Voevodsky in his quest to formul…
The Univalence Principle
Benedikt Ahrens, Paige Randall North, Michael Shulman +1
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based,…
A Higher Structure Identity Principle
Benedikt Ahrens, Paige Randall North, Michael Shulman +1
The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant und…
Reduction Monads and Their Signatures
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont +1
In this work, we study 'reduction monads', which are essentially the same as monads relative to the free functor from sets into multigraphs. Reduction monads account for two aspect…
Modular specification of monads through higher-order presentations
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont +1
In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To…
Bicategories in Univalent Foundations
Benedikt Ahrens, Dan Frumin, Marco Maggesi +2
We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent…
Presentable signatures and initial semantics
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont +1
We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we study a notion of "signature" for specifyi…
Categorical structures for type theory in univalent foundations
Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categori…
Displayed Categories
Benedikt Ahrens, Peter LeFanu Lumsdaine
We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D and functor F : D --> C", but instead of having…
From signatures to monads in UniMath
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core depend…
Non-wellfounded trees in Homotopy Type Theory
Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
We prove a conjecture about the constructibility of coinductive types - in the principled form of indexed M-types - in Homotopy Type Theory. The conjecture says that in the presenc…
Terminal semantics for codata types in intensional Martin-Löf type theory
Benedikt Ahrens, Régis Spadotti
In this work, we study the notions of relative comonad and comodule over a relative comonad, and use these notions to give a terminal coalgebra semantics for the coinductive type f…
Univalent categories and the Rezk completion
Benedikt Ahrens, Chris Kapulkin, Michael Shulman
We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this syst…
Initial Semantics for Reduction Rules
Benedikt Ahrens
We give an algebraic characterization of the syntax and operational semantics of a class of simply-typed languages, such as the language PCF: we characterize simply-typed syntax wi…