Intersection type matching with subtyping
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Type matching problems occur in a number of contexts, including library search, component composition, and inhabitation. We consider the intersection type matching problem under the standard notion of subtyping for intersection types: Given intersection types τ and σ, where σ is a constant type, does there exist a type substitution S such that S(τ) is a subtype of σ? We show that the matching problem is NP-complete. NP-hardness holds already for the restriction to atomic substitutions. The main contribution is an NP-algorithm which is engineered for efficiency by minimizing nondeterminism and running in Ptime on deterministic input problems. Our algorithm is based on a nondeterministic polynomial time normalization procedure for subtype constraint systems with intersection types. We have applied intersection type matching in optimizations of an inhabitation algorithm.
Originalsprog | Engelsk |
---|---|
Titel | Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings |
Antal sider | 15 |
Publikationsdato | 27 sep. 2013 |
Sider | 125-139 |
ISBN (Trykt) | 9783642389450 |
DOI | |
Status | Udgivet - 27 sep. 2013 |
Eksternt udgivet | Ja |
Begivenhed | 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 - Eindhoven, Holland Varighed: 26 jun. 2013 → 28 jun. 2013 |
Konference
Konference | 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 |
---|---|
Land | Holland |
By | Eindhoven |
Periode | 26/06/2013 → 28/06/2013 |
Navn | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Vol/bind | 7941 LNCS |
ISSN | 0302-9743 |
ID: 230702198