Quadratic type checking for objective type theory
Logic in Computer Science
2021-02-02 v1
Abstract
We introduce a modification of standard Martin-Lof type theory in which we eliminate definitional equality and replace all computation rules by propositional equalities. We show that type checking for such a system can be done in quadratic time and that it has a natural homotopy-theoretic semantics.
Keywords
Cite
@article{arxiv.2102.00905,
title = {Quadratic type checking for objective type theory},
author = {Benno van den Berg and Martijn den Besten},
journal= {arXiv preprint arXiv:2102.00905},
year = {2021}
}