MobilityReadingGroup

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

Process Types as a Descriptive Tool for Interaction: Control and the Pi-Calculus
Kohei HONDA , Nobuko YOSHIDA , Martin BERGER
Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014). p. 1 - 20

We demonstrate a tight relationship between linearly typed π-calculi and typed λ-calculi by giving a type-preserving translation from the call-by-value λμ-calculus into typed π-calculus. The λμ-calculus has a particularly simple representation as typed mobile processes. The target calculus is a simple variant of the linear π-calculus. We establish full abstraction up to maximally consistent observational congruences in source and target calculi using techniques from games semantics and process calculi.

Paper (invited) Electronic version via DOI 
@inproceedings{HYB2014,
  author = {Kohei Honda and Nobuko Yoshida and Martin Berger},
  title = {{Process Types as a Descriptive Tool for Interaction: Control and the Pi-Calculus}},
  booktitle = {Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications},
  series = {LNCS},
  volume = {8560},
  pages = {1--20},
  publisher = {Springer},
  year = 2014
}

@inproceedings{HYB2014,
  author = {Kohei Honda and Nobuko Yoshida and Martin Berger},
  title = {{Process Types as a Descriptive Tool for Interaction: Control and the Pi-Calculus}},
  booktitle = {Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications},
  series = {LNCS},
  volume = {8560},
  pages = {1--20},
  publisher = {Springer},
  doi = "10.1007/978-3-319-08918-8_1",
  year = 2014
}