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 $\omega$-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 for time-homogeneous Markov chains. 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 arbitrary $\epsilon$-approximation in the quantitative case. We apply our new methodology to recent results on sound and complete supermartingale certificates for almost-sure termination on 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 $\omega$-regular properties and the first sound and $\epsilon$-complete supermartingale certificates for quantitative $\omega$-regular properties on time-homogeneous Markov chains with countably infinite state spaces.

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.

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 significantly simplifies the previous decidability argument and provides a tighter analysis, thus serving as a critical step towards a tight complexity bound.

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.

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 codimension 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 rationals, we moreover obtain a complexity bound NP^RP in this case. 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.

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^3-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. For single-variable theories, we obtain positive results for the following families of predicates: (i) for perfect powers, decidability of the corresponding theory follows from the solvability of hyperelliptic Diophantine equations; (ii) for polynomials of degree at most three, we establish decidability by relying on the low genus of the resulting algebraic curves; (iii) for arbitrary polynomials, conditional decidability is entailed by an effective version of Faltings's theorem, which itself was recently proved subject to certain classical number-theoretic conjectures. In turn, we present various hardness results for theories with unresolved decidability status by using them to encode certain longstanding open Diophantine problems.

We propose a simple space-cost measure for the lambda-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, we show that the weak lambda-calculus and Turing machines can simulate each other with a constant-factor space overhead, for any computation of logarithmic or higher space complexity. This implies that the weak lambda-calculus equipped with our cost model gives a proper characterization of the classical space complexity classes, including LOGSPACE and PSPACE.

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. It is known that coverability for NCS is $\mathbf{F}_{\epsilon_0}$-complete, where $\mathbf{F}_{\epsilon_0}$ 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 $\mathbf{F}_{\Omega_k}$-complete where $\Omega_k$ is the tower of height $k$ of the $\omega$ ordinal. This gives the first natural complete problems for all of these classes. As an application of our results, we improve existing upper bounds for various problems from XML processing, graph transformation systems, $\pi$-calculus, logic and parameterized verification. Furthermore, using NRCS, we also prove $\mathbf{F}_{\Omega_k}$-completeness of the considered problems from parameterized verification and logic.

Substructural logics selectively omit structural rules from classical or intuitionistic proof calculi, providing a framework to formalize resource-sensitive reasoning. For logics with contraction or weakening admitting cut-free sequent calculi, proof search had been analyzed in the literature using well-quasi-orders on N^d (Dickson’s lemma), yielding Ackermannian 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. From the perspective of the fast-growing hierarchy, this induced a jump from Ackermannian to hyper-Ackermannian complexity. This suggested that cut-free hypersequent calculi for extensions of the commutative Full Lambek calculus with contraction or weakening (FLec/FLew) inherently entail hyper-Ackermannian upper bounds. We show that this intuition does not hold: every extension of FLec and FLew admitting a cut-free hypersequent calculus has an Ackermannian upper bound on provability. The key technical insight is avoiding the powerset. For this, we exploit novel dependencies between individual sequents within any hypersequent in backward proof search. The weakening case also introduces a Karp-Miller style acceleration. Our Ackermannian upper bound is optimal (realized by the logic FLec), and it improves the upper bound for the fundamental fuzzy logic MTL.

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.

The logic MMSNP is a well-studied fragment of Existential Second- Order logic that, from a computational perspective, captures ex- actly 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 aris- ing 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 certain technical conditions. 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 ’21).

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.

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 theorem and infinite-dimensional duality theorems for infinite-dimensional quantum states, which we use to establish completeness.

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 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 1953, 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, HoTT had only had been used to compute low-dimensional homotopy groups of spheres. 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 flavor 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.

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. 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, which is used in software verification. We moreover improve upon 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 of suitably seeded fixed point iterations: 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 finite complete axiomatization of sequence models given by finitary axioms.

