This is the artifact for the paper Dependent Session Protocols in Separation Logic from First Principles by Jules Jacobs, Jonas Kastberg Hinrichsen, and Robbert Krebbers.
This artifact is bidirectionally hyperlinked with the PDF of the paper:
- Definitions, theorems, and examples in the Coq code are hyperlinked to the corresponding location in the paper.
- Definitions, theorems, and examples in the paper are hyperlinked to the corresponding location in the Coq code.
The artifact contains the following files:
- base.v: one-shot channels without subprotocols
- sub.v: one-shot channels with subprotocols
- session.v: multi-shot session channels
- imp.v: imperative channels
- sym_close.v: symmetric close operation
- send_close.v: combined send_close operation