Jul 02, 2015

__Jan Bessai, Andrej Dudenhefner, Boris Düdder, Tzu-Chun Chen, Ugo de’Liguoro, and Jakob Rehof__

__Mixin Composition Synthesis Based on Intersection Types (TLCA 2015)__

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.

Jul 17, 2014

__Jan Bessai, Boris Düdder, Andrej Dudenhefner, Tzu-Chun Chen, Ugo de’Liguoro__

__Typing Classes and Mixins with Intersection Types (ITRS 2014)__

We study an assignment system of intersection types for a lambda-calculus with records and a record- merge operator, where types are preserved both under subject reduction and expansion. The calculus is expressive enough to naturally represent mixins as functions over recursively defined classes, whose fixed points, the objects, are recursive records. In spite of the double recursion that is involved in their definition, classes and mixins can be meaningfully typed without resorting to neither recursive nor F-bounded polymorphic types.

We then adapt mixin construct and composition to Java and C#, relying solely on existing features in such a way that the resulting code remains typable in the respective type systems. We exhibit some example code and study its typings in the intersection type system via interpretation into the lambda- calculus with records we have proposed.