https://arxiv.org/api/Hce7RFt7u7ViZ9dJiEMwu0mCUbI 2026-03-24T12:42:12Z 18920 105 15 http://arxiv.org/abs/2510.03130v3 2026-03-11T11:47:48Z

The operations to be performed by a quantum computer are almost invariably given in the form of a quantum circuit. In the final stage of compilation, a quantum circuit must be translated into the input signals accepted by the quantum hardware itself. For a quantum computer based on superconducting qubits, this will be a sequence of microwave control pulses to be sent to the various input channels. A pulse schedule gives a full specification for which pulse should be applied to which channel at what time. There is as yet no language for these pulse schedules that is very amenable to formal semantics. In this paper, we propose such a language called GRAMPUS (GRAded Modal type theory for PUlse Schedules). It is a graded modal type theory, where the grades represent timing information: a variable $x :^{50} Q_1$ will represent a state of qubit $Q_1$ that will exist 50 nanoseconds in the future, and a variable $y :^{-75} Q_2$ will represent a state of qubit $Q_2$ that existed 75 nanoseconds in the past. We give the syntax for two type theories, one with grades (the annotated language) and one without (the plain language). We prove some metatheoretic properties, and describe the semantics in terms of category theory. We show that the input signals to a quantum chip forms a model of the annotated language. We also give a syntatic model, prove that it is initial, and hence prove soundness and completeness theorems.

2025-10-03T15:58:30Z 21 pages, 1 figure Robin Adams Jean-Philippe Bernardy Lorenzo Perticone Jeremy Pope http://arxiv.org/abs/2510.27603v3 2026-03-11T10:53:48Z

We show that the Skolem Problem is decidable in finitely generated commutative rings of positive characteristic. More precisely, we show that there exists an algorithm which, given a finite presentation of a (unitary) commutative ring $\mathcal{R} = \mathbb{Z}_{/T}[X_1, \ldots, X_n]/I$ of characteristic $T > 0$, and a linear recurrence sequence $(γ_n)_{n \in \mathbb{N}} \in \mathcal{R}^{\mathbb{N}}$, determines whether $(γ_n)_{n \in \mathbb{N}}$ contains a zero term. Our proof is based on two recent results: Dong and Shafrir (2026) on the solution set of S-unit equations over $p^e$-torsion modules, and Karimov, Luca, Nieuwveld, Ouaknine, and Worrell (2025) on solving linear equations over powers of two multiplicatively independent numbers. Our result implies, moreover, that the zero set of a linear recurrence sequence over a ring of characteristic $T = p_1^{e_1} \cdots p_k^{e_k}$ is effectively a finite union of $p_i$-normal sets in the sense of Derksen (2007).

2025-10-31T16:28:27Z Corrected a small error in Lemma 3.2 Ruiwen Dong Doron Shafrir http://arxiv.org/abs/2409.02595v6 2026-03-11T02:16:12Z

We try to clarify the relationship between computation and concurrency. Base on the so-called pomsetc automata and step automata, we introduce communication and more operators, and establish the algebras modulo language equivalence and truly concurrent bisimilarities.

2024-09-04T10:23:15Z Yong Wang http://arxiv.org/abs/2603.11083v1 2026-03-11T00:12:28Z

This article introduces probabilistic disjunctive normal forms (PDNFs) as a framework for representing and reasoning about uncertainty in logical systems. Unlike classical DNFs, PDNFs assign real-valued weights to variables, encoding probabilistic information about their presence, absence, or negation. Then we construct a vector space of PDNFs that allows algebraic evidence combination. PDNFs are interpreted as probability distributions over venjunctions (temporal logic constructs) and as integrable functions over partitioned intervals, where the integrals determine variable probabilities. This dual perspective allows for a Banach space structure and the application of functional analysis. We demonstrate that, under exponential parametrisation, PDNF addition aligns with Bayesian evidence fusion and derive bounds for outcome identification from random samples. The formalism thus bridges logic, numerical methods, and continuous probability.

2026-03-11T00:12:28Z Alexander Kuznetsov http://arxiv.org/abs/2212.02444v6 2026-03-10T21:56:35Z

We show that certain diagrams of $\infty$-logoses are reconstructed in homotopy type theory extended with some lex, accessible modalities, which enables us to use plain homotopy type theory to reason about not only a single $\infty$-logos but also a diagram of $\infty$-logoses. This also provides a higher dimensional version of Sterling's synthetic Tait computability -- a type theory for higher dimensional logical relations.

2022-12-05T17:41:09Z Logical Methods in Computer Science, Volume 22, Issue 1 (March 12, 2026) lmcs:13215 Taichi Uemura 10.46298/lmcs-22(1:25)2026 http://arxiv.org/abs/2603.10236v1 2026-03-10T21:22:51Z

