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

Boris Düdder
(Technical University of Dortmund)
Oliver Garbe
(Technical University of Dortmund)
Moritz Martens
(Technical University of Dortmund)
Jakob Rehof
(Technical University of Dortmund)
Paweł Urzyczyn
(University of Warsaw)

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 — is there a combinatory term e with type tau relative to an environment Gamma? — 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.

In Stéphane Graham-Lengrand and Luca Paolini: Proceedings Sixth Workshop on Intersection Types and Related Systems (ITRS 2012), Dubrovnik, Croatia, 29th June 2012, Electronic Proceedings in Theoretical Computer Science 121, pp. 18–34.
Published: 30th July 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: