An Elementary Fragment of Second-Order Lambda Calculus
| dc.creator | Aehlig, Klaus | |
| dc.creator | Johannsen, Jan | |
| dc.date | 2002-10-25 | |
| dc.date | 2004-03-18 | |
| dc.date.accessioned | 2026-07-07T03:18:57Z | |
| dc.date.available | 2026-07-07T03:18:57Z | |
| dc.description | 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. | |
| dc.description | 16 pages; corrections | |
| dc.identifier | https://arxiv.org/abs/cs/0210022 | |
| dc.identifier | http://arxiv.org/abs/cs/0210022 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/31322 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | F.4.1; F.2.2 | |
| dc.title | An Elementary Fragment of Second-Order Lambda Calculus | |
| dc.type | text |