In this work we investigate Weighted Model Enumeration (WME): given a Boolean formula and a weight function over its satisfying assignments, enumerate models while accounting for their weights. This setting supports weight-driven queries, such as producing the top-k models or all models above a threshold. While related to AllSAT, Weighted Model Counting, and MaxSAT, these paradigms do not treat selective enumeration under weights as a native solver task. We present CDCL-based algorithms for WME that integrate weight propagation, weight-based pruning, and weight-aware conflict analysis into both chronological and non-chronological backtracking frameworks. Chronological backtracking exploits implicit blocking and keeps the clause database compact, thereby reducing memory footprint and enabling efficient propagation. In contrast, non-chronological backtracking with clause learning supports explicit blocking and restarts. We show that both approaches are feasible and complementary, highlighting trade-offs in pruning effectiveness with weights and clarifying when each performs best. This work establishes WME as a solver-level reasoning task and provides a systematic exploration of its algorithmic foundations.

2026-03-10T21:22:51Z Giuseppe Spallitta Moshe Y. Vardi http://arxiv.org/abs/2405.12917v3 2026-03-10T16:54:11Z

Several monads of probability measures have been shown to have presentations as codensity monads over small categories of stochastic maps. This paper studies how three key properties of these probability monads, relevant to categorical approaches to probability, can arise from their codensity presentations. We first derive the existence of a Kleisli law into the Giry monad, which provides a formal connection to measurable probability. In particular, from their codensity presentations, we prove a novel universal property of several probability monads as terminal liftings of the Giry monad. This generalises a result by Van Breugel on the Kantorovich monad, and proves the existence of such Kleisli laws. We additionally provide sufficient conditions for a codensity monad to be lax monoidal and affine, which provides a connection to the theory of Markov categories. In particular, we introduce the condition for a codensity monad to be exactly pointwise monoidal, which is then lax monoidal, and prove a characterisation of this condition in terms of Day convolution. We show that the Radon monad is exactly pointwise monoidal, and use our characterisation to give a description of the tensor product of free algebras of the Radon monad in terms of Day convolution. Finally, we show that the Giry monad is only exactly pointwise monoidal when restricted to standard Borel spaces, due to the existence of probability bimeasures that do not extend to measures.

2024-05-21T16:39:26Z 40 pages. Version published in Theory and Applications of Categories Theory and Applications of Categories. 45 (2026), No. 14, 461-500 Zev Shirazi http://arxiv.org/abs/2603.06931v2 2026-03-10T14:13:09Z

Whether LLMs can reason or write software is widely debated, but whether they can write software that itself reasons is largely unexplored. We present a case study in which an LLM coding agent builds a complete DPLL(T)-style SMT solver for QF_UF with zero human-written code. The solver implements the Nieuwenhuis-Oliveras congruence closure algorithm, includes preprocessing, and emits Lean proofs for unsatisfiable instances. We describe the development process and key challenges, and show that the resulting solver is competitive on SMT-LIB benchmarks.

2026-03-06T23:03:27Z Mikoláš Janota Mirek Olšák http://arxiv.org/abs/2512.24594v2 2026-03-10T14:02:58Z

Fully automated verification of large-scale software and hardware systems is arguably the holy grail of formal methods. Large language models (LLMs) have recently demonstrated their potential for enhancing the degree of automation in formal verification by, e.g., generating formal specifications as essential to deductive verification, yet exhibit poor scalability due to long-context reasoning limitations and, more importantly, the difficulty of inferring complex, interprocedural specifications. This paper presents Preguss -- a modular, fine-grained framework for automating the generation and refinement of formal specifications. Preguss synergizes between static analysis and deductive verification by steering two components in a divide-and-conquer fashion: (i) potential runtime error-guided construction and prioritization of verification units, and (ii) LLM-aided synthesis of interprocedural specifications at the unit level. We show that Preguss substantially outperforms state-of-the-art LLM-based approaches and, in particular, it enables highly automated RTE-freeness verification for real-world programs with over a thousand LoC, with a reduction of 80.6%~88.9% human verification effort.

2025-12-31T03:31:51Z Accepted at OOPSLA 2026. Publication date: April 2026 Zhongyi Wang Tengjie Lin Mingshuai Chen Haokun Li Mingqi Yang Xiao Yi Shengchao Qin Yixing Luo Xiaofeng Li Bin Gu Liqiang Lu Jianwei Yin 10.1145/3798268 http://arxiv.org/abs/2603.07595v2 2026-03-10T12:47:17Z

The Eighth International Conference on Applied Category Theory took place at the University of Florida on June 2-6 2025. The conference consisted of 2 plenary invited talks, 28 contributed talks, an online community meeting, a general community meeting, and 4 talks by junior researchers who attended the Adjoint School to present the results of their research at the school. Information regarding the conference may be found at https://gataslab.org/act2025/act2025.html. Submission to ACT2025 had three tracks: extended abstracts, software demonstrations, and proceedings. Accepted proceedings track submissions are included in this volume. The contributions to ACT2025 ranged from pure to applied and included contributions in a wide range of disciplines. ACT2025 included talks related to computer science, probability theory, chemistry, string diagrams, game semantics, quantum computation, and more.

2026-03-08T11:41:37Z EPTCS 442, 2026 Amar Hadzihasanovic Tallinn University of Technology Jean-Simon Pacaud Lemay Macquarie University 10.4204/EPTCS.442 http://arxiv.org/abs/2603.09455v1 2026-03-10T10:11:09Z

