Sciweavers

Share
POPL
2016
ACM

Effects as sessions, sessions as effects

3 years 9 days ago
Effects as sessions, sessions as effects
Effect and session type systems are two expressive behavioural type systems. The former is usually developed in the context of the λcalculus and its variants, the latter for the π-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 π-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. Categories...
Dominic A. Orchard, Nobuko Yoshida
Added 09 Apr 2016
Updated 09 Apr 2016
Type Journal
Year 2016
Where POPL
Authors Dominic A. Orchard, Nobuko Yoshida
Comments (0)
books