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	1031	February 6, 2020
Proving existence statements about coinductive types constructively Using Coq	1	635	August 4, 2020
Indiscernibility of bisimilar coinductive values: can I prove it? Using Coq	9	333	July 12, 2022
Strong specification of haskell's Replicate function Using Coq	1	832	May 23, 2021
Deriving: a library for deriving class instances for inductive types Announcements mathcomp	3	926	October 4, 2021