Domain-free pure type systems
Domain-free pure type systems
复制标题
无域纯类型系统
DOI：
--
复制
发表时间：
1997
影响因子：
1.1
通讯作者：
M. Sørensen
中科院分区：
文献类型：
--
作者：
G. Barthe;M. Sørensen
纯类型系统使用域全λ抽象λx: dm我们提出了一种纯类型系统的变体，我们称之为无域纯类型系统，它具有无域λ-抽象λx.M。与纯类型系统和所谓的类型分配系统相比，无域纯类型系统有许多优点（它们也有一些缺点），并且在理论开发和证明辅助实现中都有使用。研究了无域纯类型系统的基本性质，建立了它们与纯类型系统和类型赋值系统的形式关系，并给出了这些对应关系的一些应用。
Pure type systems make use of domain-full λ-abstractions λx:D.M. We present a variant of pure type systems, which we call domain-free pure type systems, with domain-free λ-abstractions λx.M. Domain-free pure type systems have a number of advantages over both pure type systems and so-called type assignment systems (they also have some disadvantages), and have been used in theoretical developments as well as in implementations of proof-assistants. We study the basic properties of domain-free pure type systems, establish their formal relationship with pure type systems and type assignment systems, and give a number of applications of these correspondences.