We consider a variant of VASS extended with integer counters, denoted VASS+Z. These are automata equipped with N and Z counters; the N-counters are required to remain nonnegative and the Z-counters do not have this restriction. We study the complexity of the reachability problem for VASS+Z when the number of N-counters is fixed. We show that reachability is NP-complete in 1-VASS+Z (i.e. when there is only one N-counter) regardless of unary or binary encoding. For d ≥ 2, using a KLMST-based algorithm, we prove that reachability in d-VASS+Z lies in the complexity class F_{d+2}​. Our upper bound improves on the naively obtained Ackermannian complexity by simulating the Z-counters with N-counters. To complement our upper bounds, we show that extending VASS with integer counters significantly lowers the number of N-counters needed to exhibit hardness. We prove that reachability in unary 2-VASS+Z is PSPACE-hard; without Z-counters this lower bound is only known in dimension 5. We also prove that reachability in unary 3-VASS+Z is TOWER-hard. Without Z-counters, reachability in 3-VASS has elementary complexity and TOWER-hardness is only known in dimension 8.

Extensional ESO is a fragment of existential second-order logic (ESO) that captures the following family of problems. Given a fixed ESO sentence $\Psi$ and an input structure $\mathbb A$ the task is to decide whether there is an \emph{extension} $\mathbb B$ of $\mathbb A$ that satisfies the first-order part of $\Psi$, i.e., a structure ${\mathbb B}$ such that $R^{\mathbb A}\subseteq R^{\mathbb B}$ for every existentially quantified predicate $R$ of $\Psi$, and $R^{\mathbb A} = R^{\mathbb B}$ for every non-quantified predicate $R$ of $\Psi$. 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, \emph{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 \emph{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).

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^{\leq \omega}$, i.e. by allowing quantification over sets of infinite branches. A longstanding open problem is whether the decidability can be recovered in $2^{\leq \omega}$ 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.

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.

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.

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.

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. For a language with arbitrary algebraic effects and data types, we derive conditions under which lazy evaluation computes the same result as the eager semantics. The semantic model suggests better intermediate representations of sum and product types in a lazy interpreter, along with equations that justify further optimizations. To illustrate we sketch an implementation in OCaml. Our motivation is practical: the origin of this work is a real-world application of 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.

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 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 Goedel-Loeb logic GL we obtain the following dichotomy: tabular logics have "propositionally sized" interpolants while for non-tabular logics an unconditional exponential lower bound holds.

Cubical type theories are designed around an abstract unit interval from which types of paths are defined; varying the operations available on this interval yields different type theories. A reversal is an involutive unary 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 observation is that the product of an interval and its dual is again an interval with a reversal given by swapping coordinates. Our conservativity result applies to "idealized" cubical type theories without equations for evaluating the filling operator at concrete type formers. Using the same basic observation, however, we also construct models of full cubical type theories with reversals in categories of cubical sets without reversals. In so doing, we give the first models of these theories whose homotopy theory corresponds to that of topological spaces.

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.

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 \emph{$P$-product} of series is defined coinductively by a \emph{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 \emph{$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 known results from the literature on the Hadamard, shuffle, and infiltration automata. We have formalised most results in the proof assistant Agda.

We study the uniformisation problem for monadic second-order logic (MSO) over countable ordinal chains, ie, given a formula that refines a relation between subsets of the input model, we are interested in the existence of a formula that defines a function that selects for all sets in the domain of the relation a unique set such that the pair of the two is in the relation. It is known that uniformisation of MSO is not possible over the class of countable ordinals. We show in this work that the maximal uniformisation degree is reached if we add to the logic a new predicate that selects in each set, if possible, a cofinal subset of a of order-type $\omega$. Said differently, all formulas of MSO can be uniformised over the class of countable ordinal chains by using a formula of this extended logic.

There have recently been several developments in synthetic mathematics, using extensions of dependent type theory with univalence: simplicial homotopy type theory, synthetic algebraic geometry and synthetic Stone duality. The goal of this paper is to provide a foundation of constructive higher sheaf models of type theory in a constructive meta theory, and in particular, to build constructive models of these formal systems. The main technical tools are the use of internal language for simplifying proofs of intermediate lemmas and the notion of descent data operations, which already played an important role in models of directed univalence. Even classically, we think this work can be interesting, since these models are developed in a proof theoretically weak meta theory (in particular it is predicative).

The Metropolis--Hastings (MH) algorithm is a foundational Markov chain Monte Carlo algorithm. In this paper, we ask whether it is possible to formulate and analyse MH with existing tools from categorical probability theory, using a recent involutive framework proposed for MH-type algorithms as a concrete case study. We first show how basic concepts such as invariance and reversibility can be formulated in Markov categories, and how aspects of the involutive framework can be captured using CD categories. We then study enrichments of CD categories over commutative monoids. These provide a rich setting for reasoning synthetically about a range of important probabilistic concepts, including substochastic kernels, finite and $\sigma$-finite measures, absolute continuity, singular measures, and Lebesgue decompositions. This structure allows us to give very general necessary and sufficient conditions for an MH-type sampler to be reversible with respect to a given target distribution.

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 construction is manifest, but making this connection formal requires technical developments 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 characterization of the total elements of the probabilistic coherence space $!\Bool$.

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.

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.

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 satisfiablity 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 any real Hilbert spaces of dimension greater than 2 and complex Hilbert spaces of dimension greater than 3, we demonstrate that the satisfiablity 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.

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 ordinals to specify the level of decidability of a property. In this framework, we express the property that a proposition is α-decidable, for a Brouwer 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.

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. This paper describes Continuous-Eris, a higher-order separation logic for verifying the correctness of exact sampling algorithms for computable distributions. To demonstrate Continuous-Eris, we have verified 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.

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 intricate 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 these complex constructions and obtain a more 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 route from LTL to DPA and avoids the aforementioned intricate constructions. It relies on standard operations on weak alternating automata, Miyano-Hayashi's 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.

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, and prove decidability of the model-checking problem, which determines whether a given symbolic structure satisfies a given first-order formula, for decidable base theories. This enables proving decidability for fragments of first-order logic by establishing a symbolic model property, which states that every satisfiable formula has a symbolic model. We use this approach 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.

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, and 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 term constructed in the definitional variant of the theory can be soundly embedded into the propositional variant, 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.

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 $\omega$-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 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.

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 $P^{NP[O(log^2 n)]}$-complete in combined complexity. Our result implies $P^{NP[O(log^2 n)]}$-completeness for both UNTC and UNFO^{reg}, which were left open in previous works.

We study the Guarded Fragment of first-order logic over models that interpret a family of distinguished binary predicates $E_1,E_2,\dots$ as nested equivalence relations, that is, such that $E_{k+1}$ is coarser than $E_k$ for all $k \geq 1$. We show that the equality-free Guarded Fragment with nested equivalence relations retains the finite model property and that its satisfiability problem is decidable, albeit of non-elementary complexity. When the number of distinguished predicates is fixed to~$K$, the complexity becomes $(K{+}2)$-\ExpTime{}-complete. In contrast, we show that decidability is lost as soon as the nesting condition is dropped or equality is admitted.

We present a unified, categorical theory of monads and distributive laws \emph{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 \emph{verbal categories} $\W$, in a uniform and presentation-independent manner. We define the notion of \emph{$\W$-operadic monad} (those ``defined'' in the context $\W$) and that of \emph{$\W$-commutative monad} (those ``preserved'' in the context $\W$). We present a canonical construction of a distributive law $ST\to TS$; 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. When the condition fails, we can \emph{refine} $S$ and force $\W$-operadicity; this generalizes Varacca and Winskel's construction of indexed valuations.

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 actually 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 DNF or CNF. In this work, we extend this an 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 are small-depth circuits for arithmetic operations in Chinese remainder representation, due to Beame, Cook, Hoover (1986).

We introduce \emph{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 rewriteability 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 \emph{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.

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. In particular, we focus on the question of which formal theories and proof systems can efficiently prove algebraic circuit lower bounds, as follows. - **Formalization of Rank Method** Typically, algebraic circuit lower bounds are shown using the ``rank method", i.e., by exploiting non-trivial upper bounds on the rank of matrices derived from the monomial coefficients of polynomials computable by small algebraic circuits. A recent prominent application of this method is in the constant-depth algebraic circuit lower bounds by Limaye, Srinivasan and Tavenas~\cite{LST25} for the determinant and iterated matrix multiplication over fields of characteristic zero, and the finite field analogue of these results by Forbes~\cite{For24}. We show that these rank-based arguments can be formalized in the bounded arithmetic theory VNC2, which captures ``reasoning with NC2 concepts''. This complements the work of Tzameret and Cook \cite{TC21}, who showed that basic structural \emph{upper} bounds in algebraic circuit complexity can be formalized in \VNCTwo. Moreover, it offers a unified proof-theoretic framework in which to formulate and study barriers for current algebraic complexity methods (complementing specific barriers discovered by Efremenko, Garg, Oliveira, and Wigderson~\cite{EGOW18} and Garg, Makam, Oliveira, and Wigderson~\cite{GMOW19}). - **Unconditional PCR lower bounds** 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. - **Conditional constant-depth IPS lower bounds** 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.

Semantic notions in programming language theory are commonly specified by syntax-based systems, and their metatheory --- including congruence of bisimilarity, determinacy of evaluation, confluence of reduction, and type safety --- is typically developed syntactically, relying heavily on termwise reasoning. This leads to representation-dependent results and to a systematic duplication of metatheoretic effort across different calculi and syntactic presentations. This paper proposes a pointfree, algebraic approach to the metatheory of syntax-based systems. Rather than reasoning about terms, inference mechanisms, or other syntactic notions --- or about their abstract structure --- we shift attention to the algebra of semantic predicates induced by syntax and treat such predicates as first-class objects. This algebra is defined abstractly, without reference to any underlying term structure. Term-based rules and manipulations are recast as algebraic operations, while metatheoretic properties are formulated algebraically --- typically as quasi-equations --- and established once and for all at the algebraic level, independently of any particular syntactic representation. As a first step towards a systematic algebraization of metatheory, we prove a collection of abstract metatheorems, including confluence of reduction, determinacy of evaluation, and congruence of applicative bisimilarity.

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.

Simplicial type theory (STT) was introduced by Riehl and Shulman to leverage homotopy type theory to prove results about $(\infty,1)$-categories. Initial work on simplicial type theory focused on "formal" arguments in higher category theory and, in particular, no non-trivial examples of $\infty$-category theory were constructible within STT. More recent work has changed this state of affairs by applying techniques developed initial for cubical type theory to construct the $\infty$-category of spaces. We complete this process by constructing the $\infty$-category of $\infty$-categories, recovering one of the main foundational results of $\infty$-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.

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.

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, 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.

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.

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.

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.

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\'{y}, and Vok\v{r}\'{i}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.

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 quadruple 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.

In this paper, we propose a unifying algebraic framework which allows us to connect circuit complexity classes to the properties of finite algebraic structures. 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. In particular, we characterize language classes recognized by circuits over simple algebras and over algebras from congruence modular varieties.

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 $\{\land, \lor, \neg, \mimp\}$-fragment of stronger and weaker logics: the negation simply needs to be disjointive, and the multiplicative conjunction need not be commutative (then $\mimp$ splits into two divisions $\backslash, \slash$). 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.

The problem of determining whether a probabilistic program terminates almost surely (i.e.~with probability one) is undecidable, and actually Pi^0_2-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.

Subtyping in programming languages can be analysed as an entailment relation by means of proof theory. We look at two main families of systems: intersection types and polymorphic subtyping. We introduce a restriction IS of the Lambek calculus which is stable under cut-elimination and conservatively extends these two subtyping relations. IS is an intuitionistic non-commutative linear sequent calculus which provides a natural logical setting for the study of subtyping. We recover sequent calculi from the literature as restrictions of IS (thanks to a proof-theoretical analysis: admissibility, invertibility, focusing, etc.), so that IS appears as a unifying logic. We also develop translations relating IS with relevant logic, (unconstrained) Lambek or cyclic linear logic.

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 they are unable do distinguish between a statement and its contrapositive (e.g. dependent choice and the bar induction principles). The case of (Weak) König Lemma (WKL) and Fan Theorem (FT) is particularly interesting in that regard: while KL 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 to 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.

History-deterministic automata, often also known as 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.

Presheaves and nominal sets provide alternative abstract models of sets of syntactic objects with free and bound variables, such as $\lambda$-terms. One distinguishing feature of the presheaf-based perspective is its abstract syntax-free characterization of substitution using a closed monoidal structure. In this paper, we introduce a corresponding closed monoidal structure on nominal sets, modelling substitution 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 an action. We then demonstrate that this method not only uniformly recovers known substitution tensors for various kinds of presheaf categories, but also yields novel notions of substitution tensor for nominal sets and their relatives, such as renaming sets. Our results also shed new light on the relation between presheaves and nominal sets, in which we establish novel correspondences between different versions of nominal sets and suitable (pre-)sheaf categories.

In classical mathematics, a CW complex is a topological space which can be built up inductively by gluing together cells of increasing dimension. Due to their good categorical properties, CW complexes have become the main object 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 is a theorem (the `Hurewicz approximation theorem') which shows that a classical definition of $n$-connected CW complexes agrees with the, in HoTT, usual definition of $n$-connected types -- a theorem which is far from obvious from a constructive point of view. 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.

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 solves an open problem raised by Daligault, Rao and Thomassé in 2010, and Lopez in 2025. From our proof techniques, we also derive (restricted versions of) conjectures of Pouzet regarding well-quasi-ordering of graphs under the induces subgraph relation. 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.

Monadic stability generalizes many tameness notions from structural graph theory such as planarity, bounded degree, bounded tree-width, and nowhere density. The \emph{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 \emph{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 \emph{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.

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 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 for which the expected payoff is finite under all strategies, any expected payoff can be obtained exactly by mixing finitely many strategies.

Indexed languages are a classical notion in formal language theory, which features prominently in higher-order model checking. The downward closure (i.e. set of all subwords) of an indexed language is well-known to be a regular overapproximation. Zetzsche (ICALP 2015) has shown that the downward closure of an indexed language is effectively computable. However, that algorithm yields no complexity bounds, and it has remained open whether there exists a primitive-recursive construction. We settle this question and prove a tight triply exponential upper bound. It relies on recent advances in semigroup theory, which provide bounded-size summaries of words w.r.t. a finite semigroup.

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 requiring 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.

We explain how to construct a cartesian closed fibration of higher-order regular languages using glueing techniques combined with a fibered refinement of the usual Frobenius reciprocity formula.

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 such 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.

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 $\mathcal{F}$ such as the class of planar graphs, the class of graphs of treewidth $\leq k$, pathwidth $\leq k$, or treedepth $\leq k$, was shown to be equivalent to quantum isomorphism and equivalences with respect to counting logic fragments, respectively. Via such characterizations, 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 generalized 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 $\leq g$ (and other parameters) forms a strict hierarchy.

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.

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 $\zeta$. 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 $\zeta$-expressions as the syntax of $\mu$-bicomplete categories, extended with $\zeta$-binders and parallel products, which thus have a natural denotation in containers. By interpreting certain $\zeta$-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.

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 \in (0,1)$, we construct a near linear-time computable binary sequence $X$ with $\dim_{\mathrm{FS}}(X)=s$ such that for every finite-state transducer $T$, the output satisfies $\dim_{\mathrm{FS}}(T(X)) \le 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\in(0,1)$ and every fixed $k\ge 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_{\mathrm{FS}}(T(X_1,\dots,X_k))\le s$. Thus, even independent streams do not allow bounded-memory transduction to output a normal sequence or to increase finite-state dimension.

We provide general criteria ensuring the existence of minimal canonical models of streaming transducers, namely, devices that read an input word and produce a corresponding output value by iteratively updating an internal memory. This abstract model of transducer 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 our criteria to minimize variants of the latter transducers, where outputs are terms that are constructed incrementally, by extending (tuples of) terms either at the leaves or at the roots.

We introduce a dialect of the asynchronous $\pi$-calculus, called AW$\pi$, 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) behaves as substitutions when composed with any AW$\pi$ process.Thus AW$\pi$ naturally yields a category, whose morphisms are AW$\pi$ 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 organized 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$\pi$ follows the tradition of ordinary $\pi$-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$\pi$ is to remain faithful to the operational and algebraic tradition of the $\pi$-calculi while connecting to the tradition of denotational models for programming languages.

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.

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 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 $\boldsymbol{y}' = F(\boldsymbol y)$, where $F$ is a vector of rational functions that is defined at $\boldsymbol 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.

Dynamical systems provide rigorous models of movement or evolution over time. Due to their abstract nature, they may be naturally employed for modelling 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 wide range of applicability has sparked interest in designing formal specification languages for dynamical systems which may be amenable to 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 oftentimes more suitable for representing phenomena arising from CS, 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.

An infinite structure has the finite length property (over a given field) if, for each of its finite powers, strict chains of equivariant subspaces in the corresponding free vector space are bounded in length. Prior work showed that the countable pure set and the dense linear order without endpoints have this property.We generalise these results to (a) structures approximated by finite substructures with few orbits, provided the field is of characteristic zero, and (b) generically ordered expansions of Fraïssé limits with free amalgamation, in vocabularies consisting of unary and binary relations. 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 solving orbit-finite systems of linear equations.

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 Layered Modal ML (LMML), \textit{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 LMML, establishing \textit{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.

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 behavior, 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 critical 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.