[TYPES/announce] Paper on Structured Global Programming

[Marco Carbone]

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.