Gonthier, G., & Mahboubi, A. (2010). An introduction to small scale reflection in Coq. Journal of Formalized Reasoning, 3(2), 95–152. https://doi.org/10.6092/issn.1972-5787/1979