https://arxiv.org/api/Tr7bx4nvd+EyCHzoDynib9+dAPQ 2026-07-21T16:53:10Z 19781 90 15 http://arxiv.org/abs/2607.12207v1 2026-07-13T23:16:49Z

Homotopy type theory (HoTT) is a type theory that allows for synthetic reasoning about $\infty$-groupoids. Several proof assistants (such as Rocq and Agda) implement variants of HoTT. Directed type theory is a type theory for synthetic reasoning about $\infty$-categories, where morphisms (or paths) of dimension 1 are not necessarily invertible. Among the proposals for directed type theory, the most developed is Riehl and Shulman's simplicial type theory (RSTT), based on simplicial shapes such as directed intervals and triangles. We present Rzk, a proof assistant implementing (a refinement of) RSTT for synthetic reasoning about $\infty$-categories. Specifically, the type theory implemented by Rzk is a computational variant of RSTT adjusted to make type checking practical. We define a translation from RSTT to Rzk and prove that it is sensible: every RSTT proof translates to an Rzk proof (faithfulness), and Rzk proves nothing new about RSTT types (conservativity). We also give a tutorial introduction to proving in Rzk, and describe its implementation, including the type-checking algorithm and the automated prover for the logic of shapes.

2026-07-13T23:16:49Z 54 pages, including appendices. Describes Rzk v0.7.8. Ancillary files include the code of every example in the paper and the scripts and trace behind the evaluation Nikolai Kudasov Violetta Sim Benedikt Ahrens http://arxiv.org/abs/2511.07774v3 2026-07-13T22:17:47Z

This paper gives a proof-theoretic account of how positive integers must be classified as $1$, prime, or composite in intuitionistic logic. Compositehood is expressed in $Σ^0_0$ by exhibiting a factorization; primality is expressed in $Π^0_0$ by exhibiting a lack of interior factorization. Because both searches are bounded, both predicates are decidable. Organizing the checks in stages yields a recursive sieve for the primes, a characterization of modular cancellation, and finite arithmetic certificates. The final sections distinguish what Heyting Arithmetic ($\mathsf{HA}$) proves internally from what depends on the standard interpretation of $\mathbb{N}$.

2025-11-11T02:46:13Z 42 pages, 4 figures. Corrigendum to v2: corrects the treatment of bounded factor search and separates decidable primality from oracle-strength completion principles Milan Rosko http://arxiv.org/abs/2511.09008v2 2026-07-13T19:54:42Z

Large Language Models perform well at natural language interpretation and reasoning, but their lack of formal correctness guarantees limits their adoption in regulated industries like finance and health-care that operate under strict policies. To address this limitation, we launched Automated Reasoning checks (ARc): a public service that (1) uses LLMs with optional human guidance to formalize natural language policies, allowing fine-grained control of the formalization process, and (2) uses inference-time autoformalization to validate logical correctness of natural language statements against those policies. ARc performs multiple redundant formalization steps at inference time, checking the formalizations for semantic equivalence. Our benchmarks show that ARc exceeds 99% soundness and achieves a near-zero false positive rate in identifying logical validity. Our approach produces auditable artifacts that substantiate the verification outcomes and can be used to improve the original text. ARc is the first commercial offering from a major cloud provider to integrate automated reasoning into a generative AI guardrail.

2025-11-12T06:00:37Z 28 pages, 11 figures Chenyang An Sam Bayless Stefano Buliani Darion Cassel Byron Cook Duncan Clough Rémi Delmas Nafi Diallo Ferhat Erata Nick Feng Dimitra Giannakopoulou Aman Goel Aditya Gokhale Joe Hendrix Victor Heorhiadi Marc Hudak Dejan Jovanović Andrew M. Kent Benjamin Kiesl-Reiter Jeffrey J. Kuna Nadia Labai Joseph Lilien Divya Raghunathan Zvonimir Rakamarić Niloofar Razavi Michael Tautschnig Ali Torkamani Nathaniel Weir Michael W. Whalen Jianan Yao http://arxiv.org/abs/2508.14838v4 2026-07-13T14:14:43Z

A finite relational structure A is called compact if for any infinite relational structure B of the same type, the existence of a homomorphism from B to A is equivalent to the existence of homomorphisms from all finite substructures of B to A. We show that if A has width one, then the compactness of A can be proved in the axiom system of Zermelo and Fraenkel, but otherwise, the compactness of A implies the existence of non-measurable sets in 3-space.

