Functional interpretation and inductive definitions
arXiv:0802.1938
Abstract
Extending Gödel's \emph{Dialectica} interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.
minor corrections and changes