Asynchronous games 4: a fully complete model of propositional linear logic

We construct a denotational model of propositional linear logic based on asynchronous games and winning uniform innocent strategies. Every formula A is interpreted as an asynchronous game [A] and every proof π of A is interpreted as a winning uniform innocent strategy [π] of the game [A]. We show that the resulting model is fully complete: every winning uniform innocent strategy σ of the asynchronous game [A] is the denotation [π] of a proof π of the formula A.