Skip to main content
Kent Academic Repository

Effects as Sessions, Sessions as Effects

Orchard, Dominic A., Yoshida, Nobuko (2016) Effects as Sessions, Sessions as Effects. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2016, . pp. 568-581. (doi:10.1145/2837614.2837634) (KAR id:57481)


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

Item Type: Article
DOI/Identification number: 10.1145/2837614.2837634
Uncontrolled keywords: session types, pi-calculus, effect systems, PCF, encoding, type systems, Concurrent Haskell
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Funders: Organisations -1 not found.
Organisations -1 not found.
Depositing User: Dominic Orchard
Date Deposited: 26 Sep 2016 12:41 UTC
Last Modified: 23 Apr 2022 22:07 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.