An Elementary Fragment of Second-Order Lambda Calculus
Aehlig, Klaus · Johannsen, Jan
Original · EN
A fragment of second-order lambda calculus (System F) is defined that characterizes the elementary recursive functions. Type quantification is restricted to be non-interleaved and stratified, i.e., the types are assigned levels, and a quantified variable can only be instantiated by a type of smaller level, with a slightly liberalized treatment of the level zero.
English translation
This paper has no Arabic translation yet. Be the first: it takes a few seconds, and the result is stored for every future reader.