Parameter-free polymorphic types (Q958481)

This paper concerns a fragment of the polymorphically typed \(\lambda\)-calculus (Girand's System F) in which, in every type \(\forall \alpha . \tau\), the variable \(\alpha\) is the only free variable in \(\tau\). The lambda terms with types in this fragment Aehlig shows to be exactly the functions provably recursive by finitely iterated inductive definitions. He also shows that this fragment has the same strength as a fragment of second-order arithmetic that he has previously studied. Proofs in the second-order arithmetic can be interpreted as \(\lambda\)-terms computing the function claimed to exist.