MobilityReadingGroup

Using session types as an effect system

Dominic ORCHARD, Nobuko YOSHIDA

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. 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 π-calculus with sessions and session types (into which we encode effect specifications). We demonstrate how this technique can be used to reason about, specify, and control the scope of concurrent side effects.

@inproceedings{OY2015,
  author = {Dominic Orchard and Nobuko Yoshida},
  title = {{Using session types as an effect system}},
  booktitle = {7th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software},
  pages = {1--12},
  year = 2015
}

@inproceedings{OY2015,
  author = {Dominic Orchard and Nobuko Yoshida},
  title = {{Using session types as an effect system}},
  booktitle = {7th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software},
  pages = {1--12},
  year = 2015
}