Many congratulations to [Emanuele D’Osualdo](https://www.emanueledosualdo.com/about/), [Azadeh Farzan](https://www.cs.toronto.edu/~azadeh/), Philippa Gardner and [Julian Sutherland](https://www.doc.ic.ac.uk/~jhs110/), 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)](https://dl.acm.org/journal/toplas) journal.
Many congratulations to [Emanuele D’Osualdo](https://www.emanueledosualdo.com/about/), [Azadeh Farzan](https://www.cs.toronto.edu/~azadeh/), Philippa Gardner and [Julian Sutherland](https://www.doc.ic.ac.uk/~jhs110/), whose paper [“TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs”](https://gitlab.doc.ic.ac.uk/resource-reasoning/publications/-/blob/d7c1f1ee5690694acefb7f8836dda455ae309b05/DOsualdo2020TaDa.pdf) has been accepted for publication at the [ACM Transactions on Programming Languages and Systems (TOPLAS)](https://dl.acm.org/journal/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.
