Extended Calculus of Constructions

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 F_\omega.

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 \textsf{Prop} of propositions. This is closed under impredicative quantification: for any x : A \vdash P : \textsf{Prop}, we have

  \vdash \forall x : A.\ P : \textsf{Prop}

This universe of propositions itself is a member of a universe of types, i.e.

\vdash \textsf{Prop} : \textsf{Type}_0

And there is a further cumulative hierarchy of universes, i.e.

\vdash \textsf{Type}_i : \textsf{Type}_{i+1}

Each of the \textsf{Type}_i universes are closed under \Pi and \Sigma type formers.

However, the propositional universe \textsf{Prop} is only closed under impredicative quantification (and Luo uses the \Pi notation for that too). The usual logical functions on propositions are defined impredicatively, as in CC.

References

@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}
}