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?
Algorithmic type checking for Calculus of Inductive Constructions
reference request;lambda calculus;type theory;type checking;coq
The problem of giving an algorithmic reading to the typing rules in CIC, and dependent type systems in general, is quite subtle.One recommendation is Randy Pollack's Typechecking in Pure Type Systems, Gille Barthe's Type Checking *Injective Pure Type Systems and McKinna and Pollack's Pure Type Systems formalized.The first basic idea is to push the conversion rule$$ \frac{\Gamma \vdash t: A\quad A\simeq B}{\Gamma\vdash t : B}$$into the application rule$$ \frac{\Gamma \vdash t:A\quad \Gamma\vdash u:A' \quad A\simeq \Pi x: A'.B}{\Gamma\vdash t\ u:B\{x\mapsto u\}}$$And similarly for application-like rules. The theorem is that these modified rules suffice for type-checking (without conversion), with the exception of a possible single application of conversion at the end.This makes the rules type-directed, which allows a straightforward implementation. There are additional shortcuts which allow skipping verification of $\mathrm{WF}$, for example, if it is known that it is going to be derived later, or it is admissible.As Luke notes, there is no complete treatment of such shortcuts, and the validity of these is sometimes quite complicated to prove (e.g. the expansion postponement rule).Checking conversion of terms with $\delta$-reductions (defined functions) is a whole bag of worms: when checking$$ f\ t_1\ldots t_n\simeq f\ u_1\ldots u_n$$should you just check $t_i\simeq u_i$ for each $i$, or unfold $f$? The answer is, unsurprisingly, it depends. In general clever heuristics are used, e.g. unfold $f$ if it is a projection, otherwise try checking equivalence of the arguments, and unfold $f$ if that fails.