2026-11-27

Confluence is a fundamental property of nondeterministic computations, arising from parallelism, concurrency, or freedom in the evaluation order. It guarantees that such a computation always yields the same result, regardless of the order in which steps are taken. The decreasing diagrams technique of van Oostrom is one of the most versatile methods for establishing confluence of transition systems (abstract rewriting systems). It reduces global confluence to local confluence: a system is confluent whenever its transitions admit a locally decreasing labeling. Essentially all classical confluence criteria arise as corollaries.

A central question, posed by van Oostrom in 1993, asks whether the decreasing diagrams technique is complete: Does every confluent transition system admit a locally decreasing labeling? This is Problem 56 of the RTA List of Open Problems. A positive answer was known only for countable systems, and recently up to the first uncountable cardinal ℵ1. The general case remained open.

We settle this thirty-three-year-old problem in full. We prove that every confluent transition system admits a locally decreasing labeling using only three labels. This bound is optimal, as two labels do not suffice even at the first uncountable cardinality. It follows that this single criterion can, in principle, certify the confluence of every confluent system, and hence of every confluent program. The entire development is machine-checked in the Isabelle/HOL and Lean proof assistants and relies only on classical logic and the axiom of choice.

Joint work with Ievgen Ivanov and Femke van Raamsdonk.

Substructural logics are non-classical logics that reject structural rules such as exchange, contraction and weakening. They support order-sensitive and resource-aware reasoning, and have applications in computer science, mathematics, linguistics and philosophy. Hypersequent calculi, which generalise sequent calculi by working with multisets of sequents, provide cut-free presentations for a wide range of substructural logics and are therefore a central tool for studying their computational complexity. However, hypersequent rules manipulate these multisets in intricate ways, which makes proof search hard to control.

This talk presents recent advances on the complexity of substructural logics with cut-free hypersequent calculi, using methods that combine structural proof theory with well-quasi-orders (wqos). Previous work established hyper-Ackermannian upper bounds for these logics, using length theorems for wqos over sets of sequents to bound proof search branches. We present new algorithms [1] that instead control proof search via wqos over sequents. This allows the use of a simpler length theorem and lowers the upper bound to Ackermannian. In particular, we obtain a new Ackermannian upper bound for the fundamental fuzzy logic MTL (monoidal t-norm logic), whose exact complexity is a longstanding open problem.

[1] A. R. Balasubramanian, Vitor Greati, Revantha Ramanayake: Hypersequent Calculi Have Ackermann Complexity. LICS 2026: 10:1-10:26. doi: 10.4230/LIPIcs.LICS.2026.10

Formally verified software is usually either fast or easy to verify. Stepwise refinement bridges that gap by separating the algorithmic idea from its efficient implementation. This structures the overall proof and lets verification scale to realistic, optimised code.

In this talk, we introduce the Isabelle Refinement Framework, its theoretical foundations, and the tools that make it practical. These are monads for shallowly embedded program semantics; a compositional refinement calculus that supports heap memory via separation logic; and syntax-driven automation for verification condition generation and for synthesising concrete programs from abstract ones.

We showcase the framework with two projects. The first is an efficient, distributed algorithm to compute large Bernoulli numbers, whose verification spans the whole spectrum from deep number theory through efficient algorithms to low-level optimisations. The second is LRAT-Isa, a verified UNSAT certificate checker that is on par with state-of-the-art unverified checkers and significantly faster than other verified ones. Its correctness proof spans from the syntax of DIMACS CNF files down to the LLVM code that implements it.