Interactive proofs in higher-order concurrent separation logic

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review



When using a proof assistant to reason in an embedded logic - like separation logic - one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they are cluttered with bookkeeping code related to manipulating the object logic. In this paper, we introduce a so-called proof mode that extends the Coq proof assistant with (spatial and non-spatial) named proof contexts for the object logic. We show that thanks to these contexts we can implement high-level tactics for introduction and elimination of the connectives of the object logic, and thereby make reasoning in the embedded logic as seamless as reasoning in the meta logic of the proof assistant. We apply our method to Iris: a state of the art higher-order impredicative concurrent separation logic. We show that our method is very general, and is not just limited to program verification. We demonstrate its generality by formalizing correctness proofs of fine-grained concurrent algorithms, derived constructs of the Iris logic, and a unary and binary logical relation for a language with concurrency, higher-order store, polymorphism, and recursive types. This is the first formalization of a binary logical relation for such an expressive language. We also show how to use the logical relation to prove contextual refinement of fine-grained concurrent algorithms.

Original languageEnglish
Title of host publicationProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017
EditorsAndrew D. Gordon, Giuseppe Castagna
Number of pages13
PublisherAssociation for Computing Machinery
Publication year2017
ISBN (print)978-1-4503-4660-3
ISBN (Electronic)9781450346603
Publication statusPublished - 2017
EventThe 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017) - Paris, France
Duration: 15 Jan 201721 Jan 2017
Conference number: 44


ConferenceThe 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017)

    Research areas

  • Coq, Fine-grained Concurrency, Interactive Theorem Proving, Logical Relations, Separation Logic

See relations at Aarhus University Citationformats

ID: 119402056