GaLoP 2026
17th Workshop on Games for Logic and Programming Languages

MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Contextual MetaML, the first metaprogramming language that supports storing and running open code under a strong type safety guarantee. The type system utilises contextual modal types to track and reason about free variables in code explicitly.

A crucial concern in metaprogramming-based program optimisations is whether the optimised program preserves the meaning of the original program. Addressing this question requires a notion of program equivalence and techniques to reason about it. In this paper, we provide a semantic model that captures contextual equivalence for Contextual MetaML, establishing the first full abstraction result for an imperative MetaML-style language. Our model is based on traces derived via operational game semantics, where the meaning of a program is modelled by its possible interactions with the environment. We also establish a novel closed instances of use theorem that accounts for both call-by-value and call-by-name closing substitutions.

In the continuation of works that link operational semantics (OGS) with process calculi, we build on top of a type system that enforces visibility in a sequential pi-calculus to also enforce blindness and obtain a full-abstraction result for a sequential pi-calculus with ground references.

Blindness is a game semantics notion modeling ground references in languages with exchanges of references; it was introduced by Murawski and Tzevelekos in order to prove full-abstraction for Reduced ML.

The presence of shared (or aliased) mutable state has long been recognised as the root cause of many difficulties in programming, particularly complicating understanding and reasoning about the behaviour of programs. Approaches to controlling aliasing are a rich area of study and have become increasingly adopted in mainstream programming languages, for example Rust and Linear Haskell. The policy many of these languages adopt (aliasing XOR mutability and linearity, in the examples, respectively) are incompatible with common, impure, higher-order patterns based on sharing of mutable state.

Reachability Types are a recent approach to provide control over sharing in a higher-order functional programming language, by tracking in the type system information about what resources are reachable from a term, which allows separation requirements to be enforced using types.

In this talk, I will discuss how to apply operational game semantics (OGS) to investigate the meaning of Reachability Types and the impact these have on the language. This work is detailed in my forthcoming DPhil thesis. An earlier version on this work was presented at GaLoP 2025, based upon the LICS 2025 paper Reachability Types, Traces and Full Abstraction. This talked is intended to be a update on this project, with an improved pedagogical presentation, which I hope will be of interest to the GaLoP audience.

Thins spans were recently introduced as a quantitative and proof-relevant model of programming languages based on spans of groupoids. Designed as a categorical abstraction of the model of concurrent games, they can also be seen as an extension of the relational model Rel where, in the interpretation of a program, not only some inputs are related to some outputs, but the different ways or computations a program can make to transform the given inputs to the given outputs are recorded. Interestingly, they also provide a model for a non-idempotent and non-commutative, a.k.a. rigid, intersection type system. While such a system was historically deemed partially irrelevant because it does not satisfy subject reduction, this latter property is recovered in thin spans "up to symmetry". Moreover, this intersection type system is "faithfully" represented by thin spans: each point in the interpretation of programs correspond to exactly one intersection type derivation.

In this talk, we give a presentation of the model of thin spans and of the associated rigid intersection type system.

This is joint work with Pierre Clairambault.

About ten years ago, we explained in a widely circulated manuscript how to extend tensorial logic with algebraic effects. Our main illustration was the algebraic theory of mnemoids introduced by Plotkin and Power in order to equip an object of a cartesian category with update and lookup operations on a global store. In this talk, we will give an explicit proof-theoretic and game-theoretic description of the free dialogue category D with finite sums, whose tensorial pole bot is moreover equipped with the algebraic structure (operations and equations) of a mnemoid. This work provides a first and elementary step towards the design of a functorial game semantics integrating local stores and visible strategies.

This presentation provides an overview of the ongoing work of the author's PhD project supervised by Pierre Clairambault, Giulio Manzonetto and Alexis Saurin. The presentation focuses on the connections between a polarized proof system and game semantics. In particular, we introduce a hypersequentialized proof system we designed which may be used to provide a syntactic presentation of strategies as in game semantics for MALL (multiplicative addidtive linear logic with least and greatest fixed points).

