2002/10/25 by Klaus Aehlig, Aehlig, Klaus, Jan Johannsen +1
Computer Science · Mathematics · #F.2.2 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Mathematical and Theoretical Analysis #cs.LO
paper · pdf · doi:10.48550/arxiv.cs/0210022
16 pages; corrections
openalex publication_date 2002/10/25 · arxiv created 2004/03/18 · arxiv updated 2009/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.