Parameter-free polymorphic types

DOI10.1016/J.APAL.2008.06.002MaRDI QIDQ958481zbMATH OpenOpenAlexFDO

Authors Klaus Aehlig

Publication date 5 December 2008

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2008.06.002

zbMATH Keywords

inductive definitions lambda calculus polymorphism second-order arithmetic types

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Second- and higher-order arithmetic and fragments (03F35)

Review text

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.

Recommendations

Cites work

Cited in

(10)

This page was built for publication: Parameter-free polymorphic types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q958481)