کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6874025 | 686415 | 2015 | 76 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Session typing and asynchronous subtyping for the higher-order Ï-calculus
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
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
Journal: Information and Computation - Volume 241, April 2015, Pages 227-263
نویسندگان
Dimitris Mostrous, Nobuko Yoshida,