کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
6874025 686415 2015 76 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Session typing and asynchronous subtyping for the higher-order π-calculus
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
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.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 241, April 2015, Pages 227-263
نویسندگان
, ,