客观类型论的二次类型检验
Quadratic type checking for objective type theory
摘要：
我们介绍了一个修改的标准马丁-洛夫类型论中，我们消除定义的等式，并取代所有的计算规则的命题等式。我们表明，这样一个系统的类型检查可以在二次时间，它有一个自然的同伦理论语义。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
