相依类型论的规范性与正规化
Canonicity and normalisation for Dependent Type Theory
摘要：
我们显示规范性和规范化的依赖类型论的累积序列的宇宙和布尔类型。这个论点遵循了还原论的通常概念，可以追溯到哥德尔的辩证法解释和泰特的工作。我们的方法的一个关键特征是使用证明相关的概念还原。
英文摘要：
We show canonicity and normalization for dependent type theory with a cumulative sequence of universes and a type of Boolean. The argument follows the usual notion of reducibility, going back to Godel's Dialectica interpretation and the work of Tait. A key feature of our approach is the use of a proof relevant notion of reducibility.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
