Chiarabini, L. and Danvy, O. (2011) “A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration”, Journal of Formalized Reasoning, 4(1), pp. 85–109. doi: 10.6092/issn.1972-5787/2225.