Desequentialization of games and experiments in proof-nets

Pré-publication IML 2005

We relate the dynamic semantics (games, dealing with interactions) and
the static semantics (dealing with results of interactions) of linear
logic with polarities, in the spirit of Timeless
Games [BDER97].

We carefully analyze Laurent’s polarized proof-nets (which for the
game semantics is full and faithful ([Lau03]) and we detail
the precise correspondence between cut free proof-nets and innocent
strategies, in a framework related to Bˆhm trees. We then introduce a
notion of thick subtree that is used to define a desequentializing
operation, forgetting time in games. This allows use to show a deep
relation between plays in games and Girard’s experiments on
proof-nets. We then obtain our main result : desequentializing the game
interpretation of a polarized proof-net yields its generic static
interpretation.

Documents joints

Revenu et logement, Je livre ici quelques éléments de comparaison concernant mon niveau de vie, pour couper court à quelques idées reçues, et un condensé de nombreuses (...)
Revenu et travail d’un enseignant-chercheur, Cet article complète l'article Revenu et logement, en détaillant un peu le budget de mon ménage, mon parcours d'enseignant-chercheur en terme de (...)
Cybersyn (el systemo synco), Au café, mardi 5 avril 2011, j'ai bien vu que, mis à part Antoine Allombert, personne ne connaissait l'histoire de l'extraordinaire projet chilien (...) [jpg, jpg, png]