Logic in Computer Science (LICS 1999)

Paper: Subtyping Recursive Types in Kernel Fun - Abstract (at LICS 1999)

Authors: Dario Colazzo Giorgio Ghelli

Abstract

The problem of defining and checking a subtype relation between recursive types was studied by Amadio and Cardelli (ACM TOPLAS'93) for a first order type system, but for second order systems, which combine subtyping and parametric polymorphism, only negative results are known (Ghelli, TLCA'93).This paper studies the problem of subtype checking for recursive types in system kernel Fun, a typed lambda-calculus with subtyping and bounded second order polymorphism.Along the lines of Amadio-Cardelli, we study the definition of a subtype relation over kernel Fun recursive types, and then we present a subtyping algorithm which is sound and complete with respect to this relation. We show that the natural extension of the techniques introduced by Amadio and Cardelli to compare first order recursive types gives a non complete algorithm. We prove the completeness and correctness of a different algorithm, which also admits an efficient implementation.

BibTeX

  @InProceedings{ColazzoGhelli-SubtypingRecursiveT,
    author = 	 {Dario Colazzo and Giorgio Ghelli},
    title = 	 {Subtyping Recursive Types in Kernel Fun - Abstract},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {137--146},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }