We describe a sequent calculus μLJ with primitives for inductive andcoinductive datatypes and equip it with reduction rules allowing a sound translation ofGödel’s system T. We introduce the notion of a μ-closedcategory, relying on a uniform interpretation of open μLJformulas as strong functors. We show that any μ-closed category is asound model for μLJ. We then turn to the construction of a concreteμ-closed category based on Hyland-Ong game semantics. The model relieson three main ingredients: the construction of a general class of strong functors calledopen functors acting on the category of games and strategies, thesolution of recursive arena equations by exploiting cycles in arenas, andthe adaptation of the winning conditions of parity games to build initial algebras andterminal coalgebras for many open functors. We also prove a weak completeness result forthis model, yielding a normalisation proof for μLJ.