We provide the first formal connection between Gödel’s Dialectica interpretation and Berry-Curien’s sequential algorithms model, via a parameterized version of Gödel’s Dialectica interpretation which allows us to recast both the Diller-Nahm variant of the interpretation and Berry-Curien’s sequential algorithms model. This illustrates that the Dialectica interpretation has a strong intensional flavour, as the reverse component of the Dialectica interpretation of a function (from environments in the output to environments in the input) corresponds precisely to the computation indices of sequential algorithms (which specify what is needed in the input in order to produce a given output).

While a straightforward instanciation gives the usual Diller-Nahm variant of the Dialectica inerpretation, a more involved instanciation provides exactly the sequential algorithms model. We believe that this is a first step towards a convergence between Dialectica-style computational interpretations of logic on one hand, and game semantics flavoured denotational models of various programming languages on the other hand.

In this proposed talk, we will present work in progress towards a “primitive” categorical structure for concurrent game semantics: a categorical structure that is simple and lets us derive categorically familiar models of various languages and evaluation strategies.

Bidirectional information flow is a central concept in both categorical game semantics and practical functional programming. In game semantics, the Joyal-Street-Verity's Int construction provides a canonical way to build compact closed categories from traced monoidal categories, elegantly modeling bidirectional interaction and feedback loops. Conversely, in functional programming, the Lens construction offers a robust, compositional framework for bidirectional state access and update.

This work-in-progress explores the structural relationship between these two paradigms. We propose an adjunction between the categories arising from the Lens and Int constructions. By formally connecting the state-based approach of the Lens construction with the traced monoidal approach of the Int construction, we aim to bridge abstract game-semantic models with compositional theories of bidirectional flow.

In this talk, we will outline the core functorial mappings between these categories, present the ongoing proofs of the adjunction, and discuss its potential applications to the foundations of game semantics.

For a first-order language with full ground references and iteration, we give an explicit denotational semantics.

A type denotes a “platform set”, which is a family of “platforms” that indicate the references included. A state is represented as a tree, showing the result of following chains of references, whose nodes are partitioned into finitely many equivalence classes, showing the aliasing. The model is equivalent to known models that use ends or coends, or strong nominal sets, but is simpler in the sense that a morphism is simply a function.

Program equivalence lies at the heart of programming language semantics: when are two programs indistinguishable in every possible context? For higher-order functional languages, the absence of effects makes the problem harder rather than easier: without external mechanisms for recording interaction, equivalence must be understood through the disciplined structure of pure higher-order computation itself. In this talk, I will present the first fully abstract normal form bisimulation for call-by-value PCF, a canonical language combining higher-order computation, recursion, and observable termination. The construction brings together ideas from applicative bisimulation, environmental bisimulation, and game semantics, replacing direct quantification over all program contexts with a labelled transition system that records structured traces of possible interactions with functional environments.

The resulting bisimulation is sound and complete for contextual equivalence, without relying on semantic quotienting. It also gives rise to an implementable method for checking program equivalence: I will describe a prototype bounded bisimulation checker and illustrate its behaviour on examples from the literature as well as new equivalences and inequivalences. This is joint work with Vasileios Koutavas and Yu-Yang Lin.

Operational game semantics are presented through labelled transition systems, of which the induced bisimilarity on programs is shown to be included in CIU equivalence, a variant of contextual equivalence. Soundness of operational game semantics follows from external context lemmas which state that CIU and contextual equivalences coincide.

This talk will show how one may avoid the use of CIU equivalence entirely, by changing the initial operational configurations of terms in the operational game semantics. The construction is inspired by a proof technique for the genericity lemma due to Takahashi.

We study contextual interactions in an ML-like language equipped with general references and continuations through the lens of operational game semantics, focusing on the reachability and approximation problems.

Previous work showed that these problems are decidable in the loop-free setting via automata over nested data, where bounded P-views admit a finite representation. With the addition of loops, however, P-views become unbounded, and these techniques no longer apply.

