Intersection type matching with subtyping
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
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.
Original language | English |
---|---|
Title of host publication | Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings |
Number of pages | 15 |
Publication date | 27 Sep 2013 |
Pages | 125-139 |
ISBN (Print) | 9783642389450 |
DOIs | |
Publication status | Published - 27 Sep 2013 |
Externally published | Yes |
Event | 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 - Eindhoven, Netherlands Duration: 26 Jun 2013 → 28 Jun 2013 |
Conference
Conference | 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 |
---|---|
Land | Netherlands |
By | Eindhoven |
Periode | 26/06/2013 → 28/06/2013 |
Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 7941 LNCS |
ISSN | 0302-9743 |
ID: 230702198