[lexpar]

I took a graduate class where we worked though the first and second volumes of Software Foundations (https://softwarefoundations.cis.upenn.edu/). These are very nice introductions to the Coq environment and are being actively improved. The textbook is available online, with the source file of each chapter being a valid coq script, making it easy to experiment. There are also a large amount of interesting and challenging exercises.

Here's a link to the chapter on the Curry-Howard correspondence: https://softwarefoundations.cis.upenn.edu/lf-current/ProofOb...