Session typing and asynchronous subtyping for the higher-order π-calculus

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, mobile code and asynchronous permutation of session actions, within processes that utilise structured, typed communications. Our first contribution is a session typing system for the HOπ-calculus using techniques from the linear λ-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. Our second contribution is to introduce an asynchronous subtyping system which uniformly deals with type-manifested asynchrony and linear functions. The most technical challenge for subtyping is to prove the transitivity of the subtyping relation. We also demonstrate the expressiveness of our typing system with an e-commerce example, where optimised processes can interact respecting the expected sessions.