单例类型和证明无关性的类型论的模块化类型检测算法
A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
摘要：
我们定义了一个具有单例类型和一个小类型的逻辑框架。我们给出的语义使用PER模型，它是用于构建一个规范化的评估算法。我们证明了算法的完备性和可靠性，并作为推论得到了类型构造函数的内射性。在此基础上，我们给出了一个范式项的正确的、完备的类型检验算法的定义。我们扩展的结果证明无关的命题。
英文摘要：
We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation-by-evaluation algorithm. We prove completeness and soundness of the algorithm; and get as a corollary the injectivity of type constructors. Then we give the definition of a correct and complete type-checking algorithm for terms in normal form. We extend the results to proof-irrelevant propositions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
