session-pi

A session-typed pi-calculus interpreter

Setup

1. Install nix:

$ run curl -L https://nixos.org/nix/install | sh

2. Initialize the nix environment

$ nix-shell

3. To build/run

$ dune exec --display quiet sessionPi

4. To run type-checker tests

$ dune exec test

make sure to run this command in the top-level directory

Main Paper

• Subtyping for session types in the pi calculus

Resources we may look into:

Fundamental

• Introduction to Session Types
• Linear Type Theory for Asynchronous Session Types (we should probably read this; seems very foundational)
• Foundations of Session Types and Behavioral Contracts
• Linearity, session types and pi-calculus
• Fundamentals of Session Types
• Behavioral Types in Programming Languages

Session Types + Deadlock Freedom

• Manifest Deadlock-freedom for Shared Session Types
• Deadlock-Free Session Types in Linear Haskell
• A new type system for deadlock-free processes
• A Static Verification Framework for Message Passing in Go using Behavioral Types
• Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom (2022!!!!)