Symmetric dialogue games in the proof theory of linear logic

This thesis develops an original approach to the interactive interpretation of the proof theory of linear logic. In contrast with the player/opponent dichotomy commonly associated with game semantics for logic, we propose a model in which the two players have symmetric roles. More precisely, we shift from a situation in which a player aims at proving a goal while the other one aims at refuting it to a situation in which the players aim at proving opposite goals. In the tradition of computation-as-proof-search, each step of the interaction is seen as a step in two orthogonal sequent calculus proof searches. To some extent, this work contributes to formalising the connections between proof search and proof normalisation. We first present a simple symmetric game for the additive fragment of linear logic, as a first introduction to dual proof search. We then introduce a much more involved symmetric game accounting for the multiplicative and additive fragment of linear logic. In order to get a full completeness result, we then develop a third, highly concurrent, symmetric game. Finally, we investigate a few extensions of our model.