MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Timed Multiparty Session Types
Laura BOCCHI, Weizhen YANG, Nobuko YOSHIDA
25th International Conference on Concurrency Theory (CONCUR 2014). p. 419 - 434

We introduce a simple calculus with delays and a decidable static proof system. The proof system with time constraints ensures type safety and time-error freedom, namely processes respect the prescribed timing and causalities between interactions. A decidable condition, enforceable on timed global types, guarantees global time-progress for validated processes with delays, and gives a sound and complete characterisation of a new class of CTAs with general topologies that enjoys global progress and liveness.

@inproceedings{BYY2014,
  author = {Laura Bocchi and Weizhen Yang and Nobuko Yoshida},
  title = {{Timed Multiparty Session Types}},
  booktitle = {25th International Conference on Concurrency Theory},
  series = {LNCS},
  volume = {8704},
  pages = {419--434},
  publisher = {Springer},
  year = 2014
}
@inproceedings{BYY2014,
  author = {Laura Bocchi and Weizhen Yang and Nobuko Yoshida},
  title = {{Timed Multiparty Session Types}},
  booktitle = {25th International Conference on Concurrency Theory},
  series = {LNCS},
  volume = {8704},
  pages = {419--434},
  publisher = {Springer},
  doi = "10.1007/978-3-662-44584-6_29",
  year = 2014
}