Game Semantics

Game semantics is an approach to the semantics of logic and programming languages that interprets proofs and programs as strategies in formal two-player games between an Opponent (who challenges) and a Proponent (who defends). Developed in the 1990s by Samson Abramsky, Radha Jagadeesan, Pasquale Malacaria, and others, building on earlier work by Andreas Blass and Girard's geometry of interaction, game semantics provides the first fully abstract models for a variety of programming languages — models in which two programs are semantically equal if and only if they are observationally indistinguishable.

The central move of game semantics is to replace the static, set-theoretic notion of meaning with the dynamic, interactive notion of play. A type becomes a game; a term becomes a strategy; composition becomes the interaction of strategies across shared moves. This makes game semantics particularly suited to languages with effects — state, control, nondeterminism, concurrency — where traditional denotational semantics struggles. The connection to linear logic is especially close: the games of game semantics are inherently resource-sensitive, and the strategies correspond precisely to linear proofs.

Game semantics has been extended to model concurrent and probabilistic computation, and it shares deep structural connections with dialogue games in philosophical logic and game theory in economics. The unifying insight is that computation, logic, and strategic interaction are not three distinct phenomena but three perspectives on a single underlying structure: the exchange of moves between agents with asymmetric information and complementary goals.