![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > Two Sides of the Same Coin: Session Types and Game Semantics
Two Sides of the Same Coin: Session Types and Game SemanticsAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Noam Zeilberger. 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 π-calculus processes model programs. Giving faithful models of the π-calculus and giving a precise description of strategies as a programming language are two difficult problems. In this talk, we show how these two problems can be tackled at the same time by building an accurate game semantics model of the session π-calculus. Our main contribution is to fill a semantic gap between the synchrony of the (session) π-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) π-calculus. We further strengthen this correspondence, establishing finite definability of asynchronous strategies by the internal session π-calculus. As an application of these results, we propose a 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 strategies as a very accurate model of the session calculus. We implement a prototype which computes the interpretation of session processes as synchronous strategies. This talk is part of the Theoretical computer science seminar series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsSeminars on Advanced Materials Filling in the blank – I will be ….... in 2050’ Reading Group in Combinatorics and ProbabilityOther talksTBA TBC Counting cycles in planar graphs Ultrafast Spectroscopy and Microscopy as probes of Energy Materials Control variates for computing transport coefficients The tragic destiny of Mileva Marić Einstein |