ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency

1 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.

2 Documentation

3 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-07-15 zo 11:05

Emacs 25.2.2 (Org mode 9.1.3)

Validate