Interactive Proofs in Higher-Order Concurrent Separation Logic

Introduction

This webpage contains the Coq sources corresponding to the paper:

Interactive Proofs in Higher-Order Concurrent Separation Logic,
by Robbert Krebbers, Amin Timany and Lars Birkedal,
accepted for publication at POPL'17.

In the paper, we introduce IPM: Interactive Proof Mode for embedded logics in Coq, a novel method for extending the Coq proof assistant with (spatial and non-spatial) named proof contexts for the object logic. We show that thanks to these contexts we are able to implement high-level tactics for introduction and elimination of all 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 IPM is very general, and - in contrast to earlier work - 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.

Download

The Coq sources consist of two parts:

• Iris, which includes the formalization of IPM. The version in the paper corresponds with commit 1a17276b of the Iris git repository.
• The case study, in which we have formalized logical relations using IPM. The version in the paper corresponds with commit 2463dae8.

For convenience, we have packaged these two parts, together with the examples in paper, as a tarball.

Prerequisites

The Coq formalization is known to compile with:

• Coq 8.5pl1, available at https://coq.inria.fr/distrib/V8.5pl1/files/
• Ssreflect 1.6, available at https://github.com/math-comp/math-comp/tree/release/1.6
• Autosubst 1.5, available at https://github.com/tebbi/autosubst/tree/v1.5

Building Instructions

The development can be build as follows:

• Install the Ssreflect and Autosubst libraries as a Coq user contribution. You can use either the above git repositories or OPAM. Note that installation requires super user privileges if Coq itself has been installed globally (i.e., if Coq was installed with super user privileges and not with the -local configure flag).
  Furthermore, note that you have to install just the ssreflect plugin, available in the folder mathcomp/ssreflect of the aforementioned git repository. Installing the whole mathematical components library is not necesarry.
• Go to the iris of the tarball, or obtain it via the aforementioned git repository, and run make -j [num cores] to build the full development. The development should then be installed as the Coq user contribution iris by running make install. Installation might require super user privileges if Coq itself is installed globally (i.e., if Coq was installed with super user privileges).
• Go to the iris-logrel folder, or obtain it via the aforementioned git repository, and run make to build the full development.

Getting around

• The file ProofMode.md in the iris folder contains a cheat sheet with most IPM tactics, including the grammar of introduction and specialization patterns.
• The examples of the paper are included in the examples folder. These examples require Iris to be installed as a user contribution.
• The logical relations development in the folder iris-logrel also contains formalizations of the logical relation for simpler languages (simply typed lambda calculus, System F with recursive types, System F with recursive types and load/store). These formalizations may serve as a simple introduction.