GALOP 2024
as the organisers put it
About GALOP is an international workshop on formal models for compositional program interaction and their applications. The first GALOP was held in 2005 and there have been 14 occurrences since. This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials. At the heart of GALOP is game semantics, a theory rooted in denotational semantics that models the interaction between a program and an arbitrary context as a formal game. As the mathematics of interaction between agents, games are a powerful mathematical lan ...
who it's for
programming language researchers, programming language implementers, formal methods researchers, compiler engineers, verification engineers, systems software engineers, theorem prover developers, concurrency engineers
topics
operational game semantics; normal-form bisimulation; call-by-value PCF; call-by-push-value trace models; Interaction Abstract Machine analysis; non-idempotent intersection types; denotational RA concurrency; SSA as Freyd categories; Taylor expansion and pointer games; invisible pebble tree transducers; game-enriched categorical models; compositional certified system software
| title | author | length |
|---|---|---|
| On Interaction, Efficiency, and Reversibility | Ugo Dal Lago | 45m |
Claim: the Interaction Abstract Machine (IAM) fails the usual invariance thesis — it is not invariant for time or space under natural encodings of Turing… | ||
| Normal Form Bisimulations by Value | Beniamino Accattoli, Adrienne Lancelot, Claudia Faggian | 22m |
Defines a new call-by-value normal-form bisimilarity, net bisimilarity, built on the value substituent calculus of aatan Pini; proves net is included… | ||
| Fully Abstract Normal Form Bisimulation for Call-by-Value PCF | Nikos Tzevelekos, Vasileios Koutavas, Yu-Yang Lin | 23m |
Presents the first fully abstract normal form bisimulation for call-by-value PCF, built from an LTS that mixes applicative, environmental and game-semantic… | ||
| Operational game semantics for generative algebraic effects and handlers | Hamza Jaâfar, Guilhem Jaber | 24m |
Describes a typed call-by-value λ-calculus with first-class effect instances and dynamic generation plus a public/private disclosure discipline; builds an… | ||
| An abstract, certified account of Operational Game Semantics | Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski | 21m |
An abstract, certified account builds operational game semantics formalized in Coq and gives a generic soundness theorem for OGS that covers polarized and… | ||
| Operational Algorithmic Game Semantics | Benedict Bunting, Andrzej S. Murawski | 21m |
Builds a fully abstract trace model for a call-by-push-value calculus with first-order state as a labelled transition system, then refines it (via name schemes… | ||
| Compositional Development of Certified System Software | Zhong Shao | 49m |
Claims a new semantics that makes horizontal and vertical composition of linearizable concurrent objects workable, replacing ad hoc inlining with a categorical… | ||
| SSA is Freyd Categories | Jad Elkhaleq Ghalayini | 18m |
Claim: SSA without control-flow equals Freyd categories; SSA with DAG control-flow equals distributive Freyd categories; general control-flow is a distributive… | ||
| A Denotational Approach to Release/Acquire Concurrency | Yotam Dvir, Ohad Kammar, Ori Lahav | 23m |
Presents a directionally adequate denotational semantics for Release/Acquire memory using Brookes-style trace semantics adapted to a view-based machine; traces… | ||
| Invisible pebbles and the geometry of affine higher-order tree transducers | Lê Thành Dũng Nguyễn, Gabriele Vanoni | 23m |
This work shows that affine λ-transducers with (almost) purely affine memory translate to tree-walking transducers, proving an inexpressivity conjecture of… | ||
| Taylor Expansion is Game Semantics | Lison Blondeau-Patissier, Pierre Clairambault, Lionel Vaux Auclair | 18m |
This work shows that the Taylor expansion of a simply-typed λ-term is isomorphic to its interpretation in pointer concurrent games, extending Tsukada and Ong’s… | ||
| Game-enriched categories | Paul Blain Levy | 26m |
Argues that game models should be presented as game-enriched categories (objects = arenas, homs = games whose strategies are morphisms) so different strategy… | ||
| Fair omega-Regular Games | Daniel Hausmann, Nir Piterman, Irmak Saglam, Anne-Kathrin Schmuck | 24m |
Defines games where both players must use designated fair moves and gives a formal winning rule: if one player is fair and the other not the fair player wins… | ||
| MELL proof-nets without boxes: thirty years later | Abhishek De, Kostia Chardonnet | 18m |
Claim: exponentials are encoded as fixed-point operators in a non-wellfounded sequent calculus whose coinductive proofs desequentialise into an infinite… | ||
| nothing matches | ||