Discussing "Iris from the ground up: A modular foundation for higher-order concurrent separation logic"

(Link)

Authors: Ralf Jung (Max Planck Institute for Software Systems), Robbert Krebbers (Delft University of Technology), Jacques-Henri Jourdan (Max Planck Institute for Software Systems), Aleš Bizjak (Aarhus University), Lars Birkedal (Aarhus University), Derek Dreyer (Max Planck Institute for Software Systems)

Reference: JUNG, R., KREBBERS, R., JOURDAN, J., BIZJAK, A., BIRKEDAL, L., & DREYER, D. (2018). Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28, E20. doi:10.1017/S0956796818000151

Why this paper? Cited by A Decision Procedure for Guarded Separation Logic, Mechanised Robust Safety for Virtual Machines Communicating above FF-A, and Fractional Resources in Unbounded Separation Logic

This 2018 paper is more recent than most I get referred to by the citations in my Google Scholar recommendations, but there’s no doubting the relevance to me given that three of the authors (Robbert, Aleš, and Lars) are former colleagues at Aarhus University’s Logic and Semantics Group.

This paper summarises a series of papers from 2014 on, developing a logic called Iris. This is the latest evolution of separation logic (and, in turn, Hoare logic) for reasoning formally about the correctness of programs. The game here has been to add more advanced functionality to allow reasoning about programs written in a variety of programming languages without blowing up the logic to unreasonable size and complexity. As such, Iris is packed with features which encompass some I’ve written about already in the blog, such as permissions and step-indexing, along with many others such as various notions of concurrency and higher-order store. Many of these features are derivable via a small(ish) core logic, and the whole framework is usable in the interactive theorem prover Coq to facilitate fully formal, machine-checked proofs.

I will not be attempting to exhaustively summarise a 73 page paper in a short blog post, but to take one example of the flexibility of the logic, an Iris user can define their own ‘camera’ which defines the notion of state they want to invoke separation with respect to, whether it be Reynolds’s old notion of the physical memory, or some more exotic notion of `ghost state’ which does not directly relate to physical state.