Best ETAPS Paper Award 2026

Best ETAPS Paper Award 2026 The EATCS award for the best theory paper at ETAPS 2026 is awarded to the following papers

Isa Vialard, Joël Ouaknine and Quentin Guilmant: "The value problem for weighted timed games with two clocks is undecidable”, FoSSaCS

The paper solves a long-standing open problem in the field of quantitative games. Weighted timed games were introduced in several works in the early 2000s, and constitute a fundamental model for formal verification and control. The key decision problems for quantitative games are the existence of winning strategies and the ‘value problem’: is the inf-sup across all pairs of Minimizer/Maximizer strategies smaller than a given rational? With three clocks, the value problem was proved undecidable in 2015. With a single clock, the problem was shown to be decidable in 2022. This paper finally closes the gap: with two clocks, both problems are shown to be undecidable using a novel and ingenious reduction, resulting in a deep contribution.

Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, Yue Yao: "Recursive Logical Relations for Intuitionistic Linear Logic Session Types”, ESOP

The paper solves an open challenge in the semantics of session-typed concurrency: how to construct a logical relation that supports general recursion, non-termination, and nondeterministic scheduling. Previous logical relations for session typed languages were confined to terminating languages, leaving a fundamental gap. The authors introduce the Recursive Session Logical Relation (RSLR), whose key innovation is an extensional observation index that measures external message exchanges, replacing traditional step-indexing. This elegant shift yields a well-founded yet compositional framework, naturally compatible with concurrency and parallel composition. The work establishes reflexivity, symmetry, transitivity, and, crucially, soundness and completeness with respect to weak asynchronous bisimilarity via a biorthogonality argument. Beyond its theoretical strength, RSLR enables a powerful semantic account of progress-sensitive noninterference. This constitutes a significant and lasting contribution to the semantics of concurrent programming languages.