RESTful web service composition: Extracting a process model from Linear Logic theorem proving

This paper introduces a two-stage Linear Logic based program synthesis approach to automatic RESTful web service composition. The Linear Logic theorem proof is applied at both resource and service invocation method levels, which greatly improves the searching efficiency and guarantees the correctness and completeness of the service composition. Furthermore, the process calculus is used as formalism for the composition process, which enables the approach to be executable at the business management level. The process calculus is attached to the Linear Logic inference rules in the style of type theory, so the process model is extracted directly from the complete proof. An example is given to show the extraction of a process model from a Linear Logic proof search.