ReLoC

A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity

Dan Frumin, Robbert Krebbers, Lars Birkedal

LICS 2018 paper Extended journal paper Latest version of ReLoC

ReLoC ReLoC is a mechanised logic for interactively proving contextual refinements of programs in a language with higher-order state, fine-grained concurrency, polymorphism and existential and recursive types.

ReLoC is built on top of Iris—a state of the art concurrent separation logic.

ReLoC Reloaded

A new version of ReLoC is under development and is available online at https://gitlab.mpi-sws.org/iris/reloc. Do check it out!

ReLoC Reloaded improves on the logic described in the LICS18 paper in several ways. In terms of the formalization it works with the latest version of Iris, and it is build directly on top of heap_lang – the programming language that comes directly with Iris.

Guide to the examples