Chiarabini, L.; Danvy, O. A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration. JFR 2011, 4, 85-109.