README.md

Thesis

This repository contains the artifacts of my master thesis "A logic for reasoning with mailbox types in separation logic".

Rocq development

The Rocq development is known to compile with:

• Rocq version 9.1.0
• OCaml version 4.14.1
• rocq-iris version dev.2025-11-19.0.ddfb616b
• rocq-iris-heap-lang version dev.2025-11-19.0.ddfb616b
• rocq-stdpp version dev.2025-11-18.2.f049a0f8

Ensure that opam is installed on your system and install the dependencies:

opam switch create iris-zanaris ocaml-base-compiler.4.14.1
eval $(opam env)
opam switch link iris-zanaris .
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam pin add --kind version rocq-iris-heap-lang "dev.2025-11-19.0.ddfb616b"

To build the project, run make -jN, where N is the number of CPU cores to use.

Directory structure

• The theories/mailbox directory contains the implementation of mailboxes and the proof rules (chapter 4).
  • The implementation of mailboxes and the proof rules are given in mailbox.v (section 4.2).
  • The model of patterns is given in pattern.v (section 4.1.1).
  • The definitions for predicate tables are given in table.v (section 4.1.2).
  • The definition of tags is given in tag.v.
• The theories/utils directory contains reusable utilities (section 2.4.1, section 2.4.2).
• The theories/examples directory contains the proofs of the examples (section 4.3).