BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Manifest Sharing with Session Types  - Stephanie Balzer\, Carnegie
  Mellon University
DTSTART:20170908T100000Z
DTEND:20170908T110000Z
UID:TALK79021@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Session-typed languages building on the Curry-Howard isomorphi
 sm between linear logic and session-typed communication guarantee session 
 fidelity and deadlock freedom. Unfortunately\, these strong guarantees exc
 lude many naturally occurring programming patterns pertaining to shared re
 sources. In this talk\, I report on our work on manifest sharing\, which i
 ntroduces sharing into a session-typed language such that types are strati
 fied into linear and shared layers with modal operators connecting the lay
 ers. The resulting language retains session fidelity but not the absence o
 f deadlocks\, which can arise from contention for shared processes. Our la
 nguage can accommodate examples\, such as producer-consumer queues and din
 ing philosophers\, that could previously not be expressed with linear sess
 ion types alone\, including a translation of the untyped asynchronous pi-c
 alculus into our language. 
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR