The Coq mailing list

[t x <txrev319 AT gmail.com>]

Now, assuming it's (c), where can I read up on the mathematical foundations of this? [I've looked through chapters in Coq d'Art, but it's not clear if it's defined in the book.]

If by "mathematical foundations," you mean e.g. how to prove logical soundness at the meta level, then you'll need research papers and PhD dissertations and so forth.  If you just mean how to understand the behavior of the Coq type checker, then the CPDT section whose title you've cited should be exhaustive.

I think I understand the one rule of dependent type matching now -- however, I'd really like to implement it to be sure. Are you aware of any tutorials that does "dependent type checking + inductive types" ? (no need for co-inductive types). I feel like working through an actual implementation would truly verify my understanding.