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	1086	February 6, 2020
Coq's Cumulativity Miscellaneous	2	75	June 22, 2024
A Question on Defining Mutually Inductive Types with Universe Polymorphism Using Rocq	2	60	August 12, 2024
Why is Coq consistent? What is the intended semantics? Miscellaneous faq	21	3906	September 27, 2019
Proving existence statements about coinductive types constructively Using Rocq	1	782	August 4, 2020