Interactive proofs in higher-order concurrent separation logic

Robbert Krebbers, Amin Timany, Lars Birkedal

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

85 Citations (Scopus)


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 publicationPOPL 2017 Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
Place of PublicationNew York
PublisherAssociation for Computing Machinery (ACM)
Number of pages13
ISBN (Electronic)978-1-4503-4660-3
Publication statusPublished - 2017
EventPOPL 2017: The 44th ACM SIGPLAN Symposium on Principles of Programming Languages - Paris, France
Duration: 15 Jan 201721 Jan 2017

Publication series

ISSN (Print)0362-1340
ISSN (Electronic)1558-1160


ConferencePOPL 2017


  • Separation logic
  • Interactive theorem Proving
  • Coq
  • Fine-grained concurrency
  • Logical Relations


Dive into the research topics of 'Interactive proofs in higher-order concurrent separation logic'. Together they form a unique fingerprint.

Cite this