Session Types, AFAIU are a specific implementation of a linear logic in some type system and I am not all too familiar with them in practice. However, I would l

Session Types, AFAIU are a specific implementation of a linear logic in some type system and I am not all too familiar with them in practice. However, I would like to think I am well versed in Linear Logic and Substructural Type Theory. I think the works by Wadler are a good place to start, in particular is a sort of review paper, based in intuitionistic logic (which he also covers in said paper), on linear logic. It’s called ‘A Taste of Linear Logic’ (I actually have the paper open in Safari on my iPhone as I type this) and it is written as a sort of primer on the area. Wadler’s bibliographies on the works contained in the pages you linked are a good source as well. If you are at all coming from a place of familiarity with Haskell, a decent overview of the current discussions on Linear Types in functional languages is at [2]. And lastly, if you like videos, Simon Peyton Jones has a great talk on YouTube [3] where he discusses practical linear types for Haskell, but the theory is not Haskell specific. I will warn you that the latter two references make several arguments and then discuss uniqueness typing (which is related but very different) and that is a whole other rabbit hole of sources, but generally a good topic to dig into as well. [1] https://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/lineartaste-revised.pdf https://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/lin... [2] http://edsko.net/2017/01/08/linearity-in-haskell/ http://edsko.net/2017/01/08/linearity-in-haskell/ [3] https://youtu.be/t0mhvd3-60Y https://youtu.be/t0mhvd3-60Y