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.
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.
experimental/hocap/counter.vand the ticket lock refinement is in
examples/coinflip.vand the late/early choice example is in