Tue 9 Jan 2018 16:00 - 16:10 at Crocker - Session 2-3 Chair(s): Barry Jay

Software engineering is routinely based on the premise that one starts a development process by modeling the desired application domain of interest. Iteratively and incrementally over time, further details are added in a seamless transition to a solution domain in which the final executable application is completed. Within this context it is difficult to identify the ideal place to apply software synthesis, that is, the ability to automate the generation of code which otherwise would have been written manually. The challenge is increased by the variety of modeling and programming languages, which are often predetermined by external project constraints such as developer experience or contractual agreements. When the application domain consists of a high degree of variability – found in product lines or highly configurable domains – we believe code synthesis plays an essential role in increasing the productivity of programmers and ensuring the quality of the resulting system. We have built a general framework that combines the language-neutral modeling power of algebra with a type-inhabitation based synthesis algorithm. The resulting framework is proven in Coq and an instance of it, prototypically implemented in Scala, will enable more comprehensive future evaluation in different domains.