Mixin Composition Synthesis based on Intersection Types

Research output: Contribution to journal › Journal article › Research › peer-review

Standard

Mixin Composition Synthesis based on Intersection Types. / Bessai, Jan; Chen, Tzu-Chun; Dudenhefner, Andrej; Duedder, Boris; de'Liguoro, Ugo; Rehof, Jacob.

In: Logical Methods in Computer Science, Vol. 14, No. 1, 18, 2018.

Research output: Contribution to journal › Journal article › Research › peer-review

Harvard

Bessai, J, Chen, T-C, Dudenhefner, A, Duedder, B, de'Liguoro, U & Rehof, J 2018, 'Mixin Composition Synthesis based on Intersection Types', Logical Methods in Computer Science, vol. 14, no. 1, 18. https://doi.org/10.23638/LMCS-14(1:18)2018

APA

Bessai, J., Chen, T-C., Dudenhefner, A., Duedder, B., de'Liguoro, U., & Rehof, J. (2018). Mixin Composition Synthesis based on Intersection Types. Logical Methods in Computer Science, 14(1), [18]. https://doi.org/10.23638/LMCS-14(1:18)2018

Vancouver

Bessai J, Chen T-C, Dudenhefner A, Duedder B, de'Liguoro U, Rehof J. Mixin Composition Synthesis based on Intersection Types. Logical Methods in Computer Science. 2018;14(1). 18. https://doi.org/10.23638/LMCS-14(1:18)2018

Author

Bessai, Jan ; Chen, Tzu-Chun ; Dudenhefner, Andrej ; Duedder, Boris ; de'Liguoro, Ugo ; Rehof, Jacob. / Mixin Composition Synthesis based on Intersection Types. In: Logical Methods in Computer Science. 2018 ; Vol. 14, No. 1.

Bibtex

@article{e8234b0b0e364dca981aca065d74c553,
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 record-merge 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 is a class typed by the goal type and generated by a mixin composition applied to an existing class.",
keywords = "cs.LO, F.4.1",
author = "Jan Bessai and Tzu-Chun Chen and Andrej Dudenhefner and Boris Duedder and Ugo de'Liguoro and Jacob Rehof",
year = "2018",
doi = "10.23638/LMCS-14(1:18)2018",
language = "English",
volume = "14",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "International Federation for Computational Logic",
number = "1",

}

RIS

TY - JOUR

T1 - Mixin Composition Synthesis based on Intersection Types

AU - Bessai, Jan

AU - Chen, Tzu-Chun

AU - Dudenhefner, Andrej

AU - Duedder, Boris

AU - de'Liguoro, Ugo

AU - Rehof, Jacob

PY - 2018

Y1 - 2018

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 record-merge 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 is a class typed by the goal type and generated by a mixin composition applied to an existing class.

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 record-merge 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 is a class typed by the goal type and generated by a mixin composition applied to an existing class.

KW - cs.LO

KW - F.4.1

U2 - 10.23638/LMCS-14(1:18)2018

DO - 10.23638/LMCS-14(1:18)2018

M3 - Journal article

VL - 14

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 1

M1 - 18

ER -

ID: 210198263