Frontends
Books
- Interactive Theorem Proving and Program Development aka Coq'Art (2004) by Yves Bertot and Pierre Castéran (Goodreads)
- Software Foundations (2011+) by Benjamin C. Pierce et al. (Goodreads)
- Certified Programming with Dependent Types (2013) by Adam Chlipala (PDF, Goodreads)
- Mathematical Components (2015+) by Assia Mahboubi and Enrico Tassi (PDF)
- Software Foundations: Verified Functional Algorithms (2017+) by Andrew W. Appel
Tutorials
Video Tutorials
- Introduction to the Coq Proof Assistant by Andrew Appel
- Video tutorials for the Coq proof assistant by Andrej Bauer