We introduce a new class of automata over infinite alphabets that supports unbounded nesting of data, together with new restrictions of the P-view: the shallow P-view and enriched shallow P-view. These provide a finite representation of the relevant visible fragment of unbounded traces. We establish a precise correspondence between these automata and higher-order programs with loops: the trace semantics of any such program can be captured by an automaton, and conversely, the trace language of any such automaton can be realised by an imperative higher-order program with loops.

This correspondence enables the transfer of decidability and undecidability results between the automata and programs. In particular, we show that adding loops preserves decidability of reachability, while rendering approximation undecidable.

We discuss how to solve whole hierarchies of behavioral equivalence problems as single quantitative problems about modal logics through energy games. My work on generalized equivalence checking of concurrent programs proposes the first unified way to check for whole ranges of equivalences. Its prototype implementation https://equiv.io can compute which notions from van Glabbeek's strong and weak linear-time–branching-time spectrum relate pairs of finite-state processes.

MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Contextual MetaML, the first metaprogramming language that supports storing and running open code under a strong type safety guarantee. The type system utilises contextual modal types to track and reason about free variables in code explicitly.

A crucial concern in metaprogramming-based program optimisations is whether the optimised program preserves the meaning of the original program. Addressing this question requires a notion of program equivalence and techniques to reason about it. In this paper, we provide a semantic model that captures contextual equivalence for Contextual MetaML, establishing the first full abstraction result for an imperative MetaML-style language. Our model is based on traces derived via operational game semantics, where the meaning of a program is modelled by its possible interactions with the environment. We also establish a novel closed instances of use theorem that accounts for both call-by-value and call-by-name closing substitutions.

Abstract.

We provide the first formal connection between Gödel’s Dialectica interpretation and Berry-Curien’s sequential algorithms model, via a parameterized version of Gödel’s Dialectica interpretation which allows us to recast both the Diller-Nahm variant of the interpretation and Berry-Curien’s sequential algorithms model. This illustrates that the Dialectica interpretation has a strong intensional flavour, as the reverse component of the Dialectica interpretation of a function (from environments in the output to environments in the input) corresponds precisely to the computation indices of sequential algorithms (which specify what is needed in the input in order to produce a given output).

While a straightforward instanciation gives the usual Diller-Nahm variant of the Dialectica inerpretation, a more involved instanciation provides exactly the sequential algorithms model. We believe that this is a first step towards a convergence between Dialectica-style computational interpretations of logic on one hand, and game semantics flavoured denotational models of various programming languages on the other hand.

Abstract.

The presence of shared (or aliased) mutable state has long been recognised as the root cause of many difficulties in programming, particularly complicating understanding and reasoning about the behaviour of programs. Approaches to controlling aliasing are a rich area of study and have become increasingly adopted in mainstream programming languages, for example Rust and Linear Haskell. The policy many of these languages adopt (aliasing XOR mutability and linearity, in the examples, respectively) are incompatible with common, impure, higher-order patterns based on sharing of mutable state.

Reachability Types are a recent approach to provide control over sharing in a higher-order functional programming language, by tracking in the type system information about what resources are reachable from a term, which allows separation requirements to be enforced using types.

In this talk, I will discuss how to apply operational game semantics (OGS) to investigate the meaning of Reachability Types and the impact these have on the language. This work is detailed in my forthcoming DPhil thesis. An earlier version on this work was presented at GaLoP 2025, based upon the LICS 2025 paper Reachability Types, Traces and Full Abstraction. This talked is intended to be a update on this project, with an improved pedagogical presentation, which I hope will be of interest to the GaLoP audience.

Abstract.

In the continuation of works that link operational semantics (OGS) with process calculi, we build on top of a type system that enforces visibility in a sequential pi-calculus to also enforce blindness and obtain a full-abstraction result for a sequential pi-calculus with ground references.

Blindness is a game semantics notion modeling ground references in languages with exchanges of references; it was introduced by Murawski and Tzevelekos in order to prove full-abstraction for Reduced ML.

Abstract.

We study contextual interactions in an ML-like language equipped with general references and continuations through the lens of operational game semantics, focusing on the reachability and approximation problems.

