From Lock Freedom to Progress Using Session Types

Luca Padovani

Inspired by Kobayashi's type system for lock freedom, we define a behavioral type system for ensuring progress in a language of binary sessions. The key idea is to annotate actions…