2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/31322A 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.16 pages; correctionsLogic in Computer ScienceF.4.1; F.2.2text