FUNCTIONAL PROGRAMMING:
FOUNDATIONS AND APPLICATIONS

An Introduction to the Coq Proof Assistant