Using Inhabitation in Bounded Combinatory Logic with Intersection Types for Composition Synthesis

TL;DR

This paper presents a framework for automatic software composition synthesis using inhabitation in bounded combinatory logic with intersection types, enabling the construction of programs from a repository of typed components.

Contribution

It introduces a novel approach combining inhabitation algorithms with intersection types for composition synthesis from component repositories.

Findings

Successful synthesis examples demonstrated, including GUI component composition.

Framework effectively models components as typed combinators for automated synthesis.

Potential for scalable and flexible composition in software engineering.

Abstract

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.