MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Scribbling Interactions with a Formal Foundation
Kohei HONDA , Aybek MUKHAMEDOV , Gary BROWN , Tzu-Chun CHEN , Nobuko YOSHIDA
7th International Conference on Distributed Computing and Internet Technology (ICDCIT 2011) p. 55 - 75

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
}