Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant - Chlipala (IEEE, 2003)