ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
We present a new version of ReLoC: a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of ReLoC is its refinement judgment $e \precsim e' : \tau$, which states that a program $e$ refines...
| Hoofdauteurs: | , , |
|---|---|
| Formaat: | Artikel |
| Taal: | English |
| Gepubliceerd in: |
Logical Methods in Computer Science e.V.
2021-07-01
|
| Reeks: | Logical Methods in Computer Science |
| Onderwerpen: | |
| Online toegang: | https://lmcs.episciences.org/6598/pdf |