ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency

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

Documentation

Code

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 https://gitlab.mpi-sws.org/dfrumin/logrel-conc.git

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.

Overview

Examples from the paper/technical report:

Last updated: 2018-09-04 di 14:05

Emacs 25.2.2 (Org mode 9.1.3)

Validate