Course at UPenn (in contrast with the non-coq version in 2006)
Recommended Introductory Scripts
Adam Chlipala's dissertation on Certified Programming
Math in Coq (Also see the author's homepage)
Comparing mathematical provers in proving the irrationality of sqrt(2)
A Comparison of the Coq and HOL Proof Systems for Specifying Hardware
Course at Technische Universiteit Eindhoven (2006)
Summer Schools at Radboud University Nijmegen
Course at New South Wales 2004, 2005
Course on Automated TP at San Diego
An Example Theorem Prover in Haskell
Djinn (darcs get --partial http://darcs.augustsson.net/Darcs/Djinn/)