2025-08-20T16:41:04Z Claude Tardif http://arxiv.org/abs/2509.24583v4 2026-07-13T13:56:21Z

Modal separability for modal fixpoint formulae is the problem to decide for two given modal fixpoint formulae $\varphi,\varphi'$ whether there is a modal formula $ψ$ that separates them, in the sense that $\varphi\modelsψ$ and $ψ\models\neg\varphi'$. We study modal separability and its special case modal definability over various classes of models, such as arbitrary models, finite models, trees, and models of bounded outdegree. Our main results are that modal separability is PSpace-complete over words, that is, models of outdegree $\leq 1$, ExpTime-complete over unrestricted and over binary models, and TwoExpTime-complete over models of outdegree bounded by some $d\geq 3$. Interestingly, this latter case behaves fundamentally different from the other cases also in that modal logic does not enjoy the Craig interpolation property over this class. Motivated by this we study also the induced interpolant existence problem as a special case of modal separability, and show that it is coNExpTime-complete and thus harder than validity in the logic. Besides deciding separability, we also provide algorithms for the effective construction of separators. Finally, we consider in a case study the extension of modal fixpoint formulae by graded modalities and investigate separability by modal formulae and graded modal formulae.

2025-09-29T10:46:16Z Jean Christoph Jung Jędrzej Kołodziejski http://arxiv.org/abs/2605.18688v2 2026-07-13T13:40:09Z

In this paper, we propose the frameworks of generalized performance evaluation and generalized controller synthesis. To this end, we give a true concurrent process calculus as the model of systems, and present a lattice-valued performance evaluation language as the performance specification of systems. We give a framework of generalized performance evaluation based on the process calculus and the performance evaluation language. We show that the several problems in computer science are special cases of generalized performance evaluation. A generalized performance evaluation algorithm is presented. Furthermore, we present a framework of generalized controller synthesis, which is the inverse problem of generalized performance evaluation. We show several special cases of generalized controller synthesis in computer science, and give an outline of generalized controller synthesis algorithm.

2026-05-18T17:27:21Z 16 pages Zining Cao http://arxiv.org/abs/2605.18450v2 2026-07-13T12:55:22Z

In the literature on Kleene algebra (KA), a number of variants have been proposed such as Kleene algebra with tests, commutative KA, bi-KA, and concurrent KA. The equational theories of some of these structures have then been studied in the presence of additional assumptions, called hypotheses. We propose a unifying framework encompassing all the previous structures, as well as regular tree languages. This is done by considering algebras ordered by complete lattices, where least fixpoints can be computed. We provide a canonical model consisting of closed languages, which we prove sound and complete with respect to all continuous models. Then we study quasi-equational axiomatisations. It is illusory to hope for a generic axiomatisation which would be sound and complete for all instances. Instead, we provide a generic axiomatisation which we prove sound and we setup tools that make it possible to get complete ones in a modular way, building on previous works from the literature. We showcase these tools by proving new completeness results for commutative KA, bi-KA, and regular tree languages, in each case extended with various hypotheses.

