ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency


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—state of the art concurrent separation logic.



The Coq source code is available online. The branch that corresponds to the paper is reloc1. You can also download an appropriate .zip file directly.

git clone -b reloc1

Installation instructions

The formalisation is know to compile with Coq 8.6.1 and Ssreflect 1.6.

The following libraries are the prerequisites:

Once all the dependencies are installed, just run make in the top-level directory.


Examples from the paper/technical report:

Last updated: 2019-01-15 Tue 17:27

Emacs 26.1 (Org mode 9.1.3)