## Paper: Stratified polymorphism (at LICS 1989)

**Daniel Leivant**

### Abstract

The author considers a spectrum of predicative type abstraction disciplines based on type quantification with stratified levels.
These lie in the vast middle ground between parametric abstraction and full impredicative abstraction. Stratified polymorphism
has an attractive, unproblematic semantics, and has the potential of offering new approaches to type inference, without sacrificing
useful expressive power. He shows that the functions representable in the finitely stratified λ-calculus are precisely the
superelementary functions, i.e., E_{4} in A. Grzegorczyk's (Rozprawy Mate. IV, Warsaw, 1953) subrecursive hierarchy. He also defines methods of transfinite stratification
and shows that stratification up to ω^{ω} has a simple finitary representation, making it a potentially useful concept in programming language design. The author proves
that the functions represented by stratified polymorphism up to ω^{ω} are precisely the primitive recursive functions. He points out that these results imply that the equality problem for finitely
stratified λ-calculus is not superelementary, and that the equality problem for the calculus stratified up to ω^{ω} is not primitive recursive

### BibTeX

@InProceedings{Leivant-Stratifiedpolymorph, author = {Daniel Leivant}, title = {Stratified polymorphism}, booktitle = {Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 1989)}, year = {1989}, month = {June}, pages = {39--47}, location = {Pacific Grove, CA, USA}, publisher = {IEEE Computer Society Press} }