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