Sciweavers

Share
ICFP
1999
ACM

Relating Typability and Expressiveness in Finite-Rank Intersection Type Systems (Extended Abstract)

9 years 5 months ago
Relating Typability and Expressiveness in Finite-Rank Intersection Type Systems (Extended Abstract)
d Abstract) Assaf J. Kfoury∗ Boston University http://www.cs.bu.edu/˜kfoury Harry G. Mairson† Brandeis University http://www.cs.brandeis.edu/˜mairson Franklyn A. Turbak‡ Wellesley College http://www.wellesley.edu/CS/fturbak.html J. B. Wells § Heriot-Watt University http://www.cee.hw.ac.uk/˜jbw We investigate finite-rank intersection type systems, analyzing the complexity of their type inference problems and their relation to the problem of recognizing semantically equivalent terms. Intersection types allow something of type τ1 ∧ τ2 to be used in some places at type τ1 and in other places at type τ2. A finite-rank intersection type system bounds how deeply the ∧ can appear in type expressions. Such type systems enjoy strong normalization, subject reduction, and computable type inference, and they support a pragmatics for implementing parametric polymorphism. As a consequence, they provide a conceptually simple and tractable alternative to the impredicative polymorph...
Assaf J. Kfoury, Harry G. Mairson, Franklyn A. Tur
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 1999
Where ICFP
Authors Assaf J. Kfoury, Harry G. Mairson, Franklyn A. Turbak, J. B. Wells
Comments (0)
books