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