Effects as sessions, sessions as effects
File(s)popl16-orchard-yoshida.pdf (483.58 KB)
Accepted version
Author(s)
Orchard, D
Yoshida, N
Type
Conference Paper
Abstract
Effect and session type systems are two expressive behavioural type systems. The former is usually developed in the context of the lambda-calculus and its variants, the latter for the pi-calculus. In this paper we explore their relative expressive power. Firstly, we give an embedding from PCF, augmented with a parameterised effect system, into a session-typed pi-calculus (session calculus), showing that session types are powerful enough to express effects. Secondly, we give a reverse embedding, from the session calculus back into PCF, by instantiating PCF with concurrency primitives and its effect system with a session-like effect algebra; effect systems are powerful enough to express sessions. The embedding of session types into an effect system is leveraged to give a new implementation of session types in Haskell, via an effect system encoding. The correctness of this implementation follows from the second embedding result. We also discuss various extensions to our embeddings.
Date Issued
2016-01-11
Date Acceptance
2015-10-05
Citation
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016, 51 (1), pp.568-581
ISBN
978-1-4503-3549-2
Publisher
ACM
Start Page
568
End Page
581
Journal / Book Title
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Volume
51
Issue
1
Copyright Statement
© ACM 2016. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, http://dx.doi.org/10.1145/2837614.2837634.
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Engineering & Physical Science Research Council (E
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (E
Grant Number
EP/K011715/1
612985
PO 20131167
EP/L00058X/1, PO 20131167
ERI 025567 (EP/K034413/1)
Source
43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016)
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
session types
pi-calculus
effect systems
PCF
encoding
type systems
Concurrent Haskell
NOTIONS
Software Engineering
Publication Status
Published
Start Date
2016-01-20
Finish Date
2016-01-22
Coverage Spatial
St. Petersburg, FL, USA