Imperial College London
Professor Nobuko Yoshida

ProfessorNobukoYoshida

Faculty of Engineering, Department of Computing

Academic Visitor
 
 
 
//

Contact

 

+44 (0)20 7594 8240n.yoshida Website

 
 
//

Location

 

556Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Orchard:2016:10.4204/EPTCS.203.1,
author = {Orchard, D and Yoshida, N},
doi = {10.4204/EPTCS.203.1},
publisher = {"Electronic Proceedings in Theoretical Computer Science},
title = {Using session types as an effect system},
url = {http://dx.doi.org/10.4204/EPTCS.203.1},
year = {2016}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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.
AU  - Orchard,D
AU  - Yoshida,N
DO  - 10.4204/EPTCS.203.1
PB  - "Electronic Proceedings in Theoretical Computer Science
PY  - 2016///
SN  - 2075-2180
TI  - Using session types as an effect system
UR  - http://dx.doi.org/10.4204/EPTCS.203.1
UR  - http://hdl.handle.net/10044/1/33075
ER  -
Download