Paper Info
Title
Polymorphic Intersection Type Assignment for Rewrite Systems with Abstractions and beta-Rule
Abstract
We define two type assignment systems for first-order rewriting extended with application, λ-abstraction, and β-reduction, using a combination of (Ω-free) intersection types and second-order polymorphic types. The first system is the general one, for which we prove subject reduction, and strong normalisation of typeable terms. The second is a decidable subsystem of the first, by restricting to Rank 2 (intersection and quantified) types. For this system we define, using an extended notion of unification, a notion of principal typing which is more general than ML's principal type property, since also the types for the free variables of terms are inferred.
Year
Venue
Keywords
1999
TYPES
Polymorphic Intersection Type Assignment,type assignment system,subject reduction,second-order polymorphic type,free variable,strong normalisation,principal typing,extended notion,intersection type,Rewrite Systems,decidable subsystem,principal type property
DocType
ISBN
Citations 
Conference
3-540-41517-3
2
PageRank 
References 
Authors
0.37
26
3
Name
Order
Citations
PageRank
Steffen van Bakel133528.24
Franco Barbanera235735.14
Maribel Fernández314413.09