ABSTRACT. Most implementations of sampling algorithms for continuous distributions use floating-point numbers, which introduce round-off errors and approximations. These errors can be difficult to analyze, and can cause security issues when used in algorithms for differential privacy. An alternative is to use exact sampling algorithms based on computable reals, which can lazily generate the digits of a continuous sample to arbitrary precision. However, these algorithms are intricate, and implementing and using them involves a combination of semantically challenging language features, such as probabilistic choice, higher-order functions, and dynamically-allocated mutable state. 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.

ABSTRACT. We introduce a general methodology for the construction of sound and complete proof rules for the almost-sure and quantitative acceptance of reactivity properties on time-homogeneous Markov chains with general state spaces. Reactivity captures $\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.

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

ABSTRACT. Quantitative logic reasons about the degree to which formulas are satisfied. This paper studies the fundamental reasoning principles of higher-order quantitative logic and their application to reasoning about probabilistic programs and processes. We construct an affine calculus for 1-bounded complete metric spaces and the monad for probability measures equipped with the Kantorovich distance. The calculus includes a form of guarded recursion interpreted via Banach's fixed point theorem, useful, e.g., for recursive programming with processes. We then define an affine higher-order quantitative logic for reasoning about terms of our calculus. The logic includes novel principles for guarded recursion and induction over probability measures and natural numbers. We illustrate the expressivity of the logic by a sequence of case studies: Proving upper limits on bisimilarity distances of Markov processes, showing convergence of a temporal learning algorithm and of a random walk using a coupling argument.

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

ABSTRACT. We introduce a new logic for describing properties of graphs, which we call low rank MSO. This is the fragment of monadic second-order logic in which set quantification is restricted to vertex sets of bounded cutrank. We prove the following statements about the expressive power of low rank MSO. * Over any class of graphs that is weakly sparse, low rank MSO has the same expressive power as separator logic. This equivalence does not hold over all graphs. * Over any class of graphs that has bounded VC dimension, low rank MSO has the same expressive power as flip-connectivity logic. This equivalence does not hold over all graphs. * Over all graphs, low rank MSO has the same expressive power as flip-reachability logic. Here, separator logic is an extension of first-order logic by basic predicates for checking connectivity, which was proposed by Bojańczyk [ArXiv 2107.13953] and by Schirrmacher, Siebertz, and Vigny [ACM ToCL 2023]. Flip-connectivity logic and flip-reachability logic are analogues of separator logic suited for non-sparse graphs, which we propose in this work. In particular, the last statement above implies that every property of undirected graphs expressible in low rank MSO can be decided in polynomial time.

ABSTRACT. Algorithmic meta-theorems explain the tractability of large classes of computational problems by linking logical expressibility with structural graph properties. While extensions of first-order logic such as FO+dp admit efficient model checking on graph classes excluding a fixed topological minor, comparable results for richer fragments of CMSO were previously unknown. We further develop the framework of Sau, Stamoulis, and Thilikos [SODA 2025] for fragmenting CMSO via annotated graph parameters, which restrict set quantification to vertex sets satisfying bounded structural conditions. Following this approach, we identify a fragment of CMSO namely the one defined by allowing quantification only over sets having what we call low monodimensionality, that generalizes several previously-known logics and we show that model checking for this fragment, enhanced with the disjoint-paths predicate, is fixed-parameter tractable on topological-minor-free graph classes. Such classes essentially delimit the tractability for this logic on subgraph-closed classes. As a consequence, our results lift several known algorithmic meta-theorems beyond first-order logic to the topological-minor-free setting.

ABSTRACT. We study classes of graphs with bounded clique-width that are well-quasi-ordered by the induced subgraph relation, in the presence of labels on the vertices. We prove that, given a finite presentation of a class of graphs, one can decide whether the class is labelled-well-quasi-ordered. This 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.

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

ABSTRACT. We introduce a complete equational theory for the fragment of quantum circuits generated by the real Clifford gates plus the two-qubit controlled-Hadamard gate. That is, we give a simple set of equalities between circuits of this fragment, and prove that any other true equation can be derived from these. This is the first such completeness result for a finitely-generated, universal fragment of quantum circuits, with no parameterized gates and no need for ancillas.

ABSTRACT. We present sound and complete relational program logics for infinite-dimensional quantum and classical-quantum programs. The logics model assertions as self-adjoint unbounded linear relations, which simultaneously support quantitative and qualitative reasoning. Our main theoretical results include new convergence theorem and infinite-dimensional duality theorems for infinite-dimensional quantum states, which we use to establish completeness.

ABSTRACT. The Kochen-Specker no-go theorem established that hidden-variable theories in quantum mechanics necessarily admit contextuality. This theorem is formally stated in terms of the partial Boolean algebra structure of projectors on a Hilbert space. Each partial Boolean algebra provides a semantics for interpreting propositional logic. In this paper, we examine the complexity of propositional 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.

ABSTRACT. Reachability in pushdown vector addition systems with states (PVASS) is among the longest standing open problems in Theoretical Computer Science. We show that the problem is decidable in full generality. Our decision procedure is similar in spirit to the KLMST algorithm for VASS reachability, but works over objects that support an elaborate form of procedure summarization as known from pushdown reachability.

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

