Desequentialization of games and experiments in proof-nets

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.