Type Assignment for Intersections and Unions in Call-by-Value Languages
Type Assignment for Intersections and Unions in Call-by-Value Languages
复制标题
值调用语言中交集和并集的类型分配
DOI：
10.1007/3-540-36576-1_16
复制
发表时间：
2003
影响因子：
0.6
通讯作者：
F. Pfenning
中科院分区：
文献类型：
--
作者：
Jana Dunfield;F. Pfenning
我们开发了一个系统的类型分配与交叉类型，联合类型，索引类型，通用和存在依赖类型，是声音的调用值函数语言。逻辑和计算原则的结合，我们的配方自然导致的中心思想的类型检查子项的评估顺序。因此，我们提供了一个统一的概括和解释几个早期的孤立系统。进步和类型保持的证明，通常只针对封闭项，依赖于确定替换的概念。
We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional language. The combination of logical and computational principles underlying our formulation naturally leads to the central idea of type-checking subterms in evaluation order. We thereby provide a uniform generalization and explanation of several earlier isolated systems. The proof of progress and type preservation, usually formulated for closed terms only, relies on a notion of definite substitution.