Typing the Behavior of Software Components using Session Types

Article type: Research Article

Authors: Vallecillo, Antonio | Vasconcelos, Vasco T. | Ravara, António

Affiliations: Dept. of Computer Science, University of Málaga. E-mail: av@lcc.uma.es | Dept. of Informatics, Faculty of Sciences, University of Lisbon, Portugal | CLC and Dept. of Mathematics, IST, Technical University of Lisbon, Portugal

Abstract: This paper proposes the use of session types to extend with behavioural information the simple descriptions usually provided by software component interfaces. We show how session types allow not only high level specifications of complex interactions, but also the definition of powerful interoperability tests at the protocol level, namely compatibility and substitutability of components. We present a decidable proof system to verify these notions, which makes our approach of a pragmatic nature.

Journal: Fundamenta Informaticae, vol. 73, no. 4, pp. 583-598, 2006