Using session types as an effect system

TL;DR

This paper demonstrates that session types can serve as an effect system to reason about concurrent side effects, providing a formal foundation by encoding an imperative language with effects into the pi-calculus with session types.

Contribution

It introduces an effect-preserving encoding of an imperative language with effects into session-typed pi-calculus, linking session types with effect systems for concurrent programming.

Findings

Session types can encode effect systems for stateful processes.

The encoding preserves effects from the source language.

This approach connects session types with reasoning about concurrent side effects.

Abstract

Side effects are a core part of practical programming. However, they are often hard to reason about, particularly in a concurrent setting. We propose a foundation for reasoning about concurrent side effects using sessions. Primarily, we show that session types are expressive enough to encode an effect system for stateful processes. This is formalised via an effect-preserving encoding of a simple imperative language with an effect system into the pi-calculus with session primitives and session types (into which we encode effect specifications). This result goes towards showing a connection between the expressivity of session types and effect systems. We briefly discuss how the encoding could be extended and applied to reason about and control concurrent side effects.