Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Wed 16 Jan 2019 15:43 - 16:05 at Sala II - Capabilities and Session Types I Chair(s): Dominic Orchard

Game semantics and session types are two formalisations of the same concept: message-passing open programs following certain protocols. Game semantics represents protocols as games, and programs as strategies; while session types specify protocols, and well-typed pi-calculus processes model programs.
Giving faithful models of the pi-calculus and giving a precise description of strategies as a programming language are two fundamental, but notoriously hard problems. In this paper, we show how these two problems can be tackled at the same time by building an accurate game semantics model of the session pi-calculus.

Our main contribution is to fill a semantic gap between the synchrony of the (session) pi-calculus and the asynchrony of game semantics, by developing an event-structure based game semantics for synchronous concurrent computation. This model supports the first truly concurrent fully abstract (for barbed congruence) interpretation of the synchronous (session) pi-calculus. We further strengthen this correspondence, establishing finite definability of asynchronous strategies by the internal session pi-calculus. As an application of these results, we propose an faithful encoding of synchronous strategies into asynchronous strategies by call-return protocols, which induces automatically an encoding at the level of processes. Our results bring session types and game semantics into the same picture, proposing the session calculus as a programming language for strategies, and the strategies as a very accurate model of the session calculus. We implement a prototype which computes the interpretation of session processes as synchronous strategies.

Slides (talk.pdf)909KiB

Wed 16 Jan

Displayed time zone: Belfast change

15:21 - 16:27
Capabilities and Session Types IResearch Papers at Sala II
Chair(s): Dominic Orchard University of Kent, UK
15:21
22m
Talk
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities
Research Papers
Lau Skorstengaard Aarhus University, Dominique Devriese Vrije Universiteit Brussel, Belgium, Lars Birkedal Aarhus University
Link to publication DOI Media Attached File Attached
15:43
22m
Talk
Two sides of the same coin: Session Types and Game Semantics
Research Papers
Simon Castellan Imperial College London, UK, Nobuko Yoshida Imperial College London
Link to publication DOI Pre-print Media Attached File Attached
16:05
22m
Talk
Exceptional Asynchronous Session Types: Session Types without Tiers
Research Papers
Simon Fowler The University of Edinburgh, Sam Lindley University of Edinburgh, UK, J. Garrett Morris University of Kansas, USA, Sara Décova
Link to publication DOI Pre-print Media Attached File Attached