Second-order type Isomorphisms through Game Semantics

The characterization of second-order type isomorphisms is a purely
syntactical problem (already solved by Roberto Di Cosmo in 1994) that
we popose to study under the enlightenment of game semantics. We
define a new game model of system F based on hyperforests (starting
from ideas of Hughes and Murawski-Ong) in which we show that
isomorphisms coincide with the "equality" on hyperforests associated
with types. Finally we recover Di Cosmo's equational characterization
of type isomorphisms from this equality.
This new approach leads to a more geometrical proof of the result.
Moreover, taking advantage of the high flexibility of game models, our
proof is general enough to be easily applied to different programming
features (like fix point operators and control) and thus leads to new
results.
In this talk I will present the main ideas of the proof, describe the
structure of the model and its extensions, and give some directions
towards a game semantics approach of some open problems like
Curry-style type isomorphisms.