Volume
LIPIcs, Volume 380
41st Annual Symposium on Logic in Computer Science (LICS 2026)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Logic in Computer Science (LICS)
Event
Editors
Publication Details
- published at: 2026-07-09
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-434-5
Access Numbers
- Detailed Access Statistics available here
-
Total Accesses (updated on a weekly basis)
0Documents
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 380, LICS 2026, Complete Volume
Abstract
LIPIcs, Volume 380, LICS 2026, Complete Volume
Cite as
41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 1-2218, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Proceedings{faggian_et_al:LIPIcs.LICS.2026,
title = {{LIPIcs, Volume 380, LICS 2026, Complete Volume}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {1--2218},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026},
URN = {urn:nbn:de:0030-drops-270381},
doi = {10.4230/LIPIcs.LICS.2026},
annote = {Keywords: LIPIcs, Volume 380, LICS 2026, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 0:i-0:xxx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{faggian_et_al:LIPIcs.LICS.2026.0,
author = {Faggian, Claudia and Katoen, Joost-Pieter},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {0:i--0:xxx},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.0},
URN = {urn:nbn:de:0030-drops-270371},
doi = {10.4230/LIPIcs.LICS.2026.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
A Rational Defense of Reasonable Reflection (Invited Paper)
Abstract
Computational reflection is the ability of a system to inspect and modify itself. It has resisted static reasoning, especially in reflective languages, where semantics can change during program execution. We argue that reflection should be revisited in light of progress in verification and large language models. By requiring reflective modifications to carry proofs, it becomes possible to prove system properties even for reflective systems. This "reasonable reflection" could open up new ways of organizing self-improving systems.
Cite as
Nada Amin. A Rational Defense of Reasonable Reflection (Invited Paper). In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 1:1-1:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{amin:LIPIcs.LICS.2026.1,
author = {Amin, Nada},
title = {{A Rational Defense of Reasonable Reflection}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {1:1--1:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.1},
URN = {urn:nbn:de:0030-drops-267884},
doi = {10.4230/LIPIcs.LICS.2026.1},
annote = {Keywords: reflection, verification, AI}
}
Document
Invited Paper
Formal Verification of Security Protocols: 25 Years of ProVerif (Invited Paper)
Abstract
Cryptographic protocols are essential to secure communication but remain difficult to design correctly, motivating the need for rigorous verification methods. This paper provides a brief overview of symbolic verification techniques, focusing on the evolution and impact of the tool ProVerif over the past 25 years. We discuss its core principles, key extensions for richer security properties, and recent work on handling algebraic theories such as exclusive-or (XOR). We conclude by highlighting ongoing challenges, including usability and interoperability between verification approaches.
Cite as
Stéphanie Delaune. Formal Verification of Security Protocols: 25 Years of ProVerif (Invited Paper). In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 2:1-2:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{delaune:LIPIcs.LICS.2026.2,
author = {Delaune, St\'{e}phanie},
title = {{Formal Verification of Security Protocols: 25 Years of ProVerif}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {2:1--2:9},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.2},
URN = {urn:nbn:de:0030-drops-267890},
doi = {10.4230/LIPIcs.LICS.2026.2},
annote = {Keywords: Security protocols, Formal verification}
}
Document
Complete ω-Regular Supermartingale Certificates
Abstract
We introduce a general methodology for the construction of sound and complete proof rules for the almost-sure and quantitative acceptance of reactivity properties on time-homogeneous Markov chains with general state spaces. Reactivity captures ω-regular properties and subsumes linear temporal logic. Our core technical result establishes that every reactivity property admits decomposition into multiple obligations of almost-sure termination into absorbing regions, and that appropriate absorbing regions always exist on general state spaces. This enables the extension of every complete proof rule for almost-sure termination into a proof rule for reactivity that is complete in the almost-sure case, and complete up to an arbitrarily small ε-approximation in the quantitative case. We apply our new methodology to recent results on sound and complete supermartingale certificates for almost-sure termination in the special case of countably infinite state spaces, alongside standard results on quantitative safety. As a result, we obtain the first sound and complete supermartingale certificates for almost-sure ω-regular properties and the first sound and ε-complete supermartingale certificates for quantitative ω-regular properties on time-homogeneous Markov chains with countably infinite state spaces.
Cite as
Alessandro Abate, Mirco Giacobbe, Sergey Ichtchenko, and Diptarko Roy. Complete ω-Regular Supermartingale Certificates. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 3:1-3:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{abate_et_al:LIPIcs.LICS.2026.3,
author = {Abate, Alessandro and Giacobbe, Mirco and Ichtchenko, Sergey and Roy, Diptarko},
title = {{Complete \omega-Regular Supermartingale Certificates}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {3:1--3:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.3},
URN = {urn:nbn:de:0030-drops-267905},
doi = {10.4230/LIPIcs.LICS.2026.3},
annote = {Keywords: Probabilistic Model Checking, Markov Chains on Measurable State Spaces, Omega-Regular Properties, Martingale Theory}
}
Document
A Convenient Fibration for Dependently-Typed Probability Theory
Abstract
We describe semantic structures relevant for interpreting dependent types for statistical and probabilistic modelling. Our development extends the theory of quasi-Borel spaces (qbses) of Staton et. al, which support simply-typed, higher-order probability theory with continuous distributions. It is well-known that qbses can interpret a dependent-type theory supporting dependent function-spaces through the codomain fibration. We define an equivalent split fibration based on the family fibration, which we call quasi-Borel families (qbfs), characterise its structure, equip it with fibred monads of measures and probability, and use them to develop dependently-typed probability theory.
We characterise the structure of the qbf fibration that is relevant for dependently-typed probability theory in elementary form. Our characterisations include: context extension, dependent pairs, dependent functions, extensional identity types, fibred products and coproducts, subspaces, a universe of propositions, and straightforward internalisation and externalisation principles for discrete spaces. We use these concepts to define fibred distribution and probability monads, the semantic structure needed to interpret probability distributions under a dependent context. We show that this structure satisfies a fibred version of Kock’s synthetic measure theory. We also use these concepts to develop a qbs counterpart to Kolmogorov’s conditional expectation. Our main result is a version of the conditional expectation that, under standard regularity assumptions, is measurable in both the random variables we are conditioning, and the observation map we are conditioning by.
Cite as
Danel Ahman, Ohad Kammar, and Rasmus Ejlers Møgelberg. A Convenient Fibration for Dependently-Typed Probability Theory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 4:1-4:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ahman_et_al:LIPIcs.LICS.2026.4,
author = {Ahman, Danel and Kammar, Ohad and M{\o}gelberg, Rasmus Ejlers},
title = {{A Convenient Fibration for Dependently-Typed Probability Theory}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {4:1--4:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.4},
URN = {urn:nbn:de:0030-drops-267915},
doi = {10.4230/LIPIcs.LICS.2026.4},
annote = {Keywords: probability theory, quasi-Borel space, Grothendieck fibration, fibred monad, conditional expectation, measure theory, random variables, dependent types, quasitopos, probabilistic programming, denotational semantics, synthetic measure theory}
}
Document
A Complexity Bound for Determinisation of Min-Plus Weighted Automata
Abstract
The determinisation problem for min-plus (tropical) weighted automata was recently shown to be decidable. However, the proof is purely existential, relying on several non-constructive arguments. Our contribution in this work is twofold: first, we present the first complexity bound for this problem, showing it is primitive recursive. Second, our techniques introduce a versatile framework to analyse runs of weighted automata in a constructive manner. In particular, this simplifies the previous decidability argument and provides a tighter analysis, thus serving as a critical step towards a tight complexity bound.
Cite as
Shaull Almagor, Guy Arbel, and Sarai Sheinvald. A Complexity Bound for Determinisation of Min-Plus Weighted Automata. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{almagor_et_al:LIPIcs.LICS.2026.5,
author = {Almagor, Shaull and Arbel, Guy and Sheinvald, Sarai},
title = {{A Complexity Bound for Determinisation of Min-Plus Weighted Automata}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {5:1--5:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.5},
URN = {urn:nbn:de:0030-drops-267925},
doi = {10.4230/LIPIcs.LICS.2026.5},
annote = {Keywords: Automata, Weighted Automata, Determinisation, Tropical, Min Plus, Primitive Recursive}
}
Document
Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability
Abstract
Quantitative logic reasons about the degree to which formulas are satisfied. This paper studies the fundamental reasoning principles of higher-order quantitative logic and their application to reasoning about probabilistic programs and processes.
We construct an affine calculus for 1-bounded complete metric spaces and the monad for probability measures equipped with the Kantorovich distance. The calculus includes a form of guarded recursion interpreted via Banach’s fixed point theorem, useful, e.g., for recursive programming with processes. We then define an affine higher-order quantitative logic for reasoning about terms of our calculus. The logic includes novel principles for guarded recursion, and induction over probability measures and natural numbers.
We illustrate the expressivity of the logic by a sequence of case studies: Proving upper limits on bisimilarity distances of Markov processes, showing convergence of a temporal learning algorithm and of a random walk using a coupling argument.
Cite as
Giorgio Bacci and Rasmus Ejlers Møgelberg. Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 6:1-6:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bacci_et_al:LIPIcs.LICS.2026.6,
author = {Bacci, Giorgio and M{\o}gelberg, Rasmus Ejlers},
title = {{Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {6:1--6:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.6},
URN = {urn:nbn:de:0030-drops-267935},
doi = {10.4230/LIPIcs.LICS.2026.6},
annote = {Keywords: Quantitative Logic, Probabilistic Processes, Affine Logic, Guarded Recursion, Metric Spaces}
}
Document
On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic
Abstract
We consider expansions of Presburger arithmetic with families of monadic polynomial predicates. (Examples of such predicates are the set of perfect squares, or the set of integers of the form 2n³-5n+3, etc.) Although the full attendant first-order theories are well known to be undecidable, very little is known when one restricts the number of variables. In the case of single-variable theories, we obtain positive results for the following two families of predicates: (i) for perfect fixed powers, decidability of the corresponding theory follows from the solvability of hyperelliptic Diophantine equations; and (ii) for polynomials of degree at most three, we establish decidability by relying on the low genus of the resulting algebraic curves. Finally, we discuss limitations and hardness results (via encodings of longstanding open Diophantine problems) as soon as any of the above restrictions are lifted.
Cite as
Piotr Bacik, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, Madhavan Venkatesh, and Emil Rugaard Wieser. On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bacik_et_al:LIPIcs.LICS.2026.7,
author = {Bacik, Piotr and Nieuwveld, Joris and Ouaknine, Jo\"{e}l and Vahanwala, Mihir and Venkatesh, Madhavan and Wieser, Emil Rugaard},
title = {{On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {7:1--7:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.7},
URN = {urn:nbn:de:0030-drops-267947},
doi = {10.4230/LIPIcs.LICS.2026.7},
annote = {Keywords: Presburger arithmetic, Diophantine equations, decidability, B\"{u}chi’s conjecture}
}
Document
On the Subspace Orbit Problem and the Simultaneous Skolem Problem
Abstract
The Orbit Problem asks whether the orbit of a point under a matrix reaches a given target set. When the target is a single point, the problem was shown to be decidable in polynomial time by Kannan and Lipton. This decidability result was later extended by Chonev et al. to targets of dimension 3 (in arbitrary ambient dimension), but decidability remains open for subspaces of dimension 4. At the other extreme, the special case of the Orbit Problem in which the target set is a hyperplane of co-dimension 1 is equivalent to the Skolem Problem for linear recurrence sequences, whose decidability has been open for many decades.
In this paper, we show that the Orbit Problem is decidable if the target subspace has dimension logarithmic in the dimension of the orbit. Over the rationals, we moreover obtain a complexity bound NP^RP in this case, when the target space dimension is bounded. On the other hand, we show that the version of the Orbit Problem where the dimension of the target subspace is linear in the dimension of the orbit is as hard as the Skolem Problem.
Cite as
Piotr Bacik and Anton Varonka. On the Subspace Orbit Problem and the Simultaneous Skolem Problem. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 8:1-8:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bacik_et_al:LIPIcs.LICS.2026.8,
author = {Bacik, Piotr and Varonka, Anton},
title = {{On the Subspace Orbit Problem and the Simultaneous Skolem Problem}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {8:1--8:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.8},
URN = {urn:nbn:de:0030-drops-267955},
doi = {10.4230/LIPIcs.LICS.2026.8},
annote = {Keywords: Orbit Problem, Skolem Problem, Simultaneous Skolem Problem, Linear Recurrence Sequences, Verification}
}
Document
A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-Calculus
Abstract
We propose a simple space-cost measure for the λ-calculus, that extends the natural model measuring the size of the terms by also taking into consideration their origin. This new model is able to capture sublinear space complexity and we prove that, in the context of weak reduction, it is reasonable with respect to standard complexity theory. Precisely, the weak λ-calculus and Turing machines can simulate each other with a constant-factor space overhead, for any computation of logarithmic or higher space complexity. This means that the weak λ-calculus equipped with our cost model gives a proper characterization of the classical space complexity classes, including LOGSPACE and PSPACE.
Cite as
Thibaut Balabonski. A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-Calculus. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 9:1-9:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{balabonski:LIPIcs.LICS.2026.9,
author = {Balabonski, Thibaut},
title = {{A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-Calculus}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {9:1--9:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.9},
URN = {urn:nbn:de:0030-drops-267961},
doi = {10.4230/LIPIcs.LICS.2026.9},
annote = {Keywords: Lambda-calculus, Complexity, Space, Logspace, Weak reduction}
}
Document
Hypersequent Calculi Have Ackermann Complexity
Abstract
For substructural logics with contraction or weakening admitting cut-free sequent calculi, proof search was analyzed using well-quasi-orders on ℕ^d (Dickson’s lemma), yielding Ackermann upper bounds via controlled bad-sequence arguments. For hypersequent calculi, that argument lifted the ordering to the powerset, since a hypersequent is a (multi)set of sequents. This induces a jump from Ackermann to hyper-Ackermann complexity in the fast-growing hierarchy, suggesting that cut-free hypersequent calculi for extensions of the commutative Full Lambek calculus with contraction or weakening (FL_ec/FL_ew) inherently entail hyper-Ackermann upper bounds. We show that this intuition does not hold: every extension of FL_ec and FL_ew admitting a cut-free hypersequent calculus has an Ackermann upper bound on provability.
To avoid the powerset, we exploit novel dependencies between individual sequents within any hypersequent in backward proof search. The weakening case, in particular, introduces a Karp-Miller-style acceleration, and it improves the upper bound for the fundamental fuzzy logic MTL. Our Ackermann upper bound is optimal for the contraction case (realized by the logic FL_ec).
Cite as
A. R. Balasubramanian, Vitor Greati, and Revantha Ramanayake. Hypersequent Calculi Have Ackermann Complexity. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 10:1-10:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{balasubramanian_et_al:LIPIcs.LICS.2026.10,
author = {Balasubramanian, A. R. and Greati, Vitor and Ramanayake, Revantha},
title = {{Hypersequent Calculi Have Ackermann Complexity}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {10:1--10:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.10},
URN = {urn:nbn:de:0030-drops-267970},
doi = {10.4230/LIPIcs.LICS.2026.10},
annote = {Keywords: Hypersequent calculi, Substructural logics, Ackermann complexity, Well-quasi-orders}
}
Document
The Complexity of Nested Reset Counter Systems
Abstract
Nested counter systems (NCS) are a generalization of counter systems to higher-order counters. Here, a higher-order counter is allowed to have other (lower-order) counters as elements, instead of just a number. Such systems can be viewed as working on trees, where the height of the tree naturally corresponds to the highest order counter that the system is working with. It is known that the coverability problem for NCS, which asks if a given final tree can be covered from a given initial tree, is 𝐅_ε₀-complete. Here 𝐅_ε₀ is a class in the fast-growing hierarchy of complexity classes.
In this paper, we consider an extension of NCS called nested reset counter systems (NRCS) that extends NCS with resets. We show that coverability for NRCS over order-k counters is 𝐅_{Ω_k}-complete where Ω_k is the tower of height k of the ω ordinal. This gives the first natural hierarchy of complete problems for all of these classes. Furthermore, to prove our upper bounds, we also develop length function theorems for any fixed amount of applications of the multiset operation on finite sets.
As an application of our results, we improve existing upper bounds for various problems from XML processing, graph transformation systems, π-calculus, logic and parameterized verification. Furthermore, using our completeness results for k-NRCS, we also prove 𝐅_{Ω_k}-completeness of the considered problems from the realms of parameterized verification and logic, for all k.
Cite as
A. R. Balasubramanian and Franzisco Schmidt. The Complexity of Nested Reset Counter Systems. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 11:1-11:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{balasubramanian_et_al:LIPIcs.LICS.2026.11,
author = {Balasubramanian, A. R. and Schmidt, Franzisco},
title = {{The Complexity of Nested Reset Counter Systems}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {11:1--11:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.11},
URN = {urn:nbn:de:0030-drops-267985},
doi = {10.4230/LIPIcs.LICS.2026.11},
annote = {Keywords: Nested counter systems, Fast-growing hierarchy, Complexity}
}
Document
Unbounded Data Nesting for Loops in Higher-Order Programs
Abstract
We study contextual interactions in an ML-like language equipped with general references and continuations, focusing on the reachability and approximation problems.
Previous work addressed higher-order programs with first-order references in the absence of loops using automata over nested data; however, extending these techniques to programs with loops encountered fundamental technical obstacles, stemming from the need to bound the depth of data.
We introduce a new class of automata over infinite alphabets that supports unbounded nesting of data. We establish a precise correspondence between these automata and higher-order programs with loops: the trace semantics of any such program can be captured by an automaton, and conversely, the trace language of any such automaton can be realised by an imperative higher-order program with loops.
This correspondence enables the transfer of decidability and undecidability results between the automata and programs. In particular, we show that adding loops preserves decidability of reachability, while rendering approximation undecidable.
Cite as
Adriana Baldacchino and Andrzej S. Murawski. Unbounded Data Nesting for Loops in Higher-Order Programs. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 12:1-12:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{baldacchino_et_al:LIPIcs.LICS.2026.12,
author = {Baldacchino, Adriana and Murawski, Andrzej S.},
title = {{Unbounded Data Nesting for Loops in Higher-Order Programs}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {12:1--12:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.12},
URN = {urn:nbn:de:0030-drops-267990},
doi = {10.4230/LIPIcs.LICS.2026.12},
annote = {Keywords: Automata theory, automata over infinite alphabets, programming language semantics, contextual equivalence, game semantics}
}
Document
Towards Infinite PCSP: A Dichotomy for Monochromatic Cliques
Abstract
The logic MMSNP is a well-studied fragment of Existential Second-Order logic that, from a computational perspective, captures finite-domain Constraint Satisfaction Problems (CSPs) modulo polynomial-time reductions. At the same time, MMSNP contains many problems that are expressible as ω-categorical CSPs but not as finite-domain ones.
We initiate the study of Promise MMSNP (PMMSNP), a promise analogue of MMSNP. We show that every PMMSNP problem is poly-time equivalent to a (finite-domain) Promise CSP (PCSP), thereby extending the classical MMSNP-CSP correspondence to the promise setting. We then investigate the complexity of PMMSNPs arising from forbidding monochromatic cliques, a class encompassing promise graph colouring problems. For this class, we obtain a full complexity classification conditional on the Rich 2-to-1 Conjecture, a recently proposed perfect-completeness surrogate of the Unique Games Conjecture.
As a key intermediate step which may be of independent interest, we prove that it is NP-hard, under the Rich 2-to-1 Conjecture, to properly colour a uniform hypergraph even if it is promised to admit a colouring satisfying a certain technical condition called reconfigurability. This proof is an extension of the recent work of Braverman, Khot, Lifshitz and Minzer (Adv. Math. 2025). To illustrate the broad applicability of this theorem, we show that it implies most of the linearly-ordered colouring conjecture of Barto, Battistelli, and Berg (STACS 2021).
Cite as
Demian Banakh, Alexey Barsukov, and Tamio-Vesa Nakajima. Towards Infinite PCSP: A Dichotomy for Monochromatic Cliques. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 13:1-13:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{banakh_et_al:LIPIcs.LICS.2026.13,
author = {Banakh, Demian and Barsukov, Alexey and Nakajima, Tamio-Vesa},
title = {{Towards Infinite PCSP: A Dichotomy for Monochromatic Cliques}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {13:1--13:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.13},
URN = {urn:nbn:de:0030-drops-268000},
doi = {10.4230/LIPIcs.LICS.2026.13},
annote = {Keywords: Promise Constraint Satisfaction Problem, MMSNP, Approximation Algorithms, Rainbow Colouring}
}
Document
Quantum Control and General Recursion Beyond the Unitary Case
Abstract
Coherent control, aka quantum control, is a central concept in quantum computing that is attracting increasing attention from both the quantum foundations and quantum software communities. Defining coherent control in the presence of recursion and measurement has long been known to be a major challenge. In particular, no-go results have been established for standard semantical domains like completely positive maps. We address this problem by introducing the first quantum programming language with recursion that allows for the coherent control of arbitrary quantum operations. We equip this language with both an operational and a denotational semantics that we prove to be adequate. To design these semantics, we show that combining coherent control, recursion, and measurement crucially requires describing the evolution of subprograms in the absence of input. To address this, the operational semantics takes into account a default evolution branch, while the denotational semantics uses the concept of coherent quantum operation, based on vacuum extensions. We strengthen the validity of our approach by developing an observational equivalence: two programs are equivalent if their probability of termination is the same in any context. The denotational semantics is shown to be fully abstract with respect to this observational equivalence.
Cite as
Kathleen Barsse, Romain Péchoux, and Simon Perdrix. Quantum Control and General Recursion Beyond the Unitary Case. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 14:1-14:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{barsse_et_al:LIPIcs.LICS.2026.14,
author = {Barsse, Kathleen and P\'{e}choux, Romain and Perdrix, Simon},
title = {{Quantum Control and General Recursion Beyond the Unitary Case}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {14:1--14:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.14},
URN = {urn:nbn:de:0030-drops-268017},
doi = {10.4230/LIPIcs.LICS.2026.14},
annote = {Keywords: Quantum computing, semantics of programming languages, coherent control}
}
Document
Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions
Abstract
We present sound and complete relational program logics for infinite-dimensional quantum and classical-quantum programs. The logics model assertions as self-adjoint unbounded linear relations, which simultaneously support quantitative and qualitative reasoning. Our main theoretical results include new convergence theorems and infinite-dimensional duality theorems for infinite-dimensional quantum states, which we use to establish completeness.
Cite as
Gilles Barthe, Minbo Gao, Jam Kabeer Ali Khan, Matthijs Muis, Ivan Renison, Keiya Sakabe, Michael Walter, Yingte Xu, Tianshi Yu, and Li Zhou. Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 15:1-15:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{barthe_et_al:LIPIcs.LICS.2026.15,
author = {Barthe, Gilles and Gao, Minbo and Khan, Jam Kabeer Ali and Muis, Matthijs and Renison, Ivan and Sakabe, Keiya and Walter, Michael and Xu, Yingte and Yu, Tianshi and Zhou, Li},
title = {{Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {15:1--15:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.15},
URN = {urn:nbn:de:0030-drops-268020},
doi = {10.4230/LIPIcs.LICS.2026.15},
annote = {Keywords: relational program logics, infinite-dimensional quantum programs, classical-quantum programs, linear relations, quantum optimal transport}
}
Document
A Computer Formalisation of the Serre Finiteness Theorem
Abstract
Few constructions in mathematics are as elusive as the homotopy groups of spheres. These groups, which intuitively measure n-dimensional loops on m-dimensional spheres, appear at first glance to be almost completely random - an unfortunate fact, seeing as they constitute one of the fundamental building blocks of algebraic topology and homotopy theory. However, the situation is not completely hopeless: in 1951, Serre proved his celebrated finiteness theorem, which says that these groups are almost always finite abelian groups, except in two classes of special cases when they also contain copies of the integers. In a recent paper, Barton and Campion proved a variation of this result in homotopy type theory (HoTT) - an extension of Martin-Löf type theory, particularly suitable for reasoning about and formalising algebraic topology and homotopy theory. Their result shows that the homotopy groups of spheres are all finitely presented - and constructively so. Prior to this proof, only low-dimensional homotopy groups of spheres had been computed in HoTT. This made it a major breakthrough for HoTT as a foundation and, as such, the immediate target of a full-scale formalisation project. In this paper, we present the outcome of this project: a complete formalisation of Barton and Campion’s proof of the Serre finiteness theorem in Cubical Agda, a constructive proof assistant implementing a cubical flavour of HoTT. In the light of the constructivity of Cubical Agda, we discuss the prospect of running the algorithm provided by our formalisation in order to compute concrete homotopy groups of spheres.
Cite as
Reid Barton, Axel Ljungström, Owen Milner, and Anders Mörtberg. A Computer Formalisation of the Serre Finiteness Theorem. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 16:1-16:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{barton_et_al:LIPIcs.LICS.2026.16,
author = {Barton, Reid and Ljungstr\"{o}m, Axel and Milner, Owen and M\"{o}rtberg, Anders},
title = {{A Computer Formalisation of the Serre Finiteness Theorem}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {16:1--16:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.16},
URN = {urn:nbn:de:0030-drops-268031},
doi = {10.4230/LIPIcs.LICS.2026.16},
annote = {Keywords: Homotopy type theory, synthetic homotopy theory, formalisation of mathematics, constructive mathematics}
}
Document
The Algebra of Iterative Constructions
Abstract
Fixed points are a recurring theme in computer science and are often constructed as limits of suitably seeded fixed point iterations. We present the algebra of iterative constructions (AIC) - a purely algebraic approach to reasoning about fixed point iterations of continuous endomaps on complete lattices. AIC allows derivations of constructive fixed point theorems via equational logic and avoids explicit computations with indices. For example,
F ◇ F^* ⊥ = ◇ F^* ⊥
states in AIC that sup_n Fⁿ (⊥) - a construction known from the Kleene fixed point theorem - is a fixed point of F. We demonstrate the applicability of AIC by providing algebraic proofs of several well- and less-well-known fixed point theorems: Among others, we prove the Tarski-Kantorovich principle - a generalization of the Kleene fixed point theorem - as well as a fixed point-theoretic generalization of k-induction - a technique used in software verification.
We moreover present a novel fixed point theorem. It improves a recent generalization of the Tarski-Kantorovich principle due to Olszewski for obtaining pre- and postfixed points from lattice-theoretic limit inferiors and limit superiors through iterating an endomap on an arbitrary seed element: We identify sufficient continuity conditions on the endomaps so that these limits become proper fixed points. We have mechanized our algebra in Isabelle/HOL. Isabelle’s sledgehammer tool is able to find proofs of the above fixed point theorems fully automatically.
Finally, we investigate the completeness of our axiomatization of AIC. We prove that our finite set of finitary axioms is (a) sound but incomplete for standard models of AIC (sequences of elements from a complete lattice) and that (b) a different finite set of infinitary axioms is complete. We also prove that infinitary axioms are unavoidable: there exists no complete axiomatization of standard models given by finitely many finitary axioms.
Cite as
Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Todd Schmid, and Henning Urbat. The Algebra of Iterative Constructions. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 17:1-17:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{batz_et_al:LIPIcs.LICS.2026.17,
author = {Batz, Kevin and Kaminski, Benjamin Lucien and Kehrer, Lucas and Klein, Gerwin and Schmid, Todd and Urbat, Henning},
title = {{The Algebra of Iterative Constructions}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {17:1--17:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.17},
URN = {urn:nbn:de:0030-drops-268040},
doi = {10.4230/LIPIcs.LICS.2026.17},
annote = {Keywords: fixed point theorems, fixed point iteration, algebra, equational logic}
}
Document
Minimization of Streaming Transducers
Abstract
We provide general criteria for the existence of minimal models of streaming transducers, namely devices that read an input word and produce an output value by iteratively updating an internal memory. This abstract model subsumes classical (sub)sequential transducers (Schützenberger), streaming string-to-string transducers (Alur-Černý), polynomial automata (Benedikt et al.), and variants of streaming string-to-tree transducers (Alur-D'Antoni). We then instantiate these criteria to obtain effective minimization results for variants of the latter model, where outputs are terms constructed incrementally by extending (tuples of) terms either at the leaves or at the roots.
Cite as
Christian Bianchini and Gabriele Puppis. Minimization of Streaming Transducers. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 18:1-18:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bianchini_et_al:LIPIcs.LICS.2026.18,
author = {Bianchini, Christian and Puppis, Gabriele},
title = {{Minimization of Streaming Transducers}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {18:1--18:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.18},
URN = {urn:nbn:de:0030-drops-268052},
doi = {10.4230/LIPIcs.LICS.2026.18},
annote = {Keywords: Streaming transducers, Minimization}
}
Document
Reachability in VASS Extended with Integer Counters
Abstract
We consider a variant of VASS extended with integer counters, denoted VASS+ℤ. These are automata equipped with ℕ- and ℤ-counters; the ℕ-counters are required to remain nonnegative and the ℤ-counters do not have this restriction. We study the complexity of the reachability problem for VASS+ℤ when the number of ℕ-counters is fixed. We show that reachability is NP-complete in 1-VASS+ℤ (i.e. when there is only one ℕ-counter) regardless of unary or binary encoding. For d ≥ 2, using a KLMST-based algorithm, we prove that reachability in d-VASS+ℤ lies in the complexity class ℱ_{d+2}. Our upper bound improves on the naively obtained Ackermannian complexity by simulating the ℤ-counters with ℕ-counters.
To complement our upper bounds, we show that extending VASS with integer counters significantly lowers the number of ℕ-counters needed to exhibit hardness. We prove that reachability in unary 2-VASS+ℤ is PSpace-hard; without ℤ-counters this lower bound is only known in dimension 5. We also prove that reachability in unary 3-VASS+ℤ is Tower-hard. Without ℤ-counters, reachability in 3-VASS has elementary complexity and Tower-hardness is only known in dimension 8.
Cite as
Clotilde Bizière, Wojciech Czerwiński, Roland Guttenberg, Jérôme Leroux, Vincent Michielini, Łukasz Orlikowski, Antoni Puch, and Henry Sinclair-Banks. Reachability in VASS Extended with Integer Counters. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 19:1-19:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{biziere_et_al:LIPIcs.LICS.2026.19,
author = {Bizi\`{e}re, Clotilde and Czerwi\'{n}ski, Wojciech and Guttenberg, Roland and Leroux, J\'{e}r\^{o}me and Michielini, Vincent and Orlikowski, {\L}ukasz and Puch, Antoni and Sinclair-Banks, Henry},
title = {{Reachability in VASS Extended with Integer Counters}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {19:1--19:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.19},
URN = {urn:nbn:de:0030-drops-268061},
doi = {10.4230/LIPIcs.LICS.2026.19},
annote = {Keywords: vector addition systems, Petri nets, counter automata, reachability}
}
Document
On the Computational Power of Extensional ESO
Abstract
Extensional ESO is a fragment of existential second-order logic (ESO) that captures the following family of problems. Given a fixed ESO sentence Ψ and an input structure A the task is to decide whether there is an extension B of A that satisfies the first-order part of Ψ, i.e., a structure B such that R^A ⊆ R^B for every existentially quantified predicate R of Ψ, and R^A = R^B for every non-quantified predicate R of Ψ. In particular, extensional ESO describes all pre-coloured finite-domain constraint satisfaction problems (CSPs).
In this paper we study the computational power of extensional ESO; we ask, for which problems in NP is there a polynomial-time equivalent problem in extensional ESO? One of our main results states that extensional ESO has the same computational power as hereditary first-order logic. We also characterize the computational power of the fragment of extensional ESO with monotone universal first-order part in terms of finitely bounded CSPs. These results suggest a rich computational power of this logic, and we conjecture that extensional ESO captures NP-intermediate problems. We further support this conjecture by showing that extensional ESO can express current candidate NP-intermediate problems such as Graph Isomorphism, and Monotone Dualization (up to polynomial-time equivalence). On the other hand, another main result proves that extensional ESO does not have the full computational power of NP: there are problems in NP that are not polynomial-time equivalent to a problem in extensional ESP (unless E=NE).
Cite as
Manuel Bodirsky and Santiago Guzmán-Pro. On the Computational Power of Extensional ESO. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 20:1-20:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bodirsky_et_al:LIPIcs.LICS.2026.20,
author = {Bodirsky, Manuel and Guzm\'{a}n-Pro, Santiago},
title = {{On the Computational Power of Extensional ESO}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {20:1--20:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.20},
URN = {urn:nbn:de:0030-drops-268073},
doi = {10.4230/LIPIcs.LICS.2026.20},
annote = {Keywords: Existential second-order logic, constraint satisfaction problem, complexity classification, Hereditary first-order logic, NP-intermediate problems}
}
Document
Automata for MSO over Infinite Trees with Quantification over Borel Sets of Branches
Abstract
Rabin’s Tree Theorem says that the {mso} theory of the infinite binary tree 2^* is decidable. Shelah showed that MSO logic becomes undecidable if this tree is extended to 2^{≤ω}, i.e. by allowing quantification over sets of infinite branches. A longstanding open problem is whether the decidability can be recovered in 2^{≤ω} by restricting set quantification to Borel sets. We make some progress in this direction, by identifying a suitable automaton model, and showing that most of the automata-theoretic approach to Rabin’s Theorem can be extended to the new framework. The only missing part is a conjecture about finite-memory determinacy in certain games. This paper states and explores the conjecture. We prove it in some restricted cases, and give lower bounds on the memory required in those games.
Cite as
Mikołaj Bojańczyk, Antonio Casares, Sven Manthe, and Paweł Parys. Automata for MSO over Infinite Trees with Quantification over Borel Sets of Branches. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 21:1-21:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bojanczyk_et_al:LIPIcs.LICS.2026.21,
author = {Boja\'{n}czyk, Miko{\l}aj and Casares, Antonio and Manthe, Sven and Parys, Pawe{\l}},
title = {{Automata for MSO over Infinite Trees with Quantification over Borel Sets of Branches}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {21:1--21:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.21},
URN = {urn:nbn:de:0030-drops-268080},
doi = {10.4230/LIPIcs.LICS.2026.21},
annote = {Keywords: MSO logic, automata over infinite trees, games on graphs}
}
Document
Low Rank MSO
Abstract
We introduce a new logic for describing properties of graphs, which we call low rank MSO. This is the fragment of monadic second-order logic in which set quantification is restricted to vertex sets of bounded cutrank. We prove the following statements about the expressive power of low rank MSO.
- Over any class of graphs that is weakly sparse, low rank MSO has the same expressive power as separator logic. This equivalence does not hold over all graphs.
- Over any class of graphs that has bounded VC dimension, low rank MSO has the same expressive power as flip-connectivity logic. This equivalence does not hold over all graphs.
- Over all graphs, low rank MSO has the same expressive power as flip-reachability logic. Here, separator logic is an extension of first-order logic by basic predicates for checking connectivity, which was proposed by Bojańczyk [ArXiv 2107.13953] and by Schirrmacher, Siebertz, and Vigny [ACM ToCL 2023]. Flip-connectivity logic and flip-reachability logic are analogues of separator logic suited for non-sparse graphs, which we propose in this work. In particular, the last statement above implies that every property of undirected graphs expressible in low rank MSO can be decided in polynomial time.
Cite as
Mikołaj Bojańczyk, Michał Pilipczuk, Wojciech Przybyszewski, Marek Sokołowski, and Giannos Stamoulis. Low Rank MSO. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 22:1-22:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bojanczyk_et_al:LIPIcs.LICS.2026.22,
author = {Boja\'{n}czyk, Miko{\l}aj and Pilipczuk, Micha{\l} and Przybyszewski, Wojciech and Soko{\l}owski, Marek and Stamoulis, Giannos},
title = {{Low Rank MSO}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {22:1--22:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.22},
URN = {urn:nbn:de:0030-drops-268091},
doi = {10.4230/LIPIcs.LICS.2026.22},
annote = {Keywords: First Order logic, Monadic Second Order logic, cutrank, flips}
}
Document
Dicey Games: Shared Sources of Randomness in Distributed Systems
Abstract
Consider a 4-player version of Matching Pennies where a team of three players competes against the Devil. Each player simultaneously says "Heads" or "Tails". The team wins if all four choices match; otherwise the Devil wins. If all team players randomise independently, they win with probability 1/8; if all players share a common source of randomness, they win with probability 1/2. What happens when each pair of team players shares a source of randomness? Can the team do better than win with probability 1/4? The surprising (and nontrivial) answer is yes!
We introduce Dicey Games, a formal framework motivated by the study of distributed systems with shared sources of randomness (of which the above example is a specific instance). We characterise the existence, representation and computational complexity of optimal strategies in Dicey Games, and we study the problem of allocating limited sources of randomness optimally within a team.
Cite as
Léonard Brice, Thomas A. Henzinger, and K. S. Thejaswini. Dicey Games: Shared Sources of Randomness in Distributed Systems. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 23:1-23:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{brice_et_al:LIPIcs.LICS.2026.23,
author = {Brice, L\'{e}onard and Henzinger, Thomas A. and Thejaswini, K. S.},
title = {{Dicey Games: Shared Sources of Randomness in Distributed Systems}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {23:1--23:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.23},
URN = {urn:nbn:de:0030-drops-268104},
doi = {10.4230/LIPIcs.LICS.2026.23},
annote = {Keywords: Concurrent games, Shared randomness, Topology, Algebraic Geometry}
}
Document
Layered Automata: A Canonical Model for Automata over Infinite Words
Abstract
We introduce layered automata, a subclass of alternating parity automata that generalises deterministic automata. Assuming a consistency property, these automata are history deterministic and 0-1 probabilistic. We show that every omega-regular language is recognised by a unique minimal consistent layered automaton, and that this canonical form can be computed in polynomial time from every layered or deterministic automaton. We further establish that, for layered automata, both consistency checking and inclusion testing can be performed in polynomial time. Much like deterministic finite automata, minimal consistent layered automata admit a characterisation based on congruences.
Cite as
Antonio Casares, Christof Löding, and Igor Walukiewicz. Layered Automata: A Canonical Model for Automata over Infinite Words. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 24:1-24:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{casares_et_al:LIPIcs.LICS.2026.24,
author = {Casares, Antonio and L\"{o}ding, Christof and Walukiewicz, Igor},
title = {{Layered Automata: A Canonical Model for Automata over Infinite Words}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {24:1--24:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.24},
URN = {urn:nbn:de:0030-drops-268119},
doi = {10.4230/LIPIcs.LICS.2026.24},
annote = {Keywords: Omega automata, history determinism, canonical automata}
}
Document
Lazy Intermediate Representations for Algebraic Effects
Abstract
A lazy program interpreter postpones computation until the result is actually needed. This is typically more efficient than an eager (or call-by-value) interpreter, but a concern is that the semantics is not generally preserved.
We propose a new semantic analysis of lazy evaluation that relies on a subtle combination of name generation and read-only state. Our perspective is that laziness arises from a hybrid evaluation strategy, in which only the name generation follows call-by-value.
This semantic model suggests better intermediate representations of sum and product types in a lazy interpreter, along with equations that justify further optimizations. We illustrate this with an implementation in OCaml. Our motivation is practical: the origin of this work is a real-world application of discrete probabilistic programming, in which large algebraic data types cause significant performance issues with a call-by-value interpreter. Our lazy semantics justifies better optimized representations, and provides principled foundations for other methods involving laziness in probabilistic programming.
Cite as
Simon Castellan and Hugo Paquet. Lazy Intermediate Representations for Algebraic Effects. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 25:1-25:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{castellan_et_al:LIPIcs.LICS.2026.25,
author = {Castellan, Simon and Paquet, Hugo},
title = {{Lazy Intermediate Representations for Algebraic Effects}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {25:1--25:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.25},
URN = {urn:nbn:de:0030-drops-268124},
doi = {10.4230/LIPIcs.LICS.2026.25},
annote = {Keywords: Categorical semantics, lazy evaluation, interpreter, probabilistic programming}
}
Document
The Size of Interpolants in Modal Logics
Abstract
We start a systematic investigation of the size of Craig interpolants, uniform interpolants, and strongest implicates for (quasi-)normal modal logics. Our main upper bound states that for tabular modal logics, the computation of strongest implicates can be reduced in polynomial time to uniform interpolant computation in classical propositional logic. Hence they are of polynomial dag-size iff NP is included in P/poly. The reduction also holds for Craig interpolants if the tabular modal logic has the Craig interpolation property. Our main lower bound shows an unconditional exponential lower bound on the size of Craig interpolants and strongest implicates covering almost all non-tabular standard normal modal logics. For normal modal logics contained in or containing S4 or GL we obtain the following dichotomy: tabular logics have "propositionally sized" interpolants while for non-tabular logics an unconditional exponential lower bound holds.
Cite as
Balder ten Cate, Louwe B. Kuijer, and Frank Wolter. The Size of Interpolants in Modal Logics. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 26:1-26:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{tencate_et_al:LIPIcs.LICS.2026.26,
author = {ten Cate, Balder and Kuijer, Louwe B. and Wolter, Frank},
title = {{The Size of Interpolants in Modal Logics}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {26:1--26:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.26},
URN = {urn:nbn:de:0030-drops-268132},
doi = {10.4230/LIPIcs.LICS.2026.26},
annote = {Keywords: Modal logic, strongest implicates, uniform interpolants, Craig interpolants}
}
Document
Eliminating Reversals from Cubical Type Theories
Abstract
Cubical type theories are designed around an abstract unit interval from which types of paths, used to represent equalities, are defined. Varying the operations available on this interval yields different type theories. A reversal is an involutive operator on the interval that swaps its two endpoints. We show that for cubical type theories with self-dual interval theories, such as the minimal theory of two endpoints or the theory of a bounded distributive lattice, the extension of the theory with a reversal that internalizes the duality is a conservative extension. The key tool is a "twist construction": the product of an interval and its dual is again an interval with a reversal given by swapping coordinates.
Our conservativity result applies to "opaque" cubical type theories, without strict equations reducing the filling operator at concrete type formers or eliminators from higher inductive types at path constructors. Using the same twist construction, we also construct models of strict cubical type theory with reversals in categories of cubical sets without reversals. We thereby give the first model of a theory with reversals whose homotopy theory corresponds to that of topological spaces.
Cite as
Evan Cavallo and Christian Sattler. Eliminating Reversals from Cubical Type Theories. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 27:1-27:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{cavallo_et_al:LIPIcs.LICS.2026.27,
author = {Cavallo, Evan and Sattler, Christian},
title = {{Eliminating Reversals from Cubical Type Theories}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {27:1--27:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.27},
URN = {urn:nbn:de:0030-drops-268148},
doi = {10.4230/LIPIcs.LICS.2026.27},
annote = {Keywords: Dependent type theory, univalence, cubical type theory}
}
Document
A Complete Equational Theory for Real-Clifford+CH Quantum Circuits
Abstract
We introduce a complete equational theory for the fragment of quantum circuits generated by the real Clifford gates plus the two-qubit controlled-Hadamard gate. That is, we give a simple set of equalities between circuits of this fragment, and prove that any other true equation can be derived from these. This is the first such completeness result for a finitely-generated, universal fragment of quantum circuits, with no parameterized gates and no need for ancillas.
Cite as
Alexandre Clément. A Complete Equational Theory for Real-Clifford+CH Quantum Circuits. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 28:1-28:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{clement:LIPIcs.LICS.2026.28,
author = {Cl\'{e}ment, Alexandre},
title = {{A Complete Equational Theory for Real-Clifford+CH Quantum Circuits}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {28:1--28:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.28},
URN = {urn:nbn:de:0030-drops-268159},
doi = {10.4230/LIPIcs.LICS.2026.28},
annote = {Keywords: Quantum circuits, completeness, graphical language}
}
Document
Commutative Algebras of Series
Abstract
We consider a large family of product operations of formal power series in noncommuting indeterminates, the classes of automata they define, and the respective equivalence problems. A P-product of series is defined coinductively by a polynomial product rule P, which gives a recursive recipe to build the product of two series as a function of the series themselves and their derivatives. The first main result of the paper is a complete and decidable characterisation of all product rules P giving rise to P-products which are bilinear, associative, and commutative. The characterisation shows that there are infinitely many such products, and in particular it applies to the notable Hadamard, shuffle, and infiltration products from the literature.
Every P-product gives rise to the class of P-automata, an infinite-state model where states are terms. The second main result of the paper is that the equivalence problem for P-automata is decidable for P-products satisfying our characterisation. This explains, subsumes, and extends previous results on Hadamard, shuffle, and infiltration automata. We have formalised most results in the proof assistant Agda.
Cite as
Lorenzo Clemente. Commutative Algebras of Series. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 29:1-29:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{clemente:LIPIcs.LICS.2026.29,
author = {Clemente, Lorenzo},
title = {{Commutative Algebras of Series}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {29:1--29:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.29},
URN = {urn:nbn:de:0030-drops-268167},
doi = {10.4230/LIPIcs.LICS.2026.29},
annote = {Keywords: formal power series, weighted automata, product rules, algebra, coalgebra}
}
Document
The Uniformisation of Monadic Second-Order Logic over Countable Ordinals
Abstract
We study the uniformisation problem for monadic second-order logic (MSO) over countable ordinal chains. Given a formula defining a relation between subsets of the input structure, the question is whether there exists a formula that defines a function selecting, for every set in the domain of the relation, a unique set such that the pair belongs to the relation. It is known, due to Lifsches and Shelah [Lifsches and Shelah, 1998], that MSO cannot, in general, be uniformised over the class of countable ordinals.
We show that the maximal uniformisation degree is reached by extending the logic with a predicate that, given a set, selects (when possible) a cofinal subset of order type ω. Equivalently, every MSO formula can be uniformised over the class of countable ordinal chains using a formula in this extended logic.
Cite as
Thomas Colcombet and Alexander Rabinovich. The Uniformisation of Monadic Second-Order Logic over Countable Ordinals. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 30:1-30:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{colcombet_et_al:LIPIcs.LICS.2026.30,
author = {Colcombet, Thomas and Rabinovich, Alexander},
title = {{The Uniformisation of Monadic Second-Order Logic over Countable Ordinals}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {30:1--30:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.30},
URN = {urn:nbn:de:0030-drops-268178},
doi = {10.4230/LIPIcs.LICS.2026.30},
annote = {Keywords: Monadic second-order logic, uniformisation, chains, ordinals, composition method, factorization trees}
}
Document
Constructive Higher Sheaf Models with Applications to Synthetic Mathematics
Abstract
There have recently been several developments in synthetic mathematics using extensions of dependent type theory with univalence and higher inductive types: simplicial homotopy type theory, synthetic algebraic geometry and synthetic Stone duality. We provide a foundation of higher sheaf models of type theory in a constructive metatheory and, in particular, build constructive models of these formal systems.
Cite as
Thierry Coquand, Jonas Höfer, and Christian Sattler. Constructive Higher Sheaf Models with Applications to Synthetic Mathematics. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 31:1-31:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{coquand_et_al:LIPIcs.LICS.2026.31,
author = {Coquand, Thierry and H\"{o}fer, Jonas and Sattler, Christian},
title = {{Constructive Higher Sheaf Models with Applications to Synthetic Mathematics}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {31:1--31:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.31},
URN = {urn:nbn:de:0030-drops-268184},
doi = {10.4230/LIPIcs.LICS.2026.31},
annote = {Keywords: Dependent type theory, homotopy type theory, univalence, models of type theory, higher sheaves, constructive mathematics, synthetic mathematics}
}
Document
A Categorical Account of the Metropolis-Hastings Algorithm
Abstract
Metropolis-Hastings (MH) is a foundational Markov chain Monte Carlo (MCMC) algorithm. In this paper, we ask whether it is possible to formulate and analyse MH in terms of categorical probability, using a recent involutive framework for MH-type procedures as a concrete case study. We show how basic MCMC concepts such as invariance and reversibility can be formulated in Markov categories, and how one part of the MH kernel can be analysed using standard CD categories. To go further, we then study enrichments of CD categories over commutative monoids. This gives an expressive setting for reasoning abstractly about a range of important probabilistic concepts, including substochastic kernels, finite and σ-finite measures, absolute continuity, singular measures, and Lebesgue decompositions. Using these tools, we give synthetic necessary and sufficient conditions for a general MH-type sampler to be reversible with respect to a given target distribution.
Cite as
Rob Cornish and Andi Q. Wang. A Categorical Account of the Metropolis-Hastings Algorithm. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 32:1-32:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{cornish_et_al:LIPIcs.LICS.2026.32,
author = {Cornish, Rob and Wang, Andi Q.},
title = {{A Categorical Account of the Metropolis-Hastings Algorithm}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {32:1--32:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.32},
URN = {urn:nbn:de:0030-drops-268195},
doi = {10.4230/LIPIcs.LICS.2026.32},
annote = {Keywords: Categorical probability, Metropolis-Hastings, Markov category, CD category}
}
Document
Interpreting De Finetti’s Theorem in the Category of Integrable Cones
Abstract
We establish a connection between two results in the literature on probabilistic semantics: a formulation of De Finetti’s theorem in the language of category theory due to Jacobs and Staton, and the generic construction of the free exponential of Linear Logic by Melliès et al, that has been instantiated in the model of probabilistic coherence spaces by Crubillé et al. The structural proximity of these two constructions is manifest, but making this connection formal requires technical developements on the relationship between the category of stochastic kernels and the category of integrable cones, two well-known categories in probabilistic semantics. We then use this connection to give a characterisation of the total elements of the probabilistic coherence space !Bool.
Cite as
Raphaëlle Crubillé. Interpreting De Finetti’s Theorem in the Category of Integrable Cones. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 33:1-33:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{crubille:LIPIcs.LICS.2026.33,
author = {Crubill\'{e}, Rapha\"{e}lle},
title = {{Interpreting De Finetti’s Theorem in the Category of Integrable Cones}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {33:1--33:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.33},
URN = {urn:nbn:de:0030-drops-268208},
doi = {10.4230/LIPIcs.LICS.2026.33},
annote = {Keywords: De Finetti theorem, probabilistic semantics, Lafont models of Linear Logic}
}
Document
On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic
Abstract
The problem of determining whether a probabilistic program terminates almost surely (i.e. with probability one) is undecidable, and actually Π⁰₂-complete. For this reason, a growing literature has explored classes of programs for which this and related problems can be shown (semi-)decidable. In this work we consider the termination problem for the language of Probabilistic Higher-Order Recursion Schemes (PHORS). Using the weighted relational semantics of linear logic, we translate this problem into the computation of suitable generating functions associated with the program interpreted. This way, we establish the decidability of almost sure termination for a class of programs that extends Li et al.’s affine PHORS via a type discipline with bounded exponentials. To achieve this, we show that the generating functions for such programs are always algebraic, that is, solutions of polynomial equations, yielding an effective method to answer the termination problem.
Cite as
Ugo Dal Lago, Guido Fiorillo, and Paolo Pistone. On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 34:1-34:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{dallago_et_al:LIPIcs.LICS.2026.34,
author = {Dal Lago, Ugo and Fiorillo, Guido and Pistone, Paolo},
title = {{On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {34:1--34:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.34},
URN = {urn:nbn:de:0030-drops-268211},
doi = {10.4230/LIPIcs.LICS.2026.34},
annote = {Keywords: Probabilistic \lambda-calculus, linear logic, weighted relational model, algebraic power series}
}
Document
Star Complexity of Parikh Images of Languages over Infinite Alphabets
Abstract
It has been conjectured that the Parikh (commutative) image of every language over an infinite alphabet recognized by an automaton with registers is defined by a rational expression. This conjecture is known to hold for all languages recognized by one-register automata. We refine this result by proving that the star-height of the Parikh image of any language recognized by a one-register automaton is universally bounded by two. Furthermore, we show that one-register context-free languages have rational commutative images of arbitrarily high star height. We then disprove the conjecture for multiple registers, as well as disprove the equivalence of commutative expressive power between context-free grammars and automata over infinite alphabets. In other words, we show that Parikh’s theorem fails for infinite alphabets.
Cite as
Yoav Danieli. Star Complexity of Parikh Images of Languages over Infinite Alphabets. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 35:1-35:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{danieli:LIPIcs.LICS.2026.35,
author = {Danieli, Yoav},
title = {{Star Complexity of Parikh Images of Languages over Infinite Alphabets}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {35:1--35:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.35},
URN = {urn:nbn:de:0030-drops-268229},
doi = {10.4230/LIPIcs.LICS.2026.35},
annote = {Keywords: infinite alphabets, Parikh image, rational sets, star-height}
}
Document
Dynamic Planar Graph Isomorphism Is in DynFO
Abstract
Consider two planar graphs which are subject to edge insertions and deletions. We show that whether the two graphs are isomorphic can be maintained with first-order logic formulas and auxiliary data of polynomial size. This places the dynamic planar graph isomorphism problem into the dynamic descriptive complexity class DynFO. As a consequence, there is a dynamic constant-time parallel algorithm with polynomial-size auxiliary data which maintains whether two dynamic planar graphs are isomorphic.
Cite as
Samir Datta, Asif Khan, Felix Tschirbs, Nils Vortmeier, and Thomas Zeume. Dynamic Planar Graph Isomorphism Is in DynFO. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 36:1-36:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{datta_et_al:LIPIcs.LICS.2026.36,
author = {Datta, Samir and Khan, Asif and Tschirbs, Felix and Vortmeier, Nils and Zeume, Thomas},
title = {{Dynamic Planar Graph Isomorphism Is in DynFO}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {36:1--36:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.36},
URN = {urn:nbn:de:0030-drops-268233},
doi = {10.4230/LIPIcs.LICS.2026.36},
annote = {Keywords: Dynamic complexity theory, parallel computation, dynamic algorithms}
}
Document
Complexity of Satisfiability in Kochen-Specker Partial Boolean Algebras
Abstract
The Kochen-Specker no-go theorem established that hidden-variable theories in quantum mechanics necessarily admit contextuality. This theorem is formally stated in terms of the partial Boolean algebra structure of projectors on a Hilbert space. Each partial Boolean algebra provides a semantics for interpreting propositional logic. In this paper, we examine the complexity of propositional satisfiability for various classes of partial Boolean algebras. We first show that the satisfiability problem for the class of non-trivial partial Boolean algebras is NP-complete. Next, we consider the satisfiability problem for the class of partial Boolean algebras arising from projectors on finite dimensional Hilbert spaces. For real Hilbert spaces of dimension greater 2 and any complex Hilbert spaces of dimension greater than 3, we demonstrate that the satisfiability problem is complete for the existential theory of the reals. Interestingly, the proofs of these results make use of Kochen-Specker sets as gadgets. As a corollary, we conclude that deciding quantum homomorphism in these fixed dimensions are also complete for the existential theory of the reals. Finally, we show that the satisfiability problems for the class of all Hilbert spaces and all finite-dimensional Hilbert spaces is undecidable.
Cite as
Anuj Dawar and Nihil Shah. Complexity of Satisfiability in Kochen-Specker Partial Boolean Algebras. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 37:1-37:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{dawar_et_al:LIPIcs.LICS.2026.37,
author = {Dawar, Anuj and Shah, Nihil},
title = {{Complexity of Satisfiability in Kochen-Specker Partial Boolean Algebras}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {37:1--37:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.37},
URN = {urn:nbn:de:0030-drops-268247},
doi = {10.4230/LIPIcs.LICS.2026.37},
annote = {Keywords: partial Boolean algebra, quantum logic, existential theory of the reals}
}
Document
Well-Quasi-Ordered Classes of Bounded Clique-Width
Abstract
We study classes of graphs with bounded clique-width that are well-quasi-ordered by the induced subgraph relation, in the presence of labels on the vertices. We prove that, given a finite presentation of a class of graphs, one can decide whether the class is labelled-well-quasi-ordered. This answers positively to two conjectures of Pouzet in the restricted case of bounded clique-width classes. Namely, we prove that being labelled-well-quasi-ordered by a set of size 2 or by a well-quasi-ordered infinite set are equivalent conditions, and that in such cases, one can freely assume that the graphs are equipped with a total ordering on their vertices. Finally, we provide a structural characterization of those classes as those that are of bounded clique-width and do not existentially transduce the class of all finite paths.
Cite as
Maël Dumas and Aliaume Lopez. Well-Quasi-Ordered Classes of Bounded Clique-Width. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 38:1-38:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{dumas_et_al:LIPIcs.LICS.2026.38,
author = {Dumas, Ma\"{e}l and Lopez, Aliaume},
title = {{Well-Quasi-Ordered Classes of Bounded Clique-Width}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {38:1--38:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.38},
URN = {urn:nbn:de:0030-drops-268257},
doi = {10.4230/LIPIcs.LICS.2026.38},
annote = {Keywords: well-quasi-ordering, clique-width, automata theory, monoids, factorization forests, gap embedding}
}
Document
A Naturally-Colored Translation from LTL to Parity and COCOA
Abstract
Chains of co-Büchi automata (COCOA) have recently been introduced as a new canonical representation of omega-regular languages. The co-Büchi automata in a chain assign each omega-word its natural color, which depends only on the language itself and not on the chosen automaton representation. Automata in such a chain can be minimized in polynomial time and are good-for-games, making this representation attractive for verification and reactive synthesis. However, in these applications, specifications are usually given in linear temporal logic (LTL). To make COCOA useful, an LTL specification must first be translated into the chain of automata. The only translation currently known proceeds via deterministic parity automata (LTL→DPA→COCOA), where the first step ignores natural colors and requires involved constructions due to Safra or Esparza et al. This raises the question of whether, by exploiting the definition of the natural color of words, one can avoid such constructions and obtain a direct translation from LTL to COCOA.
In this paper, we present a simple yet optimal translation from LTL to COCOA, as well as a variant that translates LTL into DPA. The translation represents a new path from LTL to DPA and exploits the definition of natural colors. It relies on standard operations on weak alternating automata, the Miyano-Hayashi breakpoint construction, the subset construction, and simple graph algorithms. Starting from weak alternating automata, the procedure also applies to specifications in linear dynamic logic. The procedure runs in asymptotically optimal doubly exponential time and produces automata of asymptotically optimal size.
Cite as
Rüdiger Ehlers and Ayrat Khalimov. A Naturally-Colored Translation from LTL to Parity and COCOA. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 39:1-39:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ehlers_et_al:LIPIcs.LICS.2026.39,
author = {Ehlers, R\"{u}diger and Khalimov, Ayrat},
title = {{A Naturally-Colored Translation from LTL to Parity and COCOA}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {39:1--39:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.39},
URN = {urn:nbn:de:0030-drops-268264},
doi = {10.4230/LIPIcs.LICS.2026.39},
annote = {Keywords: Temporal Logic, Automata over Infinite Words, Canonical Automata, Automaton Minimization, Parity Automata, Determinization}
}
Document
Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property
Abstract
Recently, symbolic structures were proposed as finite representations of potentially infinite first-order structures, where Linear Integer Arithmetic terms and formulas define the domain and interpretations of a structure. We generalize symbolic structures to use any base theory that admits a standard model. Symbolic structures induce a symbolic model property, which holds for a fragment of first-order logic if every satisfiable formula in the fragment has a symbolic model. The symbolic model property implies decidability, since the model-checking problem for symbolic structures is decidable. We use the symbolic model property to prove decidability for several fragments that extend the fragment of stratified formulas, relaxing the quantifier-alternation constraints by allowing one sort to have self-looping functions, under certain restrictions. To establish the symbolic model property for these fragments we construct a symbolic model for a formula from an arbitrary model. The construction and its correctness are proved in a generic fashion, which may be instantiated to other similarly restricted fragments.
Cite as
Neta Elad and Sharon Shoham. Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 40:1-40:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{elad_et_al:LIPIcs.LICS.2026.40,
author = {Elad, Neta and Shoham, Sharon},
title = {{Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {40:1--40:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.40},
URN = {urn:nbn:de:0030-drops-268274},
doi = {10.4230/LIPIcs.LICS.2026.40},
annote = {Keywords: first-order logic, decidability, symbolic structures}
}
Document
Definitional Proof Irrelevance Made Accessible
Abstract
A universe of propositions equipped with definitional proof irrelevance constitutes a convenient medium to express properties and proofs in type-theoretic proof assistants such as Lean, Rocq, and Agda. However, allowing accessibility predicates - used to establish semantic termination arguments - to inhabit such a universe yields undecidable typechecking, hampering the predictability and foundational bases of a proof assistant. To effectively reconcile definitional proof irrelevance and accessibility predicates with both theoretical foundations and practicality in mind, we describe a type theory that extends the Calculus of Inductive Constructions featuring observational equality in a universe of strict propositions, with two variants for handling the elimination principle of accessibility predicates: one variant safeguards decidability by sticking to propositional unfolding, and the other variant favors flexibility with definitional unfolding, at the expense of a potentially diverging typechecking procedure. Crucially, the metatheory of this dual approach establishes that any proof made in the definitional variant of the theory can be translated into a proof of the same statement in the propositional variant, all while preserving the decidability of the latter. Moreover, we prove the two variants to be consistent and to satisfy forms of canonicity, ensuring that programs can indeed be properly evaluated. We present an implementation in Rocq and compare it with existing approaches. Overall, this work introduces an effective technique that informs the design of proof assistants with strict propositions, enabling local computation with accessibility predicates without compromising the ambient type theory.
Cite as
Thiago Felicissimo, Yann Leray, Loïc Pujet, Nicolas Tabareau, Éric Tanter, and Théo Winterhalter. Definitional Proof Irrelevance Made Accessible. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 41:1-41:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{felicissimo_et_al:LIPIcs.LICS.2026.41,
author = {Felicissimo, Thiago and Leray, Yann and Pujet, Lo\"{i}c and Tabareau, Nicolas and Tanter, \'{E}ric and Winterhalter, Th\'{e}o},
title = {{Definitional Proof Irrelevance Made Accessible}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {41:1--41:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.41},
URN = {urn:nbn:de:0030-drops-268289},
doi = {10.4230/LIPIcs.LICS.2026.41},
annote = {Keywords: Dependent type theory, proof assistants, Rocq, proof irrelevance, accessibility predicates, observational equality, canonicity, set-theoretic models}
}
Document
Decidability of Interpretability
Abstract
The Bodirsky-Pinsker conjecture asserts a P vs. NP-complete dichotomy for the computational complexity of Constraint Satisfaction Problems (CSPs) of first-order reducts of finitely bounded homogeneous structures. Prominently, two structures in the scope of the conjecture have log-space equivalent CSPs if they are pp-bi-interpretable, or equivalently, if their polymorphism clones are topologically isomorphic. The latter gives rise to the algebraic approach which regards structures with topologically isomorphic polymorphism clones as equivalent and seeks to identify structural reasons for hardness or tractability in topological clones. We establish that the equivalence relation of pp-bi-interpretability underlying this approach is reasonable: On the one hand, we show that it is decidable under mild conditions on the templates; this improves a theorem of Bodirsky, Pinsker and Tsankov (LICS'11) on decidability of equality of polymorphism clones. On the other hand, we show that within the much larger class of transitive ω-categorical structures without algebraicity, the equivalence relation is of lowest possible complexity in terms of descriptive set theory: namely, it is smooth, i.e., Borel-reduces to equality on the real numbers. On our way to showing the first result, we establish that the model-complete core of a structure that has a finitely bounded homogeneous Ramsey expansion (which might include all structures of the Bodirsky-Pinsker conjecture) is computable, thereby providing a constructive alternative to previous non-constructive proofs of its existence.
Cite as
Roman Feller and Michael Pinsker. Decidability of Interpretability. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 42:1-42:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{feller_et_al:LIPIcs.LICS.2026.42,
author = {Feller, Roman and Pinsker, Michael},
title = {{Decidability of Interpretability}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {42:1--42:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.42},
URN = {urn:nbn:de:0030-drops-268299},
doi = {10.4230/LIPIcs.LICS.2026.42},
annote = {Keywords: Borel reductions, Constraint Satisfaction Problem (CSP), decidability, homogeneous structures, primitive positive interpretation, polymorphism clone, Ramsey property, countably-categorical}
}
Document
Guarded Negation Transitive Closure Logic
Abstract
We study the guarded negation fragment of transitive closure logic (GNTC). We show that the satisfiability problem for GNTC is 2ExpTime-complete, by establishing the following reductions: (i) a polynomial-time reduction from the satisfiability problem for GNTC to the satisfiability problem for the unary negation fragment UNTC of GNTC, and (ii) a direct exponential-time reduction from the satisfiability problem for UNTC to the non-emptiness problem for 2-way alternating parity tree automata. Furthermore, we show that the model checking problem for GNTC is 𝖯^NP[𝒪(log² n)]-complete in combined complexity. Our result implies 𝖯^NP[𝒪(log² n)]-completeness for both UNTC and UNFO^reg, which were left open in previous works.
Cite as
Diego Figueira, Santiago Figueira, and Yoshiki Nakamura. Guarded Negation Transitive Closure Logic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 43:1-43:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{figueira_et_al:LIPIcs.LICS.2026.43,
author = {Figueira, Diego and Figueira, Santiago and Nakamura, Yoshiki},
title = {{Guarded Negation Transitive Closure Logic}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {43:1--43:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.43},
URN = {urn:nbn:de:0030-drops-268302},
doi = {10.4230/LIPIcs.LICS.2026.43},
annote = {Keywords: Transitive closure logic, Guarded negation, Unary negation, Satisfiability, Model checking}
}
Document
The Guarded Fragment with Nested Equivalences
Abstract
The Guarded Fragment (GF) is a well-established decidable fragment of first-order logic. We study an extension of GF with nested equivalence relations, namely a family of distinguished binary predicates E₁, E₂, … interpreted as equivalence relations such that E_{k+1} is coarser than E_k for every k. We show that the equality-free GF with nested equivalence relations enjoys the finite model property and has a decidable satisfiability problem. Moreover, we establish tight complexity bounds for satisfiability: Tower-completeness in general, and (K{+}2)-ExpTime-completeness when the number of distinguished predicates is fixed to K. Finally, we show that satisfiability becomes undecidable if either the nesting condition is dropped (already with two equivalence relations) or equality is admitted (already with a single equivalence relation).
Cite as
Oskar Fiuk. The Guarded Fragment with Nested Equivalences. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 44:1-44:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{fiuk:LIPIcs.LICS.2026.44,
author = {Fiuk, Oskar},
title = {{The Guarded Fragment with Nested Equivalences}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {44:1--44:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.44},
URN = {urn:nbn:de:0030-drops-268313},
doi = {10.4230/LIPIcs.LICS.2026.44},
annote = {Keywords: guarded fragment, finite model property, nested equivalence relations}
}
Document
Monads and Distributive Laws in Substructural Contexts
Abstract
We present a categorical theory of monads and distributive laws in substructural contexts. In the study of distributive laws, the roles of (the absence of) structural rules for variable contexts have been recognized; our theory formalizes these substructural situations using Tronin’s verbal categories W, in a uniform and presentation-independent manner. We introduce the classes of W-operadic monads (those defined via the structural rules in W) and of W-commutative monads (those invariant under the structural rules in W). We give a canonical construction of a distributive law ST → TS of monads on Set; it is applicable when S is W-operadic and T is W-commutative (under mild conditions). This accounts for many known and new distributive laws. Even when S fails to be W-operadic, we can refine S and force W-operadicity; this captures Varacca and Winskel’s construction of indexed valuations.
Cite as
Soichiro Fujii, Yun Chen Tsai, Yoàv Montacute, and Ichiro Hasuo. Monads and Distributive Laws in Substructural Contexts. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 45:1-45:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{fujii_et_al:LIPIcs.LICS.2026.45,
author = {Fujii, Soichiro and Tsai, Yun Chen and Montacute, Yo\`{a}v and Hasuo, Ichiro},
title = {{Monads and Distributive Laws in Substructural Contexts}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {45:1--45:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.45},
URN = {urn:nbn:de:0030-drops-268324},
doi = {10.4230/LIPIcs.LICS.2026.45},
annote = {Keywords: Monad, distributive law, operad, category theory, effect}
}
Document
The Logic of Bunched Implications Is Undecidable
Abstract
The logic of bunched implications (BI), introduced by O’Hearn and Pym (1999), has attracted significant attention due to its elegant proof calculus, varied semantics, and close connections to the propositional fragment of separation logic. We show here that provability in BI is undecidable by encoding Wang tilings into its ternary relational semantics. Equivalently, this yields the undecidability of the equational theory of BI-algebras.
Our result is much more general, applying to the {∧, ∨, ¬, -*}-fragment of stronger and weaker logics: the negation simply needs to be disjointive, and the multiplicative conjunction need not be commutative (then -* splits into two divisions ⧵, ∕). Consequently, our result covers an interval that includes BI, the non-commutative logic GBI, and Boolean BI (BBI), the latter already known to be undecidable.
This result contrasts with a long-standing expectation that BI might be decidable. We also identify the gaps in the publications claiming decidability.
Cite as
Nikolaos Galatos, Peter Jipsen, Søren Brinck Knudstorp, and Revantha Ramanayake. The Logic of Bunched Implications Is Undecidable. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 46:1-46:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{galatos_et_al:LIPIcs.LICS.2026.46,
author = {Galatos, Nikolaos and Jipsen, Peter and Knudstorp, S{\o}ren Brinck and Ramanayake, Revantha},
title = {{The Logic of Bunched Implications Is Undecidable}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {46:1--46:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.46},
URN = {urn:nbn:de:0030-drops-268334},
doi = {10.4230/LIPIcs.LICS.2026.46},
annote = {Keywords: Bunched implication logic, Intuitionistic logic with operators, Residuated lattices, Substructural logics, Undecidable logics, Tiling problem}
}
Document
Constructing Small Monadic Decompositions in Presburger Arithmetic
Abstract
A monadic decomposition of a formula over a first-order theory is an equivalent Boolean combination of atomic formulas, each containing only one variable. Monadic decomposition is a generic simplification technique that has found applications in various settings such as quantifier elimination, string solving, and constraint databases. Previous work has mostly focused on the decision problem of whether a formula admits a monadic decomposition. However, much less is known on how to efficiently produce a small monadic decomposition, which is required for any application.
We study this question for the quantifier-free fragment of Presburger arithmetic. Here, monadic decomposability is known to be coNP-complete, and monadic decompositions can be computed in exponential time. An exponential size lower bound was only known for monadic decompositions in disjunctive or conjunctive normal form (DNF or CNF). In this work, we extend this exponential lower bound to general monadic decompositions. Guided by this lower bound, we present fragments that admit polynomially-sized monadic decompositions, which, in many cases, can be constructed efficiently. A surprising key ingredient in our proof is a family of small-depth circuits for arithmetic operations in Chinese remainder representation.
Cite as
Moses Ganardi and Marin Ricros. Constructing Small Monadic Decompositions in Presburger Arithmetic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 47:1-47:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ganardi_et_al:LIPIcs.LICS.2026.47,
author = {Ganardi, Moses and Ricros, Marin},
title = {{Constructing Small Monadic Decompositions in Presburger Arithmetic}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {47:1--47:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.47},
URN = {urn:nbn:de:0030-drops-268346},
doi = {10.4230/LIPIcs.LICS.2026.47},
annote = {Keywords: Monadic decomposition, variable independence, Presburger arithmetic}
}
Document
Graphical Algebraic Geometry: From Ideals and Varieties to Quantum Calculi
Abstract
We introduce Graphical Algebraic Geometry (GAG), a family of diagrammatic languages extending the Graphical Linear Algebra programme. We construct several languages within this family and prove that they are universal and complete for the corresponding (co)span semantics of commutative algebras and affine varieties. This framework provides clear graphical representations of algebraic structures - such as polynomials, ideals, and varieties - enabling intuitive yet rigorous diagrammatic reasoning.
We showcase two practical viewpoints on GAG. First, we show that instances of counting constraint satisfaction problem (#CSP) are recast as rewrite problems of closed diagrams in GAG. This means that deciding rewritability in GAG is #P-hard, and GAG can be viewed as a complete and compositional rewrite system for networks of polynomial constraints. Second, we characterize the qudit ZH calculus, a diagrammatic language for quantum computation, as an extension of Graphical Algebraic Geometry. This establishes the correspondence that Graphical Algebraic Geometry is to the ZH calculus what Graphical Linear Algebra is to the ZX calculus. Using this construction, we show that computing amplitudes in qudit ZH requires only a constant number of queries to a GAG oracle.
Cite as
Dichuan Gao, Razin A. Shaikh, and Aleks Kissinger. Graphical Algebraic Geometry: From Ideals and Varieties to Quantum Calculi. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 48:1-48:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{gao_et_al:LIPIcs.LICS.2026.48,
author = {Gao, Dichuan and Shaikh, Razin A. and Kissinger, Aleks},
title = {{Graphical Algebraic Geometry: From Ideals and Varieties to Quantum Calculi}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {48:1--48:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.48},
URN = {urn:nbn:de:0030-drops-268354},
doi = {10.4230/LIPIcs.LICS.2026.48},
annote = {Keywords: string diagrams, algebraic geometry, ZH calculus, constraint satisfaction}
}
Document
Meta-Mathematics of Algebraic Complexity
Abstract
We initiate the study of the meta-mathematics of algebraic circuit lower bounds, aiming both to gain insight into the methods sufficient and necessary to prove algebraic circuit lower bounds, and to contribute to the study of bounded arithmetic as a logical foundation for complexity lower bounds. We demonstrate that while algebraic circuit lower bounds are hard for somewhat weak proof systems such as polynomial calculus resolution (PCR), contemporary lower bounds are efficiently provable in proof systems and bounded arithmetic theories corresponding to NC², such as VNC² and the corresponding class of propositional Frege proofs of quasipolynomial-size. Moreover, going below VNC² into algebraic constant-depth reasoning is likely insufficient to efficiently prove already constant-depth algebraic circuit lower bounds. Specifically, we show the following.
- NC²-reasoning and rank method. Algebraic circuit lower bounds are often proved via the "rank method", with recent prominent applications including the constant-depth lower bounds of Limaye, Srinivasan and Tavenas [Limaye et al., 2025] and Forbes [Forbes, 2024]. We show that these rank-based arguments can be formalized in the bounded arithmetic theory VNC², which captures reasoning with NC² concepts. This complements the work of Tzameret and Cook [Tzameret and Cook, 2021], who formalized structural upper bounds in this theory, and provides a unified framework for studying barriers to current algebraic complexity methods, complementing barriers studied by Efremenko, Garg, Makam, Oliveira, and Wigderson [Klim Efremenko et al., 2018; Ankit Garg et al., 2019].
- Sparsity algebraic reasoning. We show that Polynomial Calculus Resolution (PCR) cannot efficiently prove superpolynomial algebraic circuit lower bounds for any family of polynomials. Moreover, PCR cannot efficiently prove exponential constant-depth circuit lower bounds for any family of polynomials.
- Constant-depth algebraic reasoning. We introduce the Tensor Rank Principle and demonstrate it is hard for PCR. We show that if this principle is hard against constant-depth Ideal Proof System (IPS) then constant-depth IPS cannot efficiently prove constant-depth algebraic circuit lower bounds.
Cite as
Michal Garlík, Svyatolav Gryaznov, Jiaqi Lu, Rahul Santhanam, and Iddo Tzameret. Meta-Mathematics of Algebraic Complexity. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 49:1-49:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{garlik_et_al:LIPIcs.LICS.2026.49,
author = {Garl{\'\i}k, Michal and Gryaznov, Svyatolav and Lu, Jiaqi and Santhanam, Rahul and Tzameret, Iddo},
title = {{Meta-Mathematics of Algebraic Complexity}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {49:1--49:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.49},
URN = {urn:nbn:de:0030-drops-268360},
doi = {10.4230/LIPIcs.LICS.2026.49},
annote = {Keywords: Complexity lower bounds, Bounded arithmetic, Feasible constructive mathematics, Algebraic complexity, Proof complexity, Meta-complexity, Algebraic circuit lower bounds, Polynomial Calculus Resolution, Barriers}
}
Document
An Algebraic Approach to Formal System Metatheory
Abstract
We introduce an algebraic approach to the metatheory of formal systems of term assertions akin to those of structural and natural operational semantics, type theories, rewriting systems, and equational theories. We rest on Term Relation Algebras, viz. pointfree algebras of structurally-defined predicates on terms, to give a common algebraic semantics to different kinds of formal systems, regardless of their inferential mechanisms and underlying term structures. This enables abstract reasoning about formal systems, and their metatheory, through the algebra of the term predicates they define. We give a faithfully term-free algebraization of semantically-relevant term predicates, such as parallel reduction, big-step evaluation, and applicative bisimilarity. We extend this algebraization also to fundamental metatheoretical properties of these notions - including congruence of applicative bisimilarity, determinacy of evaluation, and confluence of reduction - and prove these properties using algebraic methods.
Cite as
Francesco Gavazzo. An Algebraic Approach to Formal System Metatheory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 50:1-50:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{gavazzo:LIPIcs.LICS.2026.50,
author = {Gavazzo, Francesco},
title = {{An Algebraic Approach to Formal System Metatheory}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {50:1--50:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.50},
URN = {urn:nbn:de:0030-drops-268379},
doi = {10.4230/LIPIcs.LICS.2026.50},
annote = {Keywords: Relation Algebra, Term Relations, Language Metatheory, Formal System Metatheory}
}
Document
LFPL: Revisited and Mechanized
Abstract
Hofmann (1999) introduced the functional programming language LFPL to characterize the functions computable in polynomial time using an affine type system. LFPL enables a natural programming style, including nested recursion, and has inspired the development of type systems for automatic cost analysis, linear dependent type theories, and efficient memory management in functional programming languages. Despite its prominence, there does not exist a self-contained presentation, let alone a full mechanization, of LFPL and its core metatheory.
This article presents a modern account and mechanization of LFPL and its metatheory with the goal of being self-contained and accessible while streamlining the strongest-known soundness and completeness results. The soundness proof works with the language LFPL+, which extends LFPL with additional language features. The proof is novel, adapting a technique by Aehlig and Schwichtenberg (2002) to construct explicit polynomials that bound the cost of an LFPL+ expression with respect to a big-step cost semantics. The completeness proof shows that LFPL programs can simulate polynomial-time Turing machines while only relying on restricted forms of linear functions and lists. It has the same structure as the original proof by Hofmann (2002) but greatly simplifies the core argument with a novel stack-like data structure that is implemented with first-class functions and lists. The mechanization includes the full soundness and completeness proofs, and serves as one of the first case studies of mechanized metatheory in the recently developed proof assistant Istari.
Cite as
Nathaniel Glover and Jan Hoffmann. LFPL: Revisited and Mechanized. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 51:1-51:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{glover_et_al:LIPIcs.LICS.2026.51,
author = {Glover, Nathaniel and Hoffmann, Jan},
title = {{LFPL: Revisited and Mechanized}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {51:1--51:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.51},
URN = {urn:nbn:de:0030-drops-268384},
doi = {10.4230/LIPIcs.LICS.2026.51},
annote = {Keywords: Type Theory, Implicit Computational Complexity, Affine Logic}
}
Document
The ∞-Category of ∞-Categories in Simplicial Type Theory
Abstract
Simplicial type theory (STT) was introduced by Riehl and Shulman to leverage homotopy type theory to prove results about (∞,1)-categories. Initial work on simplicial type theory focused on "formal" arguments in higher category theory and, in particular, no non-trivial examples of ∞-category theory were constructible within STT. More recent work has changed this state of affairs by applying techniques developed initially for cubical type theory to construct the ∞-category of spaces. We complete this process by constructing the ∞-category of ∞-categories, recovering one of the main foundational results of ∞-category theory (straightening-unstraightening) purely type-theoretically. We also show how this construction enables new examples of the directed version of the structure identity principle: the structure homomorphism principle.
Cite as
Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. The ∞-Category of ∞-Categories in Simplicial Type Theory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 52:1-52:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{gratzer_et_al:LIPIcs.LICS.2026.52,
author = {Gratzer, Daniel and Weinberger, Jonathan and Buchholtz, Ulrik},
title = {{The ∞-Category of ∞-Categories in Simplicial Type Theory}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {52:1--52:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.52},
URN = {urn:nbn:de:0030-drops-268393},
doi = {10.4230/LIPIcs.LICS.2026.52},
annote = {Keywords: Type theory, Homotopy type theory, Category theory, Infinity category theory}
}
Document
PVASS Reachability Is Decidable
Abstract
Reachability in pushdown vector addition systems with states (PVASS) is among the longest standing open problems in Theoretical Computer Science. We show that the problem is decidable in full generality. Our decision procedure is similar in spirit to the KLMST algorithm for VASS reachability, but works over objects that support an elaborate form of procedure summarization as known from pushdown reachability.
Cite as
Roland Guttenberg, Eren Keskin, and Roland Meyer. PVASS Reachability Is Decidable. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 53:1-53:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{guttenberg_et_al:LIPIcs.LICS.2026.53,
author = {Guttenberg, Roland and Keskin, Eren and Meyer, Roland},
title = {{PVASS Reachability Is Decidable}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {53:1--53:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.53},
URN = {urn:nbn:de:0030-drops-268406},
doi = {10.4230/LIPIcs.LICS.2026.53},
annote = {Keywords: Pushdowns, Petri Nets, VASS, PVASS, Reachability, Decidability, Complexity}
}
Document
A Categorical Perspective on Constraint Satisfaction: The Wonderland of Adjunctions
Abstract
The so-called algebraic approach to the constraint satisfaction problem (CSP) has been a prevalent method of the study of complexity of these problems since early 2000’s. The core of this approach is the notion of polymorphisms which determine the complexity of the problem (up to log-space reductions). In the past few years, a new, more general version of the CSP emerged, the promise constraint satisfaction problem (PCSP), and the notion of polymorphisms and most of the core theses of the algebraic approach were generalised to the promise setting. Nevertheless, recent work also suggests that insights from other fields are immensely useful in the study of PCSPs including algebraic topology.
In this paper, we provide an entry point for category-theorists into the study of complexity of CSPs and PCSPs. We show that many standard CSP notions have clear and well-known categorical counterparts. For example, the algebraic structure of polymorphisms can be described as a set-functor defined as a right Kan extension. We provide purely categorical proofs of core results of the algebraic approach including a proof that the complexity only depends on the polymorphisms. Our new proofs are substantially shorter and, from the categorical perspective, cleaner than previous proofs of the same results. Moreover, as expected, they are applicable more widely. We believe that, in particular in the case of PCSPs, category theory brings insights that can help solve some of the current challenges of the field.
Cite as
Maximilian Hadek, Tomáš Jakl, and Jakub Opršal. A Categorical Perspective on Constraint Satisfaction: The Wonderland of Adjunctions. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 54:1-54:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{hadek_et_al:LIPIcs.LICS.2026.54,
author = {Hadek, Maximilian and Jakl, Tom\'{a}\v{s} and Opr\v{s}al, Jakub},
title = {{A Categorical Perspective on Constraint Satisfaction: The Wonderland of Adjunctions}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {54:1--54:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.54},
URN = {urn:nbn:de:0030-drops-268415},
doi = {10.4230/LIPIcs.LICS.2026.54},
annote = {Keywords: constraint satisfaction problem, categorical models and logics}
}
Document
Classifying 2-Groups in Homotopy Type Theory
Abstract
Under the homotopy hypothesis, higher dimensional groups are defined as pointed homotopy types whose homotopy groups vanish outside a certain range. In particular, a 2-group is a pointed connected homotopy 2-type. Classically, 2-groups have two equivalent algebraic descriptions: one in terms of weak monoidal categories and the other in terms of group cohomology. We present these two classifications of pointed connected 2-types in homotopy type theory, thereby providing internal, constructive counterparts to the traditional classifications of 2-groups. Our first classification (in terms of monoidal categories) takes the form of a bicategorical equivalence, while our second is a type equivalence that extends to n-groups for all n ≥ 2. We have mechanized our results in Agda.
Cite as
Perry Hart and Owen Milner. Classifying 2-Groups in Homotopy Type Theory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 55:1-55:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{hart_et_al:LIPIcs.LICS.2026.55,
author = {Hart, Perry and Milner, Owen},
title = {{Classifying 2-Groups in Homotopy Type Theory}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {55:1--55:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.55},
URN = {urn:nbn:de:0030-drops-268428},
doi = {10.4230/LIPIcs.LICS.2026.55},
annote = {Keywords: homotopy type theory, synthetic homotopy theory, 2-group, higher inductive type, bicategory, higher group, cohomology}
}
Document
One Rig to Control Them All
Abstract
Controlled commands - computations whose execution depends on a separate input - play a central role in reversible Boolean circuits and quantum circuits. However, existing formalisms typically treat control only implicitly, entangled with other aspects of computation. From a semantic perspective, control is most naturally expressed in semisimple rig categories, which - unlike standard circuit models such as props - support both parallel and conditional composition.
We present a construction that freely adjoins an explicit syntactic notion of control to a circuit theory specified as a suitable prop, subject to eight universally quantified equations. Our main result is that these equations are sound and complete for the intended semantics of control: the resulting theory satisfies a universal property, identifying it exactly as the circuit subtheory of the free semisimple rig completion. The proof combines coherence for rig categories with a new method based on induction over Gray codes.
We illustrate the usefulness of the framework by showing that it simplifies several existing sound and complete axiomatisations of quantum circuits, isolating a small and conceptually clean set of generators and equations. In addition, the same equations yield a sound and complete axiomatisation of the multiply controlled Toffoli gate set, that is universal for reversible Boolean circuits.
Cite as
Chris Heunen, Robin Kaarsgaard, and Louis Lemonnier. One Rig to Control Them All. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 56:1-56:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{heunen_et_al:LIPIcs.LICS.2026.56,
author = {Heunen, Chris and Kaarsgaard, Robin and Lemonnier, Louis},
title = {{One Rig to Control Them All}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {56:1--56:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.56},
URN = {urn:nbn:de:0030-drops-268435},
doi = {10.4230/LIPIcs.LICS.2026.56},
annote = {Keywords: Quantum control, rig categories, complete equational theories}
}
Document
Causality in Pure Quantum Computation with Quantum Control
Abstract
Indefinite causal order is a characteristic phenomenon in quantum computation, with examples including the quantum SWITCH and the OCB process. Not all such processes are believed to be physically realizable: while some implementations of the quantum SWITCH have been proposed, the OCB process is suspected to be unrealizable. This difference in realizability is commonly attributed to constraints imposed by physical causality.
This paper studies such a causality issue in a higher-order setting, proposing a typed lambda calculus with quantum control and its categorical semantics. Our calculus extends pure quantum computation with higher-order functions and quantum conditional branching, and it is equipped with a type system based on intuitionistic BV logic to enforce causality. We also present a novel model that is closely related to the Caus construction, by which we prove that some physically-unrealizable processes are not definable in our language.
Cite as
Kengo Hirata and Takeshi Tsukada. Causality in Pure Quantum Computation with Quantum Control. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 57:1-57:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{hirata_et_al:LIPIcs.LICS.2026.57,
author = {Hirata, Kengo and Tsukada, Takeshi},
title = {{Causality in Pure Quantum Computation with Quantum Control}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {57:1--57:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.57},
URN = {urn:nbn:de:0030-drops-268445},
doi = {10.4230/LIPIcs.LICS.2026.57},
annote = {Keywords: Quantum computing, supermap, categorical model, linear logic, BV logic, programming language, type system}
}
Document
Fat Cell Structures and Generalized Algebraic Theories
Abstract
We give a new syntax-independent account of finitely-presented generalized algebraic theories (GATs) as finite cell complexes in the category of categories with families (CwFs), in which GATs are constructed by successive pushouts along the CwF morphisms generically postulating a sort, an operation, or an equation. Inspired by the fat small object argument of Makkai, Rosický, and Vokřínek, we introduce fat GAT presentations, thereby allowing infinite presentations with non-linear dependency structure. Then, motivated by wanting our GATs to self-describe, we extend presentations to admit infinitary arities, including infinitely deep dependency chains. Finally, we verify that these generalized GATs satisfy expected semantic properties including Frey’s Gabriel–Ulmer duality.
Cite as
Xu Huang and Carlo Angiuli. Fat Cell Structures and Generalized Algebraic Theories. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 58:1-58:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{huang_et_al:LIPIcs.LICS.2026.58,
author = {Huang, Xu and Angiuli, Carlo},
title = {{Fat Cell Structures and Generalized Algebraic Theories}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {58:1--58:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.58},
URN = {urn:nbn:de:0030-drops-268451},
doi = {10.4230/LIPIcs.LICS.2026.58},
annote = {Keywords: Generalized algebraic theories, quotient inductive-inductive types, categories with families, cell complexes, logical frameworks, Gabriel-Ulmer duality}
}
Document
Generalized Decidability via Brouwer Trees
Abstract
In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable, or undecidable". We work in homotopy type theory and use Brouwer tree ordinals to specify the level of decidability of a property. In this framework, we express the property that a proposition is α-decidable, for an ordinal α, and show that it generalizes decidability and semidecidability. Further generalizing known results, we show that α-decidable propositions are closed under binary conjunction, and discuss for which α they are closed under binary disjunction. We prove that if each P(i) is semidecidable, then the countable meet ∀ i ∈ ℕ. P(i) is ω²-decidable, and similar results for countable joins and iterated quantifiers. We also discuss the relationship with countable choice. All our results are formalized in Cubical Agda.
Cite as
Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, and Fredrik Nordvall Forsberg. Generalized Decidability via Brouwer Trees. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 59:1-59:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{dejong_et_al:LIPIcs.LICS.2026.59,
author = {de Jong, Tom and Kraus, Nicolai and Mohammadzadeh, Aref and Nordvall Forsberg, Fredrik},
title = {{Generalized Decidability via Brouwer Trees}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {59:1--59:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.59},
URN = {urn:nbn:de:0030-drops-268466},
doi = {10.4230/LIPIcs.LICS.2026.59},
annote = {Keywords: Decidability in constructive mathematics, homotopy type theory, ordinals, Brouwer trees, countable choice}
}
Document
Computation and Size of Interpolants for Hybrid Modal Logics
Abstract
Recent research has established complexity results for the problem of deciding the existence of interpolants in logics lacking the Craig interpolation property (CIP). The proof techniques developed so far are non-constructive, and no meaningful bounds on the size of interpolants are known. Hybrid modal logics (or modal logics with nominals) are a particularly interesting class of logics without CIP: in their case, CIP cannot be restored without sacrificing decidability and, in applications, interpolants in these logics can serve as definite descriptions and separators between positive and negative data examples in description logic knowledge bases. In this contribution we show, using a new hypermosaic elimination technique, that in many standard hybrid modal logics Craig interpolants can be computed in fourfold exponential time, if they exist. On the other hand, we show that the existence of uniform interpolants is undecidable, which is in stark contrast to modal or intuitionistic logic where uniform interpolants always exist.
Cite as
Jean Christoph Jung, Jędrzej Kołodziejski, and Frank Wolter. Computation and Size of Interpolants for Hybrid Modal Logics. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 60:1-60:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{jung_et_al:LIPIcs.LICS.2026.60,
author = {Jung, Jean Christoph and Ko{\l}odziejski, J\k{e}drzej and Wolter, Frank},
title = {{Computation and Size of Interpolants for Hybrid Modal Logics}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {60:1--60:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.60},
URN = {urn:nbn:de:0030-drops-268475},
doi = {10.4230/LIPIcs.LICS.2026.60},
annote = {Keywords: Interpolation, Modal Logic, Hybrid Logic, Separator Computation}
}
Document
Complexity Classes Arising from Circuits over Finite Algebraic Structures
Abstract
Most classical results in circuit complexity theory concern circuits over the Boolean domain. Besides their simplicity and the ease of comparing different languages, the actual architecture of computers is also an important motivating factor. On the other hand, by restricting attention to Boolean circuits, we lose sight of the much richer landscape of circuits over larger domains. Our goal is to bridge these two worlds: to use deep algebraic tools to obtain results in computational complexity theory, including circuit complexity, and to apply results from computational complexity to gain a better understanding of the structure of finite algebras.
In this paper, we propose a unifying algebraic framework which we believe will help achieve this goal. Our work is inspired by branching programs and nonuniform deterministic automata introduced by Barrington, as well as by their generalization proposed by Idziak et al. We begin our investigation by studying the languages recognized by natural classes of algebraic structures. In particular, we characterize language classes recognized by circuits over simple algebras and over algebras from congruence modular varieties.
Cite as
Piotr Kawałek and Jacek Krzaczkowski. Complexity Classes Arising from Circuits over Finite Algebraic Structures. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 61:1-61:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{kawalek_et_al:LIPIcs.LICS.2026.61,
author = {Kawa{\l}ek, Piotr and Krzaczkowski, Jacek},
title = {{Complexity Classes Arising from Circuits over Finite Algebraic Structures}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {61:1--61:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.61},
URN = {urn:nbn:de:0030-drops-268489},
doi = {10.4230/LIPIcs.LICS.2026.61},
annote = {Keywords: Circuit Complexity, Universal Algebra, algebraic branching programs}
}
Document
The Logic of Intersection Subtyping
Abstract
The subtyping relation of programming languages can be analysed as an entailment relation by means of proof theory. We are interested in two main families of systems: intersection types and polymorphic subtyping. They share the fact that implication has some distributivity property: over intersection in the first case and over universal quantification in the second one.
We introduce a restriction of the second-order (full) Lambek calculus which is stable under cut-elimination and conservatively extends these two subtyping relations. This new system IS is an intuitionistic non-commutative linear sequent calculus which provides a natural logical setting for the study of subtyping relations.
We recover sequent calculi from the literature (as well as new variants) as restrictions of IS (thanks to the proof-theoretical analysis of the system: admissible rules, invertibility, focusing, etc.), so that IS appears as a unifying logic for subtyping. We also develop translations relating IS with relevant logic, the (unconstrained) Lambek calculus or cyclic linear logic.
Cite as
Olivier Laurent. The Logic of Intersection Subtyping. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 62:1-62:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{laurent:LIPIcs.LICS.2026.62,
author = {Laurent, Olivier},
title = {{The Logic of Intersection Subtyping}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {62:1--62:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.62},
URN = {urn:nbn:de:0030-drops-268497},
doi = {10.4230/LIPIcs.LICS.2026.62},
annote = {Keywords: Intersection types, subtyping, polymorphic subtyping, Lambek calculus, linear logic, cut elimination}
}
Document
Oracles Just for Fan: A Robust Computational Interpretation of the Fan Theorem
Abstract
Friedman-Simpson’s original program of reverse mathematics, as is also the case for most of standard mathematics, has been developed in classical subsystems of second-order arithmetic. As such, (classical) reverse mathematics presents various limitations from a constructive point of view, since for instance it is unable to distinguish between a statement and its contrapositive (e.g. dependent choice and the bar induction principles). The case of (Weak) Kőnig’s Lemma (WKL) and Fan Theorem (FT) is particularly interesting in that regard: while WKL is well-known to imply FT, and if constructivists like Brouwer rejected the former while admitting the latter, the converse implication has not been much studied for years. It is only recently that a growing enthusiasm for constructive reverse mathematics pushed towards a finer-grained analysis of the connection between such principles.
In addition to intuitionistic reverse mathematics, the realizability approach to logical principles adds a computational meaning to purely logical statements. We follow this path to investigate the computational meaning of Brouwer’s Fan Theorem: building on recent work by Lubarsky and Rathjen, we first construct a realizability interpretation of higher-order logic validating FT while refuting WKL. This interpretation relies on a λ-calculus extended with oracles while preserving a notion of continuity for realizers.
We then push this approach a step further to show the robustness of this realizability interpretation by identifying, in the abstract and general setting of evidenced frames, sufficient computational conditions entailing FT.
Cite as
Titouan Leclercq and Étienne Miquey. Oracles Just for Fan: A Robust Computational Interpretation of the Fan Theorem. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 63:1-63:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{leclercq_et_al:LIPIcs.LICS.2026.63,
author = {Leclercq, Titouan and Miquey, \'{E}tienne},
title = {{Oracles Just for Fan: A Robust Computational Interpretation of the Fan Theorem}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {63:1--63:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.63},
URN = {urn:nbn:de:0030-drops-268500},
doi = {10.4230/LIPIcs.LICS.2026.63},
annote = {Keywords: Constructive Mathematics, Reverse mathematics, Fan Theorem, Oracles, Realizability, Evidenced frames}
}
Document
Checking History Determinism for Parity Automata Is in NP
Abstract
History-deterministic automata, often also called good-for-games, are an intermediate model between deterministic and nondeterministic automata, which are particularly well-suited for applications in verification and reactive synthesis. We show that deciding whether a parity automaton is history-deterministic is in NP. Our result matches an NP-hardness lower bound (Prakash 2024) and builds on insights from a fixed-parameter tractable algorithm (Lehtinen and Prakash 2025). This settles the complexity of the problem, which has been open since 2006.
Cite as
Karoliina Lehtinen, Keya Prakash, and Michał Skrzypczak. Checking History Determinism for Parity Automata Is in NP. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 64:1-64:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{lehtinen_et_al:LIPIcs.LICS.2026.64,
author = {Lehtinen, Karoliina and Prakash, Keya and Skrzypczak, Micha{\l}},
title = {{Checking History Determinism for Parity Automata Is in NP}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {64:1--64:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.64},
URN = {urn:nbn:de:0030-drops-268517},
doi = {10.4230/LIPIcs.LICS.2026.64},
annote = {Keywords: History-determinism, parity automata, good-for-games}
}
Document
A Unified Treatment of the Substitution Tensor for Presheaves, Nominal Sets, Renaming Sets, and so on
Abstract
Presheaves and nominal sets provide alternative abstract models of sets of syntactic objects with free and bound variables, such as λ-terms. One distinguishing feature of the presheaf-based perspective is its elegant syntax-free characterization of substitution using a closed monoidal structure. In this paper, we introduce a corresponding closed monoidal structure on nominal sets, in the spirit of Fiore et al.’s substitution tensor for presheaves over finite sets. To this end, we present a general method to derive a closed monoidal structure on a category from a given action of a monoidal category on that category. We demonstrate that this method not only uniformly recovers known substitution tensors for various kinds of presheaf categories but also yields notions of substitution tensor for nominal sets and their relatives, such as renaming sets. In the process, we shed new light on different incarnations of nominal sets and (pre-)sheaf categories and establish a number of correspondences between them.
Cite as
Fabian Lenke, Stefan Milius, and Henning Urbat. A Unified Treatment of the Substitution Tensor for Presheaves, Nominal Sets, Renaming Sets, and so on. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 65:1-65:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{lenke_et_al:LIPIcs.LICS.2026.65,
author = {Lenke, Fabian and Milius, Stefan and Urbat, Henning},
title = {{A Unified Treatment of the Substitution Tensor for Presheaves, Nominal Sets, Renaming Sets, and so on}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {65:1--65:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.65},
URN = {urn:nbn:de:0030-drops-268523},
doi = {10.4230/LIPIcs.LICS.2026.65},
annote = {Keywords: Substitution, Presheaves, Nominal Sets, Monoidal Category}
}
Document
Cellular Methods in Homotopy Type Theory
Abstract
In classical mathematics, a CW complex is a topological space which can be built up inductively by gluing together cells of increasing dimension. Thanks to their excellent categorical properties, CW complexes have become one of the main objects of interest in algebraic topology. Although their quasi-combinatorial nature suggests that a constructive treatment is possible, there seems to be little literature on the subject - perhaps because of the important role played by the axiom of choice in the classical theory of CW complexes.
In this paper, we present a synthetic and constructive account of the theory of CW complexes in homotopy type theory. Our first main result is a finitary version of the cellular approximation theorem which, among other things, allows us to construct a cellular homology functor without needing the axiom of choice or relying on a pre-existing notion of homology. Our second main result, which we call the "Hurewicz approximation theorem", shows that the CW complexes that are n-connected types are precisely the ones that can be presented by a CW structure with no nontrivial cells up to dimension n. This theorem is standard in the classical treatment of CW complexes, but it is far from being obvious in a constructive setting. As a corollary, we give a new proof of the Hurewicz theorem for CW complexes, which relates the first non-vanishing homotopy group of a CW complex with the corresponding homology group. All key theorems presented in this paper have been mechanised in Cubical Agda.
Cite as
Axel Ljungström and Loïc Pujet. Cellular Methods in Homotopy Type Theory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 66:1-66:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ljungstrom_et_al:LIPIcs.LICS.2026.66,
author = {Ljungstr\"{o}m, Axel and Pujet, Lo\"{i}c},
title = {{Cellular Methods in Homotopy Type Theory}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {66:1--66:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.66},
URN = {urn:nbn:de:0030-drops-268536},
doi = {10.4230/LIPIcs.LICS.2026.66},
annote = {Keywords: Homotopy type theory, Univalent foundations, constructive mathematics, synthetic homotopy theory, CW complexes, cellular homology, Hurewicz theorem}
}
Document
Existential Positive Transductions of Sparse Graphs
Abstract
Monadic stability generalizes many tameness notions from structural graph theory such as planarity, bounded degree, bounded tree-width, and nowhere density. The sparsification conjecture predicts that the (possibly dense) monadically stable graph classes are exactly those that can be logically encoded by first-order (FO) transductions in the (always sparse) nowhere dense classes. So far this conjecture has been verified for several special cases, such as for classes of bounded shrub-depth, and for the monadically stable fragments of bounded (linear) clique-width, twin-width, and merge-width.
In this work we propose the existential positive sparsification conjecture, predicting that the more restricted co-matching-free, monadically stable classes are exactly those that can be transduced from nowhere dense classes using only existential positive FO formulas. While the general conjecture remains open, we verify its truth for all known special cases of the original conjecture. Even stronger, we find the sparse preimages as subgraphs of the dense input graphs.
As a key ingredient, we introduce a new combinatorial operation, called subflip, that arises as the natural co-matching-free analog of the flip operation, which is a central tool in the characterization of monadic stability. Using subflips, we characterize the co-matching-free fragment of monadic stability by appropriate strengthenings of the known flip-flatness and flipper game characterizations for monadic stability.
In an attempt to generalize our results to the more expressive MSO logic, we discover (rediscover?) that on relational structures (existential) positive MSO has the same expressive power as (existential) positive FO.
Cite as
Nikolas Mählmann and Sebastian Siebertz. Existential Positive Transductions of Sparse Graphs. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 67:1-67:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{mahlmann_et_al:LIPIcs.LICS.2026.67,
author = {M\"{a}hlmann, Nikolas and Siebertz, Sebastian},
title = {{Existential Positive Transductions of Sparse Graphs}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {67:1--67:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.67},
URN = {urn:nbn:de:0030-drops-268544},
doi = {10.4230/LIPIcs.LICS.2026.67},
annote = {Keywords: Transductions, Existential Positive Logic, Structural Graph Theory, Monadic Stability, Monadic Dependence}
}
Document
Mixing Any Cocktail with Limited Ingredients: On the Structure of Payoff Sets in Multi-Objective POMDPs and Its Impact on Randomised Strategies
Abstract
We consider multi-dimensional payoff functions in partially observable Markov decision processes. We study the structure of the set of expected payoff vectors of all strategies (policies) and study what kind are needed to achieve a given expected payoff vector. In general, pure strategies (i.e., not resorting to randomisation) do not suffice for this problem.
We prove that for any payoff function for which the expectation is well-defined under all strategies, it is sufficient to mix (i.e., randomly select a pure strategy at the start of a play and committing to it for the rest of the play) finitely many pure strategies to approximate any expected payoff vector up to any precision. Furthermore, for any payoff function for which the expected payoff is finite under all strategies, any expected payoff vector can be obtained exactly by mixing finitely many strategies. These results are already novel in the context of (perfect information) Markov decision processes.
Cite as
James C. A. Main and Mickael Randour. Mixing Any Cocktail with Limited Ingredients: On the Structure of Payoff Sets in Multi-Objective POMDPs and Its Impact on Randomised Strategies. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 68:1-68:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{main_et_al:LIPIcs.LICS.2026.68,
author = {Main, James C. A. and Randour, Mickael},
title = {{Mixing Any Cocktail with Limited Ingredients: On the Structure of Payoff Sets in Multi-Objective POMDPs and Its Impact on Randomised Strategies}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {68:1--68:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.68},
URN = {urn:nbn:de:0030-drops-268559},
doi = {10.4230/LIPIcs.LICS.2026.68},
annote = {Keywords: partially observable Markov decision process, multiple objectives, randomised strategies, mixed strategies, strategy complexity}
}
Document
The Complexity of Downward Closures of Indexed Languages
Abstract
Indexed languages are a classical notion in formal language theory, which has attracted attention in recent decades due to its role in higher-order model checking: They are precisely the languages accepted by order-2 pushdown automata.
The downward closure of an indexed language - the set of all (scattered) subwords of its members - is well-known to be a regular over-approximation. It is known since 2015 that the downward closure of a given indexed language is effectively computable. However, the algorithm comes with no complexity bounds, and it has remained open whether a primitive-recursive construction exists.
We settle this question and provide a triply (resp. quadruply) exponential construction of a non-deterministic (resp. deterministic) automaton. We also prove (asymptotically) matching lower bounds. For the upper bounds, we rely on recent advances in semigroup theory, which let us compute bounded-size summaries of words with respect to a finite semigroup. By replacing stacks with their summaries, we are able to transform an indexed grammar into a context-free one with the same downward closure, and then apply existing bounds for context-free grammars.
Cite as
Richard Mandel, Corto Mascle, and Georg Zetzsche. The Complexity of Downward Closures of Indexed Languages. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 69:1-69:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{mandel_et_al:LIPIcs.LICS.2026.69,
author = {Mandel, Richard and Mascle, Corto and Zetzsche, Georg},
title = {{The Complexity of Downward Closures of Indexed Languages}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {69:1--69:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.69},
URN = {urn:nbn:de:0030-drops-268562},
doi = {10.4230/LIPIcs.LICS.2026.69},
annote = {Keywords: Higher-order pushdown automata, well quasi-orders, semigroup algebra}
}
Document
Differential Tree Automata
Abstract
In this paper we introduce the notion of a differential tree automaton. Differential tree automata generalise weighted tree automata (over a field) by allowing the transition weights to be rational functions of the tree size. Whereas the class of generating functions of weighted tree automata coincides with the class of algebraic power series, our main result is that the class of generating functions of differential tree automata coincides with the class of differentially algebraic power series. As a corollary, we obtain a decision procedure for determining equivalence of differential tree automata. In the course of proving our main result we identify a class of recurrences that characterises the sequence of coefficients of a differentially algebraic power series, generalising Reutenauer’s matrix representation of polynomially recursive sequences. We further identify a natural syntactic subset of differential tree automata whose generating functions are given by rational dynamical systems, that is, as components of the solution of a system of differential equations y' = F(y), where F is a vector of rational functions that is defined at y(0). We further show that this class of power series can be characterised in terms of the classical notion of weighted tree automata by using a labelled generating function on trees.
Cite as
Rida Ait El Manssour, Vincent Cheval, Mahsa Shirmohammadi, and James Worrell. Differential Tree Automata. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 70:1-70:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{aitelmanssour_et_al:LIPIcs.LICS.2026.70,
author = {Ait El Manssour, Rida and Cheval, Vincent and Shirmohammadi, Mahsa and Worrell, James},
title = {{Differential Tree Automata}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {70:1--70:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.70},
URN = {urn:nbn:de:0030-drops-268570},
doi = {10.4230/LIPIcs.LICS.2026.70},
annote = {Keywords: Combinatorial species, Differentially algebraic series, Weighted automata}
}
Document
Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
Abstract
Most implementations of sampling algorithms for continuous distributions use floating-point numbers, which introduce round-off errors and approximations. These errors can be difficult to analyze, and can cause security issues when used in algorithms for differential privacy. An alternative is to use exact sampling algorithms based on computable reals, which can lazily generate the digits of a continuous sample to arbitrary precision. However, these algorithms are intricate, and implementing and using them involves a combination of semantically challenging language features, such as probabilistic choice, higher-order functions, and dynamically-allocated mutable state.
In this paper we present Continuous-Eris, a higher-order separation logic for verifying the correctness of exact sampling algorithms for computable distributions. To demonstrate Continuous-Eris, we verify the correctness of computable samplers for the uniform, Gaussian, and Laplace distributions, as well as a library for exact real arithmetic for working with generated samples. All of the results in this paper have been verified in the Rocq proof assistant.
Cite as
Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, and Joseph Tassarotti. Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 71:1-71:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{demedeiros_et_al:LIPIcs.LICS.2026.71,
author = {de Medeiros, Markus and Liu, Puming and Li, Kwing Hei and Aguirre, Alejandro and Birkedal, Lars and Tassarotti, Joseph},
title = {{Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {71:1--71:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.71},
URN = {urn:nbn:de:0030-drops-268584},
doi = {10.4230/LIPIcs.LICS.2026.71},
annote = {Keywords: Probabilistic Programming, Separation Logic, Formal Verification}
}
Document
Local Combinatorial Analogues for Bounded VC Dimension
Abstract
Stable graphs, or equivalently Littlestone classes, were characterized by existence of linear-sized "good" sets, a kind of strongly homogeneous set, in work of Malliaris-Shelah and Malliaris-Moran. We prove a parallel result for VC classes, showing these are characterized by existence of linear-sized symmetric or asymmetric good pairs (which we define). We give several proofs, each drawing from methods and results from different areas, and resulting in different kinds of bounds. We finish with a few words on our learning theory motivation for these investigations and state some further research directions.
Cite as
Olga Medrano Martín del Campo. Local Combinatorial Analogues for Bounded VC Dimension. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 72:1-72:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{medranomartindelcampo:LIPIcs.LICS.2026.72,
author = {Medrano Mart{\'\i}n del Campo, Olga},
title = {{Local Combinatorial Analogues for Bounded VC Dimension}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {72:1--72:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.72},
URN = {urn:nbn:de:0030-drops-268591},
doi = {10.4230/LIPIcs.LICS.2026.72},
annote = {Keywords: Littlestone, Vapnik-Chervonenkis, good sets, Regularity Lemma, Haussler Packing Lemma, Fundamental Theorem of Statistical Learning}
}
Document
A Cartesian Closed Fibration of Higher-Order Regular Languages
Abstract
We explain how to construct in two different ways a cartesian closed fibration of higher-order regular languages in the sense of Salvati. In the first construction, we use fibrational techniques to derive the cartesian closed fibration from the various categories of regular languages of λ-terms associated to finite sets of ground states. In the second construction, we take advantage of the recent notion of profinite λ-calculus to define the cartesian closed fibration by a change-of-base from the fibration of clopen subsets over the category of Stone spaces, using an elegant idea coming from Hermida. We illustrate the expressive power of the cartesian closed fibration by generalizing the notion of Brzozowski derivative to higher-order regular languages, using an Isbell-like adjunction in the sense of Melliès and Zeilberger.
Cite as
Paul-André Melliès and Vincent Moreau. A Cartesian Closed Fibration of Higher-Order Regular Languages. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 73:1-73:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{mellies_et_al:LIPIcs.LICS.2026.73,
author = {Melli\`{e}s, Paul-Andr\'{e} and Moreau, Vincent},
title = {{A Cartesian Closed Fibration of Higher-Order Regular Languages}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {73:1--73:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.73},
URN = {urn:nbn:de:0030-drops-268604},
doi = {10.4230/LIPIcs.LICS.2026.73},
annote = {Keywords: automata theory, categorical models and logics, logics of programs, programming language semantics}
}
Document
From Co-Coverages to Radicals in Complete Lattices
Abstract
Completeness and representation theorems in abstract algebra, lattice theory, and theoretical computer science are tied to the existence of ideal objects, and thus to transfinite methods such as Zorn’s lemma. Yet many concrete uses of those theorems appeal to finite approximations only, which carry a clear computational meaning. In this paper, we introduce co-coverages on complete lattices as a uniform way to specify ideal elements, and associate to each co-coverage a canonical closure operator with a folding property reminiscent of the covering principles at work in constructive algebra. This yields finitary, choice-free alternatives for arguments in which ideal objects are employed to reduce a computational problem to subcases. In a classical setting, our closure operators admit bases which allow to recover a host of primality principles such as the universal Krull–Lindenbaum theorem and Henkin’s lemma.
Cite as
Daniel Misselbeck-Wessel. From Co-Coverages to Radicals in Complete Lattices. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 74:1-74:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{misselbeckwessel:LIPIcs.LICS.2026.74,
author = {Misselbeck-Wessel, Daniel},
title = {{From Co-Coverages to Radicals in Complete Lattices}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {74:1--74:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.74},
URN = {urn:nbn:de:0030-drops-268619},
doi = {10.4230/LIPIcs.LICS.2026.74},
annote = {Keywords: Closure operator, prime element, spectrum, completeness theorem, point-free topology, transfinite method, dynamical algebra}
}
Document
Distinguishing Graphs by Counting Homomorphisms from Sparse Graphs
Abstract
Lovász (1967) showed that two graphs G and H are isomorphic if, and only if, they are homomorphism indistinguishable over all graphs, i.e., G and H admit the same number of number of homomorphisms from every graph F. Subsequently, a substantial line of work studied homomorphism indistinguishability over restricted graph classes. For example, homomorphism indistinguishability over minor-closed graph classes ℱ such as the class of planar graphs, the class of graphs of treewidth ≤ k, pathwidth ≤ k, or treedepth ≤ k, was shown to be equivalent to quantum isomorphism and equivalences with respect to counting logic fragments, respectively.
Via such characterisations, the distinguishing power of e.g. logical or quantum graph isomorphism relaxations can be studied with graph-theoretic means. In this vein, Roberson (2022) conjectured that homomorphism indistinguishability over every graph class excluding some minor is not the same as isomorphism. We prove this conjecture for all vortex-free graph classes. In particular, homomorphism indistinguishability over graphs of bounded Euler genus is not the same as isomorphism. As a negative result, we show that Roberson’s conjecture fails when generalised to graph classes excluding a topological minor.
Furthermore, we show homomorphism distinguishing closedness for several graph classes including all topological-minor-closed and union-closed classes of forests, and show that homomorphism indistinguishability over graphs of genus ≤ g (and other parameters) forms a strict hierarchy.
Cite as
Daniel Neuen and Tim Seppelt. Distinguishing Graphs by Counting Homomorphisms from Sparse Graphs. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 75:1-75:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{neuen_et_al:LIPIcs.LICS.2026.75,
author = {Neuen, Daniel and Seppelt, Tim},
title = {{Distinguishing Graphs by Counting Homomorphisms from Sparse Graphs}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {75:1--75:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.75},
URN = {urn:nbn:de:0030-drops-268628},
doi = {10.4230/LIPIcs.LICS.2026.75},
annote = {Keywords: homomorphism indistinguishability, graph homomorphism, vortex-free Hadwiger number, topological minor, connector}
}
Document
Fixed-Parameter Tractable Inference for Discrete Probabilistic Programs, via String Diagram Algebraisation
Abstract
Discrete probabilistic programs (DPPs) provide a highly expressive formalism for compactly defining arbitrary finite probabilistic models. This expressivity comes at a price: DPP inference is PSPACE-hard. In this work, we show that DPP inference only takes polynomial time for programs that are "structurally simple". More precisely, inference can be performed in polynomial time when the primal graph of each function appearing in the probabilistic program has bounded treewidth, and the inverse acceptance probability is at most exponential in the size of the probabilistic program. Existing algorithms do not achieve this performance guarantee.
Our method relies on finding suitable decompositions, algebraisations, of the string diagrams underlying DPPs, employing existing algorithms for tree decompositions. This is independent of the probabilistic setting of DPPs and has direct applications to many problems, such as evaluating queries on relational databases and cybersecurity risk assessment via attack trees.
Cite as
Benedikt Peterseim and Milan Lopuhaä-Zwakenberg. Fixed-Parameter Tractable Inference for Discrete Probabilistic Programs, via String Diagram Algebraisation. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 76:1-76:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{peterseim_et_al:LIPIcs.LICS.2026.76,
author = {Peterseim, Benedikt and Lopuha\"{a}-Zwakenberg, Milan},
title = {{Fixed-Parameter Tractable Inference for Discrete Probabilistic Programs, via String Diagram Algebraisation}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {76:1--76:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.76},
URN = {urn:nbn:de:0030-drops-268637},
doi = {10.4230/LIPIcs.LICS.2026.76},
annote = {Keywords: probabilistic programming, string diagrams, treewidth, fixed-parameter tractability, probabilistic inference, parameterised complexity, hypergraph categories}
}
Document
Problems with Fixpoints of Polynomials of Polynomials
Abstract
Motivated by applications in computable analysis, we study fixpoints of certain endofunctors over categories of containers. More specifically, we focus on fibred endofunctors over the fibrewise opposite of the codomain fibration that can be themselves be represented by families of polynomial endofunctors. In this setting, we show how to compute initial algebras, terminal coalgebras and another kind of fixpoint ζ. We then explore a number of examples of derived operators inspired by Weihrauch complexity and the usual construction of the free polynomial monad.
We introduce ζ-expressions as the syntax of μ-bicomplete categories, extended with ζ-binders and parallel products, which thus have a natural denotation in containers. By interpreting certain ζ-expressions in a category of type-2 computable maps, we are able to capture a number of meaningful Weihrauch degrees, ranging from closed choice on {0,1} to determinacy of infinite parity games, via an "answerable part" operator.
Cite as
Cécilia Pradic and Ian Price. Problems with Fixpoints of Polynomials of Polynomials. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 77:1-77:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{pradic_et_al:LIPIcs.LICS.2026.77,
author = {Pradic, C\'{e}cilia and Price, Ian},
title = {{Problems with Fixpoints of Polynomials of Polynomials}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {77:1--77:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.77},
URN = {urn:nbn:de:0030-drops-268642},
doi = {10.4230/LIPIcs.LICS.2026.77},
annote = {Keywords: Polynomial functors, containers, fixpoints, Weihrauch complexity}
}
Document
Randomness Extraction Fails for Finite-State Dimension
Abstract
Finite-state dimension, introduced as a finite-state analogue of Hausdorff dimension, quantifies the lower asymptotic density of information in an infinite sequence as perceived by finite-state automata. It admits several equivalent formulations; two particularly useful are via finite-state gambling strategies and via the optimal asymptotic compression ratio achieved by information-lossless finite-state compressors.
Normal sequences represent the highest level of algorithmic randomness visible to finite automata, and are exactly those sequences having finite-state dimension equal to 1. This motivates a bounded-memory notion of randomness extraction: can a finite-state transducer, reading a single sequence streamingly, extract a normal output from a single input source? More modestly, can it always transform the input into an output of strictly higher finite-state dimension? Finite-state transducers can perform surprisingly effective one-pass transformations: even with constant memory they can implement variable-length coding schemes including Shannon-Fano coding, remove local redundancy, and increase the apparent randomness rate on many structured or stochastic inputs.
We show randomness extraction using transducers is impossible in a strong, explicit form. For every rational s ∈ (0,1), we construct a near linear-time computable binary sequence X with dim_FS(X) = s such that for every finite-state transducer T, the output satisfies dim_FS(T(X)) ≤ s. Thus, for these sequences, finite-state transduction cannot extract normality - indeed it cannot even improve finite-state dimension. Our proof proceeds by a structural analysis of finite-state transducers together with a dimension-preserving diagonal construction that, for each target s, builds a sequence whose organization defeats every such transducer’s attempt to concentrate randomness. The result is a finite-state analogue of Miller’s non-extractability phenomenon for effective dimension, but its proof relies on substantially different techniques, tailored to the finite-state setting.
Furthermore, we show that the impossibility persists even with multiple independent input streams. We treat two notions of independence: (i) Kolmogorov-complexity–based independence (via joint prefix complexity), and (ii) a finite-state notion of relative independence, formulated via relative finite-state dimension. By sharp contrast with the effective-dimension setting - where two independent sources suffice for a uniform effective procedure that boosts randomness rate arbitrarily close to 1 - we show that finite-state dimension exhibits no comparable multi-source extraction phenomenon. Specifically, for every rational s ∈ (0,1) and every fixed k ≥ 2, there exist k independent sources, each of finite-state dimension s, such that for every k-input finite-state transducer T, the output satisfies dim_FS(T(X_1,… ,X_k)) ≤ s. Thus, even independent streams do not allow bounded-memory transduction to output a normal sequence or to increase finite-state dimension.
Cite as
Subin Pulari and Akhil S. Randomness Extraction Fails for Finite-State Dimension. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 78:1-78:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{pulari_et_al:LIPIcs.LICS.2026.78,
author = {Pulari, Subin and S, Akhil},
title = {{Randomness Extraction Fails for Finite-State Dimension}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {78:1--78:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.78},
URN = {urn:nbn:de:0030-drops-268656},
doi = {10.4230/LIPIcs.LICS.2026.78},
annote = {Keywords: Finite-state dimension, normal numbers, randomness extraction, finite-state transducers}
}
Document
Wiring the π-Calculus to Denotational Semantics
Abstract
We introduce a dialect of the Asynchronous π-calculus, called AWπ, in which (1) an input name may be owned, at any time, by at most one process; (2) each name has either only the input or only the output capability. As a result, special processes called wires (aka forwarders, that is, processes that receive values at one name and re-transmit) behave as substitutions when composed with any AWπ process. Thus AWπ naturally yields a category, whose morphisms are AWπ processes (modulo the reference behavioural equivalence, barbed congruence) and whose objects are types; and where wires act as identity morphisms. We show that the category of processes can be further organised into (sub)categories with the structures needed for the interpretation of common higher-order language features in the literature by drawing on insights from game semantics; notably, we construct a relative Seely category, the categorical structure that concurrent game semantics has. At the same time, AWπ follows the tradition of ordinary π-calculi in that expressiveness is preserved and the operational and algebraic theory are developed in a similar manner, notwithstanding substantial technical differences in their development and proofs. In short, the goal of AWπ is to remain faithful to the operational and algebraic tradition of the π-calculi while connecting to the tradition of denotational models for programming languages.
Cite as
Ken Sakayori, Davide Sangiorgi, Simon Castellan, and Pierre Clairambault. Wiring the π-Calculus to Denotational Semantics. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 79:1-79:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{sakayori_et_al:LIPIcs.LICS.2026.79,
author = {Sakayori, Ken and Sangiorgi, Davide and Castellan, Simon and Clairambault, Pierre},
title = {{Wiring the \pi-Calculus to Denotational Semantics}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {79:1--79:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.79},
URN = {urn:nbn:de:0030-drops-268669},
doi = {10.4230/LIPIcs.LICS.2026.79},
annote = {Keywords: \pi-calculus, denotational semantics, game semantics, wire process}
}
Document
Model Checking for Low Monodimensionality Fragments of CMSO on Topological-Minor-Free Graph Classes
Abstract
Algorithmic meta-theorems explain the tractability of large classes of computational problems by linking logical expressibility with structural graph properties. While extensions of first-order logic such as FO+dp admit efficient model checking on graph classes excluding a fixed topological minor, comparable results for richer fragments of CMSO were previously unknown. We further develop the framework of Sau, Stamoulis, and Thilikos [SODA 2025] for fragmenting CMSO via annotated graph parameters, which restrict set quantification to vertex sets satisfying bounded structural conditions. Following this approach, we identify a fragment of CMSO, namely the one defined by allowing quantification only over sets having what we call low monodimensionality, that generalizes several previously-known logics and we show that model checking for this fragment, enhanced with the disjoint-paths predicate, is fixed-parameter tractable on topological-minor-free graph classes. Such classes essentially delimit the tractability for this logic on subgraph-closed classes. As a consequence, our results lift several known algorithmic meta-theorems beyond first-order logic to the topological-minor-free setting.
Cite as
Ignasi Sau, Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, Dimitrios M. Thilikos, and Alexandre Vigny. Model Checking for Low Monodimensionality Fragments of CMSO on Topological-Minor-Free Graph Classes. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 80:1-80:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{sau_et_al:LIPIcs.LICS.2026.80,
author = {Sau, Ignasi and Schirrmacher, Nicole and Siebertz, Sebastian and Stamoulis, Giannos and Thilikos, Dimitrios M. and Vigny, Alexandre},
title = {{Model Checking for Low Monodimensionality Fragments of CMSO on Topological-Minor-Free Graph Classes}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {80:1--80:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.80},
URN = {urn:nbn:de:0030-drops-268676},
doi = {10.4230/LIPIcs.LICS.2026.80},
annote = {Keywords: Monadic second-order logic, Dynamic programming, Graph minors, Monodimentionality, Annotated parameters}
}
Document
Axiomatizability of Alexandrov Dynamic Topological Logic
Abstract
Dynamical systems provide rigorous models of movement or evolution over time. Due to their abstract nature, they may be naturally employed for representing e.g. physical, biological, or financial phenomena. Specifically in the context of Computer Science, computational processes, machine learning algorithms, and multi-agent systems may be regarded as dynamical systems. This has sparked interest in designing formal specification languages for dynamical systems which could potentially be employed for automated or computer-assisted deduction, leading to the introduction of dynamic topological logic (DTL). When space is continuous but time is discrete, it is known that a sound and complete deductive calculus for DTL exists. However, discrete spaces are not uncommon in CS applications , and in this setting, whether such a calculus exists even in principle has been an open question for more than two decades. More precisely, it was unknown whether the DTL of Alexandrov spaces is computably enumerable. In this paper, we use model search techniques to provide an affirmative answer.
Cite as
Niels C. Vooijs and David Fernández-Duque. Axiomatizability of Alexandrov Dynamic Topological Logic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 81:1-81:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{vooijs_et_al:LIPIcs.LICS.2026.81,
author = {Vooijs, Niels C. and Fern\'{a}ndez-Duque, David},
title = {{Axiomatizability of Alexandrov Dynamic Topological Logic}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {81:1--81:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.81},
URN = {urn:nbn:de:0030-drops-268689},
doi = {10.4230/LIPIcs.LICS.2026.81},
annote = {Keywords: dynamic topological logic, Alexandrov spaces, computable enumerability, modal logic, temporal logic}
}
Document
The Finite Length Property of the Rado Graph and Friends
Abstract
An infinite structure has the finite length property (over a given field) if, for each of its finite powers, chains of equivariant subspaces in the corresponding free vector space are bounded in length. Prior work showed that the countable pure set and the countable dense linear order without endpoints have this property. We generalise these results to (a) any structure approximated by finite substructures with few orbits, provided the field is of characteristic zero, and (b) any Fraïssé limit with free amalgamation in a finite vocabulary consisting of unary and binary relations, possibly expanded with a generic total order. As a special case, we deduce the finite length property of the Rado graph using both methods. We also describe some connections with function spaces, weighted register automata, and orbit-finite systems of linear equations.
Cite as
Jingjie Yang, Mikołaj Bojańczyk, and Bartek Klin. The Finite Length Property of the Rado Graph and Friends. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 82:1-82:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{yang_et_al:LIPIcs.LICS.2026.82,
author = {Yang, Jingjie and Boja\'{n}czyk, Miko{\l}aj and Klin, Bartek},
title = {{The Finite Length Property of the Rado Graph and Friends}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {82:1--82:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.82},
URN = {urn:nbn:de:0030-drops-268695},
doi = {10.4230/LIPIcs.LICS.2026.82},
annote = {Keywords: Rado graph, oligomorphic structure, orbit-finite set, orbit-finitely spanned vector space, equivariant subspace, finite length}
}
Document
Contextual MetaML: Syntax and Full Abstraction
Abstract
MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Contextual MetaML, the first metaprogramming language that supports storing and running open code under a strong type safety guarantee. The type system utilises contextual modal types to track and reason about free variables in code explicitly.
A crucial concern in metaprogramming-based program optimisations is whether the optimised program preserves the meaning of the original program. Addressing this question requires a notion of program equivalence and techniques to reason about it. In this paper, we provide a semantic model that captures contextual equivalence for Contextual MetaML, establishing the first full abstraction result for an imperative MetaML-style language. Our model is based on traces derived via operational game semantics, where the meaning of a program is modelled by its possible interactions with the environment. We also establish a novel closed instances of use theorem that accounts for both call-by-value and call-by-name closing substitutions.
Cite as
Haoxuan Yin, Andrzej S. Murawski, and C.-H. Luke Ong. Contextual MetaML: Syntax and Full Abstraction. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 83:1-83:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{yin_et_al:LIPIcs.LICS.2026.83,
author = {Yin, Haoxuan and Murawski, Andrzej S. and Ong, C.-H. Luke},
title = {{Contextual MetaML: Syntax and Full Abstraction}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {83:1--83:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.83},
URN = {urn:nbn:de:0030-drops-268708},
doi = {10.4230/LIPIcs.LICS.2026.83},
annote = {Keywords: Metaprogramming, operational game semantics, trace model, contextual modal type theory}
}
Document
Forgetting Event Order in Higher-Dimensional Automata
Abstract
Higher-dimensional automata (HDAs) provide a geometric model of true concurrency, yet their standard formulation encodes an artificial total order on events. This representational artifact causes a fundamental mismatch between the combinatorial structure of HDAs and their observable behaviour, leading to logical asymmetries and complicating the application of categorical tools. In this paper, we resolve this tension by developing a semantics for HDAs that is independent of event order, based on interval ipomsets (partially ordered multisets with interfaces) that preserve only precedence and concurrency. We prove that for any HDA, the traditional ST–trace of an execution path corresponds precisely to its associated interval ipomset. On the structural side, we show that the presheaf-theoretic presentation with an unordered base and the combinatorial presentation of symmetric HDAs are categorically isomorphic. Finally, by characterizing ST- and hereditary history-preserving (hhp) bisimulation via ipomset isomorphism, we provide a unified, order-free foundation for HDA semantics. Our results resolve several ambiguities in the literature: they provide the necessary path-category structure to canonically apply the Open Maps framework, eliminate representational artifacts in temporal and modal logics, and bridge systematic mismatches between HDAs and other models of concurrency such as Petri nets.
Cite as
Safa Zouari. Forgetting Event Order in Higher-Dimensional Automata. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 84:1-84:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{zouari:LIPIcs.LICS.2026.84,
author = {Zouari, Safa},
title = {{Forgetting Event Order in Higher-Dimensional Automata}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {84:1--84:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.84},
URN = {urn:nbn:de:0030-drops-268711},
doi = {10.4230/LIPIcs.LICS.2026.84},
annote = {Keywords: higher-dimensional automata, true concurrency, pomsets with interfaces, interval pomsets, pomsets, presheaf semantics, bisimulation, event order, ST-trace}
}