The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping
The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping
复制标题
使用交叉类型绑定器和子类型扩展纯类型系统的构造的隐式演算
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Alexandre Miquel
中科院分区：
文献类型：
--
作者：
Alexandre Miquel
在本文中，我们引入了一个新的类型系统，即构造的隐式计算，这是我们通过添加相交类型粘合剂来扩展的构造的咖喱式变体，与隐式依赖性产品不同。类型分配系统，隐式产品可以在宇宙层次结构中的每个地方使用。我们还以一种自然的方式来说明构造的特殊性，通过重新审视构造的命令性的编码，我们证明它们转化为隐式计算有助于反映基础术语的计算含义。
In this paper, we introduce a new type system, the Implicit Calculus of Constructions, which is a Curry-style variant of the Calculus of Constructions that we extend by adding an intersection type binder— called the implicit dependent product. Unlike the usual approach of Type Assignment Systems, the implicit product can be used at every place in the universe hierarchy. We study syntactical properties of this calculus such as the βη-subject reduction property, and we show that the implicit product induces a rich subtyping relation over the type system in a natural way. We also illustrate the specificities of this calculus by revisitting the impredicative encodings of the Calculus of Constructions, and we show that their translation into the implicit calculus helps to reflect the computational meaning of the underlying terms in a more accurate way.