Resources
Coq
- Coq Home Page
- Installation instructions
- Coq reference manual and tactics overview
- Coq Documentation
- Coq Wiki
Books
- Software Foundations (by Benjamin Pierce and others)
- Certified Programming with Dependent Types (by Adam Chlipala), with exercises
- Formal Reasoning About Programs (by Adam Chlipala)
- Mathematical components (the book) (by Assia Mahboubi, Enrico Tassi and others)
Tutorials and other sources
- Type classes tutorial (by Benjamin Pierce)
- Canonical structures for the working user (by Assia Mahboubi and Enrico Tassi)
- The new Coq tactic engine (by Pierre-Marie Pédrot)
- A Gentle Introduction to Type Classes and Relations in Coq (by Pierre Castéran and Matthieu Sozeau)
- Equations package documentation (by Matthieu Sozeau)