Thick Subtrees, Games and Experiments

photo CC-By-Nc-Sa par kirkh

, par Pierre

Conférence TLCA 09

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 [1].

The polarized game semantics is full and faithfull for polarized
proof-nets [2]. We detail the correspondence between cut
free proof-nets and innocent strategies, in a framework related to
abstract Böhm trees.

A notion of thick subtree allows us to reveal a deep relation between
plays in games and Girard’s experiments on proof-nets. We then define
a desequentializing operation, forgetting time in games which
coincides with the usual way of computing a result of interaction from
an experiment. We then obtain our main result : desequentializing the
game interpretation of a polarized proof-net yields its standard
relational model interpretation (static semantics).

Portfolio

spip_logo

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]