Focusing in Asynchronous Games

10 years 9 months ago
Focusing in Asynchronous Games
Game semantics provides an interactive point of view on proofs, which enables one to describe precisely their dynamical behavior during cut elimination, by considering formulas as games on which proofs induce strategies. We are specifically interested here in relating two such semantics of linear logic, of very different flavor, which both take in account concurrent features of the proofs: asynchronous games and concurrent games. Interestingly, we show that associating a concurrent strategy to an asynchronous strategy can be seen as a semantical counterpart of the focusing property of linear logic. A cut-free proof in sequent calculus, when read from bottom up, progressively introduces the connectives of the formula that it proves, in the order specified by the syntactic tree constituting the formula, following the conventions induced by the logical rules. In this sense, a formula can be considered as a playground that the proof will explore. The formula describes the rules that th...
Samuel Mimram
Added 19 Jul 2010
Updated 19 Jul 2010
Type Conference
Year 2010
Where CIE
Authors Samuel Mimram
Comments (0)