  We present a rigorous framework for the composition of Web Services within a
higher order logic theorem prover. Our approach is based on the
proofs-as-processes paradigm that enables inference rules of Classical Linear
Logic (CLL) to be translated into pi-calculus processes. In this setting,
composition is achieved by representing available web services as CLL
sentences, proving the requested composite service as a conjecture, and then
extracting the constructed pi-calculus term from the proof. Our framework,
implemented in HOL Light, not only uses an expressive logic that allows us to
incorporate multiple Web Services properties in the composition process, but
also provides guarantees of soundness and correctness for the composition.
