Second-Order Type Isomorphisms Through Game Semantics

The characterization of second-order type isomorphisms is a purely syntactical problem that we propose to study under the enlightenment of game semantics. We study this question in the case of second-order λ$μ$-calculus, which can be seen as an extension of system F to classical logic, and for which we define a categorical framework: control hyperdoctrines. Our game model of λ$μ$-calculus is based on polymorphic arenas (closely related to Hughes' hyperforests) which evolve during...