STRONG FUNCTORS AND INTERLEAVING FIXPOINTS IN GAME SEMANTICS

We describe a sequent calculus mu LJ with primitives for inductive and coinductive datatypes and equip it with reduction rules allowing a sound translation of Godel's system T. We introduce the notion of a mu-closed category, relying on a uniform interpretation of open mu LJ formulas as strong functors. We show that any mu-closed category is a sound model for mu LJ. We then turn to the construction of a concrete mu-closed category based on Hyland-Ong game semantics. The model relies on three main ingredients: the construction of a general class of strong functors called open functors acting on the category of games and strategies, the solution of recursive arena equations by exploiting cycles in arenas, and the adaptation of the winning conditions of parity games to build initial algebras and terminal coalgebras for many open functors. We also prove a weak completeness result for this model, yielding a normalisation proof for mu LJ.