# Strong Normalization of Extended Calculus of Constructions (CC with cumulative universes)

There are some proofs around to prove the strong normalization of the calculus of constructions (i.e. that all type systems in the lambda cube are strongly normalizing). I have analyzed the proof available from Herman Geuvers which is not an easy read, but understandable.

I am interested in proof of strong normalization of calculi like CC which have cumulative universes i.e. which have sorts $$\text{sort} ::= * \mid \Box_i \quad 0 \le i,$$ allow subtyping $$\begin{array}{c} \Gamma \vdash t : T \\ T \le U \\ \hline \Gamma \vdash t : U \end{array}$$ where $$\le$$ is based on the ordering of sorts $$* < \Box_0 < \Box_1 \ldots$$

and the typing rules are practically the same as for pure type systems where $$*$$ is impredicative and all $$\Box_i$$ are predicative.

A simple generalization of the proof of Herman Geuvers does not work because it heavily depends on a distinction between kinds and types and objects and type constructors (based on having only two sorts $$*$$ and $$\Box$$ and no cumulativity).

I have searched a lot but I cannot find a comprehensible proof of strong normalization. This is strange because this type system is a subset of the type system of Coq which is in use for several decades now and supposedly strongly normalizing.

Can anybody give hints to understandable proofs of such type systems?

Thanks for any hint.

From the first comment of Cody I conclude that there might be no easier to grasp proofs than the proof in Zhaohui Luo's Phd thesis which I already have but it is a big bullet to bite.

I don't need the full power of cumulative universes, but the calculus of constructions is not sufficient for me, because I have to make a Coq like split between propositions and "normal" types. Is there a way to generalize the proof of strong normalization of CoC to such a type system?

Furthermore a proof of strong normalization would be nice, but a proof of weak normalization would be sufficient at least to make type checking decidable. Is there a simpler proof for weak normalization for systems with cumulative universes?. But, of course, this does not prove that the system is sound (i.e. free of contradictions) which is a major drawback.

• A first hint: the normalization of this system is notoriously hard to prove, and unfortunately there probably is no easy to read proof. A second hint: check Luo's phd dissertation: era.lib.ed.ac.uk/bitstream/handle/1842/12487/… – cody Dec 9 '18 at 16:12