A Type-Theoretic Framework for Automated Synthesis of Workflows in Service-Oriented Computing

We describe a technique for automatic synthesis of workflows in service-oriented systems from a typetheoretic specification of coordination requirements. The technique presented involves formal semantics-based, automatic synthesis of service coordination workflows from the business logic of the clients using type and effect inference. The type and effect deduction, apart from synthesizing the workflow, provides formal proofs that the business requirements of the clients in a service-oriented system are met. The service descriptions and the business requirements are specified as a set of type judgements in an (intuitionistic) type theory. Workflows can be generated from a (type and effect) inference of the requirements from the "service theory".