Sciweavers

ESOP
2009
Springer

Global Principal Typing in Partially Commutative Asynchronous Sessions

13 years 10 months ago
Global Principal Typing in Partially Commutative Asynchronous Sessions
We generalise a theory of multiparty session types for the π-calculus through asynchronous communication subtyping, which allows partial commutativity of actions with maximal flexibility and safe optimisation in message choreography. A sound and complete algorithm for the subtyping relation, which can calculate conformance of optimised end-point processes to an agreed global specification, is presented. As a complementing result, we show a type inference algorithm for deriving the principal global specification from end-point processes which is minimal with respect to subtyping. The resulting theory allows a programmer to choose between a top-down and a bottom-up style of communication programming, ensuring the same desirable properties of typable processes.
Dimitris Mostrous, Nobuko Yoshida, Kohei Honda
Added 19 May 2010
Updated 19 May 2010
Type Conference
Year 2009
Where ESOP
Authors Dimitris Mostrous, Nobuko Yoshida, Kohei Honda
Comments (0)