Towards modular reasoning for concurrent higher-order imperative code

Kasper Svendsen

Modern programming languages support powerful combinations of shared mutable state, concurrency and higher-order functions. This makes it notoriously difficult to write correct code and requires new formal reasoning techniques.

In this talk I will give an overview of recent work by me and my coauthors on developing program logics that support modular reasoning for concurrent higher-order imperative code. Our goal is to develop reasoning principles that allow libraries that use these features internally to be verified against abstract specifications that hide these complications from clients. For instance, fine-grained concurrent data structures are carefully written not to expose interleavings of internal memory operations to clients. Ideally, our logics should be able to exploit this to allow clients to reason in terms of the abstract operations provided by the data structure.

I will introduce the main ideas behind two recent program logics, iCAP and Iris. Both logics are based on higher-order separation logic and aim to support modular reasoning about fine-grained concurrent data structures and re-entrant higher-order code.

This talk is based on joint work with Lars Birkedal, Filip Sieczkowski, Ralf Jung, David Swasey, Aaron Turon and Derek Dreyer.