Certified Programming with Dependent Types
A handbook to the Coq software for writing and checking mathematical proofs, with a practical engineering focus.