ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Fourth Annual IEEE Symposium on

Logic in Computer Science (LICS 1989)

Paper: Stratified polymorphism (at LICS 1989)

Authors: Daniel Leivant


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., E4 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


    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}

Last modified: 2022-10-3113:49
Sam Staton