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