Previous work showed that these problems are decidable in the loop-free setting via automata over nested data, where bounded P-views admit a finite representation. With the addition of loops, however, P-views become unbounded, and these techniques no longer apply.

We introduce a new class of automata over infinite alphabets that supports unbounded nesting of data, together with new restrictions of the P-view: the shallow P-view and enriched shallow P-view. These provide a finite representation of the relevant visible fragment of unbounded traces. We establish a precise correspondence between these automata and higher-order programs with loops: the trace semantics of any such program can be captured by an automaton, and conversely, the trace language of any such automaton can be realised by an imperative higher-order program with loops.

This correspondence enables the transfer of decidability and undecidability results between the automata and programs. In particular, we show that adding loops preserves decidability of reachability, while rendering approximation undecidable.

Abstract.

About ten years ago, we explained in a widely circulated manuscript how to extend tensorial logic with algebraic effects. Our main illustration was the algebraic theory of mnemoids introduced by Plotkin and Power in order to equip an object of a cartesian category with update and lookup operations on a global store. In this talk, we will give an explicit proof-theoretic and game-theoretic description of the free dialogue category D with finite sums, whose tensorial pole bot is moreover equipped with the algebraic structure (operations and equations) of a mnemoid. This work provides a first and elementary step towards the design of a functorial game semantics integrating local stores and visible strategies.

Abstract.

This presentation provides an overview of the ongoing work of the author's PhD project supervised by Pierre Clairambault, Giulio Manzonetto and Alexis Saurin. The presentation focuses on the connections between a polarized proof system and game semantics. In particular, we introduce a hypersequentialized proof system we designed which may be used to provide a syntactic presentation of strategies as in game semantics for MALL (multiplicative addidtive linear logic with least and greatest fixed points).

Abstract.

In this proposed talk, we will present work in progress towards a “primitive” categorical structure for concurrent game semantics: a categorical structure that is simple and lets us derive categorically familiar models of various languages and evaluation strategies.

Abstract.

We discuss how to solve whole hierarchies of behavioral equivalence problems as single quantitative problems about modal logics through energy games. My work on generalized equivalence checking of concurrent programs proposes the first unified way to check for whole ranges of equivalences. Its prototype implementation https://equiv.io can compute which notions from van Glabbeek's strong and weak linear-time–branching-time spectrum relate pairs of finite-state processes.

Abstract.

Bidirectional information flow is a central concept in both categorical game semantics and practical functional programming. In game semantics, the Joyal-Street-Verity's Int construction provides a canonical way to build compact closed categories from traced monoidal categories, elegantly modeling bidirectional interaction and feedback loops. Conversely, in functional programming, the Lens construction offers a robust, compositional framework for bidirectional state access and update.

This work-in-progress explores the structural relationship between these two paradigms. We propose an adjunction between the categories arising from the Lens and Int constructions. By formally connecting the state-based approach of the Lens construction with the traced monoidal approach of the Int construction, we aim to bridge abstract game-semantic models with compositional theories of bidirectional flow.

In this talk, we will outline the core functorial mappings between these categories, present the ongoing proofs of the adjunction, and discuss its potential applications to the foundations of game semantics.

Abstract.

Operational game semantics are presented through labelled transition systems, of which the induced bisimilarity on programs is shown to be included in CIU equivalence, a variant of contextual equivalence. Soundness of operational game semantics follows from external context lemmas which state that CIU and contextual equivalences coincide.

This talk will show how one may avoid the use of CIU equivalence entirely, by changing the initial operational configurations of terms in the operational game semantics. The construction is inspired by a proof technique for the genericity lemma due to Takahashi.

Abstract.

For a first-order language with full ground references and iteration, we give an explicit denotational semantics.

A type denotes a “platform set”, which is a family of “platforms” that indicate the references included. A state is represented as a tree, showing the result of following chains of references, whose nodes are partitioned into finitely many equivalence classes, showing the aliasing. The model is equivalent to known models that use ends or coends, or strong nominal sets, but is simpler in the sense that a morphism is simply a function.

Abstract.