Detail

On the Relative Expressiveness of Higher-Order Session Processes

By integrating constructs from the ?-calculus and the ?-calculus, in higher-order process calculi exchanged values may contain processes.

In this talk I will overview recent results on 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. By exploring a new bisimulation for HO, we show that HO can encode HO? more precisely han
the first-order session ?-calculus (?).

Overall, under session types, HO?, HO, and ? are equally expressive; however, HO? and HO are more tightly related than HO? and ?.