[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Dear All, we are pleased to announce the paper: "Structured Global Programming for Communication Behaviour" by M. Carbone, K. Honda and N. Yoshida This work is intended to offer one of the central formal underpinnings of W3C's web service choreography description language, WS-CDL. The development of the theory has benefited greatly from the dialogue between the invited scientists of W3C WS-CDL Working Group and WG's members. The type theory of the pi-calculus plays an important role in this work. You can find the paper at http://www.dcs.qmul.ac.uk/~carbonem/cdlpaper/SGPCBmiddle.pdf A longer version containing the detailed proofs and more examples will also be published as W3C working note together with R. Milner, G. Brown and S. Ross-Talbot. The document is available at http://www.dcs.qmul.ac.uk/~carbonem/cdlpaper/workingnote.pdf Best Regards, Marco, Kohei and Nobuko - Abstract This paper presents two different paradigms of description of communication behaviour, one focusing on global message flows and another on end-point behaviours, as formal calculi based on session types. The global calculus originates from Choreography Description Language, a web service description language developed by W3C WS-CDL working group. The end-point calculus is a typed pi-calculus. The global calculus describes an interaction scenario from a vantage viewpoint; the endpoint calculus precisely identifies a local behaviour of each participant. After introducing the static and dynamic semantics of these two calculi, we explore a theory of endpoint projection which defines three principles for well-structured global description. The theory then defines a translation under the three principles which is sound and complete in the sense that all and only behaviours specified in the global description are realised as communications among end-point processes. Throughout the theory, underlying type structures play a fundamental role.