55 citations · 97 across the 13 of their papers we have counts for
4 papers · 1 filter
An extensible equality checking algorithm for dependent type theories
Andrej Bauer, Anja Petković Komel
We present a general and user-extensible equality checking algorithm that is applicable to a large class of type theories. The algorithm has a type-directed phase for applying exte…
What is algebraic about algebraic effects and handlers?
Andrej Bauer
This note recapitulates and expands the contents of a tutorial on the mathematical theory of algebraic effects and handlers which I gave at the Dagstuhl seminar 18172 "Algebraic ef…
Design and Implementation of the Andromeda Proof Assistant
Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter +2
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromed…
The HoTT Library: A formalization of homotopy type theory in Coq
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine +3
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including un…