Intersection type matching with subtyping

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-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 languageEnglish
Title of host publicationTyped Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings
Number of pages15
Publication date27 Sep 2013
Pages125-139
ISBN (Print)9783642389450
DOIs
Publication statusPublished - 27 Sep 2013
Externally publishedYes
Event11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 - Eindhoven, Netherlands
Duration: 26 Jun 201328 Jun 2013

Conference

Conference11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013
LandNetherlands
ByEindhoven
Periode26/06/201328/06/2013
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7941 LNCS
ISSN0302-9743

ID: 230702198