BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A continuation passing translation for functional session types - 
 Sam Lindley\, LFCS\, School of Informatics\, University of Edinburgh\, Sco
 tland
DTSTART:20151204T140000Z
DTEND:20151204T150000Z
UID:TALK62499@talks.cam.ac.uk
CONTACT:Ohad Kammar
DESCRIPTION:Session types provide a static guarantee that a concurrent pro
 gram\nrespects a communication protocol. Recently\, Luis Caires and Frank\
 nPfenning developed a correspondence between the propositions of linear\nl
 ogic and session typed pi-calculus processes. As part of the ABCD (A\nBasi
 s for Concurrency and Distribution) project we have added session\ntypes t
 o the Links functional web programming language. Session types\nin Links a
 re based on GV\, a small extension of an intuitionistic\nlinear lambda cal
 culus. Garrett Morris and I recently showed a tight\ncorrespondence betwee
 n GV\, and Phil Wadler's classical linear logic\ninterpretation of session
  types\, CP: reduction in GV and cut-reduction\nin CP can simulate one ano
 ther. Thus\, there are strong connections\nbetween the core of Links and c
 lassical linear logic.\n\nI will present an alternative semantics for GV b
 y defining a\ncontinuation passing translation into plain lambda calculus.
  The\ntranslation seems a little unsatisfactory in that certain\nsession-t
 yping constructs are translated differently depending on\nwhether they con
 cern communication channels whose next action is an\ninput or an output. I
  will show how to define a more uniform\ncontinuation passing translation 
 on a polarised variant of\nGV. Different reduction strategies in the targe
 t language correspond\nto different schedules in the source language.
LOCATION:FW26
END:VEVENT
END:VCALENDAR