A Calculus of Global Interaction based on Session Types

AbstractThis paper proposes a calculus for describing communication-centred programs and discusses its use through a formal description of several use cases from real business protocols. The formalism, called global calculus, aims at representing global message flows as structured communications. The global calculus originates from the Choreography Description Language (CDL), a web service description language developed by W3C's WS-CDL Working Group. Its type discipline is based on session types which have been studied over long years in the context of the π-calculus [Honda, K., V. Vasconcelos and M. Kubo, Language primitives and type disciplines for structured communication-based programming, in: ESOP'98, LNCS 1381, 1998, pp. 22–138; Dezani-Ciancaglini, M., D. Mostrous, N. Yoshida and S. Drossopoulou, Session Types for Object-Oriented Languages, in: Proceedings of ECOOP'06, LNCS, 2006; Vasconcelos, V., A. Ravara and S.J. Gay, Session types for functional multithreading., in: CONCUR'04, LNCS 3170, 2004, pp. 497–511; Bonelli, E., A.B. Compagnoni and E.L. Gunter, Correspondence assertions for process synchronization in concurrent communications., JFP 15 (2005), pp. 219–247]. Session types offer a high-level abstraction and articulation for complex communication behaviours, and play a fundamental role to guide the programmer towards a clear, well-structured description of business protocols