In this talk we present our work on sessions for the higher-order pi-calculus facilitating asynchronous protocol subtyping. Our system provides two complementary methods for communication code optimisation, mobile code and asynchronous permutation of session actions, within processes that utilise structured, typed communications.
First we will give an overview of sessions in a language based on the HO pi-calculus. Then we explain linear type theory as applied to ensure type-safety of mobile code containing active sessions. We then introduce a simulation-based method for subtyping which incorporates rules that allow partial permutation of actions within a session type.
Highlights of the work include proving essential properties of our subtyping, mainly transitivity, while dealing with with type-manifested asynchrony, linear functional types, and higher-order communications.
We also demonstrate the expressiveness of our typing system with an e-commerce example, where optimised processes can interact respecting the expected sessions.