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...
| Principais autores: | , , |
|---|---|
| Formato: | Artigo |
| Idioma: | English |
| Publicado em: |
Logical Methods in Computer Science e.V.
2021-07-01
|
| coleção: | Logical Methods in Computer Science |
| Assuntos: | |
| Acesso em linha: | https://lmcs.episciences.org/6598/pdf |