Constructor Subtyping in the Calculus of Inductive Constructions
Constructor Subtyping in the Calculus of Inductive Constructions
复制标题
归纳构造微积分中的构造函数子类型
DOI：
10.1007/3-540-46432-8_2
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
F. Raamsdonk
中科院分区：
文献类型：
--
作者：
G. Barthe;F. Raamsdonk
归纳构造演算（CIC）是一个强大的类型系统，具有依赖类型和归纳定义，构成了Coq和Lego等证明辅助系统的基础。我们用构造子类型来扩展CIC，这是子类型的一种基本形式，其中归纳类型σ被视为另一个归纳类型τ的子类型，如果τ比σ有更多的元素。结果表明，演算是良好的行为，并提供了一个合适的基础，形式化的自然语义证明开发系统。
The Calculus of Inductive Constructions (CIC) is a powerful type system, featuring dependent types and inductive definitions, that forms the basis of proof-assistant systems such as Coq and Lego. We extend CIC with constructor subtyping, a basic form of subtyping in which an inductive typeσis viewed as a subtype of another inductive typeτifτhas more elements thanσ. It is shown that the calculus is well-behaved and provides a suitable basis for formalizing natural semantics in proof-development systems.