[larsberg]

If you're interested in this topic, I'd highly recommend watching Stephanie Balzer's sessions at the Oregon Programming Language Summer School on “Session-Typed Concurrent Programming”. The lectures are available online (https://www.cs.uoregon.edu/research/summerschool/summer18/to...).

Her recent work (sponsored, in part, by Mozilla Research) really advances session types and the ability to get termination/progress guarantees: http://www.cs.cmu.edu/~balzers/publications/manifest_deadloc...

[YorkshireSeason]

In what sense does this work really advance session types? Prima facie it looks like yet another tiny delta on Honda's original work that cannot and does not get around session types' core problem of data-dependent communication topology. Let me quote from the paper (Page 22, Section 6):

"The typing discipline presented in the previous sections, while rich enough to account for a wide range of interesting programs, cannot type programs that spawn a statically undetermined number of shared sessions that are then to be used."

That has been the problem of this approach to typing message passing for nearly 3 decades, and like all predecessor papers in this theory tradition, an ad-hoc approach is proposed that makes core session types incredibly complicated without solving the problem. In order to get a publication out of this, a different problem is solved, a yet another Curry-Howard corresponce for some small delta of Linear Logic is given.