Greetings. Can anyone give me a link to a proof of strongly or weakly normalization of Calculus of Inductive Constructions (CIC) and a proof of consistency strength of CIC? I use the word “CIC” as the system presented in “Inductively defined types” by Coquand, Paulin in 1990. Similar questions ar…

Proof on normalization of CIC and its consistency

Blaisorblade September 24, 2019, 5:48pm 2

Topic		Replies	Views
Does proof of coq consistency need axiom of choice? Miscellaneous	3	1083	February 6, 2020
Coq's Cumulativity Miscellaneous	2	68	June 22, 2024
A Question on Defining Mutually Inductive Types with Universe Polymorphism Using Coq	2	49	August 12, 2024
Why is Coq consistent? What is the intended semantics? Miscellaneous faq	21	3864	September 27, 2019
Strong specification of haskell's Replicate function Using Coq	1	901	May 23, 2021