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
Keywords Behavioural types, Concurrency, Expressiveness, Process calculi, Session types
Persistent URL
Journal Information and Computation
Kouzapas, D, Pérez Parra, J.A, & Yoshida, N. (2019). On the relative expressiveness of higher-order session processes. Information and Computation. doi:10.1016/j.ic.2019.06.002