BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Effects as sessions\, sessions as effects - Dominic Orchard\, Comp
 uter Laboratory
DTSTART:20160205T140000Z
DTEND:20160205T150000Z
UID:TALK62549@talks.cam.ac.uk
CONTACT:Ohad Kammar
DESCRIPTION:Effect and session type systems are two expressive behavioural
  type systems. The former is usually developed in the context of the λ- c
 alculus and its variants\, the latter for the π-calculus. In this talk\, 
 I explore their relative expressive power. Firstly\, I give an embedding f
 rom PCF\, augmented with a parameterised effect system\, into a session-ty
 ped π-calculus (session calculus)\, showing that session types are powerf
 ul enough to express effects. Secondly\, I give a reverse embedding\, from
  the session calculus back into PCF\, by instantiating PCF with concurrenc
 y primitives and its effect system with a session-like effect algebra\; ef
 fect systems are powerful enough to express sessions. The embedding of ses
 sion types into an effect system is leveraged to give a new implementation
  of session types in Haskell\, via an effect system encoding. The correctn
 ess of this implementation follows from the second embedding result. This 
 is joint work with Nobuko Yoshida\, presented at POPL'16.
LOCATION:SS03
END:VEVENT
END:VCALENDAR