
(CL)S is a type-based synthesizer framework for component repositories/libraries. The framework is based on Microsoft™ F#/C# and offers a cloud service for synthesizing components with feature vectors.
- In order to make the type-based approach to software synthesis from a repository of components feasible and accessible for experiments we implemented the synthesis tool (CL)S. The core synthesis-algorithm is based on an inhabitation procedure which is implemented in Microsoft™ F# and C# using the Microsoft™ .NET-framework. (CL)S enriches the algorithmic framework in various ways in order to increase usability and performance of component-synthesis. (CL)S is provided as a (web-)service with exposed endpoints offering SOAP and REST access. Furthermore, the implementation is parallelized. This allows for a usage in our cluster computing environment with multiple concurrent users. Various editor-extensions featuring syntax-highlighting and auto-completion, for example, exist. Finally, (CL)S provides graphical representations of synthesized terms and of execution graphs in addition to various logging functionalities which are all crucial features with regard to debugging and analysing experiments.
- Syntax-highlighting in an editor:

- Example figure of an execution graph:

- Publications
- Overview Research Program
- Towards Combinatory Logic Synthesis (J. Rehof) BEAT'13, 1st International Workshop on Behavioural Types, Proceedings at http://beat13.cs.aau.dk.
- Peer-reviewed papers
- Staged Composition Synthesis (B. Düdder, M. Martens, and J. Rehof) in ESOP 2014, European Symposium on Programming, to appear.
- Intersection Type Matching with Subtyping (B. Düdder, M. Martens, and J. Rehof) in TLCA 2013, Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 7941.
- Bounded Combinatory Logic (B. Düdder, M. Martens, J. Rehof, and P. Urzyczyn) in CSL Computer Science Logic, 2012.
- Using Inhabitation in Bounded Combinatory Logic with Intersection Types for GUI Synthesis (B. Düdder, O.Garbe, M. Martens, J. Rehof, and P. Urzyczyn) in ITRS Intersection Types and Related Systems, 2012.
- The Complexity of Inhabitation with Explicit Intersection (J. Rehof and P. Urzyczyn) in R.L. Constable and A. Silva (Eds.): Logic and Program Semantics. Essays Dedicated to Dexter Kozen. Lecture Notes in Computer Science 7230, 2012.
- Finite Combinatory Logic with Intersection Types (J. Rehof and P. Urzyczyn) in TLCA 2011, Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 6690.
- Technical Reports
- Using Inhabitation in Bounded Combinatory Logic with Intersection Types for Composition Synthesis (Extended Version) (B. Düdder, M. Martens, J. Rehof, and P. Urzyczyn) in Technical Reports in Computer Science (Technische Universität Dortmund), TR 842, October 2012.
- Intersection Type Matching and Bounded Combinatory Logic (Extended Version) (B. Düdder, M. Martens, and J. Rehof) in Technical Reports in Computer Science (Technische Universität Dortmund), TR 841, October 2012.
- Bounded Combinatory Logic (Extended Version) (B. Düdder, M. Martens, J. Rehof, and P. Urzyczyn) in Technical Reports in Computer Science (Technische Universität Dortmund), TR 840, June 2012, revised October 2012.
- Contact
- Image of a complex execution graph:
