GALOP 2025
16th Workshop on Games
for Logic and Programming Languages
19-20 July, Birmingham, UK
GALOP is an international workshop on formal models for program interaction. It has a broad interest, in both the foundational aspects of these models as well as their practical applications.
The central focus of GALOP is game semantics, a set of techniques used to represent the interaction of a program and its environment as a formal game. This is a powerful framework for reasoning about programs and interactive systems, and game semantics is relevant to many aspects of programming language theory. Game semantics also has deep connections to logic and other fields of mathematics.
Scope. GALOP aims to gather researchers with a range of expertise who share an interest in reasoning about the interactive behaviour of programs using formal mathematical methods, in any context including proof theory, denotational semantics, or program verification. Specific areas of interest include, but are not limited to:
The first GALOP was held in 2005. Some information about previous editions can be found on the following pages: 2024, 2011-2020.
Interaction Equivalence
Contextual equivalence is the de facto standard notion of program equivalence. A key theorem is that contextual equivalence is an equational theory. Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does not induce an equational theory, for an apparently essential reason: cost is not invariant under reduction. In the paradigmatic case of the untyped λ-calculus, we introduce interaction equivalence. Inspired by game semantics, we observe the number of interaction steps between terms and contexts but—crucially—ignore their internal steps. We prove that interaction equivalence is an equational theory and characterize it as ℬ, the well-known theory induced by Böhm tree equality. It is the first observational characterization of ℬ obtained without enriching the discriminating power of contexts with extra features such as non-determinism. To prove our results, we develop interaction-based refinements of the Böhm-out technique and of intersection types. Joint work with Beniamino Accattoli, Giulio Manzonetto and Gabriele Vanoni.
Probabilistic trace strategies: definability and the tensor completeness problem
(joint work with Nathan Bowler and Sergey Goncharov)
Programs that combine I/O and countable probabilistic choice, modulo either bisimilarity or trace equivalence, can be seen as describing a probabilistic strategy. In the case of well-founded programs, we might expect to axiomatize bisimilarity via a sum of equational theories and trace equivalence via a tensor of such theories. This is by analogy with similar results for nondeterminism, established previously. While bisimilarity is indeed axiomatized via a sum of theories, and the tensor is indeed at least sound for trace equivalence, completeness in general, remains an open problem. Nevertheless, we show completeness in the case that either the probabilistic choice or the I/O operations used are finitary. We also show completeness up to impersonation, i.e.\ that the tensor theory regards trace equivalent programs as solving the same system of equations. This entails completeness up to the cancellation law of the probabilistic choice operator. Furthermore, we show that a probabilistic trace strategy %(function on traces) arises as the semantics of a well-founded program iff it is victorious. This means that, when the strategy is played against any partial counterstrategy, the probability of play continuing forever is zero. We link our results (and open problem) to particular monads that can be used to model computational effects. We also link them to initial algebras and final coalgebras for suitable endofunctors.
09:00–10:00 — Invited talk: Probabilistic trace strategies: definability and the tensor completeness problem, Paul Blain Levy
10:30–11:00 — Honest Linearizability, Arthur Oliveira Vale
11:00–11:30 — Monadic Second Order Logic for Higher Dimensional Automata, Amazigh Amrane
(Lunch from 12:30.)
14:00–14:30 — Getting Thin Spans in Order, Victor Blanchi, Pierre Clairambault, Raphaëlle Crubillé, and Simon Forest
14:30–15:00 — Relational Semantics: From Simple to Non-Idempotent Intersection Types and Back, Victor Arrial, Giulio Guerrieri, and Vincent Sommella
15:00–15:30 — Linear Realisability and Cobordism: Understanding the Trefoil Property, Valentin Maestracci and Thomas Seiller
09:00–10:00 — Invited talk: Interaction Equivalence, Adrienne Lancelot
10:30–11:00 — Reachability Types, Traces and Full Abstraction, Benedict Bunting and Andrzej Murawski
11:00–11:30 — Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence, Vasileios Koutavas, Yu-Yang Lin, and Nikos Tzevelekos
11:30–12:00 — A Trace Model of an Imperative Multi-Stage Language, Haoxuan Yin, Andrzej Murawski, and Luke Ong
(Lunch from 12:30.)
Authors are asked to submit an abstract (up to 2 pages) describing a talk which they would give at the workshop, at the following address:
Supplementary material may be submitted, and will be considered at the discretion of the PC.