A. Chlipala, “An Introduction to Programming and Proving with Dependent Types in Coq”, JFR, vol. 3, no. 2, pp. 1–93, Jan. 2010.