13 citations · 17 across the 5 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
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…
cs.LO2026
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…
cs.LO2019★ 2 cited
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…