Awesome

MPCTT Textbook Project

Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant
Gert Smolka

pdf
Coq