Parameter-free polymorphic types

Consider the following restriction of the polymorphically typed lambda calculus ("System F"). All quantifications are parameter free. In other words, in every universal type ., the quantified variable is the only free variable in the scope of the quantification. This fragment can be locally proven terminating in a system of intuitionistic second-order arithmetic known to have strength of finitely iterated inductive definitions.

• Type: Journal
• Year: 2008
• Where: APAL
• Authors: Klaus Aehlig
• Keywords: APAL 2008, Iterated Inductive Definitions, System F, Typed Lambda Calculus