Games semantics for full propositional linear logic

We present a model of propositional classical linear logic (all the connective except for the additive constants) where the formulas are seen as two person games in which connectives are used as tokens, while the proofs are interpreted as strategies for one player. We discuss the intimate connection between these games and the structure of proofs, and prove a full completeness theorem. The main technical innovation is a “double negation” interpretation of CLL into intuitionistic linear logic