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 条
  • [1] ECC, AN EXTENDED CALCULUS OF CONSTRUCTIONS
    LUO, ZH
    FOURTH ANNUAL SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, 1989, : 386 - 395
  • [2] Inductive types in the calculus of algebraic constructions
    Blanqui, F
    TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2003, 2701 : 46 - 59
  • [3] Inductive types in the calculus of algebraic constructions
    Blanqui, F
    FUNDAMENTA INFORMATICAE, 2005, 65 (1-2) : 61 - 86
  • [4] Inductive Types Deconstructed The Calculus of United Constructions
    Monnier, Stefan
    TYDE '19: PROCEEDINGS OF THE 4TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON TYPE-DRIVEN DEVELOPMENT, 2019, : 52 - 63
  • [5] A Calculus of Inductive Linear Constructions
    Fu, Qiancheng
    Xi, Hongwei
    PROCEEDINGS OF THE 8TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON TYPE-DRIVEN DEVELOPMENT, TYDE 2023, 2023, : 1 - 13
  • [6] Gradualizing the Calculus of Inductive Constructions
    Lennon-Bertrand, Meven
    Maillard, Kenji
    Tabareau, Nicolas
    Tanter, Eric
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2022, 44 (02):
  • [7] Inductive Consequences in the Calculus of Constructions
    Walukiewicz-Chrzaszcz, Daria
    Chrzaszcz, Jacek
    INTERACTIVE THEOREM PROVING, PROCEEDINGS, 2010, 6172 : 450 - 465
  • [8] On the formalization of the modal μ-calculus in the calculus of inductive constructions
    Miculan, M
    INFORMATION AND COMPUTATION, 2001, 164 (01) : 199 - 231
  • [9] Constructor subtyping in the Calculus of Inductive Constructions
    Barthe, G
    van Raamsdonk, F
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, 2000, 1784 : 17 - 34
  • [10] Formalization of CTL in calculus of inductive constructions
    Tsai, Ming-Hsien
    Wang, Bow-Yaw
    ADVANCES IN COMPUTER SCIENCE - ASIAN 2006: SECURE SOFTWARE AND RELATED ISSUES, 2007, 4435 : 316 - 330
12345