Quadratic type checking for objective type theory

02/01/2021
by   Benno van den Berg, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset