π-calculus, Session Types research at Imperial College
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
}