Second-order Game Semantics and Type Isomorphisms

Thanks to its precision and its simplicity, game semantic can be a powerful tool for analysing syntax. This is the case in particular for type isomorphisms, which can be efficiently captured by game models. I will present a game model of polymorphic lambda-calculus (system F), inspired by preceding works on the subject, and explain how it can be applied first to retrieve Church-style type isomorphisms, and then to give a new, complete characterisation of Curry-style ones. The question of parametricity in this context will be introduced as a perspective.