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 paper, 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.