Intensionality, extensionality, and proof irrelevance in modal type theory
Intensionality, extensionality, and proof irrelevance in modal type theory
复制标题
模态类型理论中的内涵性、外延性和证明无关性
DOI：
10.1109/lics.2001.932499
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
F. Pfenning
中科院分区：
文献类型：
--
作者：
F. Pfenning
我们开发了一种统一的类型理论，该理论将直觉，扩展性和证明无关紧要。任何对象都可以进行直觉处理（仅受/spl alpha/-sconversion），延伸（也要接受/spl beta // spl eta/-conversion），或无关紧要（等于同一类型的任何其他对象），取决于发生的位置。 R. Harper等人开发的模态限制。 （2000年）用于单一类型，并采用了这些类型的概括，以确保对象的这些观点之间的一致性。潜在的应用程序在逻辑框架，功能编程和一阶模态逻辑的基础中。我们的类型理论与先前的方法形成鲜明对比的是，先验，杰出的命题（其证明都是确定的 - 只有它们的存在很重要）（其实现均受到某种定义平等的影响）。
We develop a uniform type theory that integrates intensionality, extensionality and proof irrelevance as judgmental concepts. Any object may be treated intensionally (subject only to /spl alpha/-conversion), extensionally (subject also to /spl beta//spl eta/-conversion), or as irrelevant (equal to any other object at the same type), depending on where it occurs. Modal restrictions developed by R. Harper et al. (2000) for single types are generalized and employed to guarantee consistency between these views of objects. Potential applications are in logical frameworks, functional programming and the foundations of first-order modal logics. Our type theory contrasts with previous approaches that, a priori, distinguished propositions (whose proofs are all identified - only their existence is important) from specifications (whose implementations are subject to some definitional equalities).