Session types are a type-based approach to the verification of safety and liveness properties for message-passing programs. They encode the behavioural structure of message-passing programs by prescribing what and when should be exchanged through communication channels. Session types have been much studied in the context of core concurrent calculi, such as the π-calculus; a substantial amount of literature has clarified their fundamental properties. These studies, however, have not fully explored how session types can be integrated into existing programming languages. In practice, programming languages based on message-passing models (Go, Akka) do not rely on session types to verify communication correctness. Given this context, a natural question is: what is missing for the integration of session types into existing programming languages?

The main aim of my PhD work is to develop both indispensable theoretical underpinnings and practical tools that will help bridge the gap between the theory and the practice of session types. As an initial step towards this goal, we have recently studied the absolute expressiveness of session types. We have identified an elementary formulation of session types which we call minimal session types: it seems to be particularly relevant for the practical adoption of session types. In this note, we briefly summarize the key intuitions of minimal session types, and compare our approach with a few related works.