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?
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.