Focusing in Asynchronous Games

TL;DR

This paper explores the relationship between asynchronous and concurrent game semantics in linear logic, showing how associating strategies in these frameworks relates to the focusing property, thus linking proof dynamics with game semantics.

Contribution

It establishes a semantic connection between asynchronous and concurrent game models, highlighting how strategy association reflects the focusing property in linear logic.

Findings

Associating concurrent strategies to asynchronous strategies models focusing in linear logic.

Provides a semantic interpretation of focusing through game semantics.

Bridges two different game semantics frameworks for linear logic.

Abstract

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.