GALOP 2025
16th Workshop on Games for Logic and Programming Languages

About the Workshop

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:

• Games and other interaction-based denotational models
• Game-based program analysis and verification
• Logics for games and games for logics
• Algorithmic aspects of game semantics
• Categorical aspects of game semantics
• Geometry of interaction and ludics
• Taylor expansion of programs and intersection type systems
• Relational models and their categorifications
• String diagrams and compositionality
• Open and normal form bisimulation
• Trace semantics
• Connections between games and other forms of denotational models
• Compositional certification of programs and interactive program behaviour

The first GALOP was held in 2005. Some information about previous editions can be found on the following pages: 2024, 2011-2020.

Workshop Programme

Saturday 19 July

09:00–10:00 — Invited talk: Paul Blain Levy (details TBA)

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

Sunday 20 July

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 (Extended Abstract), 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.)

Submission information

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.

• Submission Deadline: 7 May 2025 21 May 2025, AoE.
• Notification: 21 May 2025, 4 June 2025.
• Workshop: 19-20 July 2025.

This is an informal workshop that welcomes submissions of work in progress, overviews of larger projects, programmatic or position papers, and propositions of tutorials.

Invited Speakers

• Adrienne Lancelot, INRIA, École Polytechnique and Université Paris Cité, IRIF
• Paul Blain Levy, University of Birmingham

Program Committee

• Matteo Acclavio, University of Sussex, UK
• Peio Borthelle, Université Savoie Mont Blanc, France
• Benedict Bunting, University of Oxford, UK
• Claudia Faggian, CNRS and IRIF, France
• Naohiko Hoshino, Sojo University, Japan
• Jérémie Koenig, Yale University, USA
• James Laird, University of Bath, UK (co-chair)
• Koko Muroya, National Institute of Informatics, Japan
• Hugo Paquet, Inria and ENS, France (co-chair)
• Thomas Seiller, CNRS and LIPN, France
• Glynn Winskel, Queen Mary University of London, UK