5 citations · 5 across the 3 of their papers we have counts for
4 papers
An Introduction to Different Approaches to Initial Semantics
Thomas Lamiaux, Benedikt Ahrens
Characterizing programming languages with variable binding as initial objects, was first achieved by Fiore, Plotkin, and Turi in their seminal paper published at LICS'99. To do so,…
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…
Initiality for Typed Syntax and Semantics
Benedikt Ahrens
In this thesis we give an algebraic characterization of the syntax and semantics of simply-typed languages. More precisely, we characterize simply-typed binding syntax equipped wit…