Abstract: Game semantics provides a representation of open programs as sequences of actions representing any possible interactions with the environment. Such a framework enables a module to be represented as the set of interactions with any client written in the same programming language. This form of semantics is particularly suited to studying higher-order programming languages with computational effects, like control operators (call/cc, exceptions) and mutable state. Indeed, it provides fully-abstract semantics, i.e. models that capture the observational power of the programming language.

In this talk, we will provide a gentle introduction of game semantics, from an operational point of view. We focus on a representation of programs as labelled transition systems (LTS) generating the interactions. A notion of composition of programs is then deduced from synchronization of LTS. We will exemplify the semantics on various features found in the programming language OCaml, ranging from dynamically-allocated mutable references, exceptions, to abstract data-types and GADTs. As the manipulated sequences of actions are of simple complexity, it also allows one to reason automatically about such programs, via model-checking techniques, that we will briefly present if time permits.

Guilhem Jaber obtained his PhD in computer science from the École des Mines de Nantes in 2014, under the supervision of Alexandre Miquel and Nicolas Tabareau. From 2014 to 2018, he held various post-doctoral positions at Queen Mary University of London, IRIF (Paris Cité Université), and LIP (ENS de Lyon). Since September 2018, he is an associate professor at Nantes University, in the Inria Gallinette team. His research interests include programming language semantics, type theory, and software model checking.

--
Comunicaciones DCC