An Elementary Fragment of Second-Order Lambda Calculus
<|reference_start|>An Elementary Fragment of Second-Order Lambda Calculus: 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.<|reference_end|>
@article{aehlig2002an,
    title={An Elementary Fragment of Second-Order Lambda Calculus},
    author={Klaus Aehlig, Jan Johannsen},
    journal={arXiv preprint arXiv:cs/0210022},
    year={2002},
    archivePrefix={arXiv},
    eprint={cs/0210022},
    primaryClass={cs.LO}
}