Blanchette, J. C., Kaliszyk, C., Paulson, L. C. and Urban, J. (2016) “Hammering towards QED”, Journal of Formalized Reasoning, 9(1), pp. 101–148. doi: 10.6092/issn.1972-5787/4593.