Jump label

Service navigation

Main navigation

You are here:

Main content

Combinatory Logic Synthesizer

CLSLogo

(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 execution graph
  • Example figure of an execution graph:
    Example 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
  • Contact
  • Image of a complex execution graph:
    Complex example