A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance

A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
复制标题

具有单例类型和证明无关性的类型论模块化类型检查算法

DOI：
--
复制
发表时间：
2009
期刊：
International Conference on Typed Lambda Calculus and Applications
影响因子：
--
通讯作者：
Miguel Pagano
Miguel Pagano
中科院分区：
--
文献类型：
--
作者：
Andreas Abel;T. Coquand;Miguel Pagano

文献摘要

被引文献

相似文献

我们定义了一个逻辑框架，具有单型类型和一个小型宇宙。我们使用每个模型给出语义；它用于构建逐评算法的正常化。我们证明了算法的完整性和健全性；并获得类型构造函数的注入性。然后，我们给出以正常形式的术语的正确且完整的类型检查算法的定义。我们将结果扩展到证明的命题。
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.