MobilityReadingGroup

π-calculus, Session Types research at the University of Oxford

Intensional and Extensional Characterisation of Global Progress in the π-Calculus
Luca FOSSATI , Kohei HONDA , Nobuko YOSHIDA
23rd International Conference on Concurrency Theory (CONCUR 2012). p. 287 - 301

We introduce an observational theory of global progress properties such as non-blockingness and wait-freedom based on a linear π-calculus. The theory uniformly captures such properties both extensionally and intensionally, by using fair transition relations and partial failures, which represent stalling activities. A fairness-enriched bisimilarity preserves these properties and is a congruence. The framework is applied to the semantic characterisation and separation results for concurrent data structures including different queue implementations.

Paper Electronic version via DOI 
@inproceedings{FHY2012,
  author = {Luca Fossati and Kohei Honda and Nobuko Yoshida},
  title = {{Intensional and Extensional Characterisation of Global Progress in the π-Calculus}},
  booktitle = {23rd International Conference on Concurrency Theory},
  series = {LNCS},
  volume = {7454},
  pages = {287--301},
  publisher = {Springer},
  year = 2012
}

@inproceedings{FHY2012,
  author = {Luca Fossati and Kohei Honda and Nobuko Yoshida},
  title = {{Intensional and Extensional Characterisation of Global Progress in the π-Calculus}},
  booktitle = {23rd International Conference on Concurrency Theory},
  series = {LNCS},
  volume = {7454},
  pages = {287--301},
  publisher = {Springer},
  doi = "10.1007/978-3-642-32940-1_21",
  year = 2012
}