Session Typing and Asynchronous Subtyping for the Higher-Order π-Calculus
File(s)main.pdf (941.06 KB) 1-s2.0-S0890540115000139-main.pdf (968.64 KB)
Accepted version
Published Version
Author(s)
Yoshida, N
Mostrous, D
Type
Journal Article
Abstract
This paper proposes a session typing system for the higher-order -calculus (the HOc-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 r-calculus using -calculus. Integration of arbitrary higherorder 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.
Date Issued
2015-02-07
Date Acceptance
2014-10-24
Citation
Information and Computation, 2015, 241, pp.227-263
ISSN
1090-2651
Publisher
Elsevier
Start Page
227
End Page
263
Journal / Book Title
Information and Computation
Volume
241
Copyright Statement
© 2015 The Authors. Published by Elsevier Inc. This is an open access article under the CC
BY license (http://creativecommons.org/licenses/by/4.0/).
BY license (http://creativecommons.org/licenses/by/4.0/).
License URL
Publication Status
Published