THE EXTENDED CALCULUS OF CONSTRUCTIONS (ECC) WITH INDUCTIVE TYPES

被引：6
|
作者：
ORE, CE
机构：
[1] Department of Computer Science, University of Oslo
来源：
INFORMATION AND COMPUTATION | 1992年 / 99卷 / 02期
关键词：
D O I：
10.1016/0890-5401(92)90031-A
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Luo's Extended Calculus of Constructions (ECC) is a higher order functional calculus based on Coquand's and Huet's Calculus of Constructions, but has in addition strong sums and a predicative cumulative type hierarchy. In this paper I introduce inductive types on the predicative type levels of ECC. I also show how the ω-Set model for ECC can be extended to a model for this augmented calculus. © 1992.
引用
收藏
页码：231 / 264
页数：34
相关论文
共 50 条
12345