Philippa Gardner, Emanuele D’Osualdo and Julian Sutherland attended the first edition of the Iris workshop.

The two-day workshop, held at Aarhus University, Denmark focused on Iris, a Higher-Order Concurrent Separation Logic Framework implemented and verified in the proof assistant Coq that can be used for reasoning about safety of concurrent programs.

Philippa gave a talk on their joint work on “Compositional Reasoning for the Termination of Fine-grained Concurrent Programs”.