Using session types as an effect system
File(s)1602.03591v1.pdf (218.4 KB)
Published version
Author(s)
Orchard, D
Yoshida, N
Type
Journal Article
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.
Date Issued
2016-02-10
Date Acceptance
2015-04-18
Citation
Electronic Proceedings in Theoretical Computer Science, 2016, 203
ISSN
2075-2180
Publisher
"Electronic Proceedings in Theoretical Computer Science
Journal / Book Title
Electronic Proceedings in Theoretical Computer Science
Volume
203
Copyright Statement
© 2016 Orchard and Yoshida.
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Grant Number
ERI 025567 (EP/K034413/1)
PO 1553380
EP/K011715/1
Source
Eighth International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2015)
Subjects
cs.PL
F.3.3; D.3.2; F.3.2
Publication Status
Published
Start Date
2015-04-18
Date Publish Online
2016-02-10