A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
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.
experimental/hocap/counter.vand the ticket lock refinement is in
examples/coinflip.vand the late/early choice example is in