Many congratulations to Emanuele D’Osualdo, Azadeh Farzan, Philippa Gardner and Julian Sutherland, whose paper “TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs” has been accepted for publication at the ACM Transactions on Programming Languages and Systems (TOPLAS) journal.
The paper introduces TaDA Live, a separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The logic contributes several innovations to obtain modular rely/guarantee style reasoning for liveness properties and to blend them with logical atomicity.
TOPLAS is the bimonthly ACM peer-reviewed scientific journal on programming languages. TOPLAS reports in depth on recent research advances in the areas of programming languages. Papers published at TOPLAS must contain innovative and novel content that advances the state of the art of programming languages and systems; many congratulations to all on a fine achievement after a lot of hard work.