Mixin composition synthesis based on intersection types
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Standard
Mixin composition synthesis based on intersection types. / Bessai, Jan; Düdder, Boris; Dudenhefner, Andrej; Chen, Tzu Chun; De'Liguoro, Ugo; Rehof, Jakob.
13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015. red. / Thorsten Altenkirch. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2015. s. 76-91 (Leibniz International Proceedings in Informatics, LIPIcs, Bind 38).Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Mixin composition synthesis based on intersection types
AU - Bessai, Jan
AU - Düdder, Boris
AU - Dudenhefner, Andrej
AU - Chen, Tzu Chun
AU - De'Liguoro, Ugo
AU - Rehof, Jakob
PY - 2015/7/1
Y1 - 2015/7/1
N2 - We present a method for synthesizing compositions of mixins using type inhabitation in intersection types. First, recursively defined classes and mixins, which are functions over classes, are expressed as terms in a lambda calculus with records. Intersection types with records and recordmerge are used to assign meaningful types to these terms without resorting to recursive types. Second, typed terms are translated to a repository of typed combinators. We show a relation between record types with record-merge and intersection types with constructors. This relation is used to prove soundness and partial completeness of the translation with respect to mixin composition synthesis. Furthermore, we demonstrate how a translated repository and goal type can be used as input to an existing framework for composition synthesis in bounded combinatory logic via type inhabitation. The computed result corresponds to a mixin composition typed by the goal type.
AB - We present a method for synthesizing compositions of mixins using type inhabitation in intersection types. First, recursively defined classes and mixins, which are functions over classes, are expressed as terms in a lambda calculus with records. Intersection types with records and recordmerge are used to assign meaningful types to these terms without resorting to recursive types. Second, typed terms are translated to a repository of typed combinators. We show a relation between record types with record-merge and intersection types with constructors. This relation is used to prove soundness and partial completeness of the translation with respect to mixin composition synthesis. Furthermore, we demonstrate how a translated repository and goal type can be used as input to an existing framework for composition synthesis in bounded combinatory logic via type inhabitation. The computed result corresponds to a mixin composition typed by the goal type.
KW - Combinatory logic
KW - Intersection type
KW - Mixin
KW - Record calculus
KW - Type inhabitation
UR - http://www.scopus.com/inward/record.url?scp=84958695525&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.TLCA.2015.76
DO - 10.4230/LIPIcs.TLCA.2015.76
M3 - Article in proceedings
AN - SCOPUS:84958695525
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 76
EP - 91
BT - 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015
A2 - Altenkirch, Thorsten
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015
Y2 - 1 July 2015 through 3 July 2015
ER -
ID: 230702560