Robbert Krebbers
Delft University of Technology, Netherlands
Relational reasoning using concurrent separation logic
Relational reasoning in the form of program refinement and program equivalence plays an important role in computer science---for example, it is used to show that optimized versions of data structures behave the same as their non-optimized versions, to prove linearizability of concurrent data structures, and to prove correctness of program transformations. In this talk, I will describe recent developments in concurrent separation logic (especially in the Iris framework in the Coq proof assistant) that make it possible to prove contextual refinements for rich languages with higher-order state and fine-grained concurrency in a modular and mechanized fashion.
