ABSTRACT. 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, \textit{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 \textit{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. 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. 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. 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. We provide the first formal connection between G¨odel’s Dialectica interpretation and Berry-Curien’s sequential algorithms model, via a parameterized version of G¨odel’s Dialectica inter- pretation 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 pre- cisely 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.