A decidable intersection type system based on relevance

ABSTRACT. In this paper we introduce a notion of "relevance" for type assignment systems including intersection types. We define a relevant system which is an extension of a particular rank 2 intersection system and of the polymorphic type discipline limited to rank 2. We study some of its properties and finally state the decidability of type inference providing an algorithm which is sound and complete.

• pdf , ps , ps.gz ( © Springer-Verlag )

BIBTEX.

@conference{Damiani-Giannini:TACS-94,
   author    = {F. Damiani and P. Giannini},
   title     = {A Decidable Intersection Type System based on Relevance},
   booktitle = {TACS'94},
   year      = {1994},
   publisher = {Springer},
   pages     = {707-725},
   series    = {LNCS 789}
}