Intersection type matching with subtyping

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Standard

Intersection type matching with subtyping. / Düdder, Boris; Martens, Moritz; Rehof, Jakob.

Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings. 2013. p. 125-139 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7941 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Harvard

Düdder, B, Martens, M & Rehof, J 2013, Intersection type matching with subtyping. in Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7941 LNCS, pp. 125-139, 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013, Eindhoven, Netherlands, 26/06/2013. https://doi.org/10.1007/978-3-642-38946-7_11

APA

Düdder, B., Martens, M., & Rehof, J. (2013). Intersection type matching with subtyping. In Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings (pp. 125-139). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 7941 LNCS https://doi.org/10.1007/978-3-642-38946-7_11

Vancouver

Düdder B, Martens M, Rehof J. Intersection type matching with subtyping. In Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings. 2013. p. 125-139. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7941 LNCS). https://doi.org/10.1007/978-3-642-38946-7_11

Author

Düdder, Boris ; Martens, Moritz ; Rehof, Jakob. / Intersection type matching with subtyping. Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings. 2013. pp. 125-139 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7941 LNCS).

Bibtex

@inproceedings{f5caaa71a4cb4b818317c380c0492d6d,
title = "Intersection type matching with subtyping",
abstract = "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.",
author = "Boris D{\"u}dder and Moritz Martens and Jakob Rehof",
year = "2013",
month = sep,
day = "27",
doi = "10.1007/978-3-642-38946-7_11",
language = "English",
isbn = "9783642389450",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "125--139",
booktitle = "Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings",
note = "11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 ; Conference date: 26-06-2013 Through 28-06-2013",

}

RIS

TY - GEN

T1 - Intersection type matching with subtyping

AU - Düdder, Boris

AU - Martens, Moritz

AU - Rehof, Jakob

PY - 2013/9/27

Y1 - 2013/9/27

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84884509674&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-38946-7_11

DO - 10.1007/978-3-642-38946-7_11

M3 - Article in proceedings

AN - SCOPUS:84884509674

SN - 9783642389450

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 125

EP - 139

BT - Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings

T2 - 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013

Y2 - 26 June 2013 through 28 June 2013

ER -

ID: 230702198