π-calculus, Session Types research at Imperial College
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.
@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
}