Loading...
Please wait, while we are loading the content...
Similar Documents
Principality and Decidable Type Inference for Finite-Rank Intersection Types (1999)
| Content Provider | CiteSeerX |
|---|---|
| Author | Kfoury, A. J. Wells, J. B. |
| Description | IN CONF. REC. POPL ’99: 26TH ACM SYMP. PRINC. OF PROG. LANGS |
| Abstract | Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable -terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. This is also in contrast to earlier presentations of intersection types where the status (decidable or undecidable) of these properties is unknown for the finite-rank restrictions at 3 and above. Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than severa... |
| File Format | |
| Publisher Date | 1999-01-01 |
| Access Restriction | Open |
| Subject Keyword | Principal Typing Intersection Type Normalizable Term Type Inference Finite Rank Restriction First Notion Finite-rank Restriction Decidable Type Inference Finite-rank Intersection Type Finite Rank Typable Term Intersection Type System |
| Content Type | Text |
