On the relative expressiveness of higher-order session processes
File(s)
Accepted version
Author(s)
Kouzapas, Dimitrios
Pérez, Jorge A
Yoshida, Nobuko
Type
Journal Article
Abstract
By integrating constructs from the λ-calculus and the π-calculus, in higher-order process calculi
exchanged values may contain processes. This paper studies the relative expressiveness of HOπ,
the higher-order π-calculus in which communications are governed by session types. Our main
discovery is that HO, a subcalculus of HOπ which lacks name-passing and recursion, can serve
as a new core calculus for session-typed higher-order concurrency. We show that HO can encode
HOπ fully abstractly (up to typed contextual equivalence) more precisely and efficiently than the
first-order session π-calculus (π). Overall, under the discipline of session types, HOπ, HO, and π
are equally expressive; however, we show that HOπ is more tightly related to HO than to π.
exchanged values may contain processes. This paper studies the relative expressiveness of HOπ,
the higher-order π-calculus in which communications are governed by session types. Our main
discovery is that HO, a subcalculus of HOπ which lacks name-passing and recursion, can serve
as a new core calculus for session-typed higher-order concurrency. We show that HO can encode
HOπ fully abstractly (up to typed contextual equivalence) more precisely and efficiently than the
first-order session π-calculus (π). Overall, under the discipline of session types, HOπ, HO, and π
are equally expressive; however, we show that HOπ is more tightly related to HO than to π.
Date Issued
2019-10
Date Acceptance
2019-06-07
Citation
Information and Computation, 2019, 268, pp.1-54
ISSN
0890-5401
Publisher
Elsevier BV
Start Page
1
End Page
54
Journal / Book Title
Information and Computation
Volume
268
Copyright Statement
© 2019 Elsevier Ltd. All rights reserved. This manuscript is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International Licence http://creativecommons.org/licenses/by-nc-nd/4.0/
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Identifier
https://www.sciencedirect.com/science/article/pii/S0890540119300495
Grant Number
ERI 025567 (EP/K034413/1)
PO 20015393
EP/K011715/1
612985
Subjects
Science & Technology
Technology
Physical Sciences
Computer Science, Theory & Methods
Mathematics, Applied
Computer Science
Mathematics
Concurrency
Process calculi
Behavioural types
Session types
Expressiveness
LINEARITY
CALCULUS
08 Information and Computing Sciences
Computation Theory & Mathematics
Publication Status
Published
Date Publish Online
2019-06-29