Definitely check out the website for the book, lots of materials there: https://www.cis.upenn.edu/~bcpierce/tapl/index.html
Benjamin Pierce is also the author of Software Foundations: https://softwarefoundations.cis.upenn.edu/
Software Foundations is a book in Coq, where you need to prove theorems to compile the next chapters and such.