Chlipala, A. An Introduction to Programming and Proving With Dependent Types in Coq. JFR 2010, 3, 1-93.