2019-06-29
On the relative expressiveness of higher-order session processes
Publication
Publication
Information and Computation , Volume 268 p. 104433:1- 104433:54
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 π.
| Additional Metadata | |
|---|---|
| , , , , | |
| doi.org/10.1016/j.ic.2019.06.002 | |
| Information and Computation | |
|
Kouzapas, D., Pérez Parra, J., & Yoshida, N. (2019). On the relative expressiveness of higher-order session processes. Information and Computation, 268, 104433:1–104433:54. doi:10.1016/j.ic.2019.06.002 |
|
