Chlipala, A. 2010. An Introduction to Programming and Proving with Dependent Types in Coq. Journal of Formalized Reasoning. 3, 2 (Jan. 2010), 1–93. DOI:https://doi.org/10.6092/issn.1972-5787/1978.