Parameter-free polymorphic types
type: Item
instance of: scholarly article
title: Parameter-free polymorphic types
zbMATH Open document ID: 1156.03012
author: Klaus Aehlig
published in: Annals of Pure and Applied Logic
publication date: 2008-12-05T00:00:00Z
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.
reviewed by: Martin W. Bunder
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03F35
zbMATH DE Number: 5378321
zbMATH Keywords: lambda calculus
zbMATH Keywords: types
zbMATH Keywords: polymorphism
zbMATH Keywords: second-order arithmetic
zbMATH Keywords: inductive definitions
MaRDI profile type: Publication
full work available at URL: j.apal.2008.06.002
OpenAlex ID: W2046193889
cites work: Induction and inductive definitions in fragments of second order arithmetic
cites work: Q2778814
cites work: On the computational content of the axiom of choice
cites work: Handbook of proof theory
cites work: Q4215632
cites work: Q3997016
cites work: Q4720069
cites work: Q4215633
cites work: Q4068054
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
DOI: 10.1016/J.APAL.2008.06.002
description: scientific article; zbMATH DE number 5378321