2 papers
math.LO2020
A general definition of dependent type theories
Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine
We define a general class of dependent type theories, encompassing Martin-Löf's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and…
cs.LO2018
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…