The recent introduction of manifest sharing into session-typed message-passing programming has increased the range of applicability of session-typed programming from a purely linear setting to one supporting shared resources. As opposed to persistent servers available through the exponential modality in linear session types, which have a copying semantics, shared resources have a sharing semantics and thus can accommodate server resources, such as shared data bases or shared output devices. To uphold the benefits of linear session-typed programming, manifest sharing integrates linear session types and shared session types using adjoint modalities. Semantically, the modalities give rise to an acquire-release discipline, where an acquire yields exclusive access to a shared process, if the process is available, and a release relinquishes exclusive access.

In this tutorial, we review linear session types and their logical foundation, based on the existence of a Curry-Howard isomorphism between linear logic and the session-typed π-calculus. We then focus on manifest sharing, explore its logical foundation, and discuss its resulting gain in program expressiveness, which is witnessed by an encoding of the untyped asynchronous π-calculus into shared session types. The encoding crucially depends on the existence of shared channels, which are key to introducing observable non-determinism in the resulting language. Various program examples are used throughout the tutorial for illustration purposes.