π-calculus, Session Types research at Imperial College
In this paper we discuss our ongoing endeavour to apply notations and algorithms based on the π-calculus and its theories for the development of large-scale distributed systems. The execution of a large-scale distributed system consists of many structured conversations (or sessions) whose protocols can be clearly and accurately specified using a theory of types for the π-calculus, called session types. The proposed methodology promotes a formally founded, and highly structured, development framework for modelling and building distributed applications, from high-level models to design and implementation to static checking to runtime validation. At the centre of this methodology is a formal description language for representing protocols for interactions, called Scribble. We illustrate the usage and theoretical basis of this language through use cases from different application domains.
@inproceedings{HMBCY2011, author = {Kohei Honda and Aybek Mukhamedov and Gary Brown and Tzu-Chun Chen and Nobuko Yoshida}, title = {{Scribbling Interactions with a Formal Foundation}}, booktitle = {7th International Conference on Distributed Computing and Internet Technology}, series = {LNCS}, volume = {6536}, pages = {55--75}, publisher = {Springer}, year = 2011 }
@inproceedings{HMBCY2011, author = {Kohei Honda and Aybek Mukhamedov and Gary Brown and Tzu-Chun Chen and Nobuko Yoshida}, title = {{Scribbling Interactions with a Formal Foundation}}, booktitle = {7th International Conference on Distributed Computing and Internet Technology}, series = {LNCS}, volume = {6536}, pages = {55--75}, publisher = {Springer}, doi = "10.1007/978-3-642-19056-8_4", year = 2011 }