MobilityReadingGroup

Global Principal Typing in Partially Commutative Asynchronous Sessions

Dimitris MOSTROUS, Nobuko YOSHIDA, Kohei HONDA

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.

Note: It turns out that a variant of the asynchronous subtyping (1), (2) is undecidable, see here.

@inproceedings{MYH2009,
  author = {Dimitris Mostrous and Nobuko Yoshida and Kohei Honda},
  title = {{Global Principal Typing in Partially Commutative Asynchronous Sessions}},
  booktitle = {18th European Symposium on Programming Languages and Systems},
  series = {LNCS},
  volume = {5502},
  pages = {316--332},
  publisher = {Springer},
  year = 2009
}

@inproceedings{MYH2009,
  author = {Dimitris Mostrous and Nobuko Yoshida and Kohei Honda},
  title = {{Global Principal Typing in Partially Commutative Asynchronous Sessions}},
  booktitle = {18th European Symposium on Programming Languages and Systems},
  series = {LNCS},
  volume = {5502},
  pages = {316--332},
  publisher = {Springer},
  doi = "10.1007/978-3-642-00590-9_23",
  year = 2009
}