Using Inhabitation in Bounded Combinatory Logic with Intersection Types for Composition Synthesis
This work addresses software engineering challenges in component-based development, though it appears incremental as it builds on existing combinatory logic and intersection type frameworks.
The authors tackled the problem of automatic composition synthesis from software component repositories by modeling components as typed combinators in bounded combinatory logic with intersection types, using an inhabitation algorithm to synthesize programs that meet specified goals, with examples including GUI-component synthesis.
We describe ongoing work on a framework for automatic composition synthesis from a repository of software components. This work is based on combinatory logic with intersection types. The idea is that components are modeled as typed combinators, and an algorithm for inhabitation {\textemdash} is there a combinatory term e with type tau relative to an environment Gamma? {\textemdash} can be used to synthesize compositions. Here, Gamma represents the repository in the form of typed combinators, tau specifies the synthesis goal, and e is the synthesized program. We illustrate our approach by examples, including an application to synthesis from GUI-components.