A Decidable Intersection Type System based on Relevance

In this paper we introduce a notion of ldquorelevancerdquo 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.