Abstract 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, weak bisimilarity of associated strategies entails contextual equivalence. OGS has been applied to a variety of languages, with rather tedious soundness proofs. In this paper, we contribute to the unification and mechanisation of OGS. Indeed, we propose an abstract notion of language with evaluator, for which we construct a generic OGS interpretation, which we prove sound. Our framework covers a variety of simply-typed and untyped lambda-calculi with various evaluation strategies. These calculi notably feature recursive definitions, first-class continuations, and a wide variety of datatypes. All constructions and proofs are entirely mechanised in the Coq proof assistant.

Abstract This artifact report is a companion to the ESOP’25 paper An abstract, certified account of operational game semantics [3]. The paper describes the construction of a sound model for an abstract notion of language. The model is built using a semantic technique named Operational Game Semantics (OGS). All our results are mechanised in the Coq proof assistant: this mechanisation (The proof artifact is archived at https://doi.org/10.5281/zenodo.14697618 .) constitutes the artifact we discuss in the present document. More specifically, our mechanisation covers our main result, the soundness of the abstract OGS model w.r.t. substitution equivalence (Theorem 8), as well as four example calculi: two variants of call-by-value $$\lambda $$ λ -calculus and two variants of $$\mu \tilde{\mu }$$ μ μ ~ -calculus [4, 5]. The only axiom used is the Axiom K [17] for equality proof irrelevance (To ease dependent pattern matching due to the intrinsically scoped representation.). The explains the installation process and the structure of the code. An online rendering ( https://lapin0t.github.io/ogs/esop25/Readme.html .) is available thanks to Alectryon [12]. Furthermore, the main paper provides systematic hyperlinks from statements to their Coq counterparts. We encourage the interested reader to use these tools to navigate the code. In this document, we focus first on users: how to read and instantiate our main result. We then detail salient technical aspects of our mechanisation.

By abstracting over well-known properties of De Bruijn's representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi's approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms.

Abstract By abstracting over well-known properties of De Bruijn’s representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi’s approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms.

This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition monads, thus covering new applications such as lambda-bar-mu-calculus, pi-calculus, Positive GSOS specifications, differential lambda-calculus, and the big-step, simply-typed, call-by-value lambda-calculus. Moreover, we design a suitable notion of signature for transition monads.

Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky (1990). Howe (1996) gave a direct proof that it is a congruence, and generalised the result to all languages complying with a suitable format. We propose a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. Example instances include standard applicative bisimilarity in call-by-name, call-by-value, and call-by-name non-deterministic $\lambda$-calculus, and more generally all languages complying with a variant of Howe's format.

This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition monads, thus covering new applications such as ̅λμ-calculus, π-calculus, Positive GSOS specifications, differential λ-calculus, and the big-step, simply-typed, call-by-value λ-calculus. Finally, we design a suitable notion of signature for transition monads.

We introduce a categorical framework for operational semantics, in which we define substitution-closed bisimilarity, an abstract analogue of the open extension of Abramsky's applicative bisimilarity. We furthermore prove a congruence theorem for substitution-closed bisimilarity, following Howe's method. We finally demonstrate that the framework covers the call-by-name and call-by-value variants of λ-calculus in big-step style. As an intermediate result, we generalise the standard framework of Fiore et al. for syntax with variable binding to the skew-monoidal case.

We propose a categorical framework for structural operational semantics, in which we prove that under suitable hypotheses bisimilarity is a congruence. We then refine the framework to prove soundness of bisimulation up to context, an efficient method for reducing the size of bisimulation relations. Finally, we demonstrate the flexibility of our approach by reproving known results in three variants of the π-calculus.

Game semantics is a rich and successful class of denotational models for programming languages. Most game models feature a rather intuitive setup, yet surprisingly difficult proofs of such basic results as associativity of composition of strategies. We seek to unify these models into a basic abstract framework for game semantics, game settings. Our main contribution is the generic construction, for any game setting, of a category of games and strategies. Furthermore, we extend the framework to deal with innocence, and prove that innocent strategies form a subcategory. We finally show that our constructions cover many concrete cases, mainly among the early models [5, 23] and the recent, sheaf-based ones [40].

In this article, we give precise mathematical form to the idea of a structure whose data and axioms are faithfully represented by a graphical calculus; some prominent examples are operads, polycategories, properads, and PROPs. Building on the established presentation of such structures as algebras for monads on presheaf categories, we describe a characteristic property of the associated monads—the shapeliness of the title—which says that ‘any two operations of the same shape agree’. An important part of this work is the study of analytic functors between presheaf categories, which are a common generalization of Joyal’s analytic endofunctors on sets and of the parametric right adjoint functors on presheaf categories introduced by Diers and studied by Carboni–Johnstone, Leinster and Weber. Our shapely monads will be found among the analytic endofunctors, and may be characterized as the submonads of a universal analytic monad with ‘exactly one operation of each shape’. In fact, shapeliness also gives a way to define the data and axioms of a structure directly from its graphical calculus, by generating a free shapely monad on the basic operations of the calculus. In this article, we do this for some of the examples listed above; in future work, we intend to use this to obtain canonical notions of denotational model for graphical calculi such as Milner’s bigraphs, Lafont’s interaction nets or Girard’s multiplicative proof nets.

Recent developments of game semantics have given rise to new models of concurrent languages. On the one hand, an approach based on string diagrams has given models of CCS and the pi-calculus, and on the other hand, Tsukada and Ong have designed a games model for a non-deterministic lambda-calculus. There is an obvious, shallow relationship between the two approaches, as they both define innocent strategies as sheaves for a Grothendieck topology embedding "views" into "plays". However, the notions of views and plays differ greatly between the approaches: Tsukada and Ong use notions from standard game semantics, while the authors of this paper use string diagrams. We here aim to bridge this gap by showing that even though the notions of plays, views, and innocent strategies differ, it is mostly a matter of presentation.

Following previous work on CCS, we propose a compositional model for the $\pi$-calculus in which processes are interpreted as sheaves on certain simple sites. Such sheaves are a concurrent form of innocent strategies, in the sense of Hyland-Ong/Nickau game semantics. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any innocent strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, relying on a combinatorial presentation of $\pi$-calculus traces in the spirit of string diagrams.

Following previous work on CCS, we propose a compositional model for the pi-calculus in which processes are interpreted as sheaves on certain simple sites. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, whose heart is a combinatorial presentation of pi-calculus traces in the spirit of string diagrams. As in previous work, the sheaf condition is analogous to innocence in Hyland-Ong/Nickau games.

The ML module system provides powerful parameterization facilities, but lacks the ability to split mutually recursive definitions across modules and provides insufficient support for incremental programming. A promising approach to solve these issues is Ancona and Zucca's mixin module calculus CMS . However, the straightforward way to adapt it to ML fails, because it allows arbitrary recursive definitions to appear at any time, which ML does not otherwise support. In this article, we enrich CMS with a refined type system that controls recursive definitions through the use of dependency graphs. We then develop and prove sound a separate compilation scheme, directed by dependency graphs, that translates mixin modules down to a call-by-value λ-calculus extended with a nonstandard let rec construct.

This paper formalizes and proves correct a compilation scheme for mutually-recursive definitions in call-by-value functional languages. This scheme supports a wider range of recursive definitions than standard call-by-value recursive definitions. We formalize our technique as a translation scheme to a lambda-calculus featuring in-place update of memory blocks, and prove the translation to be faithful.