DOI

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.
Original languageEnglish
Title of host publicationLICS'18
Subtitle of host publicationProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
Place of PublicationNew York, NY
PublisherAssociation for Computing Machinery (ACM)
Pages442-451
Number of pages10
ISBN (Print)978-1-4503-5583-4
DOIs
Publication statusPublished - 2018
EventLICS'18: The 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018

Conference

ConferenceLICS'18
Abbreviated titleLICS 2018
CountryUnited Kingdom
CityOxford
Period9/07/1812/07/18

    Research areas

  • Separation logic, logical relations, fine-grained concurrency, Iris, atomicity

ID: 47928947