Jump label

Service navigation

Main navigation

You are here:

Sub navigation

  • Staff pages+

Main content

Research - Prof. Jakob Rehof

General interests

  • Algorithms and complexity in type theory and logic, typed lambda-calculi, principles of programming languages, and their applications in automated methods for software construction, including composition synthesis, code generation, configuration, service- and component repositories
  • Cloud computing
  • Process algebra, process models, process-oriented systems, workflow systems
  • Model checking
  • Proof theory

Current research topics

My current research focuses on automated software composition synthesis, motivated by several application areas, including service engineering and cloud computing, process-oriented systems, planning, web-programming.

The general idea is: you have a repository of software components and you want to be able to synthesize more complex objects by composing objects from the repository. In order to achieve this, we need to be able to specify the components semantically, and we need algorithms to do the composition. We have initiated an approach in which we explore type theory, specifically combinatory logic and fragments of intersection type systems, as a basis for composition synthesis. Intersection type systems combine logical simplicity with enormous semantic expressive power. We explore applications in several areas, including automatic generation of user interfaces, robotics, automatic platform configuration, service composition. This work is in collaboration with P. Urzyczyn of Warsaw and my co-workers in Dortmund, B. Düdder and M. Martens.

The theoretical basis of this work includes:

  • Type-based composition synthesis
  • Combinatory logic with intersection types
  • The inhabitation problem for restrictions of the intersection type system
  • Bounded restrictions of Hilbert-style proof systems
  • The organization of semantic repositories

Ongoing funded projects

  • EU Cost Action IC1201, Behavioral Types for Reliable Large-Scale Software Systems (BETTY), MC member
  • Cloud computing infrastructure (DfG and TU-Dortmund)
  • Cloud computing for logistics (Fraunhofer innovation cluster)
  • Service Design Studio (BMBF Spitzencluster)

Some past projects

  • Process-oriented systems and workflow
  • Context-bounded model chekcing of concurrent software
  • Behavioral type systems and programming languages for distributed software
  • Process algebra (conformance theory)
  • Explicit state model checker for concurrent software (Zing)
  • Large scale program analysis
  • Complexity of subyping systems
  • Constraint satisfaction
  • Dynamic typing
  • Curry-Howard isomorphism and classical logic