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