Abstract

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.