Intersection, Universally Quantified, and Reference Types

The aim of this paper is to understand the interplay between intersection, universally quantified, and reference types. Putting together the standard typing rules for intersection, universally quantified, and reference types leads to loss of subject reduction. The problem comes from the invariance of the reference type constructor and the rules of intersection and/or universal quantification elimination, which are subsumption rules. We propose a solution in which types have a kind saying whether the type is (or contains in the case of intersection) a reference type or not. Intersection elimination is limited to intersections not containing reference types, and the reference type constructor can only be applied to closed types. The type assignment is shown to be safe, and when restricted to pure -calculus, as expressive as the full standard type assignment system with intersection and universally quantified types.

• Type: Conference
• Year: 2009
• Where: CSL
• Authors: Mariangiola Dezani-Ciancaglini, Paola Giannini, Simona Ronchi Della Rocca
• Keywords: Automated Reasoning, CSL 2009, Reference Type, Reference Type Constructor, Universally Quantified