| BDDCdLR15 (In proceedings)
|
| Author(s) | Jan Bessai, Andrej Dudenhefner, Boris Düdder, Tzu-Chun Chen, Ugo de' Liguoro and Jakob Rehof |
| Title | « Mixin Composition Synthesis Based on Intersection Types » |
| In | 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland |
| Series | LIPIcs |
| Editor(s) | Thorsten Altenkirch |
| Volume | 38 |
| Page(s) | 76--91 |
| Year | 2015 |
| Publisher | Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik |
| ISBN number | 978-3-939897-87-3 |
| URL | http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.76 |
| Abstract |
| We present a method for synthesizing compositions of mixins using type inhabitation in inter- section 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 corresponds to a mixin composition typed by the goal type. |
@inproceedings{BDDCdLR15,
volume = {38},
author = {Jan Bessai and Andrej Dudenhefner and Boris D{\"{u}}dder and
Tzu{-}Chun Chen and Ugo de' Liguoro and Jakob Rehof},
series = {LIPIcs},
booktitle = {13th International Conference on Typed Lambda Calculi and
Applications, {TLCA} 2015, July 1-3, 2015, Warsaw, Poland},
editor = {Thorsten Altenkirch},
url = {http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.76},
isbn = {978-3-939897-87-3},
tag = {TLCA'15},
abstract = {We present a method for synthesizing compositions of mixins using
type inhabitation in inter- section 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 corresponds to a mixin composition typed by the goal
type.},
title = {Mixin Composition Synthesis Based on Intersection Types},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
doi = {10.4230/LIPIcs.TLCA.2015.76},
pages = {76--91},
year = {2015},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
