The Extended Calculus of Constructions (ECC) is a type theory presented by Zhaohui Luo in his 1990 PhD thesis.
Like Coquand and Huet's calculus of constructions (CC), the ECC tries to combine Martin-Löf type theory with higher-order impredicative polymorphism in the style of System .
However, instead of relying on impredicative encodings of data types - which do not give good induction principles - Luo's ECC stratifies the system further.
At the very bottom of the type hierarchy is an impredicative universe of propositions. This is closed under impredicative quantification: for any , we have
This universe of propositions itself is a member of a universe of types, i.e.
And there is a further cumulative hierarchy of universes, i.e.
Each of the universes are closed under and type formers.
However, the propositional universe is only closed under impredicative quantification (and Luo uses the notation for that too). The usual logical functions on propositions are defined impredicatively, as in CC.
Luo, Zhaohui. 1990. ‘An Extended Calculus of Constructions’. PhD thesis, University of Edinburgh. https://era.ed.ac.uk/handle/1842/12487.
@phdthesis{luo_1990,
type = {{PhD} thesis},
title = {An {Extended} {Calculus} of {Constructions}},
url = {https://era.ed.ac.uk/handle/1842/12487},
school = {University of Edinburgh},
author = {Luo, Zhaohui},
year = {1990}
}