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

Read the journal paper Download the Coq source code

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.

Publications and case studies

Guide to the examples

The Coq formalization comes with a number of examples, intended to demonstrate and evaluate ReLoC: