University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > A continuation passing translation for functional session types

A continuation passing translation for functional session types

Add to your list(s) Download to your calendar using vCal

  • UserSam Lindley, LFCS, School of Informatics, University of Edinburgh, Scotland World_link
  • ClockFriday 04 December 2015, 14:00-15:00
  • HouseFW26.

If you have a question about this talk, please contact Ohad Kammar.

Session types provide a static guarantee that a concurrent program respects a communication protocol. Recently, Luis Caires and Frank Pfenning developed a correspondence between the propositions of linear logic and session typed pi-calculus processes. As part of the ABCD (A Basis for Concurrency and Distribution) project we have added session types to the Links functional web programming language. Session types in Links are based on GV, a small extension of an intuitionistic linear lambda calculus. Garrett Morris and I recently showed a tight correspondence between GV, and Phil Wadler’s classical linear logic interpretation of session types, CP: reduction in GV and cut-reduction in CP can simulate one another. Thus, there are strong connections between the core of Links and classical linear logic.

I will present an alternative semantics for GV by defining a continuation passing translation into plain lambda calculus. The translation seems a little unsatisfactory in that certain session-typing constructs are translated differently depending on whether they concern communication channels whose next action is an input or an output. I will show how to define a more uniform continuation passing translation on a polarised variant of GV. Different reduction strategies in the target language correspond to different schedules in the source language.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity