POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Wed 14 Jan 2026 16:10 - 16:35 at Dortoirs - Decision Procedures Chair(s): Andrés Goens

We study properties that allow first-order theories to be disjointly combined, including stable infiniteness, shininess, strong politeness, and gentleness. Specifically, we describe a Galois connection between sets of decidable theories, which picks out the largest set of decidable theories that can be combined with a given set of decidable theories. Using this, we exactly characterize the sets of decidable theories that can be combined with those satisfying well-known theory combination properties. This strengthens previous results and answers in the negative several long-standing open questions about the possibility of improving existing theory combination methods to apply to larger sets of theories. Additionally, the Galois connection gives rise to a complete lattice of theory combination properties, which allows one to generate new theory combination methods by taking meets and joins of elements of this lattice. We provide examples of this process, introducing new combination theorems. We situate both new and old combination methods within this lattice.

Wed 14 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

16:10 - 17:25
Decision ProceduresPOPL at Dortoirs
Chair(s): Andrés Goens TU Darmstadt
16:10
25m
Talk
Characterizing Sets of Theories That Can Be Disjointly Combined
POPL
Benjamin Przybocki Carnegie Mellon University, Guilherme V. Toledo Bar-Ilan University, Yoni Zohar
DOI
16:35
25m
Talk
Context-Free-Language Reachability for Almost-Commuting Transition Systems
POPL
Nikhil Pimpalkhare Princeton University, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin-Madison
DOI
17:00
25m
Talk
Determination Problems for Orbit Closures and Matrix Groups
POPL
Rida Ait El Manssour University of Oxford, George Kenison Liverpool John Moores University, Mahsa Shirmohammadi CNRS, Anton Varonka TU Wien, James Worrell University of Oxford
DOI