I often see it asserted that type checking is decidable for CIC, but I haven't seen it proven. Is there a good paper (or simple demonstration) of this?
Proof of decidability of type checking of calculus of (co)inductive constructions?
type theory;decidability;calculus of constructions
I found another reference that goes through a detailed proof of the decidability of typechecking for systems of dependent types up to the CIC:Chapter 2 of Advanced Topics in Types and Programming Languages: Dependent Types, David Aspinall & Martin Hofmann.As you probably know, the proof of decidability is conditional on decidability of $\beta$-equality, which itself is implied by the normalization of the calculus.The proof of that statement is significantly more difficult, partly because it implies consistency of the logical system.