π-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 }