Skip to main content

Using session types as an effect system

Orchard, Dominic, Yoshida, Nobuko (2016) Using session types as an effect system. Electronic Proceedings in Theoretical Computer Science, 203 . pp. 1-13. ISSN 2075-2180. (doi:10.4204/EPTCS.203.1) (KAR id:61624)

PDF Publisher pdf
Language: English


Download (216kB) Preview
[thumbnail of 1602.03591.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL
https://doi.org/10.4204/EPTCS.203.1

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.

Item Type: Article
DOI/Identification number: 10.4204/EPTCS.203.1
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Dominic Orchard
Date Deposited: 05 May 2017 15:11 UTC
Last Modified: 24 Nov 2021 10:43 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/61624 (The current URI for this page, for reference purposes)
  • Depositors only (login required):