Strong functors and interleaving fixpoints in game semantics
Pierre Clairambault (2013)
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
Similarity:
We describe a sequent calculus with primitives for inductive and coinductive datatypes and equip it with reduction rules allowing a sound translation of Gödel’s system T. We introduce the notion of a , relying on a uniform interpretation of open formulas as strong functors. We show that any -closed category is a sound model for . We then turn to the construction of a concrete -closed category based on Hyland-Ong game semantics. The model relies on three main ingredients:...