A Calculus of Global Interaction based on Session Types

ABSTRACT

This 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 @p-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.

REFERENCES

• [1].: Rajeev Alur , Kousha Etessami , Mihalis Yannakakis, Realizability and verification of MSC graphs, Theoretical Computer Science, v.331 n.1, p.97-114, 15 February 2005 [doi>10.1016/j.tcs.2004.09.034]
• [2]: J. C. M. Baeten , H. M. A. van Beek , S. Mauw, Specifying internet applications with DiCons, Proceedings of the 2001 ACM symposium on Applied computing, p.576-584, March 2001, Las Vegas, Nevada, United States [doi>10.1145/372202.372466]
• [3]: Nick Benton , Luca Cardelli , Cédric Fournet, Modern concurrency abstractions for C#, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.5, p.769-804, September 2004 [doi>10.1145/1018203.1018205]
• [4]: Gérard Berry , Gérard Boudol, The chemical abstract machine, Theoretical Computer Science, v.96 n.1, p.217-248, 6 April 1992
• [5]: Bhargavan, K., C. Fournet and A. Gordon, Verified reference implementations of WS-Security protocols, in: WS-FN'06, LNCS, 2006
• [6]: Eduardo Bonelli , Adriana Compagnoni , Elsa Gunter, Correspondence assertions for process synchronization in concurrent communications, Journal of Functional Programming, v.15 n.2, p.219-247, March 2005 [doi>10.1017/S095679680400543X]
• [7]: Briais, S. and U. Nestmann, A formal semantics for protocol narrations, in: TGC, 2005, pp. 163--181
• [8]: Busi, N., Gorrieri, R., Guidi, C., Lucchi, R. and Zavattaro, G., Choreography and orchestration conformance for system design. In: LNCS, 4038. pp. 63-81.
• [9]: Carbone, M., K. Honda, N. Yoshida, R. Milner, G. Brown and S. Ross-Talbot, A theoretical basis of communication-centred concurrent programming, To be published by W3C. Available at http://www.dcs.qmul.ac.uk/~carbonem/cdlpaper/workingnote.pdf (2006)
• [10]: Dezani-Ciancaglini, M., D. Mostrous, N. Yoshida and S. Drossopoulou, Session Types for Object-Oriented Languages, in: Proceedings of ECOOP'06, LNCS, 2006
• [11]: Simon Gay , Malcolm Hole, Subtyping for session types in the pi calculus, Acta Informatica, v.42 n.2, p.191-225, November 2005 [doi>10.1007/s00236-005-0177-z]
• [12]: Guidi, C., R. Lucchi, G. Zavattaro, N. Busi and R. Gorrieri, Sock: a calculus for service oriented computing, in: ICSOC '06, LNCS, 2006
• [13]: Joshua D. Guttman , F. Javier Thayer , Lenore D. Zuck, The faithfulness of abstract protocol analysis: message authentication, Proceedings of the 8th ACM conference on Computer and Communications Security, November 05-08, 2001, Philadelphia, PA, USA [doi>10.1145/501983.502009]
• [14]: Jesper G. Henriksen , Madhavan Mukund , K. Narayan Kumar , Milind Sohoni , P. S. Thiagarajan, A theory of regular MSC languages, Information and Computation, v.202 n.1, p.1-38, October 10, 2005 [doi>10.1016/j.ic.2004.08.004]
• [15]: Kohei Honda , Vasco Thudichum Vasconcelos , Makoto Kubo, Language Primitives and Type Discipline for Structured Communication-Based Programming, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.122-138, March 28-April 04, 1998
• [16]: Laneve, C. and Padovani, L., Smooth orchestrators. In: LNCS, 3921. pp. 32-46.
• [17]: Milner, R., Functions as processes. MSCS. v2. 119-141.
• [18]: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• [19]: Benjamin C. Pierce , David N. Turner, Pict: a programming language based on the Pi-Calculus, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
• [20]: Kaku Takeuchi , Kohei Honda , Makoto Kubo, An Interaction-based Language and its Typing System, Proceedings of the 6th International PARLE Conference on Parallel Architectures and Languages Europe, p.398-413, July 04-08, 1994
• [21]: van der Aalst, W., Inheritance of interorganizational workflows: How to agree to disagree without loosing control?. Info. Tech. and Management J. v2. 195-231.
• [22]: Vasconcelos, V., Ravara, A. and Gay, S.J., Session types for functional multithreading. In: LNCS, 3170. pp. 497-511.
• [23]: http://www.w3.org/TR/2004/WD-ws-cdl-10-20040427/

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  H. Information Systems
  H.3 INFORMATION STORAGE AND RETRIEVAL
      H.3.5 On-line Information Services
          Subjects: Web-based services

General Terms:
Theory

Keywords:
π-Calculus, Communication-Centred Programming, Session Types, Web Services