2026-05-18T14:18:24Z 37th International Conference on Concurrency Theory (CONCUR '26), Sep 2026, Liverpool, United Kingdom Lukas Mulder PLUME Damien Pous PLUME Jana Wagemaker http://arxiv.org/abs/2607.11435v1 2026-07-13T11:41:13Z

Linearizability is a standard correctness condition for concurrent data structures. It guarantees that operations behave as if they took effect at some atomic instant between their call and return points. Despite the central role linearizability plays, prior work has argued for instead using a style of specification that internalizes the atomicity of operations in terms of the logic's reasoning rules, known as logical atomicity. These logically atomic specifications are intended to be easier to compose inside of the logic than linearizability. Prior work has shown that in the Iris separation logic framework, a certain form of logically atomic specifications implies that a data structure is linearizable. However, the converse remained an open question: for every linearizable data structure, is it always possible to derive a corresponding logically atomic specification? This paper resolves this question in the affirmative. We prove a completeness theorem for Iris that derives a logically atomic specification for any linearizable data structure. As a consequence, we are able to embed a variety of linearizability proof techniques into Iris and use them to derive logically atomic specifications. We apply this to three linearizability proof methods: aspect-oriented linearizability proofs, forward simulations with commit points, and meta-configuration tracking. Using these embeddings, we derive logically atomic specifications for the Herlihy-Wing queue and the Baskets Queue. We furthermore establish a connection between logical atomicity and an encoding of refinement in Iris that has been used in prior logical relations models. This result allows us to transport logically atomic specifications across refinements, which we apply to the Folly MPMC queue implementation. All of the results in this paper have been mechanized in the Rocq Prover.

2026-07-13T11:41:13Z Zichen Zhang Simon Oddershede Gregersen Joseph Tassarotti http://arxiv.org/abs/2607.11404v1 2026-07-13T11:10:27Z

Links between physicals systems and computability properties have been an active field of investigation in recent years. Inspired by a previous work in the context of positive temperature Gibbs measures, we prove here that in the context of zero-temperature ergodic optimisation, for a computable potential and provided with several reasonable assumptions, the maximum ergodic average is a computable real number, and the set of maximising measures is a $Π_1$-computable compact set. Then, in the more specific context of symbolic dynamics, with finite-range interactions on subshifts of finite type, we provide an explicit algorithm to compute both the maximum ergodic average and the set of maximising measures in finite time, with a matching code repository.

2026-07-13T11:10:27Z Léo Gayral Mathieu Hoyrup http://arxiv.org/abs/2607.11352v1 2026-07-13T10:15:00Z

Intuitionistic modal logic (IML) has inspired several developments in programming languages including modal type systems for staging, computational effects and language-based security. IMLs are typically studied using Kripke-style relational semantics, which simplifies proofs of meta-theoretic properties, such as completeness and consistency, by making it easy to construct models. Kripke-style relational semantics, however, relies upon classical reasoning principles, which makes it unappealing from a computational perspective and unsuitable for formalization in a constructive type theory. Goldblatt provides an alternative semantics for IMLs by extending Beth-Kripke-Joyal-style "cover" semantics for intuitionistic propositional logic with relations to support modalities. Goldblatt's "relational cover" semantics overcomes classical reasoning but introduces a new limitation: it relies upon a "modal localization" condition that restricts the class of models and complicates model construction. Goldblatt bypasses this restriction by using intricate order-theoretic completion arguments to prove completeness. In this article, we present a conservative extension of relational cover semantics that alleviates this restriction and is amenable to simpler and standard model construction techniques. We formalize our semantics in Agda and prove completeness constructively in the style of Normalization by Evaluation for a variety of IMLs featuring independent box and diamond modalities.

2026-07-13T10:15:00Z Presented at MFPS 2026 Nachiappan Valliappan http://arxiv.org/abs/2607.11329v1 2026-07-13T09:48:19Z

Universes are central to dependent type theory, and they are notoriously difficult to handle in a way that is both correct and usable. We propose a new "fuss-free" generalised algebraic presentation for polymorphic cumulative universes that dispenses with the intricate theory of coherent universe coercions in favour of a simpler formulation, which we prove equivalent by means of a normalisation theorem for the former. Evidence for the utility of the fuss-free formulation is provided in the form of (1) an abstract specification of its bidirectional elaboration algorithm, and (2) a concrete implementation in Haskell. We also describe and implement an extension of the fuss-free universe hierarchy with a judgemental notion of datatype description from which prior notions of cumulative inductive type may be derived.

2026-07-13T09:48:19Z Raphaël Sterbac Jonathan Sterling http://arxiv.org/abs/2607.09564v2 2026-07-13T09:19:53Z

Surface syntax in proof assistants like Rocq, Lean, Agda, and Idris is highly implicit, lacking many details that are needed for user-written code to denote precisely defined mathematical objects. Elaboration is an algorithm that accounts for these details by translating surface syntax to an explicit enough core syntax. The reliability and predictability of elaboration relies on several critical properties of the core type system, including decidability of judgemental equality and the injectivity of type constructors; these dependencies are witnessed in a concrete system by explicit calls to conversion checking and weak-head reduction subroutines. We introduce a dependently typed monadic domain specific language for the executable specification of correct-by-construction elaboration algorithms that is abstracted from any particular representation of normal forms or algorithm for conversion checking. In particular, we represent a bidirectionally typed surface language for Martin-Löf type theory by shallow embedding in this DSL so that the translation of surface terms into core terms amounts to elementary equational calculation. This translation is correct by construction in the sense that it cannot produce ill-typed terms, and is automatically stable under judgemental equality of core terms and even under substitution; from the latter property, we obtain a new denotational interpretation of the suspension of elaboration problems. Finally, a concrete elaboration algorithm is extracted by algebraic means from a presheaf model of the DSL built out of the bi-initial natural model of Martin-Löf type theory.

2026-07-10T16:10:31Z Andrew Slattery Jonathan Sterling http://arxiv.org/abs/2607.11121v1 2026-07-13T05:53:17Z

The Bandwidth Multicoloring Problem (BMCP) is an NP-hard extension of the Bandwidth Coloring Problem (BCP) with important applications in telecommunications, resource allocation, and scheduling. While state-of-the-art metaheuristics can efficiently produce high-quality solutions, they cannot certify global optimality. Existing exact approaches based on Constraint Programming (CP) and Integer Programming (IP) provide such guarantees but typically require extensive computation and still lag behind metaheuristics in solution quality, leaving many benchmark instances without optimality certificates. In this paper, we present the first SAT-based exact framework for the BMCP. Our main contribution is an efficient SAT encoding that compactly models both intra-vertex and inter-vertex color distance constraints. Combined with tight color domain reduction and an incremental SAT-solving strategy, the proposed formulation significantly prunes the search space and enables efficient exact optimization. Experimental results on the GEOM and MS-CAP benchmark suites demonstrate substantial improvements over previous exact approaches. On the challenging GEOM benchmark, the proposed framework proves optimality for more instances within only one hour of computation than the previous CP/IP approach, which required a 48-hour time limit, while also verifying the optimality of several previously reported best-known solutions. These results demonstrate that SAT-based reasoning provides an effective exact optimization framework for the BMCP and substantially expands the range of benchmark instances whose optimality can be certified.

2026-07-13T05:53:17Z Duc Trung Kim Nguyen Khanh Van To http://arxiv.org/abs/2607.10941v1 2026-07-12T22:04:50Z

Monadic dependence is a proposed structural dividing line for fixed-parameter tractability of first-order model checking on hereditary graph classes. A graph class is \emph{monadically dependent} if the class of all graphs cannot be interpreted in its vertex-colored members using a fixed first-order formula. We prove two structural consequences of monadic dependence. First, every monadically dependent class has \emph{almost linear neighborhood complexity}: for every graph $G$ in the class and every set $A\subseteq V(G)$, the family $\{N_G(v)\cap A : v\in V(G)\}$ has size $|A|^{1+o(1)}$. Second, every $n$-vertex graph in a monadically dependent class has radius-1 merge-width $n^{o(1)}$. Here, merge-width is the decomposition parameter of Dreier and Toruńczyk based on construction sequences; its radius-$r$ version measures local reachability among parts through already resolved pairs. This settles the radius-1 case of the conjectured connection between monadic dependence and almost bounded merge-width and provides the first decomposition-based structural description of monadically dependent graph classes. Our proof is algorithmic: we give an $\mathcal{O}(n^5)$-time algorithm that, given an $n$-vertex graph $G$ such that $|\{N_G(v)\cap A : v\in V(G)\}|\le O(|A|^d)$ for every $A\subseteq V(G)$, computes a construction sequence witnessing radius-1 merge-width $\mathcal{O}(n^{1-1/d}\log n)$.

2026-07-12T22:04:50Z Jan Dreier Nikolas Mählmann Rose McCarty Michał Pilipczuk Szymon Toruńczyk http://arxiv.org/abs/2607.10939v1 2026-07-12T22:03:25Z

A graph class is $k$-WQO if its $k$-labeled graphs are well-quasi-ordered under label-preserving induced subgraph embeddings. We show that every hereditary graph class that is $2$-WQO has bounded clique-width. Combined with the recent result of Dumas and Lopez, this confirms a long-standing conjecture of Pouzet: A hereditary graph class is $2$-WQO if and only if it is $k$-WQO for all $k\geq 2$, if and only if it is $\forall$-WQO, that is, its labeled graphs are well-quasi-ordered for every possible well-quasi-ordered label set. Our proof builds on a recent structure/non-structure dichotomy for the model theoretic notion of monadic dependence by Dreier, Mählmann, and Toruńczyk. Through the non-structure characterization by forbidden induced subgraphs, we show that every hereditary $2$-WQO graph class is monadically dependent. Leveraging the Ramsey-theoretic structural properties provided by monadic dependence, we then establish bounded clique-width by ruling out the existence of large well-linked sets, which are the canonical obstructions for clique-width.

2026-07-12T22:03:25Z Julien Duron Nikolas Mählmann Szymon Toruńczyk