π-calculus, Session Types research at Imperial College
This paper proposes a session typing system for the higher-order π-calculus (the HOπ-calculus) with asynchronous communication subtyping, which allows partial commutativity of actions in higher-order processes. The system enables two complementary kinds of optimisation of communication code, mobile code and asynchronous permutation of session actions, within processes that utilise structured, typed communications. Our first contribution is to establish a session typing system for the higher-order π-calculus using λ-calculus. Integration of arbitrary higher-order code mobility and sessions leads to technical difficulties in type soundness, because linear usage of session channels and completion of sessions are required in executed code. Our second contribution is to introduce the asynchronous subtyping system which uniformly deals with type-manifested asynchrony and linear functional types. The most technical challenge for the asynchronous subtyping is to prove the transitivity of the subtyping relation. For the runtime system we propose a new compact formulation that takes into account stored higher-order values with open sessions, as well as asynchronous commutativity. The paper also demonstrates the expressiveness of our typing system with an e-commerce example, where optimised processes can interact respecting the expected sessions.
@article{MY2015,
author = {Dimitris Mostrous and Nobuko Yoshida},
title = {{Session Typing and Asynchronous Subtyping for the Higher-Order π-Calculus}},
journal = {Inform. Comput.},
volume = {241},
pages = {227--263},
publisher = {Elsevier},
year = 2015
}
@article{MY2015,
author = {Dimitris Mostrous and Nobuko Yoshida},
title = {{Session Typing and Asynchronous Subtyping for the Higher-Order π-Calculus}},
journal = {Journal of Information and Computation},
volume = {241},
pages = {227--263},
publisher = {Elsevier},
doi = "10.1016/j.ic.2015.02.002",
year = 2015
}