论文标题
依赖类型理论的一般定义
A general definition of dependent type theories
论文作者
论文摘要
我们定义了一类依赖类型理论，其中包括Martin-Löf的直觉类型理论，变体和扩展。主要目的是务实：统一和组织他们的研究，允许在合理的一般性中给出结果和结构，而不仅仅是针对特定理论。与其他方法相比，我们的定义更接近直接或幼稚的语法阅读，从而尽可能接近传统的特定理论。 具体而言，我们给出了三个主要定义：原始类型理论，一种最小的设置，用于讨论相关类型的衍生性。可接受的类型理论，包括额外的条件，确保行为良好；以及良好的类型理论，概括了在传统演示中，随着类型理论的建立，如何逐步建立了类型理论的良好行为。在这些之后，我们表明，各种基本的适应性属于这种通用性。 目前的大部分工作都是在证明助理Coq中正式化的。
We define a general class of dependent type theories, encompassing Martin-Löf's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and organise their study, allowing results and constructions to be given in reasonable generality, rather than just for specific theories. Compared to other approaches, our definition stays closer to the direct or naive reading of syntax, yielding the traditional presentations of specific theories as closely as possible. Specifically, we give three main definitions: raw type theories, a minimal setup for discussing dependently typed derivability; acceptable type theories, including extra conditions ensuring well-behavedness; and well-presented type theories, generalising how in traditional presentations, the well-behavedness of a type theory is established step by step as the type theory is built up. Following these, we show that various fundamental fitness-for-purpose metatheorems hold in this generality. Much of the present work has been formalised in the proof assistant Coq.
