There are video lectures with the author covering this book at a fast pace from this year's Oregon PL summer school (bottom of the page): http://www.cs.uoregon

There are video lectures with the author covering this book at a fast pace from this year's Oregon PL summer school (bottom of the page): http://www.cs.uoregon.edu/Research/summerschool/summer12/curriculum.html http://www.cs.uoregon.edu/Research/summerschool/summer12/cur... I've read the first chapter and it's very good, I highly recommend working through the literate Coq files in Proof General, if you're familiar enough with Emacs. It's a pretty cool environment.