Abstract
We give a finitary normalisation proof for the restriction of system F where we quantify only over first-order type. As an application, the functions representable in this fragment are exactly the ones provably total in Peano Arithmetic. This is inspired by the reduction of ∏11 -comprehension to inductive definitions presented in [Buch2] and this complements a result of [Leiv]. The argument uses a finitary model of a fragment of the system AF2 considered in [Kriv, Leiv]. © Springer-Verlag Berlin Heidelberg 2001.
Cite
CITATION STYLE
Altenkirch, T., & Coquand, T. (2001). A finitary subsystem of the polymorphic λ-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2044 LNCS, pp. 22–28). Springer Verlag. https://doi.org/10.1007/3-540-45413-6_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
