1 Programming, Logic and Semantics, Software & Systems, The Department2 Theoretical Computer Science, The Department3 Process and System Models, Software & Systems, The Department4 Programming Logic and Semantics, Theoretical Computer Science, The Department5 Queen Mary University of London6 Imperial College London
This article relates two different paradigms of descriptions of communication behavior, one focusing on global message flows and another on end-point behaviors, using formal calculi based on session types. The global calculus, which originates from a Web service description language (W3C WS-CDL), describes an interaction scenario from a vantage viewpoint; the end-point calculus, an applied typed π -calculus, precisely identifies a local behavior of each participant. We explore a theory of end-point projection, by which we can map a global description to its end-point counterparts preserving types and dynamics. Three principles of well-structured description and the type structures play a fundamental role in the theory.
A C M Transactions on Programming Languages and Systems, 2012, Vol 34 (2), Issue 8