RAIRO-Theor. Inf. Appl.
Volume 47, Number 1, January-March 20136th Workshop on Fixed Points in Computer Science (FICS'09)
|Page(s)||25 - 68|
|Published online||10 January 2013|
Strong functors and interleaving fixpoints in game semantics∗
Computer Laboratory, University of Cambridge,
15 J. J. Thomson Avenue,
Accepted: 28 September 2012
We describe a sequent calculus μLJ 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 μ-closed category, relying on a uniform interpretation of open μLJ formulas as strong functors. We show that any μ-closed category is a sound model for μLJ. We then turn to the construction of a concrete μ-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 μLJ.
Mathematics Subject Classification: 18C50 / 03F05 / 68Q55 / 91A40
Key words: Game semantics / strong functors / initial algebras / terminal coalgebras / inductive types / coinductive types
© EDP Sciences 2013
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.