Write a Blog >>
Thu 21 Jan 2016 16:30 - 16:55 at Grand Bay South - Track 2: Sessions and processes Chair(s): Matteo Maffei

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 π-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.

Thu 21 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

16:30 - 17:45
Track 2: Sessions and processesResearch Papers at Grand Bay South
Chair(s): Matteo Maffei Saarland University
16:30
25m
Talk
Effects as sessions, sessions as effects
Research Papers
Dominic Orchard Imperial College London, Nobuko Yoshida Imperial College London, UK
Pre-print Media Attached
16:55
25m
Talk
Monitors and Blame Assignment for Higher-Order Session Types
Research Papers
Limin Jia Carnegie Mellon University, Hannah Gommerstadt Carnegie Mellon University, Frank Pfenning Carnegie Mellon University
Media Attached File Attached
17:20
25m
Talk
Environmental Bisimulations for Probabilistic Higher-Order Languages
Research Papers
Davide Sangiorgi University of Bologna, Valeria Vignudelli University of Bologna/INRIA
Media Attached