Mixin composition synthesis based on intersection types

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

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. ed. / Thorsten Altenkirch. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2015. p. 76-91 (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 38).

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

Harvard

Bessai, J, Düdder, B, Dudenhefner, A, Chen, TC, De'Liguoro, U & Rehof, J 2015, Mixin composition synthesis based on intersection types. in T Altenkirch (ed.), 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Leibniz International Proceedings in Informatics, LIPIcs, vol. 38, pp. 76-91, 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, Warsaw, Poland, 01/07/2015. https://doi.org/10.4230/LIPIcs.TLCA.2015.76

APA

Bessai, J., Düdder, B., Dudenhefner, A., Chen, T. C., De'Liguoro, U., & Rehof, J. (2015). Mixin composition synthesis based on intersection types. In T. Altenkirch (Ed.), 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015 (pp. 76-91). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. Leibniz International Proceedings in Informatics, LIPIcs Vol. 38 https://doi.org/10.4230/LIPIcs.TLCA.2015.76

Vancouver

Bessai J, Düdder B, Dudenhefner A, Chen TC, De'Liguoro U, Rehof J. Mixin composition synthesis based on intersection types. In Altenkirch T, editor, 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2015. p. 76-91. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 38). https://doi.org/10.4230/LIPIcs.TLCA.2015.76

Author

Bessai, Jan ; Düdder, Boris ; Dudenhefner, Andrej ; Chen, Tzu Chun ; De'Liguoro, Ugo ; Rehof, Jakob. / Mixin composition synthesis based on intersection types. 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015. editor / Thorsten Altenkirch. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2015. pp. 76-91 (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 38).

Bibtex

@inproceedings{a8094e3437b34240918181d9d8af71e8,
title = "Mixin composition synthesis based on intersection types",
abstract = "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.",
keywords = "Combinatory logic, Intersection type, Mixin, Record calculus, Type inhabitation",
author = "Jan Bessai and Boris D{\"u}dder and Andrej Dudenhefner and Chen, {Tzu Chun} and Ugo De'Liguoro and Jakob Rehof",
year = "2015",
month = jul,
day = "1",
doi = "10.4230/LIPIcs.TLCA.2015.76",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
pages = "76--91",
editor = "Thorsten Altenkirch",
booktitle = "13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015",
note = "13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015 ; Conference date: 01-07-2015 Through 03-07-2015",

}

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