一句话：提出用交集类型居留合成 Mixin 组合，并将带记录与合并的类型项翻译为组合子仓库。
论文解决如何自动合成由若干混入（Mixin）组合得到的类的问题。作者先将递归定义的类与混入（视为类上的函数）编码为带记录的 lambda 演算项，并使用带记录及记录合并的交集类型为其赋予有意义类型，而无需递归类型。随后把带类型项翻译为带类型组合子仓库，证明带记录合并的记录类型与带构造子的交集类型之间的关系，并据此证明该翻译相对于混入组合合成的可靠性与部分完备性。最后展示翻译后的仓库与目标类型可作为已有有界组合逻辑组合合成框架的输入，通过类型居留计算得到由目标类型定型、并由应用在已有类上的混入组合生成的类。
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.
@article{paperbot423,
title = {Mixin Composition Synthesis based on Intersection Types},
author = {Jan Bessai and Tzu-Chun Chen and Andrej Dudenhefner and Boris Düdder and Ugo de'Liguoro and Jakob Rehof},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 1},
year = {2018},
doi = {10.23638/lmcs-14(1:18)2018}
}