Intersection type matching with subtyping

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfæ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.

OriginalsprogEngelsk
TitelTyped Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings
Antal sider15
Publikationsdato27 sep. 2013
Sider125-139
ISBN (Trykt)9783642389450
DOI
StatusUdgivet - 27 sep. 2013
Eksternt udgivetJa
Begivenhed11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 - Eindhoven, Holland
Varighed: 26 jun. 201328 jun. 2013

Konference

Konference11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013
LandHolland
ByEindhoven
Periode26/06/201328/06/2013
NavnLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind7941 LNCS
ISSN0302-9743

ID: 230702198