Jump label

Service navigation

Main navigation

You are here:

Main content

Research Motivation

The inherent theoretical complexity of the software-synthesis problem as well as the pragmatic complexity of writing and understanding software specifications are the greatest challenges in reducing software synthesis to practice. One approach to avoid part of this complexity is component-oriented synthesis where as opposed to the traditional approach, that does synthesis from scratch, systems are composed from glueing components from a given repositoriy, that has been designed for a very specific usage-context, together. However, even though the component-based abpproach enhances reusability and helps structuring software, the actual job of retrieving, configuring, and glueing the suitable components takes up unproportionally much time in the process of realizing a piece of software. A high degree of automation is desirable, here.

Image: Synthesis from Components

On a more general scale, the Synthesisproblem (Alonzo Church, 1957), i.e., the problem of automatically generating a program or system satisfying a given specification, is fundamental in (theoretical) Computer Science. A series of results regarding automatic synthesis exist, however, they do not seem fit to be applied to synthesis of real-world software, because of the pragmatic complexity mentioned above.

The motivation behind the research at SEAL is to apply recent fundamental research on the Synthesisproblem based on type theory to software synthesis from a repository of components. The type-based approach is natural, since type theory is inherently component-oriented and components exhibit types in a natural way through their interfaces. Furthermore, if one relies on the fact that the components are correctly specified, specifications for complex software become much more simple (exactly because not everything has to be specified from scratch). We use intersection types (Coppo-Dezani-Sallé types) to enrich implementation language interfaces (i.e., the native input/output types of the components) with semantic information. This allows for an intuitive way of specifying software components because, using concepts, a component may be described to an almost arbitrary degree of detail. The resulting specification logic (combinatory logic) is simple but enormously expressive. We used various type-theoretical results on combinatory logic with intersection types to implement a powerful framework for automatic component composition based on an automatic theorem prover for combinatory logic.

Image: Editor with Intersection Types