A Type-Based Approach to Component-Oriented Synthesis

The synthesis problem (given a logical specification, to construct a program satisfying the specification) is one of the most challenging problems in computer science. The problem is intrinsically of high computational complexity. Moreover, a no less important problem from a pragmatic perspective is the challenge of specification complexity – how to allow for adequate specifications that can be naturally connected to code without requiring unrealistic human effort. One recent line of approaches towards meeting these challenges is to consider synthesis as a component-based problem, that is, as a problem of program composition from a collection (“repository”) of components which may embody human design intelligence (rather than as a problem of synthesis “from scratch”). Our approach (“Combinatory Logic Synthesis”, CLS) is based on the theory of inhabitation (is there a term having a given type?) in combinatory logic with intersection types which are used to specify components semantically. In this course we will present an overview of both the theoretical foundations of CLS as well as applications of CLS within a framework implemented as a language extension to the programming language Scala.

More info at http://phdopen.mimuw.edu.pl/index.php?page=z17w2.