Mechanization of "Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)"

Prerequisites

The Coq code is known to compile with:

• Coq: 8.16.1
• A development version of Iris (dev.2023-05-31.0.a22a81c2)

The Iris repository includes instructions on how to install it: https://gitlab.mpi-sws.org/iris/iris/

Compilation

The Coq code can be compiled using make. This will compile all the files in the theories directory.

Artifact description

The artifact is described in miniactris_annotated.pdf.