Abstract
We present ReLoC: a logic for proving refinements of programs in a language with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of our logic is a judgement e ⪯ e': τ, which expresses that a program e refines a program e' at type τ. In contrast to earlier work on refinements for languages with higher-order state and concurrency, ReLoC provides type- and structure-directed rules for manipulating this judgement, whereas previously, such proofs were carried out by unfolding the judgement into its definition in the model. These more abstract proof rules make it simpler to carry out refinement proofs.
Moreover, we introduce logically atomic relational specifications: a novel approach for relational specifications for compound expressions that take effect at a single instant in time. We demonstrate how to formalise and prove such relational specifications in ReLoC, allowing for more modular proofs.
ReLoC is built on top of the expressive concurrent separation logic Iris, allowing us to leverage features of Iris such as invariants and ghost state. We provide a mechanisation of our logic in Coq, which does not just contain a proof of soundness, but also tactics for interactively carrying out refinements proofs. We have used these tactics to mechanise several examples, which demonstrates the practicality and modularity of our logic.
Moreover, we introduce logically atomic relational specifications: a novel approach for relational specifications for compound expressions that take effect at a single instant in time. We demonstrate how to formalise and prove such relational specifications in ReLoC, allowing for more modular proofs.
ReLoC is built on top of the expressive concurrent separation logic Iris, allowing us to leverage features of Iris such as invariants and ghost state. We provide a mechanisation of our logic in Coq, which does not just contain a proof of soundness, but also tactics for interactively carrying out refinements proofs. We have used these tactics to mechanise several examples, which demonstrates the practicality and modularity of our logic.
Original language | English |
---|---|
Title of host publication | LICS'18 |
Subtitle of host publication | Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science |
Place of Publication | New York, NY |
Publisher | Association for Computing Machinery (ACM) |
Pages | 442-451 |
Number of pages | 10 |
ISBN (Print) | 978-1-4503-5583-4 |
DOIs | |
Publication status | Published - 2018 |
Event | LICS'18: The 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - Oxford, United Kingdom Duration: 9 Jul 2018 → 12 Jul 2018 |
Conference
Conference | LICS'18 |
---|---|
Abbreviated title | LICS 2018 |
Country/Territory | United Kingdom |
City | Oxford |
Period | 9/07/18 → 12/07/18 |
Keywords
- Separation logic
- logical relations
- fine-grained concurrency
- Iris
- atomicity