Voir la notice de l'article provenant de la source Numdam
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.
@article{ITA_2013__47_1_25_0,
author = {Clairambault, Pierre},
title = {Strong functors and interleaving fixpoints in game semantics},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
pages = {25--68},
publisher = {EDP-Sciences},
volume = {47},
number = {1},
year = {2013},
doi = {10.1051/ita/2012028},
mrnumber = {3072310},
zbl = {1302.03072},
language = {en},
url = {http://geodesic.mathdoc.fr/articles/10.1051/ita/2012028/}
}
TY - JOUR AU - Clairambault, Pierre TI - Strong functors and interleaving fixpoints in game semantics JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications PY - 2013 SP - 25 EP - 68 VL - 47 IS - 1 PB - EDP-Sciences UR - http://geodesic.mathdoc.fr/articles/10.1051/ita/2012028/ DO - 10.1051/ita/2012028 LA - en ID - ITA_2013__47_1_25_0 ER -
%0 Journal Article %A Clairambault, Pierre %T Strong functors and interleaving fixpoints in game semantics %J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications %D 2013 %P 25-68 %V 47 %N 1 %I EDP-Sciences %U http://geodesic.mathdoc.fr/articles/10.1051/ita/2012028/ %R 10.1051/ita/2012028 %G en %F ITA_2013__47_1_25_0
Clairambault, Pierre. Strong functors and interleaving fixpoints in game semantics. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 47 (2013) no. 1, pp. 25-68. doi: 10.1051/ita/2012028
Cité par Sources :