All coq code and exercises from Software Fundations by Michael Clarkson.
The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.
formal-verification
type-theory
functional-programming
discrete-mathematics