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

Prerequisites

The Coq code is known to compile with:

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

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

The artifact is described in miniactris_annotated.pdf.