It is fair to say that expressiveness has been key to the success and impact of session types: enhancing the expressivity of typed processes and/or the properties enforced by typing is often a strong motivation for developing new typed frameworks. Rigorously contrasting different variants of session types from an expressiveness perspective is a pressing and non-trivial challenge.
This talk gives a unified overview of some of our works in this direction; they cover various angles, including: higher-order communication, binary and multiparty protocols, and “propositions-as-sessions”. The proposed talk is meant to elucidate (recent) achievements but also avenues for future exploration