From the 2 of 4 linked papers with an AI index.
4 papers
Verification of a DPLL Transition System in Rocq
Julia Dijkstra, Benedikt Ahrens
The paper formally verifies an abstract DPLL transition system, including its syntax, semantics, and properties like correctness, completeness, and termination, using the Coq proof…
Rzk: a Proof Assistant for Synthetic -Categories
Nikolai Kudasov, Violetta Sim, Benedikt Ahrens
The paper introduces Rzk, a proof assistant that implements a computational variant of Riehl‑Shulman’s simplicial type theory for synthetic reasoning about ∞‑categories, and shows…
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…
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…