Paper: ECC, an extended calculus of constructions (at LICS 1989)

Authors: Zhaohui Luo

Abstract

A higher-order calculus ECC (extended calculus of constructions) is presented which can be seen as an extension of the calculus of constructions by adding strong sum types and a fully cumulative type hierarchy. ECC turns out to be rather expressive so that mathematical theories can be abstractly described and abstract mathematics may be adequately formalized. It is shown that ECC is strongly normalizing and has other nice proof-theoretic properties. An ω-set (realizability) model is described to show how the essential properties of the calculus can be captured set-theoretically

BibTeX

  @InProceedings{Luo-ECCanextendedcalcul,
    author = 	 {Zhaohui Luo},
    title = 	 {ECC, an extended calculus of constructions},
    booktitle =  {Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 1989)},
    year =	 {1989},
    month =	 {June}, 
    pages =      {386--395},
    location =   {Pacific Grove, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }