Good description of Calculus of Inductive Construction
You can try the Coq user manual, in particular this section is pretty nice (the server seems to be down at the moment though).

For meta-theory you can try some recent work of Benjamin Werner et al., see Proof-irrelevant model of CC with predicative induction and judgmental equality
 and On the strength of proof-irrelevant type theories for the most salient work.