Thick Subtrees, Games and Experiments

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).