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