Scenario-based testing is a key method for cost-effective and safe validation of autonomous vehicles (AVs). Existing approaches rely on imperative scenario definitions, requiring developers to manually enumerate numerous variants to achieve coverage. Declarative languages, such as OpenSCENARIO DSL (OS2), raise the abstraction level but lack systematic methods for instantiating concrete, specification-compliant scenarios as simulations. To our knowledge, currently, no open-source solution provides this capability. We present RoadLogic that bridges declarative OS2 specifications and executable simulations. It uses Answer Set Programming to generate abstract plans satisfying scenario constraints, motion planning to refine the plans into feasible trajectories, and specification-based monitoring to verify correctness. We evaluate RoadLogic on instantiating representative OS2 scenarios as simulations in the CommonRoad framework. Results show that RoadLogic consistently produces realistic, specification-satisfying simulations within minutes and captures diverse behavioral variants through parameter sampling, thus opening the door to systematic scenario-based testing for autonomous driving systems.

2026-03-10T10:11:09Z Accepted at the 29th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2026). The final version will appear in the ACM Digital Library Ezio Bartocci Alessio Gambi Felix Gigler Cristinel Mateis Dejan Ničković http://arxiv.org/abs/2503.05457v2 2026-03-10T09:43:45Z

Directed wiring diagrams can be used as a composition pattern for composing input/output systems such as Moore machines. In a Moore machine, the input parametrizes an internal state and the internal state defines the output. Because the value of the output is shielded from the input by the internal state, Moore machines can compose by connecting the output of any machine to the input of any other machine. These connections are defined by the trace wires in a directed wiring diagram. Unlike Moore machines, Mealy machines allow the output to be directly and instantaneously affected by the input. In order to compose such machines via directed wiring diagrams, it is necessary to avoid cycles between trace wires in the wiring digram and dependencies of outputs on inputs. To capture these patterns of composition, we introduce an operad of dependent directed wiring diagrams. We then define an algebra of Mealy machines on this operad and an algebra of stock and flow diagrams in which the values of auxiliary variables are parameterized by inputs. Finally, we give a semantics for this algebra of stock and flow diagrams by giving a morphism of algebras from stock and flow diagrams into Mealy machines.

2025-03-07T14:30:10Z In Proceedings ACT 2025, arXiv:2603.07595 EPTCS 442, 2026, pp. 15-29 Keri D'Angelo Cornell University Sophie Libkind Topos Institute 10.4204/EPTCS.442.2 http://arxiv.org/abs/2603.09379v1 2026-03-10T08:53:54Z

The observation that optimum circuit size changes by at most $O(n)$ under a one-point truth table perturbation is implicit in prior work on the Minimum Circuit Size Problem. This note states the bound explicitly for arbitrary fixed finite complete bases with unit-cost gates, extends it to general Hamming distance via a telescoping argument, and verifies it exhaustively at $n = 4$ in the AIG basis using SAT-derived exact circuit sizes for 220 of 222 NPN equivalence classes. Among 987 mutation edges, the maximum observed difference is $4 = n$, confirming the bound is tight at $n = 4$ for AIG.

2026-03-10T08:53:54Z 4 pages, 1 table. Code and data: https://github.com/krinkin/bounds Kirill Krinkin http://arxiv.org/abs/2603.08646v1 2026-03-09T17:24:20Z

Inquisitive team logic is a variant of inquisitive logic interpreted in team semantics, which has been argued to provide a natural setting for the regimentation of dependence claims. With respect to sentences, this logic is known to be expressively equivalent with first-order logic. In this article we show that, on the contrary, the expressive power of open formulas in this logic properly exceeds that of first-order logic. On the way to this result, we show that if inquisitive team logic is extended with the range-generating universal quantifier adopted in dependence logic, the resulting logic can express finiteness, and as a consequence, it is neither compact nor recursively axiomatizable. We further extend our results to standard inquisitive first-order logic, showing that some sentences of this logic express non first-order properties of models.

2026-03-09T17:24:20Z Juha Kontinen Ivano Ciardelli http://arxiv.org/abs/2406.17082v6 2026-03-09T15:07:33Z

We define an extension of lambda-calculus with dependents types that enables us to encode transparent and opaque probabilistic programs and prove a strong normalisation result for it by a reducibility technique. While transparent nondeterministic programs are formalised by rather usual techniques, opaque nondeterministic programs are formalised by introducing in the syntax oracle constants, the behaviour of which is governed by oracular functions. The generality of these functions and the fact that their values are determined by the form of the whole term inside which the relative oracle occurs also enable us to simulate learning-like behaviours. We then extend the calculus in order to define a computational trustworthiness predicate. The extension of the calculus does not only enable us to precisely formalise a notion of trustworthiness and to encode the procedures required to test it on programs, but also to reason, by means of the type system, on the behaviour of programs with respect to trustworthiness.

2024-06-24T19:14:06Z Francesco A. Genco