TY - GEN
T1 - Intersection, Universally quantified, and reference types
AU - Dezani-Ciancaglini, Mariangiola
AU - Giannini, Paola
AU - Della Rocca, Simona Ronchi
N1 - Funding Information:
Work partially supported by MIUR PRIN’06 EOS DUE, and MIUR PRIN’07 CONCERTO projects. The funding bodies are not responsible for any use that might be made of the results presented here.
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/70350381268
U2 - 10.1007/978-3-642-04027-6_17
DO - 10.1007/978-3-642-04027-6_17
M3 - Conference contribution
AN - SCOPUS:70350381268
SN - 3642040268
SN - 9783642040269
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 209
EP - 224
BT - Computer Science Logic - 23rd International Workshop, CSL 2009 - 18th Annual Conference of the EACSL, Proceedings
T2 - 23rd International Workshop on Computer Science Logic, CSL 2009 - 18th Annual Conference of the EACSL
Y2 - 7 September 2009 through 11 September 2009
ER -