Relational Semantics for Recursive Types and Bounded Quantification
Relational Semantics for Recursive Types and Bounded Quantification
复制标题
递归类型和有界量化的关系语义
DOI：
--
复制
发表时间：
1989
期刊：
影响因子：
--
通讯作者：
F. Cardone
中科院分区：
文献类型：
--
作者：
F. Cardone
语言FUN[Cardelli，Wegner，1985]是一种类型化的多态Lambda演算，具有记录类型、在给定类型的子类型上进行量化和继承。本文用递归类型对其进行扩展，并通过构造其类型的解释为一种特殊类型的部分等价关系来证明结果语言的一致性，术语被解释为非类型化术语的底层语言模型的元素的等价类，对这种关系进行模运算。
The language Fun [Cardelli, Wegner, 1985] is a typed polymorphic lambda calculus with record types, quantification over subtypes of a given type and inheritance. In this paper it is extended with recursive types, and the consistency of the resulting language is proved by constructing an interpretation of its types as partial equivalence relations of a special kind, terms being interpreted as equivalence classes, modulo such relations, of elements of a model of the underlying language of untyped terms.