Operational game semantics (OGS) is a method for interpreting programs as strategies in suitable games, or more precisely as labelled transition systems over suitable games, in the sense of Levy and Staton. Such an interpretation is called sound when, for any two given programs, bisimilarity of associated strategies entails contextual equivalence. OGS has been applied to a variety of languages, with rather tedious soundness proofs. Concretely they transform a reduction relation into a full blown model interpreting open terms as a strategy for interacting with all possible execution environments. We have developed a Coq formalization of this construction, abstracting away some syntactic details of the considered language and keeping the computational content intact.

I will start this talk by motivating and presenting OGS intuitively, and will then give an overview of our contributions. Finally I will detail a technical point of the soundness proof, namely well-definedness of the composition of Proponent- and Opponent-strategies. Indeed this crucial point involves a variant of the so-called infinite chattering problem, which we solve by looking into uniqueness properties of fixpoint equations in iterative monads.