ECC, an extended calculus of constructions
- 7 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 386-395
- https://doi.org/10.1109/lics.1989.39193
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 omega -set (realizability) model is described to show how the essential properties of the calculus can be captured set-theoretically.Keywords
This publication has 14 references indexed in Scilit:
- A categorical semantics of constructionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Combinatory reduction systems: introduction and surveyTheoretical Computer Science, 1993
- On Functors Expressible in the Polymorphic Typed Lambda CalculusInformation and Computation, 1993
- A small complete categoryAnnals of Pure and Applied Logic, 1988
- Pebble, a kernel language for modules and abstract data typesInformation and Computation, 1988
- The calculus of constructionsInformation and Computation, 1988
- The system F of variable types, fifteen years laterTheoretical Computer Science, 1986
- Proof theory and set theorySynthese, 1985
- Abstract types have existential typesPublished by Association for Computing Machinery (ACM) ,1985
- Structured theories in LCFPublished by Springer Nature ,1983