Certified Programming with Dependent Types (available online as well http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/) is also a good resource for

Certified Programming with Dependent Types (available online as well http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/) is also a good resource for learning Coq (note: I just started working through the material this weekend).