Algorithmic type checking for Calculus of Inductive Constructions

Question

So from reading "Advanced Topics in Types and Programming Languages" (ATTPL) I know of the calculus of constructions (CoC). It also presents the "algorithmic" type checking rules. Reading Coq's documentation on the Calculus of Inductive Constructions (CioC) you can get a sense of things but it is far from algorithmic. Is there any reference on algorithmic type checking for CioC?