A continuation passing translation for functional session types

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

• Sam Lindley, LFCS, School of Informatics, University of Edinburgh, Scotland
• Friday 04 December 2015, 14:00-15:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.