LICS 2025 Accepted Papers
The Identity Problem in virtually solvable matrix groups over algebraic numbers
Homological Invariants of Higher-Order Equational Theories
Completing Gordon’s Higher-Order Logic
The internal languages of univalent categories
Approximate Evaluation of Quantitative Second Order Queries
The Yoneda embedding in simplicial type theory
Convergence laws for extensions of first order logic with averaging
Separation and Definability in Fragments of Two-Variable First-Order Logic with Counting
Hofmann–Streicher Lifting of Fibred Categories
3D-grids are not transducible from planar graphs
When is the partial map classifier a Sierpiński cone?
Ordinal Exponentiation in Homotopy Type Theory
Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests
Pushdown Model Checking above the Cubic Bottleneck
#P is Sandwiched by One and Two #2DNF Calls: Is Subtraction Stronger Than We Thought?
The Qualitative Collapse of Concurrent Games
Logical relations for call-by-push-value models, via internal fibrations in a 2-category
Compositional Taylor expansion in cartesian differential categories
Alternating Nominal Automata with Name Allocation
Transductions of Graph Classes Admitting Product Structure
Flipping and Forking
Minimal History-Deterministic Co-Büchi Automata: Congruences and Passive Learning
Syntactic Effectful Realizability in Higher-Order Logic
Binary symmetries of tractable non-rigid structures
Reachability Types, Traces and Full Abstraction
A Complexity Dichotomy for Semilinear Target Sets in Automata with One Counter
Recognisability Equals Definability for Finitely Representable Matroids of Bounded Path-Width
Semantical Analysis of Intuitionistic Modal Logics between CK and IK
Proof Compression via Subatomic Logic and Guarded Substitutions
Quantifier Elimination for Regular Integer Linear-Exponential Programming
Effectful Mealy Machines: Bisimulation and Trace
Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs
Initial Algebra Correspondence under Reachability Conditions
Multiple Reachability in Linear Dynamical Systems
Regular Grammars for Sets of Graphs of Tree-Width 2
Risk-aware Markov Decision Processes Using Cumulative Prospect Theory
Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution
Learning Weighted Automata over Number Rings, Concretely and Categorically
Graphs of unbounded linear cliquewidth must transduce all trees
Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity
The sorrows of a smooth digraph: the first hardness criterion for infinite directed graph-colouring problems
Naturality for higher-dimensional path types
The commutativity problem for effective varieties of formal series, and applications
Characterization and Decidability of FC-Definable Regular Languages
Learning Deterministic One-Counter Automata in Polynomial Time
If At First You Don’t Succeed: Extended Monitorability through Multiple Executions
Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games
Conformance Games for Graded Semantics
Functional Stream Semantics for a Synchronous Block-Diagram Compiler
Random Variables, Conditional Independence and Categories of Abstract Sample Spaces
Navigational hierarchies of regular languages
Operator Spaces, Linear Logic and the Heisenberg-Schrödinger Duality of Quantum Theory
Probabilistic Strategies: Definability and the Tensor Completeness Problem
The Steenrod squares via unordered joins
Group Order Logic
Complete Quantum Relational Hoare Logics from Optimal Transport Duality
Multiplicative Rewards in Markovian Models
Algebraic and algorithmic synergies between promise and infinite-domain CSPs
The Blurred Drinker Paradox: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem
Relators and Notions of Simulation Revisited
On the denotation of circular and non-wellfounded proofs in linear logic with fixed points
Closure and Complexity of Temporal Causality
Classical simulation of quantum CSP strategies
Behavioural Conformances based on Lax Couplings
Interpolation for the two-way modal µ-calculus
Thin Coalgebraic Behaviours Are Inductive
LICS Sponsorship
The symposium is sponsored by ACM SIGLOG and the IEEE Technical Committee on Mathematical Foundations of Computing.
Website by Sam Staton based on a bootstrap design by Hartmut Eilers and Eric Koskinen.