The objective of this work was to provide formal tools that allowed the declarative and operational analysis of communication-based systems. In particular we intended to show that it is possible to build a framework in which it is possible to transfer reasoning tools for declarative models of concurrency to session-based models of concurrency. The thesis was developed under Dr. Camilo Rueda and Dr. Jorge A. PĂ©rez.