ABSTRACT. Nested counter systems (NCS) are a generalization of counter systems to higher-order counters. Here, a higher-order counter is allowed to have other (lower-order) counters as elements, instead of just a number. 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.

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

ABSTRACT. Coherent control, aka quantum control, is a central concept in quantum computing that is attracting increasing attention from both the quantum foundations and quantum software communities. Defining coherent control in the presence of recursion and measurement has long been known to be a major challenge. In particular, no-go results have been established for standard semantical domains like completely positive maps. We address this problem by introducing the first quantum programming language with recursion that allows for the coherent control of arbitrary quantum operations. We equip this language with both an operational and a denotational semantics that we prove to be adequate. To design these semantics, we show that combining coherent control, recursion, and measurement crucially requires describing the evolution of subprograms in the absence of input. To address this, the operational semantics takes into account a default evolution branch, while the denotational semantics uses the concept of coherent quantum operation, based on vacuum extensions. We strengthen the validity of our approach by developing an observational equivalence: two programs are equivalent if their probability of termination is the same in any context. The denotational semantics is shown to be fully abstract with respect to this observational equivalence.

ABSTRACT. Indefinite causal order is a characteristic phenomenon in quantum computation, with examples including the quantum SWITCH and the OCB process. Not all such processes are believed to be physically realizable: while some implementations of the quantum SWITCH have been proposed, the OCB process is suspected to be unrealizable. This difference in realizability is commonly attributed to constraints imposed by physical causality. This paper studies such a causality issue in a higher-order setting, proposing a typed lambda calculus with quantum control and its categorical semantics. Our calculus extends pure quantum computation with higher-order functions and quantum conditional branching, and it is equipped with a type system based on intuitionistic BV logic to enforce causality. We also present a novel model that is closely related to the Caus construction, by which we prove that some physically-unrealizable processes are not definable in our language.

ABSTRACT. Controlled commands---computations whose execution depends on a separate input---play a central role in reversible Boolean circuits and quantum circuits. However, existing formalisms typically treat control only implicitly, entangled with other aspects of computation. From a semantic perspective, control is most naturally expressed in semisimple rig categories, which---unlike standard circuit models such as props---support both parallel and conditional composition. We present a construction that freely adjoins an explicit syntactic notion of control to a circuit theory specified as a suitable prop, subject to eight universally quantified equations. Our main result is that these equations are sound and complete for the intended semantics of control: the resulting theory satisfies a universal property, identifying it exactly as the circuit subtheory of the free semisimple rig completion. The proof combines coherence for rig categories with a new method based on induction over Gray codes. We illustrate the usefulness of the framework by showing that it simplifies several existing sound and complete axiomatisations of quantum circuits, isolating a small and conceptually clean set of generators and equations. In addition, the same equations yield a sound and complete axiomatisation of the multiply controlled Toffoli gate set, that is universal for reversible Boolean circuits.

ABSTRACT. Finite-state dimension, introduced as a finite-state analogue of Hausdorff dimension, quantifies the lower asymptotic density of information in an infinite sequence as perceived by finite-state automata. It admits several equivalent formulations; two particularly useful are via finite-state gambling strategies and via the optimal asymptotic compression ratio achieved by information-lossless finite-state compressors. Normal sequences represent the highest level of algorithmic randomness visible to finite automata, and are exactly those sequences having finite-state dimension equal to $1$. This motivates a bounded-memory notion of randomness extraction: can a finite-state transducer, reading a single sequence streamingly, extract a normal output from a single input source? More modestly, can it always transform the input into an output of strictly higher finite-state dimension? Finite-state transducers can perform surprisingly effective one-pass transformations: even with constant memory they can implement variable-length coding schemes including Shannon--Fano coding, remove local redundancy, and increase the apparent randomness rate on many structured or stochastic inputs. We show randomness extraction using transducers is impossible in a strong, explicit form. For every rational $s \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.

ABSTRACT. We study contextual interactions in an ML-like language equipped with general references and continuations, focusing on the reachability and approximation problems. Previous work addressed higher-order programs with first-order references in the absence of loops using automata over nested data; however, extending these techniques to programs with loops encountered fundamental technical obstacles, stemming from the need to bound the depth of data. We introduce a new class of automata over infinite alphabets that supports unbounded nesting of data. We establish a precise correspondence between these automata and higher-order programs with loops: the trace semantics of any such program can be captured by an automaton, and conversely, the trace language of any such automaton can be realised by an imperative higher-order program with loops. This correspondence enables the transfer of decidability and undecidability results between the automata and programs. In particular, we show that adding loops preserves decidability of reachability, while rendering approximation undecidable.

ABSTRACT. It has been conjectured that the Parikh (commutative) image of every language over an infinite alphabet recognized by an automaton with registers is defined by a rational expression. This conjecture is known to hold for all languages recognized by one-register automata. We refine this result by proving that the star-height of the Parikh image of any language recognized by a one-register automaton is universally bounded by two. Furthermore, we show that one-register context-free languages have rational commutative images of arbitrarily high star height. We then disprove the conjecture for multiple registers, as well as disprove the equivalence of commutative expressive power between context-free grammars and automata over infinite alphabets.