Viðburðadagatal TD

ICE-TCS seminar: Effects in a pi - using session types as an effect system

  • 3.6.2015, 11:00 - 12:00

PLACE and TIME: Room M102 at 11am on Wednesday the 3rd of June
SPEAKER: Dominic Orchard (Imperial College, London, UK; WWW:
TITLE: Effects in a pi - using session types as an effect system

Milner showed that the pi-calculus subsumes the expressivity of the
lambda-calculus by giving a translation of lambda terms into
pi-calculus processes.  Recently it has been shown that a typed
translation is also possible: the simply-typed lambda calculus can be
translated into the pi-calculus augmented with the session-typing
discipline. That is, the type theory of the lambda calculus is
subsumed by session types, which describe and restrict the
communication behaviour of pi-calculus programs.

But session types are even more powerful than this. In this talk, I
show that session types also subsume effect systems. This is shown by
an effect-preserving translation from the lambda calculus with a
type-and-effect system (for example, for reasoning about state side
effects) into the session-typed pi-calculus; effect types are
represented as session types.  This expressivity result can be
leveraged, for example, to safely introduce implicit parallelism when
compiling functional code, even in the presence of possible

This is joint work with Nobuko Yoshida.