Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

BTDDdLR18 (Article)
Author(s) Jan Bessai, Tzu-Chun Chen, Andrej Dudenhefner, Boris Dï¿œdder, Ugo de' Liguoro and Jakob Rehof
Title« Mixin Composition Synthesis based on Intersection Types »
JournalLogical Methods in Computer Science
VolumeVolume 14, Issue 1
Year2018
URLhttp://lmcs.episciences.org/4319
Abstract & Keywords
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: Computer Science - Logic in Computer Science ; F.4.1

BibTeX code

@article{BTDDdLR18,
  volume = {{Volume 14, Issue 1}},
  month = Feb,
  author = {Bessai, Jan and Chen, Tzu-Chun and Dudenhefner, Andrej and D�dder,
            Boris and de' Liguoro, Ugo and Rehof, Jakob},
  keywords = {Computer Science - Logic in Computer Science ; F.4.1},
  url = {http://lmcs.episciences.org/4319},
  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.},
  tag = {Logical Methods in Computer Science},
  title = {{Mixin Composition Synthesis based on Intersection Types}},
  doi = {10.23638/LMCS-14(1:18)2018},
  journal = {{Logical Methods in Computer Science}},
  year = {2018},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)

Valid HTML 4.01!