On the Relative Expressiveness of Higher-Order Session Processes
Apr 2016
By integrating constructs from the lambda-calculus and the pi-calculus, in higher-order process calculi exchanged values may contain processes.
This paper studies the relative expressiveness of HOpi, the higher-order pi-calculus in which communications are governed by session types. Our main discovery is that HO, a subcalculus of HOpi which lacks name-passing and recursion, can serve as a new core calculus for session-typed higher-order concurrency. By exploring a new bisimulation for HO, we show that HO can encode HOpi fully abstractly (up to typed contextual equivalence) more precisely and efficiently than the first-order session pi-calculus (pi).
Overall, under session types, HOpi, HO, and pi are equally expressive; but HOpi and HO are more tightly related than HOpi and pi.
