I recently started working through the first volume of "Software Foundations" [1] by Pierce et al. If anyone wants to learn Coq with me this summer, feel free to email me at [hn username]@gmail.com :)

[1] https://softwarefoundations.cis.upenn.edu/