%0 Journal Article
%T A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration
%A Luca Chiarabini
%A Olivier Danvy
%J Journal of Formalized Reasoning
%D 2011
%I University of Bologna
%X We revisit both the usual ``going-up'' induction principle and Manna and Waldinger's ``going-down'' induction principle for primitive recursion,`a la Goedel, and primitive iteration, `a la Church. We use 'Kleene's trick' to show that primitive recursion and primitive iteration are as expressive as the other, even in the presence of accumulators. As a result, we can directly extract a variety of recursive and iterative functional programs of the kind usually written or optimized by hand.
%U http://jfr.cib.unibo.it/article/view/2225