arXiv weekly literature review

Proof assistants and mechanized formalization · primary corpus · published 2026-07-13T23:16:49Z
Nikolai Kudasov, Violetta Sim, Benedikt Ahrens
arXiv categories: cs.LO, cs.PL, math.CT

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.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-14T00:15:23Z
Jam Kabeer Ali Khan, Petros Markopoulos, Nico Lehmann, Ranjit Jhala
arXiv categories: cs.PL, cs.LO, cs.SE

SMT-based program verifiers are hamstrung by two problems: expressiveness, because predictable verification restricts to the boundaries of SMT decidability, and trust, because the solver is a large, unverified artifact whose soundness bugs may quietly compromise every tool built on it. We present FLEX, a foundational Constrained Horn Clause (CHC) solver implemented in LEAN, that reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code, via three contributions. First, FLEX encodes CHCs as plain LEAN propositions where the Horn variables are existentially bound predicates, and shows how to implement CHC solvers as tactics (meta-programs) that compute kernel checkable proofs of the CHC propositions. Second, we show how to implement two verified CHC generators in LEAN: a Floyd-Hoare style generator for an imperative language, and a refinement-type-based generator for a functional calculus, which can be composed with the solving tactics to yield the first end-to-end foundational CHC-based verifiers. Finally, we show how FLEX allows us to leapfrog the expressiveness limitations of SMT by unleashing LEAN's entire ecosystem of proof machinery to prove arbitrary functional correctness properties of various low-level Rust libraries using the FLUX refinement type checker, and demonstrate the viability of FLEX as a trustworthy CHC backend, by showing it automatically discharges 95.7% of the CHCs from FLUX's benchmark suite.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-14T11:37:25Z
Lea Trogni, Gabriele Cecilia, Alberto Momigliano
arXiv categories: cs.LO

We formalize strong barbed similarity for the pi-calculus in the Beluga proof assistant, completing a line of work addressing the Concurrent Calculi Formalization Benchmark. By extending previous developments to include replication, we give a coinductive encoding of behavioral equivalence based on barbs and internal actions. Using Beluga's copattern-based coinduction, we obtain concise and compositional proofs, including compatibility properties and a context lemma characterizing barbed precongruence. The case study demonstrates the effectiveness of combining HOAS and coinductive reasoning for mechanizing concurrent calculi.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-14T11:37:57Z
Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Maria Júlia Dias Lima, Temur Kutsia, Marcos Mercandeli-Rodrigues
arXiv categories: cs.LO

In syntactic anti-unification, one is concerned with finding the commonalities between terms, while (uniformly) abstracting their differences. The original goal of anti-unification development in the seventies was to automate inductive reasoning. Recent applications of anti-unification techniques include efficiently transforming sequential code into parallel code, detecting code clones, and preventing software failures. Previous work addressed the elements required to verify, in the Prototype Verification System (PVS), termination and soundness of a functional algorithm based on inference rules for syntactic anti-unification. This paper dissects all aspects required to formally establish the completeness of the rule-based algorithm, highlighting the significant differences in the formalizations of anti-unification and unification.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-14T11:38:14Z
Mathews George, Kathrin Stark
arXiv categories: cs.LO

Autosubst enables automatic equality-checking up to the sigma-calculus for assumption-free equalities, allowing users to avoid cumbersome reasoning about de Bruijn indices. While effective in many cases, this approach is inapplicable when matching against typing rules, reduction relations, or lemmas, requiring users to either phrase typing rules in a way that they work with Autosubst or even stating explicitly an alternative de Bruijn term. But even without beta-reduction, solutions of matching may not be unique. This paper presents a work-in-progress method for automatically pattern matching against assumptions, evaluated on standard case studies including the POPLMark and POPLMark Reloaded challenges.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-15T05:40:08Z
Kwing Hei Li, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
arXiv categories: cs.LO, cs.PL

Probabilistic programs are important for many applications. For security applications in particular, one is interested in establishing properties that hold in the presence of arbitrary adversaries, i.e., unknown pieces of code. We present Elton, a higher-order separation logic for reasoning about higher-order probabilistic programs utilizing unknown adversarial code. Elton incorporates novel logical facilities for specifying invariants over distributional properties using delayed samplings at the language level, and a new kind of separation-logic predicate called urn resources at the logic level. We show that these extensions are sound and can be erased back to a standard call-by-value semantics. Combined with other features, e.g. invariants and ghost resources, Elton is expressive enough to prove error bounds on a wide range of security examples, some of which are beyond the scope of previous techniques. All proofs are mechanized with the Rocq proof assistant and the Iris separation logic framework.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-15T07:32:07Z
Ho-Lin Chen, Xiang Huang
arXiv categories: cs.LO, cs.DC, cs.ET, eess.SY

We present Ripple, an open, AI-formalized Lean 4 framework for the mathematics of computing with chemical reaction networks (CRNs) -- one extensible, machine-checked development that gathers several strands of the field into a single setting, and is built to grow. It formalizes: the theory of which real numbers a CRN can compute -- a single Lean definition of real-time CRN computation, the class of reals it captures, and the compilation pipeline (a GPAC / polynomial-ODE layer, a dual-rail compiler, and four stages down to large-population protocols) that realizes them, built so that adding a new number is a plug-in; three landmark population-protocol majority algorithms -- approximate, exact, and self-stabilizing exact majority; the stochastic-to-deterministic bridge, through three machine-checked versions of Kurtz's mean-field theorem; and two classical Turing-completeness results -- Bournez--Graca--Pouly for the deterministic GPAC and Soloveichik--Cook--Winfree--Bruck for stochastic CRNs. Each of these is verified to depend on exactly the three Mathlib foundational axioms, with no sorry. Along the way the formalization repaired genuine, previously unnoticed gaps in published proofs -- a compilation step that can transiently leave the unit interval, and an algebraic-number construction that silently rests on Catalan's conjecture -- and surfaced a sharp open problem about when a holonomic series admits an exact, rational-data polynomial-ODE encoding. The whole development is open and every proof is kernel-checked, so the results can be independently re-verified; and because it was written predominantly by AI agents using only publicly available models, the workflow that produced it can be reproduced with the same public toolchain.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-16T09:43:01Z
Kenji Tokuo
arXiv categories: cs.LO, math.LO

This paper determines the structural and proof-theoretic consequences of the forcing condition in relational quantum modal logic, under which every modal transition available at a world is also available at every world compatible with it. We prove that modal successor sets are constant on compatibility components, so boxed truth sets belong to the Boolean algebra of unions of these components. The relation holding exactly between worlds in the same component assigns to each stable proposition its greatest lower and least upper approximations by unions of components, and in hard superselection models these are exactly the approximations by central propositions. We adopt local validity for sequents with multiple conclusions to give a semantics for modal excluded middle on frames with several components. A connectedization obtained by adding one point then shows that component frames, equivalence frames satisfying the forcing condition, and connected compatibility frames with universal modal accessibility have the same logic for sequents with one conclusion. Finally, maximal consistent pairs yield a canonical model, and the calculus obtained by adding T, 4, and B is proved sound and complete for the three frame classes. These results characterize the logical scope of the forcing condition and establish a complete proof theory for component modalities.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-16T13:46:33Z
Julia Dijkstra, Benedikt Ahrens
arXiv categories: cs.LO

We present a formal verification of an abstract transition-system presentation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure in the Rocq proof assistant. Following Nieuwenhuis et al., SAT solving is modeled as a set of rule-based transitions between states rather than as a concrete algorithm. We formalize the syntax and semantics of propositional formulas, define the classical and base DPLL transition systems, and prove their key metatheoretic properties. In particular, we establish correctness and completeness with respect to satisfiability, and we prove termination by showing that the transition relation is well-founded. The formalization extends the original abstract system by also including the pure literal rule. Building on the verified transition system, we introduce an abstract notion of strategy and derive a terminating solver from any strategy satisfying suitable conditions. We then implement a concrete strategy in Rocq and show that it satisfies the strategy specification.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-16T16:22:59Z
Xueying Qin, Marco Peressotti, Fabrizio Montesi
arXiv categories: cs.PL

Choreographic programming (CP) is a programming paradigm for the correct-by-construction development of concurrent and distributed systems: programmers write the intended overall behaviour of a system from a global perspective in a choreography, which is then automatically compiled into communicating endpoint programs by a procedure known as endpoint projection (EPP). The central promise is that the projected endpoint programs, when executed together, are behaviourally equivalent to the source choreography. Fulfilling this promise becomes delicate for expressive CP languages. Existing mechanisations of CP treat only restricted fragments, while textbook and general purpose language implementations with rich features leave crucial interactions informal. In particular, general branching in knowledge of choice, general recursion, and nondeterministic choice in choreographies have not yet been integrated in a machine-checked theory. We present Mech, a new mechanisation of CP in Lean 4 that captures these features. There are two central technical challenges in our development of Mech. First, the sketched semantics from the literature does not correctly capture how nondeterministic choice interacts with concurrency. We therefore formulate new semantics that align nondeterministic choreographic executions with the behaviours of projected endpoint programs. Second, managing all these features in proofs is complex. We address this by uncovering new algebraic laws for choreographies, the operators used in their semantics, EPP, and their combinations. Using our development, we prove completeness and soundness of EPP and derive communication safety and deadlock-freedom for projected networks, yielding the most extensive mechanised theory of CP to date.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-17T05:05:31Z
Karen Sargsyan
arXiv categories: cs.LO, cs.AI, math.CT

Topos causal models recast causal inference inside a topos: a causal world is a presheaf, an intervention is a characteristic map into the subobject classifier, and reasoning is carried out in the intuitionistic internal language. We give the first machine-checked account of this 1-topos core, in Cubical Agda, over a previously verified probability monad and do-calculus. We build the classifier of sieves and realise the intervention $\mathrm{do}(X := x_0)$ as a characteristic map with its classification theorem; prove the sheaf gluing of independent mechanisms, which the source asserts but never proves; and machine-check the Kripke-Joyal forcing clauses of the internal language. In the modal layer we find and repair a gap: the three standard Lawvere-Tierney axioms do not force a closure operator. With the missing law restored, we exhibit the double-negation topology as a concrete instance and show that interventions and Pearl's rules are stable under every topology. Transportability of a counterfactual across a cover of regimes then coincides with this $j$-stability, understood as invariance across the cover. We further add a phenomenon the programme does not consider: a machine-checked contextuality obstruction, where pairwise-consistent local data admit no global model. The development assumes no axioms and typechecks under Agda's --safe flag, with the ordered field discharged concretely at $\mathbb{Q}$; the scope is the presheaf (1-topos) fragment, with type-level sheafification and the directed lift left to future work.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-18T10:18:43Z
Jacob Kowalczyk, Jindrich Zapletal
arXiv categories: math.LO

We prove the consistency of Zermelo--Fraenkel set theory with the Axiom of Dependent Choices, no Vitali sets and a large fragment of the Boolean Prime Ideal Theorem.

arXiv abstract · PDF

Proof assistants and mechanized formalization · primary corpus · published 2026-07-18T15:40:06Z
Hongqin Lyu, Junxing Dong, Yonghao Wang, Zhiteng Chao, Tiancheng Wang, Huawei Li
arXiv categories: cs.AR, cs.LO

Formal verification with interactive theorem provers can provide strong correctness guarantees for register transfer level designs, but applying it to existing SystemVerilog code requires substantial manual effort in semantic modeling and proof construction. This paper presents Rtl2lean, a framework that automatically translates RTL designs into executable Lean 4 models and builds a hierarchical theorem library for subsequent verification. The generated model represents hardware execution as a pure state transition function, while a four layer theorem framework captures combinational semantics, sequential updates, single cycle behavior, and reachability and invariants. When a high level property cannot be discharged by the existing theorem base, an LLM based proving loop proposes intermediate lemmas from the current proof context and Lean feedback. Only lemmas accepted by the Lean kernel are added to the reusable lemma pool. Experiments on six SystemVerilog designs generate 403 theorems, all of which are successfully checked by Lean. Among 358 foundational lemmas, 287 are available for automatic reuse, yielding a reusable lemma ratio of 80.2 percent. The results demonstrate that Rtl2lean can construct machine checked RTL proof libraries with low checking overhead and substantial cross property lemma reuse.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-07-14T21:58:52Z
Marcus J. Min, Mike He, Zhaoyu Li, Zixuan Yi, Sharad Malik, Aarti Gupta, Xujie Si, Osbert Bastani
arXiv categories: cs.AI, cs.CL, cs.LG, cs.PL

Autoformalization translates informal natural language into formal, machine-verifiable languages. While most work focuses on individual statements, real formalization efforts are inherently theory-level: they require an entire web of axioms, definitions, and lemmas before target theorems can even be stated. In this position paper, we argue for theory-level autoformalization: formalizing complete theories, including all their inter-dependencies, as structured libraries. We examine the significance of this shift, address alternative views, identify open challenges, and propose three promising paths forward. Our survey of autoformalization is available at https://github.com/marcusm117/Awesome-Autoformalization.

arXiv abstract · PDF

Formalized mathematics and autoformalization · selected cs.SE · published 2026-07-14T22:12:14Z
Hongyi Liu, Madhusudan Parthasarathy, Adithya Murali
arXiv categories: cs.SE, cs.AI

Formal contracts are essential for software testing and verification, yet writing them remains labor-intensive and error-prone. LLMs offer a promising path toward autoformalization: synthesizing executable assertions from natural-language specifications and thereby bridging the gap between informal developer intent and formal executable specifications. We present Monty: an autoformalization framework for assertions that tackles the challenges of expectations of validity of assertions and ambiguity in natural-language. Our techniques are based on filtering formalizations using a novel conformance score metric and validity scores obtained from testing the code against formalized assertions. We evaluate our approach on 541 assertion-generation tasks derived from 22 collection-like Java classes, and show that our technique produces the ground truth more reliably (improving upto 20 points in precision on average) than when using LLMs naively to translate assertions.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-07-18T23:10:00Z
Neel Somani
arXiv categories: cs.AI, cs.LG, cs.LO

Mathematicians distinguish proofs that explain, simplify, or introduce a nonstandard route, but these judgments are difficult to operationalize. We study a deliberately narrower construct: time-relative proof-route nonstandardness in formal mathematics. For a Lean theorem, PriorProof extracts the dependency footprint of its elaborated proof term and scores the weighted surprisal of that footprint under a retrieval-conditioned, hierarchically smoothed prior built only from an earlier quarterly snapshot of Mathlib. The method requires no hand-built technique ontology and no human labels: statement retrieval is learned from proof-derived contrastive pairs, while the scored object is read mechanically from proof terms. In a blinded topology study, 100 presentations collapse to 76 distinct underlying pairs: 12 canonical contrasts shown three times for consistency screening and 64 distinct stratified pairs. Against the majority of three retained domain raters, PriorProof agrees on 53/76 pairs (69.7%, Wilson 95% CI 58.7-78.9%), including 11/12 canonical pairs (91.7%, 64.6-98.5%) and 42/64 stratified pairs (65.6%, 53.4-76.1%). Score-gap quartiles are nonmonotone after repeat collapse; the endpoints are 12/19 (63.2%, 41.0-80.9%) in the smallest-gap bin and 16/19 (84.2%, 62.4-94.5%) in the largest, supporting an endpoint-calibration tendency rather than a resolved staircase. The best language-model condition agrees on 60/76 pairs (78.9%, 68.5-86.6%); on paired outcomes, PriorProof alone is correct on 8 pairs and the model alone on 15 (exact two-sided McNemar p = 0.210), so the difference is not established at this sample size. We therefore present PriorProof not as a replacement for expert or model judgment, but as a decomposable, time-anchored signal whose score gap provides an interpretable reliability indicator.

arXiv abstract · PDF

Formalized mathematics and autoformalization · primary corpus · published 2026-07-19T10:20:53Z
Kenji Tokuo
arXiv categories: quant-ph, math.LO

QBism interprets quantum theory as a normative discipline for an agent's probability assignments and their revision across possible experience. This paper develops a logical formalization of that picture. A well-formed core datum consists of an admissible prior space, a finite family of actual measurements, Born kernels, and update kernels. For each such datum, we introduce a guarded dynamic language for histories and posterior states and prove a global reduction theorem. We next consider effectively semialgebraic data over an effectively presented real closed field. For data in this class, we translate the fragment without dynamic operators into first-order formulas in the corresponding language of ordered rings, thereby reducing validity to first-order reasoning over real closed fields. Together, the reduction and first-order translation yield a sound and complete recursive calculus and a decision procedure for validity. Finally, assuming a symmetric informationally complete (SIC) reference measurement, we show that quantum theory in finite dimensions realizes the framework through SIC coordinates, POVMs, and quantum instruments. We also prove that the corresponding SIC image satisfies the standard qplex geometry conditions, namely the consistency bounds and the lower polar condition, and that under explicit coefficient field hypotheses the resulting quantum datum is effectively semialgebraic.

arXiv abstract · PDF

Program verification, analysis, and software security · selected cs.SE · published 2026-07-13T09:21:38Z
Yiming Zhang, Jiangrong Wu, Yuhong Nan
arXiv categories: cs.SE, cs.CR

Data-flow analysis is foundational to Android app privacy and security auditing. Recent coding agents can assist with non-trivial source-to-sink data-flow analysis tasks by searching, reading, and reasoning over repository code. However, when these tasks are executed as a batch workload, current agentic analysis setups incur substantial re-analysis cost. Agent instances assigned to different taint sources may inspect shared code fragments, because code reuse in the target app can cause different data-flow paths to converge on shared program logic. Since these agent instances are context-isolated, analysis of these shared code fragments can be repeated within a batch, unnecessarily consuming API budget and limiting scalability. We propose FlowArk, a knowledge-reuse system that reduces re-analysis cost in batch agentic data-flow analysis by making knowledge from completed analyses available to later agent instances. Specifically, FlowArk distills completed analysis histories into reusable knowledge candidates, packages these candidates into matchable knowledge entries, and injects matched entries into a later agent instance's context. We implement FlowArk on OpenCode and evaluate it on 4,685 source-to-sink data-flow analysis tasks from 50 open-source Android apps. Compared with standard OpenCode, FlowArk-enabled OpenCode maintains comparable analysis quality while reducing end-to-end API cost by 26.83%. In addition, under a USD 100 budget, FlowArk completes 36.66% more tasks (1,060 vs. 776).

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-13T11:41:13Z
Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti
arXiv categories: cs.LO, cs.PL

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.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-13T14:02:55Z
Alexandre Moine, Sam Westrick, Joseph Tassarotti
arXiv categories: cs.PL

We present Parcas, a concurrent separation logic for verifying the parallel time complexity of fork-join programs. In order to abstract from the specifics of the machine, time complexity for parallel programs is given in terms of two metrics: the work, measuring the total number of operations, and the span, measuring the longest chain of sequential dependencies. Together, these two metrics determine the running time on any number of processors. For proving bounds on the work and span, Parcas is equipped with work credits and span credits, logical devices that represent permissions to incur costs. Work credits are a straightforward adaptation of time credits, a standard tool for bounding time complexity of sequential programs, and can be split additively between parallel tasks. Span credits, however, require a fundamentally different treatment. Indeed, the span of the parallel composition of two tasks is the maximum of the span of the two tasks. To account for this, we propose a rule for duplicating span credits at fork points, with each copy tagged by a logical task identifier that restricts which task may spend them. A transfer rule allows unused span credits to be forwarded across sequential compositions to subsequent tasks. The logic is expressive enough to give modular, higher-order specifications for common parallel primitives such as a parallel for loop and a tabulate function. We demonstrate Parcas on several case studies, including parallel prefix sums, parallel merge sort, and a variant of Treiber's lock-free stack that mixes concurrency with parallelism. All the presented results are mechanized in the Rocq prover using the Iris separation logic framework.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-13T14:33:08Z
Alexandre Moine, Sam Westrick, Joseph Tassarotti
arXiv categories: cs.PL

Large language models are increasingly used to find bugs in real-world programs, but they also produce a flood of false alarms that waste developers' time. We propose a method to prevent these false alarms by requiring an LLM to accompany each bug report with a machine-checked proof, in a program logic, that the reported bug is real. We follow the approach of incorrectness logics, whose under-approximate reasoning establishes that a claimed behavior is genuinely reachable, and hence a true positive. In our case, however, the logic must model a realistic programming language, have a mechanization so that proofs can be checked, and be complete, so that no real bug is ruled out for want of a derivation. We present Mizzle, an incorrectness separation logic for concurrent programs written in a substantial subset of OCaml, parametric in the notion of incorrectness. We mechanize Mizzle in the Rocq proof assistant on top of the Iris framework, and we prove that it is both sound (that is, it never justifies a false alarm) and complete (that is, every incorrect execution admits a derivation). We instantiate Mizzle with three notions of incorrectness: stuckness (triggering undefined behavior), the non-linearizability of a data structure, and the presence of a race. As a proof of concept, we illustrate how an LLM can use Mizzle in order to certify the existence of a bug.

arXiv abstract · PDF

Program verification, analysis, and software security · selected cs.SE · published 2026-07-13T19:10:10Z
Zedong Peng, Chenggang Wang, Shangyue Zhu
arXiv categories: cs.CR, cs.SE

Large language models (LLMs) frequently generate code with security vulnerabilities, yet these weaknesses are rarely isolated: they often span multiple concern areas simultaneously, reflecting the cross-cutting nature of security in software. We present a framework that combines security-oriented Metamorphic Relations (MRs) with Association Rule (AR) mining to detect vulnerabilities in LLM-generated code, uncover their co-violation structure, and trace that structure back to prompt-level risk factors. We define nine MRs covering major CWE categories, including SQL injection, XSS, command injection, path traversal, hard-coded credentials, weak cryptography, and memory-safety errors, and apply them using an LLM-based judge to 3,700 code snippets generated by five open models from the LLMSecEval benchmark. The results show that 68.8% of snippets violate at least one MR, with hard-coded credentials (79.1%) and command injection (74.4%) among the most prevalent applicable failures. AR mining reveals strong cross-cutting co-violation patterns, notably that XSS and weak cryptography co-violations predict hard-coded credentials with 82.5% confidence (lift = 3.23), along with tightly coupled clusters linking authentication, credential handling, and cryptographic weakness, as well as input-handling and memory-safety failures. We then perform prompt-level risk analysis and find that database- and authentication-related prompts are strong predictors of broad cross-cutting insecurity, while 65.5% of prompts yield consistent violation outcomes across all five models. These findings show that insecure code generation is not merely a collection of independent defects, but a structured and prompt-conditioned phenomenon, motivating cluster-aware verification and prompt-level intervention for safer LLM-assisted programming.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-14T02:32:06Z
Alexander Y. Bai, Joseph Tassarotti
arXiv categories: cs.PL

Recent work has developed many techniques for formally verifying probabilistic programs. However, existing verification frameworks for probabilistic programs are restricted to idealized languages designed for verification. As a result, they cannot be used to verify off-the-shelf probabilistic programs written in standard languages. In contrast, for non-probabilistic programs, a number of verification tools now support verifying realistic code written in widely used languages such as Go, C, and Rust. To verify probabilistic programs written in these languages, it would be useful to be able to reuse, as much as possible, the extensive development work that has gone into such tools. This paper presents Alerus, a framework for verifying probabilistic Rust programs. Alerus is based on Verus, a verification tool for Rust that supports SMT-based automation and separation-logic-inspired reasoning features. Alerus extends Verus with support for probabilistic reasoning while retaining these expressive features. To do so, Alerus uses a lightweight encoding of probabilistic error credits, a form of ghost state for randomized reasoning introduced in the Eris program logic. By deriving an appropriate specification using error credits, Alerus supports verifying the correctness of randomized sampling algorithms. We use this technique to verify several sampling routines for discrete distributions, including samplers for the discrete Gaussian distributions, the alias method, and the fast loaded dice roller. We establish the soundness of our error credit extension by adapting VerusBelt, a recently developed logical relations model of Verus that encodes its features in terms of the Iris separation logic. To do so, we replace the use of Iris's standard weakest precondition in this model with Eris's probabilistic weakest precondition instead. The resulting soundness proof is fully mechanized in Rocq.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-14T09:06:02Z
Christina Gehnen, Dominique Unruh, Joost-Pieter Katoen
arXiv categories: cs.LO, cs.PL, quant-ph

Quantum weakest preconditions are a fundamental tool for program verification of quantum programs. Many variations have been reported in the literature. We revisit quantum weakest preconditions from the perspective of expected runtime analysis of quantum programs and introduce a novel pre-expectation framework that enables to reason about the preconditions of quantum programs without the need of an upper bound. This is particularly interesting for quantum programs involving reward statements. The overall goal is to analyze runtime behavior even in the case of programs with potentially infinite expected runtime. This paper presents several ways to do so, e.g., a program transformation such that the expected runtime of a quantum program can be expressed using the weakest pre-expectation calculus with rewards.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-14T11:21:43Z
Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti
arXiv categories: cs.LO, cs.PL

One strategy for reasoning about programs that have certain kinds of effects is to use program logics that provide specialized rules for reasoning about these effects. However, developing program logics requires skills that are distinct from those needed for using program logics, making the development of new logics challenging and less accessible. Moreover, when developing new logics, it can be difficult to reuse components from prior logics or combine support for different effects. In this paper, we propose an approach for operationally building extensible program logics based on effect handlers. Our starting point is an expressive program logic for reasoning about programs written in a pure, sequential language with support for effect handlers. Within this language, we implement handlers that model concurrency, distributed execution, and crash-recovery behavior. Then, by proving properties about these handlers, we extend the program logic and derive expressive rules for reasoning about these effects. In some cases, this approach leads to stronger reasoning rules than those found in prior program logics targeting these features. In addition, we develop a relational logic for proving contextual refinements between programs using effects. As with unary reasoning, handlers enable this relational logic to be developed in an extensible way.

arXiv abstract · PDF

Program verification, analysis, and software security · selected cs.SE · published 2026-07-14T12:23:22Z
Maha Ayub, Michael Konstantinou, Ahmed Khanfir, Nikolaos Tsantalis, Mike Papadakis
arXiv categories: cs.SE, cs.AI

Distinguishing semantic-preserving commits from changing ones remains an open challenge in software repository mining. While existing approaches detect refactoring commits accurately, they cannot ensure that a commit is purely semantic-preserving, without any interleaving behaviour-changing modification. This limitation can impact several tasks, such as debugging, fault localisation, bug dataset construction, rollback analysis, and bug fixes backporting. To fill this gap, we propose SemaDiff, a novel approach for identifying semantic-preserving commits through behaviour-based analysis; comparison of similar test execution on pre- and post-commit versions. As code impacted by the refactoring is often hard to test and different accross both versions, we propose generating additional calling methods to that code, which serve as testing target. Given a commit, SemaDiff analyses the diff to identify modified code and extracts unchanged dependent code that calls it. It then generates an additional dependent class using a large language model to exercise the changed code in both versions, and automatically generates tests for the dependent code. This way, we obtain the same tests for the different code versions, enabling the behavioural-difference detection. The commit is classified as semantic-preserving only if all generated tests produce identical outcomes across the two versions. To evaluate SemaDiff, we construct and annotate manually a dataset of 183 commits, gathered from well-known open-source Java projects. The obtained results show that SemaDiff distinguishes accurately semantic-preserving from -- changing commits in about 76% of the cases, with a 100% precision in semantic-changing commit detection.

arXiv abstract · PDF

Program verification, analysis, and software security · selected cs.SE · published 2026-07-14T12:52:56Z
Qiyuan Fan, Zhi Li, Junjie Li, XiaoFeng Wang, Bin Yuan, Deqing Zou
arXiv categories: cs.CR, cs.AI, cs.SE

Filesystem isolation in container ecosystems is often weakened by cross-boundary path misresolution, causing path traversal (PaTra) vulnerabilities. These vulnerabilities stem from insecure host-container interactions and have become increasingly pervasive as cloud systems mount shared resources, such as GPUs and agent workspaces, into containers to support AI workloads. Existing defenses remain inadequate. Kernel-level protections are intrusive, can destabilize system calls, and have therefore not been accepted into the Linux mainline. Detection methods rely on static rule matching or manual code auditing. Static rules can flag path-related functions but fail to capture the semantics needed to determine whether a host-container interaction exists, causing many false positives. Manual review requires domain expertise, making it costly, inefficient, and difficult to scale. To address this threat, we present Bulkhead, an automated framework that integrates large language models (LLMs) with formal methods for semantic vulnerability discovery and remediation. Bulkhead uses a multi-agent system to identify and repair PaTra vulnerabilities through multi-dimensional knowledge patterns generalized from known cases. It first applies high-risk functional patterns to locate entry points for cross-boundary interactions in containerized code, then uses call-chain patterns to recover the corresponding execution paths at suitable depth. The Detection pipeline analyzes these call chains against the application scenarios and threat model, identifying vulnerabilities such as missing security checks and TOCTOU flaws in cross-boundary interactions, and generating proof-of-concept (PoC) exploits for validation. These PoCs then guide patch generation. To ensure remediation correctness, the Patch pipeline performs assertion-driven verification using predefined model-checking templates.

arXiv abstract · PDF

Program verification, analysis, and software security · selected cs.SE · published 2026-07-15T04:49:05Z
Mingyang Sun, Guozhu Meng
arXiv categories: cs.CR, cs.SE

Large language models (LLMs) are increasingly applied to vulnerability detection due to their strong code comprehension capabilities, but most existing approaches rely on isolated functions or context extracted by fixed program-analysis rules. These methods cannot adaptively explore repository-level dependencies to gather sufficient context when vulnerabilities span multiple functions or files, compromising detection reliability. We present DREA (Decoupled Reasoning and Exploration Agents), a hypothesis-driven framework for repository-level vulnerability detection. DREA decouples reasoning from exploration through two collaborating agents: a planning agent backed by an advanced LLM that forms vulnerability hypotheses and directs the investigation, and an explorer agent powered by a lightweight model that retrieves repository-level context on demand. Goal-directed context acquisition is the primary source of detection improvement in this design, while offloading token-heavy exploration to the local model keeps inference economically tractable. To support evaluation, we construct RepoPairBench, a repository-grounded benchmark of validated Python vulnerability-fix pairs from real-world projects. Beyond binary detection accuracy, we introduce a reasoning correctness evaluation to assess whether a model's rationale matches the documented vulnerability mechanism. Across three LLMs, DREA improves Pair-Correctness from 19-26% to 30-42% while offloading over 93% of tokens to the explorer, reducing estimated billable API cost by a factor of 16-48. Reasoning correctness analysis further reveals that 26-55% of true positives, for both DREA and the function-only baseline, are correct predictions supported by flawed rationales, identifying security reasoning quality as a shared bottleneck for current LLMs.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-15T14:05:33Z
Saima Afrin, Md. Zahidul Haque, Antonio Mastropaolo
arXiv categories: cs.SE, cs.LG, cs.PL

The growing adoption of local inference frameworks such as Ollama has made it increasingly common for developers to run large code models on laptops and other resource-constrained hardware. In these settings, post-training quantization is essential for reducing memory footprint and enabling practical deployment, yet its impact on generated code remains insufficiently understood. We empirically evaluate six state-of-the-art quantization methods (GPTQ, AWQ, QuIP#, AQLM, BitsAndBytes, and GGUF) on two representative large code model families, Qwen2.5-Coder and CodeLlama, using the multilingual McEval and CoderEval benchmarks for Python and Java. We assess functional correctness (pass@1) together with maintainability, reliability, security, and structural complexity. We also introduce a novel analysis of robustness under varying prompt complexity, characterized by Shannon entropy and token length. Our results show that quantization techniques differ meaningfully in their impact on correctness and code quality. AQLM consistently matches or exceeds the full-precision baseline, whereas QuIP# exhibits the largest correctness degradation, particularly on complex prompts. Security attributes remain stable across models, benchmarks, and programming languages, while robustness to prompt complexity varies across techniques. These findings provide practical guidance for selecting quantization strategies for deploying large code models on resource-constrained hardware and highlight the importance of evaluating quantized models beyond functional correctness.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-15T16:08:36Z
Benedikt Bollig, Matthias Függer, Thomas Nowak, Paul Zeinaty
arXiv categories: cs.LO, cs.FL

We study model checking for an epistemic metric temporal logic with past, interpreted over finite Büchi automata under synchronous perfect recall. The logic is motivated by observation-based verification problems such as diagnosis and opacity, where an observer sees only a projection of an execution and reasons about events that may have occurred earlier. These requirements use no alternation between different agents' knowledge. We therefore consider the agent-alternation-free fragment, in which nested knowledge operators must refer to the same agent. We show that model checking for this fragment is EXPSPACE-complete. The lower bound already holds with one agent, one occurrence of the knowledge operator, and no non-trivial metric bounds. For the upper bound, we combine temporal test automata with perfect-recall observers. Because past formulas may have different truth values on indistinguishable histories ending in the same system state, the observer must track temporal automaton states in addition to system states.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-15T23:15:15Z
Thomas Lu, Qiancheng Fu, Kevin Batz, Oliver Bøving, Tiago Ferreira, Mark Moeller, Nate Foster, Alexandra Silva
arXiv categories: cs.PL

When designing a network, engineers must navigate trade-offs (e.g., one topology offers more aggregate bandwidth, another lower latency or better resilience) that demand reasoning about quantitative properties. We present a fast analyzer for quantitative network properties based on weighted NetKAT (wNetKAT), a domain-specific language that provides a semantic foundation for quantitative reasoning by modeling network behavior using weights drawn from a semiring. At the core of our development is the design of a symbolic data structure -- weighted symbolic packet programs (wSPPs) -- that compactly represent the semantics of weighted policies, for which a direct implementation would be intractable. We show how to compute all policy constructs symbolically; unsurprisingly, the crux is Kleene star, for which we design a tailored algorithm. We further develop trace-carrying Pareto semirings, which compute multi-objective frontiers together with the network paths that realize them. We formalize the development in Lean and provide an optimized Rust implementation. Being parametric on a semiring, our implementation covers both classical and quantitative analyses: we show that it is competitive with KATch, a heavily optimized Boolean-reachability verifier, and orders of magnitude faster than McNetKAT and Storm on probabilistic analyses. A case study comparing Fat-tree and Jellyfish data-center topologies shows the framework supports multi-objective design-time analysis.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-16T14:13:19Z
Milan Lopuhaä-Zwakenberg
arXiv categories: cs.LO, math.CO, math.PR

Model checking is the automated verification of properties (specified in some modal logic) in labeled transition systems (LTSs); it is an essential tool in ensuring software systems function as intended. State spaces of software grow exponentially, and heuristics are needed to ensure model checking remains feasible in real-world applications. Heuristics, in turn, require a good understanding on the typical behaviour of LTSs. In this paper, we use random graph theory to create a probabilistic model of large LTSs. From a theoretical analysis of the creation of large LTSs, backed by empirical data from the Model Checking Contest, we endow these models with realistic parameter values. Then, we analyze the asymptotic behaviour of this model under LTL and CTL, two modal logics popular in model checking. We show that, depending on the precise model, as the size grows to infinity we either have a convergence law (for every formula, the probability that it holds converges to a limit) or a 0-1 law (...and this limit is 0 or 1). We also discuss the theoretical complexity of determining these limits, and give algorithms for doing so. These results are the starting point towards a deep theoretical understanding of typical LTS behaviour, and highlight the promising applicability of random graph theory to model checking. \keywords{Model checking \and Random graphs \and 0-1 laws

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-16T17:27:28Z
Mishel Carelli, Bernd Finkbeiner
arXiv categories: cs.LO

We introduce Disintegration Temporal Logic (DTL), a new probabilistic temporal logic that can express a wide range of probabilistic hyperproperties, including probabilistic non-interference and perfect indistinguishability. DTL is based on the notion of measure disintegration from probability theory, which allows for conditioning probabilities on a finite or infinite sequence of events occurring during a program execution. This naturally supports reasoning about interacting stochastic systems, where complete executions of one component induce conditional probability distributions over another. We illustrate applications of DTL to systems interacting with stochastic environments, distributional properties of Markov decision processes, and probabilistic automata on infinite words, and discuss its relationship to existing probabilistic logics. While model checking Markov chains against full DTL is undecidable, we identify two decidable fragments that capture many hyperproperties of interest. The linear fragment admits a polynomial-time model-checking procedure based on linear-algebraic techniques and captures probabilistic information-flow properties such as perfect indistinguishability and history-based probabilistic non-interference. The qualitative fragment admits an automata-theoretic model-checking procedure that extends the standard algorithm for $\mathit{HyperCTL}^*$ with reasoning about bottom strongly connected components.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-16T18:33:42Z
Hazel Torek, Long Tien Nguyen, Priyam Gupta, Jenna DiVincenzo, Jonathan Aldrich
arXiv categories: cs.PL

Unfolding expressions, which temporarily unfold a predicate to leverage its owned fields when evaluating a heap-dependent expression, and pure functions, which are heap-dependent functions that can be used in specifications, are used in deductive program verifiers based on implicit dynamic frames, such as Gradual C0, Gobra, Nagini, and SnaKt, to increase the modularity of specifications involving ownership. In this paper, we present the formal semantics for unfolding expressions and pure functions for a static verifier using symbolic execution, extend it for a gradual verifier, and provide a proof of soundness. To support Gradual C0, our proof is in the setting of gradual verification, a deductive program verification system that combines static and dynamic verification to allow partial specifications. However, because the gradual verifier is a conservative extension of a static verifier, our results also apply to static verifiers that use symbolic execution, such as the Silicon symbolic execution backend for the Viper verification infrastructure used by Gobra, Nagini, and SnaKt.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-17T11:43:47Z
Anders Alnor Mathiasen, Amin Timany, Lars Birkedal
arXiv categories: cs.PL

We present a new ML-like programming language Yarrow with algebraic effects and region-based memory management. Reconciling these programming language features into one language is challenging: the non-local control flow of algebraic effects break the stack discipline of function calls and returns that region-based memory management relies on, and multi-shot effect handlers break the invariant that regions can be exited at most once. We present a program logic, called Yarrow Logic (YL), that supports safe and modular reasoning about regions in the presence of one-shot and multi-shot effect handlers. We prove the logic sound w.r.t. the operational semantics of Yarrow which is inspired by the runtime of OCaml but refined for regions. We use YL to prove correctness of a number of case studies with algebraic effects, including checkpointing, asynchronous computation and a LIFO data structure implementation. Since all memory locations used in these case studies are allocated in regions, these case studies avoid using the less efficient garbage collected heap memory. We have formalized Yarrow's operational semantics, the Yarrow program logic, and all our case studies using the Iris separation logic framework on top of the Rocq Prover.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-17T13:18:18Z
Giacomo Boldini, Luca Negrini, Luca Olivieri, Pietro Ferrara
arXiv categories: cs.PL, cs.SE

Advanced static program analysis requires reasoning on the semantics of non-trivial program behaviors (e.g., pointers and complex data structures such as lists and sets, functions, and objects) and how they affect the memory. In most programming languages, static and dynamic allocations are typically managed by the stack and the heap, respectively. However, how allocations behave and how the memory is managed at runtime can vary significantly depending on the programming language being analyzed. Proper handling of these aspects is essential, as an accurate memory model enables the detection of critical issues such as buffer overflows and underflows, use-after-free errors, and null pointer exceptions prior to execution, that is, before such erroneous behaviors occur. In this paper, we propose and formalize a generic memory framework to handle stack and heap memory during the analysis, that is able to support various behaviors from different programming languages (e.g., C, C++, Java, and Python), while remaining parametric, allowing different memory and value analyses to be independently chosen and combined. It relies on the Abstract Interpretation theory and enables sound approximation of different memory models and program behaviors. We introduce a split state abstraction that separates value and memory analyses into two modular abstract domains. These domains interact through a set of memory identifiers, along with a set of operations defined by the domains to manipulate them, allowing the framework to capture both value information and structural memory relationships.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-17T22:16:17Z
Hanxi Chen, Noam Zilberstein, Andrew C. Myers, Alexandra Silva
arXiv categories: cs.PL, cs.LO

In the context of probabilistic programs, an oblivious adversary resolves nondeterminism without seeing the outcomes of random draws. Obliviousness is a common assumption in online algorithms and distributed protocols, but the complex interaction between random draws and adversarial choices makes it challenging to reason about correctness. While there has been significant progress toward reasoning about programs that combine randomization with nondeterminism, most of the work has focused on the adaptive model, whose omniscient view of program state is too powerful to establish correctness for certain classes of programs. We introduce Oblivious Probabilistic Outcome Logic (opOL), a new logic for reasoning about probabilistic programs with nondeterminism controlled by an oblivious adversary. Building on Outcome Logic and Probabilistic Separation Logic, opOL models adversarial choice as a resource and uses probabilistic independence to ensure that random outcomes are hidden from the adversary. The opOL proof system provides expressive and compositional rules for case analysis on both random and nondeterministic outcomes, and for proving almost-sure termination. Expressivity is tested through several case studies, including a paging algorithm and a leader election protocol. The opOL metatheory and case studies are mechanized in Lean 4.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-19T12:23:43Z
Akihisa Yagi, Ken Sakayori, Naoki Kobayashi
arXiv categories: cs.PL

WebAssembly is a stack-based imperative language widely used to develop safe and efficient Web applications. In this paper, we propose an automated static verification method for a subset of WebAssembly using a constrained Horn clauses (CHCs) satisfiability solver. Our main challenges are how to handle indirect function calls effectively and how to analyze huge panic handlers. A naïve approach to the former problem would be to model a function reference table as an array of functions' entry points, but it would suffer from having too many candidates for indirect calls, resulting in a large case analysis. We address the problem by utilizing type information and filtering candidates for each indirect function call. For the latter problem, a panic handler, which is a function that is called when an error occurs, can be very large and complex. We mitigate this problem by summarizing the panic handler using control-flow analysis. We confirmed the effectiveness of our approach through preliminary experiments.

arXiv abstract · PDF

Program verification, analysis, and software security · primary corpus · published 2026-07-19T15:15:51Z
Liam Davis, Duo Zhou, Huan Zhang, Guy Katz, Clark Barrett, Haoze Wu
arXiv categories: cs.LG, cs.AI, cs.LO

In this work, we investigate the effect of lookahead branching strategies in neural network verification. We present a general recipe to integrate lookahead into any branch-and-bound verifier and demonstrate how one of the current state-of-the-art branching heuristics, FSB, can be viewed as a special instantiation of the lookahead branching strategy. We also describe how, in addition to improving the quality of branching decisions, lookahead can generate additional lemmas that accelerate verification. We instantiate the method in two representative branch-and-bound-based verifiers (Marabou and $α$-$β$-CROWN), and demonstrate that lookahead leads to consistent speedups in verification time and up to $57\%$ more solved instances. Code is available at https://github.com/ai-ar-research/lookahead-branching.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-13T09:48:19Z
Raphaël Sterbac, Jonathan Sterling
arXiv categories: cs.PL, cs.LO, math.LO

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.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-13T22:53:56Z
Max Carroll, Anil Madhavapeddy, Cyrus Omar
arXiv categories: cs.PL

Development tools report what type an expression has, but not why it has that type. This paper develops a theory of type slicing: a programmer selects a term, queries any part of its type information, and receives a program slice that is sufficient to reproduce the queried type. We formulate type slicing for bidirectional type systems, where synthesis slices explain the type a term synthesises and analysis slices explain the type expected by its surrounding context. The theory applies to any bidirectional system equipped with precision orders on types and terms satisfying a downwards static graduality property. We develop the metatheory over a core calculus with holes, products, sums, and explicit polymorphism, based on the Hazelnut and marked lambda calculi. We prove that every query has a minimal slice and that refining a query monotonically shrinks its minimal slices. We then show how to calculate these slices both exactly and approximately. Finally, integrating type slicing with error marking theory extends these results to arbitrary ill-typed programs, so a single mechanism explains both types and type errors in complete, incomplete, and erroneous code. The metatheory is mechanised in Agda, and a linear-time approximation of type slicing is implemented for the Hazel programming environment.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-14T05:46:22Z
Paolo Bottoni, Anna Labella, Ion Petre
arXiv categories: cs.LO, cs.FL

Reaction systems have evolved into a rich family of computational models differing in their treatment of multiplicities, resource management, concurrency, and state evolution. We introduce a unified semantic framework based on interval structures and interval-based transformation systems. The framework decomposes operational semantics into independent resource, production, update, and execution strategies, providing a common basis for describing, comparing, and constructing reaction-system variants. We show that classical reaction systems, restricted reaction systems, multiset reaction systems, reaction systems with concentration, and resource-preserving multiset reaction systems are all recovered as instantiations of the framework. Quantitative reaction systems are accommodated through an additional preprocessing stage. We further demonstrate that the framework naturally extends beyond reaction systems to other computational models, including Petri nets. The proposed framework provides a common semantic foundation for existing models and a flexible basis for developing and analysing new computational formalisms.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-15T10:06:45Z
Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu, Meven Lennon-Bertrand, Paul-André Melliès, Stephanie Weirich
arXiv categories: cs.LO, cs.PL

We contribute a new proof technique, based on domain theory, to prove key meta-theoretic properties of dependent type systems: definitional inversion properties, i.e. injectivity and no-confusion of type constructors. This proof technique is independent of normalisation, and indeed applies even for the "type-in-type" rule of Martin-Löf's original type theory. Our proof is the first to establish injectivity of type constructors for such a system in the presence of $η$ laws. More generally, the technique is motivated by, and intended for, the metatheory of systems such as Idris, Lean, or dependent Haskell, whose underlying type theory is known to be non-normalising, as well as projects such as MetaRocq or Lean4Lean, where Gödel's second incompleteness theorem means we cannot show normalisation of the object logic in itself. We showcase the method on a small type theory, then explain how it extends to more ambitious extensions.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-15T15:17:53Z
Diogo Simm, Fernando Lucatelli Nunes, Matthijs Vákár
arXiv categories: cs.PL

We analyse reverse-mode automatic differentiation (AD) for discrete probabilistic programs. Our construction is formulated in the framework of Combinatory Homomorphic Automatic Differentiation (CHAD), treating AD as a structure-preserving transformation of programs, guided by a denotational semantics. The main case study is the finite atomic distribution monad, whose computations have finite support and differentiable weights. The key point is that differentiating probabilistic programs requires cotangents to flow backwards not only through deterministic computations, but also through the probabilistic structure itself. We define the corresponding reverse-mode code transformation and prove its correctness, for handled real-output programs, by a categorical logical-relations argument. Although the paper focuses on finite discrete probability, the construction gives a reusable pattern for differentiating discrete-output algebraic effects, including finite multiset non-determinism (e.g., from fork-join parallelism), exceptions, and writer-style accumulation (e.g., for in-place accumulation of high-dimensional vectors). More broadly, we view this work as a foundational step towards extending CHAD to richer probabilistic languages and to other algebraic effects with handlers.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-15T19:45:03Z
Celia Mengyue Li, Steven Ramsay
arXiv categories: cs.PL

Two-sided type systems, introduced in POPL'24, are an extension of the traditional notion of type system that allows for stating and deriving typing judgements in which (a) assumptions can be made about the types of arbitrary terms and not only variables, and (b) conclusions can be made about any number of type assignments, and not exactly one. In this work, we investigate the logical foundations of two-sided type systems in the sense of the propositions-as-types paradigm. We introduce new two-sided type systems 2$λ$Int and 2$λ$Int$^{\sim}$ that correspond with Wansing's bilateral logic 2Int and its extension with Nelson's strong negation respectively. Going beyond the propositional case, we introduce 2$λ$HOL as an extension of Guevers' $λ$HOL, and we show its expressive adequacy, its consistency and that it satisfies both the existence property and its dual.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-17T11:40:25Z
Kengo Hirata, Takeshi Tsukada
arXiv categories: cs.PL, cs.LO, quant-ph

In contrast to a classical bit, which can only take the value $0$ or $1$, its quantum counterpart -- a qubit -- can exist in a superposition of $0$ and $1$. This is a superposition of data values, naturally raising the question of whether one can superpose not only data but also programs. For example, a particular superposition of programs, known as the quantum SWITCH, has attracted much attention, and its implementations and computational advantages have been studied extensively within the physics community. A naive way to control a program by a qubit is by means of a controlled operation. Given an operation $F$, this amounts to considering an operation that behaves as $F$ when the control qubit is $|1\rangle$, and as the identity operation when the control qubit is $|0\rangle$. This idea works well when $F$ is a unitary operation, but it is not well-defined for a general quantum channel. By contrast, the quantum SWITCH is free from the well-definedness issue. This contrast leads to the key insight of this paper: controlled operations and the quantum SWITCH should be regarded as different kinds of quantum control mechanisms. Building on this insight, we develop a novel quantum programming language with quantum control and measurement that can express the quantum SWITCH over quantum channels. Using a semantic analysis based on program transformations, we identify the source of the ill-behavedness of controlled operations as the \emph{correspondence problem}: a lack of coordination between the measurements performed in the then- and else-branches of quantum conditional branching. We address this problem with a linear type system that enforces alignment of the quantum operations used in the two branches, yielding a well-behaved language capable of expressing the quantum SWITCH.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-17T12:26:34Z
Valeria de Paiva, Thaynara Arielly de Lima
arXiv categories: cs.LO

This volume contains the proceedings of the 21st Workshop on Logical and Semantic Frameworks with Applications (LSFA 2026), held in Lisbon, Portugal, from July 18 to July 19, 2026. LSFA aims to promote techniques and results from the theoretical side, ranging from well-established ones such as lambda calculus and type theory to state-of-the-art ones such as machine learning, and provide feedback on integrating, implementing, and using such methods and results from the practical side.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-17T13:10:20Z
Kengo Hirata, Takeshi Tsukada
arXiv categories: cs.PL, cs.LO, quant-ph

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.

arXiv abstract · PDF

Programming-language semantics, types, and calculi · primary corpus · published 2026-07-17T15:39:23Z
Wenhao Tang, Shengyi Jiang, Aghilas Y. Boussaa, Sam Lindley, Bruno C. d. S. Oliveira
arXiv categories: cs.PL

Bidirectional typing makes use of local information flow between functions and arguments. Conventional bidirectional typing only supports unidirectional information flow, typically from functions to arguments, which is insufficient to infer first-class polymorphism. Existing work on improving information flow either has limited support for mixed information flow or requires ad hoc mechanisms that harm predictability. We propose Fresco, a novel bidirectional type inference approach to first-class polymorphism. Fresco enables local type information to flow back and forth between functions and arguments via skeletons, with ghosts representing unknown type information, and allows users to customise the direction of information flow by freezing. The flexible information flow of Fresco enables expressive and predictable inference for first-class polymorphism. We provide a declarative specification for Fresco, a simple type inference algorithm that is sound and complete with respect to the declarative system, and a prototype implementation that further generalises Fresco to infer modal effect types.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-13T14:53:37Z
Vinod Grover, Manjunath Kudlur
arXiv categories: cs.PL

We introduce a notion of convergence for the nodes and edges of a control-flow graph that captures whether a barrier placed at that location is guaranteed to synchronize all threads of a thread block in every execution. Convergence analysis lets a compiler determine when a barrier lies in a uniformly executed region and therefore avoid the code transformations otherwise required to implement thread-block barriers correctly on warp-synchronous hardware. We formalize convergent nodes, convergent edges, and well-synchronized programs; give two inference rules (a branch rule and a merge rule); and present a linear-time iterative work-list algorithm that propagates convergence information bidirectionally through the flow graph. We then describe refinements that improve precision using single-entry single-exit region information, path information, and thread-variance information.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-13T15:09:04Z
Shengyuan Yang, Charles Yuan
arXiv categories: cs.PL, quant-ph

Runtime assertions are a promising mechanism for testing and debugging quantum programs. But unlike the classical world, checking a quantum program that contains multiple assertions often requires using additional space or running the program additional times. For example, on current quantum hardware where mid-circuit measurement is restricted or costly, an assertion's pass/fail outcome cannot be revealed immediately. Instead, it is routed into an ancilla qubit during execution and read out by a terminal measurement. For a program with $n$ assertions, a naive strategy uses $n$ ancillas to learn all $n$ outcomes, while an alternative uses one ancilla but repeats program execution over $n$ rounds, checking one assertion per round. Both satisfy $S \cdot T = O(n)$, where $S$ is the number of ancillas and $T$ the number of executions: a fundamental time-space trade-off. Can one do asymptotically better? We reveal that the answer depends sharply on the information to be learned. Reporting the outcomes of all assertions requires linear complexity, but two partial-information tasks of detecting whether any assertion fails, and of identifying the first failing assertion, require only logarithmic complexity -- an asymptotic improvement. Moreover, the checking strategies for these tasks can trade time for space in useful ways. In this work, we formalize the complexity of checking multiple assertions in a quantum program. Using this definition, we establish its landscape of asymptotic lower bounds and constructive upper bounds. We confirm via a case study on Grover's algorithm that the resource costs of constructed strategies match theoretical predictions, illustrating the practical design space for quantum programmers.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-14T03:31:14Z
Zhuohao Zhang, Junkun Liu, Rui Yang, Yinzhi Cao, Ziyang Li
arXiv categories: cs.PL, cs.SE

Dynamic taint analysis (DTA) for interpreted languages like JavaScript and Python requires three capabilities: observing host-runtime operations, maintaining parallel taint states, and defining how taint propagates. Existing systems couple these capabilities within an instrumentation mechanism -- source-rewriting or engine-native -- either incurring high runtime overhead or demanding engine-specific embeddings. There is yet to be a runtime-independent abstraction of a general DTA that separates taint semantics and state transitions from how a host runtime executes them. We set out to develop a DTA engine that is extensible, performant, and accurate. To achieve this, we introduce a Shadow Virtual Machine executing alongside host runtimes that tracks multi-level taint, provenance, and cross-invocation context. We design Mystra, a declarative taint specification language with formal operational semantics. Mystra is designed to be language model friendly, and is equipped with validators enabling trustworthy automated synthesis of rules. Mystra is also the first to express higher-order function taint transfer declaratively. Further, Mystra rules are compiled ahead of time to a binary representation and dispatch in constant runtime. We implement our vision into a tool named Shar, which contains a shared core engine and instantiations on three runtimes: V8 in both Node$.$js and Chromium (embedding), SpiderMonkey (engine), and CPython (language). Accuracy wise, on SecBench$.$js (493 in-scope CVEs across four CWE categories), our V8 instantiation achieves 95.5% recall with zero false positives on patched-version testing. Regarding performance, the runtime overhead of Shar is 1.85$\times$ over vanilla Node$.$js on NodeMedic's benchmarks, and is 22.7$\times$ lower than NodeMedic-FINE on identical workloads, all the while producing 33.2% higher recall in its supported categories.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-14T15:51:46Z
Chong Li, Corinne Ancourt, Gaétan Hains
arXiv categories: cs.DC, cs.PL

This volume contains the ten peer-reviewed papers presented at HLPP 2026, the 19th International Symposium on High-Level Parallel Programming and Applications, held on 9-10 July 2026 at the Institut Henri Poincare in Paris, France. The symposium covers high-level approaches to parallel programming: programming models, languages, libraries, algorithmic skeletons, compilers, and runtime systems for multi-core, GPU, and distributed platforms. The 2026 edition extended this scope towards artificial intelligence, with new topics on the parallel programming and performance of AI systems and on AI-assisted generation of parallel code, and opened with a dedicated session on parallelism and AI. Papers were selected through a single-blind review process, with three Program Committee reviews per submission, and appear in the order of the symposium program. Edited by Chong Li, Corinne Ancourt, and Gaetan Hains.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-15T15:00:22Z
Niels Mündler-Sasahara, Hristo Venev, Dawn Song, Martin Vechev, Jingxuan He
arXiv categories: cs.PL, cs.AI, cs.LG

Languages with rich static semantics, such as Rust, provide stronger guarantees for AI-generated code, but their strictness makes generation more difficult. Off-the-shelf compilers can provide useful feedback post-generation, but does not guide intermediate generation steps, such as those during autoregressive LLM decoding. Constrained decoding intervenes earlier by rejecting invalid tokens during sampling, but requires white-box model access and costly reimplementation for semantic constraints. We introduce generative compilation, the first approach to obtaining compiler feedback on partial programs during generation. The core technical device is a sealor: a lightweight, mostly syntax-guided transformation that converts partial programs into complete ones that standard compilers can diagnose. It is designed such that possible-to-complete partial programs are never rejected, while preserving enough code context to catch genuine dead ends early. We construct such a sealor on a core Rust-like calculus and prove that it satisfies these properties, all mechanized in Lean. We extend it to the first partial-program checker for real Rust. We evaluate our method on challenging repository-level Rust coding tasks, across both frontier black-box and open-weight models. We show that generative compilation reduces non-compiling outputs and improves functional correctness, relative to standard post-generation feedback. It does so by detecting a broad range of errors close to their source and early during generation, thereby reducing errors cascades and enabling focused diagnostics. More broadly, generative compilation is a step toward making compilers a first-class citizen of AI-assisted programming active during generation, rather than a separate post-generation check.

arXiv abstract · PDF

Compilers, code generation, and programming tools · primary corpus · published 2026-07-19T19:43:14Z
Fot Nikolai, Vinarsky Alexander
arXiv categories: cs.SE, cs.PL

The paper investigates the possibility of predicting function-inlining decisions in compact compilers, source-to-source tools, and interpreters where the reuse of GCC or LLVM optimization infrastructure is impractical. The relevance of this work is determined by the need to transfer mature inlining heuristics to systems with limited compiler infrastructure, restricted runtime dependencies, and reduced access to target-specific analysis. Existing production compilers already contain strong inliners, but their decisions depend on internal intermediate representations (IRs), pass ordering, target models, and analysis stacks that are difficult to reproduce in lightweight systems. To overcome these constraints, we propose a portable inlining-prediction framework. Production compiler diagnostics serve as supervision; a separate extractor reconstructs caller-callee callsites, prepares sterile source snippets, normalizes them into a universal AST, optionally lowers them to a lightweight structural IR, and exports scalar features for model training. Thus, a trained predictor can be emitted as ordinary C code without a compiler-runtime dependency. To evaluate the proposed framework, we constructed a dataset comprising 336,938 callsites from fifteen open-source C projects, including 79,287 compiler-reported inline events. A comparison of several tabular models is performed using project-aware validation. Under leave-one-project-out validation, CatBoost reaches ROC-AUC 0.928 and PR-AUC 0.713; after threshold tuning, F1 improves from 0.670 to 0.729 and the false-positive rate drops from 0.192 to 0.084. Feature analysis shows that most signal is concentrated in source locality, explicit inline intent, callee size, side effects, branch and call structure, signature shape, and callsite argument shape.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-13T10:07:50Z
Chenglin Yu, Li Yin, Ying Yu, Qingxin Fan, RunyangRay Zhong, Hongxia Yang, Ming Li
arXiv categories: cs.AI, cs.PL

Enterprise agents must follow long-horizon, conditional, safety-critical standard operating procedures (SOPs). We compile machine-readable SOP constraints into executable pseudo-code and run them with a program-guided (PG) stack machine that pages the active frame while an LLM performs semantic execution. A three-arm SOPBench study across six models separates representation from runtime: compiled text never significantly hurts and gains up to 16.0 points where official prose underperforms. Runtime guidance is capability-gated. Two strong models independently show positive seven-domain PG contrasts (58:19 and 75:31 discordant pairs), whereas weak models are harmed. A full-program cursor ablation (active frame first, complete program retained) recovers much of the strong-model refusal gain; selective visibility adds a smaller improvement. Paired probe and audit measurements track this divide to spontaneous state discipline rather than reconstruction ability. On Bank the three primary arms rise from 70.4 to 86.4 to 92.8, with 100% refusal correctness. Practical guidance: compile first; enable active-frame paging only after a model-level discipline check.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-13T12:48:09Z
Sridhar Mahadevan
arXiv categories: cs.LG, cs.AI, math.CT

Agentic systems increasingly improve themselves by editing skills: prompts, rubrics, plans, tool contracts, examples, validators, and traces. Skill edits are not independent coordinates in a vector space: they are local repairs to structured artifacts whose effects are observed only after rollout, validation, and critique. Distinct edits can have the same immediate visible effect while differing in routing context, template state, guardrail scope, or future composability. The order of edits can matter as well: repairing a schema before a normalization rule need not be equivalent to applying the same edits in the reverse order. This paper introduces a new framework for skill optimization called LASKO, for Lie Algebroid SKill Optimization. LASKO models typed, anchored Markdown skills as the base category and available edit policies as sections of a controlled Lie algebroid with anchor $ρ$. The anchor maps an edit policy to its visible Markdown effect; the kernel $\ker(ρ)$ represents latent template, routing, or implementation structure; and the algebroid bracket measures noncommuting edit composition. As shown in the paper, LASKO achieves order-of-magnitude speedups in skill optimization in our preliminary benchmark results, primarily because it substitutes inexpensive Lie-bracket screening tests that run in microseconds, before investing in expensive validations that require running large language models. On a causal extraction from natural language task, LASKO achieved a speedup of almost $15 \times$ compared to a brute-force approach that validated all edits by running them through a DeepSeek V3.1 4-bit model with 671B parameters.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-14T00:16:28Z
Jean-Jacques Dubray
arXiv categories: cs.PL

Can large language models write faithful formal specifications of real systems, and does it matter whether they write in a formal language they have seen rarely or in a mainstream language abundant in their training data? We study this on SysMoBench, which grades a generated specification in four phases, the decisive one replaying execution traces captured from the running system. We add JS-SAM, its first non-formal backend, in which a specification is executable JavaScript written in the SAM pattern, a pattern whose semantics mirror TLA+, and run a controlled comparison that separates three variables an ordinary head-to-head entangles: the language, the specification contract (the shape the model must fill), and the prompt. The study spans four frontier models and three systems (an operating-system spinlock, a distributed lock service, and the Etcd Raft consensus implementation), with counterexample-driven repair. Three findings emerge. First, conformance against the real system is the only phase that discriminates among models; internal consistency is inexpensive to satisfy, and a specification that looks right is not thereby right. Second, once the comparison is drawn like for like, the specification contract, not the language, governs fidelity: JavaScript in the shape of the TLA+ transition relation is as faithful as TLA+. Third, a minimal contract carries transcription but not semantic derivation: at consensus scale the difficulty becomes understanding the protocol, which no contract shape and no language supplies. We frame executable JavaScript as a checkable specification substrate that complements, rather than replaces, the verification TLA+ provides, and present the study as a case study.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · selected cs.SE · published 2026-07-14T02:23:17Z
Xiaoning Ren, Yinxing Xue, Lei Ma, Yuheng Huang
arXiv categories: cs.SE, cs.AI, cs.CL

As Code Large Language Models (LLMs) become central to modern software engineering, their inherent stochasticity poses significant real-world risks, where even minor errors can lead to severe functional, security, or safety consequences. Reliable automation, therefore, demands the ability to distinguish between confident, well-supported predictions and stochastic guessing. However, existing uncertainty estimation methods face a critical gap: white and grey-box techniques are often inapplicable to closed-source models, while standard "black-box" text metrics fail to capture the unique fragility of code, where syntactic variation does not always imply semantic divergence. To bridge this syntax-semantics gap, we introduce Code-MUE, a purely black-box framework that measures uncertainty through execution-based Semantic Interaction Graphs. Different from prior approaches that rely on superficial textual similarity, Code-MUE grounds uncertainty in observable runtime behavior, calculating the Von Neumann entropy of the solution space to quantify global semantic diversity. A large-scale empirical study across eight state-of-the-art LLMs demonstrates that Code-MUE achieves a strong negative correlation with functional correctness (Spearman's correlation up to -0.98), significantly outperforming lexical and embedding-based baselines while enabling robust risk detection and selective prediction in practical workflows.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · selected cs.SE · published 2026-07-14T04:40:45Z
Weifeng Yuan, Wenbo Guo, Feng Dong, Haoyu Wang, Yang Liu
arXiv categories: cs.SE, cs.CR

LLM agents acquire new capabilities by downloading skills from open registries. Instead of browsing these catalogs manually, developers typically ask the agent to recommend and install a skill. This convenience hides a risk: agents frequently invent names for skills that exist in no registry. We term this flaw skill name hallucination. A fake name may seem harmless, but it opens the door to supply-chain attacks. Because registries rarely verify publishers, an adversary can prompt the agent, collect the fake names it returns, pre-register malicious skills under them, and wait for a victim to install the payload. We conducted the first large-scale measurement of skill name hallucination, evaluating 15,000 prompts across 12 configurations (4 standalone LLMs and 8 agents). We conservatively counted a name as hallucinated only if it was missing from all live registries and GitHub. The results reveal a systemic vulnerability: every configuration hallucinates. Rates average 36.0% for standalone LLMs and 36.9% for agents, rising to 43.1% on real-world developer questions. In total, the systems generated 5,669 distinct hallucinated names. Crucially, these names are not random noise. Agents repeat the same fake names across prompts and models, giving attackers highly reliable targets to hijack. Finally, we tested four model-level defenses and found a severe conflict between security and usability. The strongest, retrieval grounding, cut the hallucination rate from 40.8% to 3.2% but crippled usefulness: even the best-defended system recommended the correct skill only about one in six times. Skill name hallucination is thus a highly exploitable vulnerability requiring minimal attacker effort. Fixing it cannot rely on prompt engineering or model tuning alone. It demands ecosystem-wide structural changes: registry-level name reservations and verified recommendation pipelines.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-14T08:23:24Z
Zhiyuan Liu, Yihe Li, Trevor E. Carlson, Huiyan Wang, Ruijie Meng, Gregory J. Duck
arXiv categories: cs.PL

Due to token and cognitive limits, Large Language Models (LLMs) typically perform program reasoning over incomplete code fragments/prompts rather than complete programs. Such reasoning therefore must rely on {assumptions about omitted code and context. As a result, the meaning of an inference over a program fragment is not absolute, but depends on an implicit completion model describing how the fragment may be refined into a complete program. In this paper, we introduce completion semantics for LLM-based program reasoning. We formalize incomplete programs as denoting a space of possible refinements and define the correctness of existential inferences relative to a completion model. Under this view, a reported bug is correct whenever there exists a completion within the model that witnesses the bug. This perspective explains why many LLM-generated reports are neither simply correct nor incorrect, but instead depend on assumptions about omitted context. We have instantiated our approach in the form of a witness-generation workflow that concretizes completions underlying an inference by constructing executable refinements of the original program fragment. Witnesses serve both as evidence for existential claims and as a mechanism for exposing the assumptions required to support them. We evaluate our approach on real-world LLM-generated bug reports and program-analysis tasks. Our results show that witness generation effectively distinguishes inferences supported by plausible completions from those requiring unrealistic assumptions, providing a practical mechanism for validating reasoning over incomplete programs.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · selected cs.SE · published 2026-07-14T10:33:29Z
Zhili Huang, Ling Xu, Hongyu Zhang
arXiv categories: cs.SE, cs.AI

Large language models (LLMs) have improved automated program repair (APR), but two limitations remain. First, raw execution traces are often too large and repetitive to serve as effective model context. Second, repeated patch sampling may produce different implementations without yielding distinct root-cause hypotheses or repair strategies. We present CT-Repair, an agentic APR framework representing static and dynamic evidence as queryable Code Property Graph (CPG) and Temporal Execution Graph (TEG). CT-Repair applies a three-stage filtering pipeline to construct compact TEGs. Three finite-state-machine-guided agents analyze each bug from static, dynamic, and hybrid perspectives and independently produce evidence-grounded repair strategies. A strategy-guided generation procedure instantiates these strategies as candidate patches and uses validation feedback to refine the most promising strategy. We evaluate CT-Repair on 854 Java bugs from Defects4J v3.0. In the mixed-model configuration, CT-Repair correctly repairs 489 bugs. Under a controlled GPT-5.4-mini configuration, it repairs 388 bugs, 19 and 30 more than ReinFix and RepairAgent, respectively. The union of the three evidence perspectives repairs 99 more bugs than the strongest individual perspective. The filtering pipeline also compacts runtime evidence, with execution filtering narrowing the candidate method scope by 94.85% on average and behavior filtering further reducing retained runtime records by 55.97%. These results show that structured runtime evidence and multi-perspective reasoning can improve repair effectiveness without relying solely on a larger patch-generation budget.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · selected cs.SE · published 2026-07-14T11:33:44Z
Junyu Ren
arXiv categories: cs.LG, cs.AI, cs.CY, cs.SE

Tool access alone does not make LLM empirical reasoning governable: accepted outputs need not descend from attested evidence, and accepted deductions need not hold up under formal scrutiny. We present EG-VAR (Evidence-Grounded Verified Agentic Reasoning), a Lean 4-based tool-calling architecture in which the Lean kernel is the sole minter of Verified claims via tool-attestation axioms and declared source lifts. Every verified output structurally descends from an attested tool call (Thm. 3.1) and a kernel-checked chain of valid inference (Thm. 3.2); residual outputs are honest Abstain with a replayable audit trail. On a subcollection of TableBench numerical reasoning (n=120), EG-VAR attains 120/120 versus a 95% same-tool baseline; on counterfactual stress tests (5 domains x 2 models), EG-VAR stays 100% source-faithful while same-tool drops to 80-90% (no-tool 50-80%). With the LLM as deployment-time formalizer, residual semantic-formalization error is 3.3% on Sonnet and 1.7% on Opus. We position EG-VAR as a technical-governance interface for high-stakes empirical claims: a formal sidecar makes the target proposition, source scope, evidence boundary, proof obligation, and abstention condition auditable, eliminating unsupported Verified outputs today while turning formalization errors, lift and source-authority disputes, ambiguities, and abstentions into explicit audit targets. Over time, typed sidecars in datasets, APIs, public records, and AI-generated documents can amortize this formalization burden into reusable infrastructure.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-14T12:39:05Z
Pedro Orvalho, Guillem Alenyà, Felip Manyà
arXiv categories: cs.AI, cs.LO

Vision--Language Models (VLMs) have recently demonstrated promising performance on structured visual reasoning tasks, including grid-based puzzles. However, despite strong perceptual capabilities, these models lack explicit mechanisms for enforcing logical consistency and frequently generate assignments that violate underlying constraints. In this paper, we propose a neuro-symbolic approach that integrates formal constraint reasoning into the VLM solving process via a Maximum Satisfiability (MaxSAT) oracle. Rather than computing solutions directly, the symbolic component acts as a consistency validator and refinement engine. Candidate placements generated by the VLM are encoded as soft clauses in a partial MaxSAT formulation, while Sudoku constraints remain hard clauses. When inconsistencies arise, the MaxSAT solver identifies a largest mutually consistent subset of assignments, which is then translated into structured textual and visual feedback to guide subsequent refinements. We evaluate our approach on a Sudoku dataset across multiple open-source and closed-access VLMs. Results show that MaxSAT-based feedback improves logical consistency and increases the number of solved instances, particularly in full-board refinement mode. These findings demonstrate that symbolic optimisation can enhance the reliability of vision-language reasoning.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-16T10:37:02Z
Ruben Martins
arXiv categories: cs.LO, cs.AI

We report on CoreForge, an experience in using large language models (LLMs) to build an unweighted MaxSAT solver from research papers rather than from an existing solver codebase. The project focuses on unsatisfiability-based MaxSAT algorithms and follows an iterative workflow that combines paper discussions with ChatGPT, implementation through Codex prompts, and repeated LLM-assisted code audits and revisions. Although the codebase implements several algorithms and solver components, our evaluation focuses on configurations that combine core-guided optimization, lightweight preprocessing, core minimization, integration with integer linear optimization backends, and a new core-sequence lookahead approach. Our experience suggests that LLMs can support solver implementation from papers, while requiring external validation, benchmarking, and human guidance. In our experiments, fuzzing and MaxSAT Evaluation instances did not reveal wrong answers in the tested configurations, although performance remains below the best hand-engineered MaxSAT solvers. We summarize what worked, what remained difficult, and the lessons for future LLM-assisted solver development.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-16T15:18:58Z
Sridhar Mahadevan
arXiv categories: cs.LG, math.CT

This paper develops a categorical framework -- Learning in Infinitesimal Non-Compositional Sketches (LINCS) -- as the repair of non-compositionality: failures of diagrams to factor through quotient sketches lifted to the tangent category setting. Machine learning problems are specified as sketches: graphs with commutativity conditions $\mathcal D$, limit cones $\mathcal L$, and colimit cocones $\mathcal K$, generalizing the usual scalarization of loss functions or vector space assumptions. Non-compositionality is defined purely as failure of a universal factorization problem, not as arithmetic error between the desired and actual predictions. Given a learning sketch $\mathbb S=(S,\mathcal D,\mathcal L,\mathcal K)$, whose underlying graph is $S$, and a model $D:J \rightarrow C$, the base defect is the obstruction to factorization $\mbox{Obs}(\mbox{Fact}_{\mathbb S}(D))$. The tangent lift applies the tangent functor $T$ to obtain $TD:J \rightarrow C$, and LINCS is defined as the obstruction $\mbox{Obs}(\mbox{Fact}_{\mathbb S}(TD))$ -- asking whether infinitesimal perturbations preserve the compositionality constraints.The paper also introduces Tangent Learning Sketches, which are sketches equipped with Cockett-Cruttwell tangent structure. The paper defines the INC endofunctor, which iterates the tangent lift, producing a tower $D,TD,T^2D, \cdots$ of factorization problems. ML is thereby formulated as the search for a coalgebraic fixed point where successive tangent unfoldings stabilize ($νT_{\mbox{INC}}$). Using the Aczel--Mendler theorem, we prove existence of a final INC coalgebra whenever $T_{\mbox{INC}}$ admits a set-based class realization that creates its final carrier. A detailed experimental evaluation of LINCS is underway in a number of concrete ML settings, including deep learning, large language models, and reinforcement learning, and is described in companion papers.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-17T14:43:43Z
Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang, Wenda Li, Haonan Li, Luke Ong, Conrad Watt
arXiv categories: cs.SE, cs.AI, cs.LG, cs.PL

Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this effort, but their heavy token consumption and API cost remain a major obstacle. We trace this cost to a shared root: current agents operate on serialized concrete syntax, emitting proofs as source text and recovering proof states through separate, line-number-based queries, so every edit shifts later lines and forces repeated relocation of errors and states. This same dependence on concrete syntax also blocks adoption of Minilang, a recent proof language that reaches SOTA on LLM-based proving but is too new for LLMs' training corpora. We address both problems by lifting the agent off source text and onto the abstract syntax tree (AST): the model supplies proofs as JSON representations of Minilang's AST -- native to tool-calling LLMs -- and drives the prover through a tree-edit model that fuses proof operations and states into one proof tree, so each operation carries its own subgoal's state, readable directly off the tree. We realize this design in \emph{Agent over AST} (AoA). Against Amazon's Isabelle Agent on miniF2F and NTP4VC-Pearl common success sets, AoA cuts API cost by 2.3--4.7x (normalized input-cache accounting), uses 2.9--6.9x fewer tokens and 3.9--8.9x fewer tool calls, and finishes 1.4--2.0x faster -- while also solving far more problems on the harder verification benchmark.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-17T20:39:40Z
Joseph Tafese, Karthik Nukala, Hassen Saïdi, Natarajan Shankar, Arie Gurfinkel, Giuliano Losa
arXiv categories: cs.LO, cs.SE

We present a case study on proof-driven software understanding of mature, security-critical infrastructure. While formal methods are traditionally applied during the design phase, we present our experience applying formal reasoning onto a mature industrial C++ codebase. We focus on a formal analysis of the core algorithm that implements the Stellar blockchain's SDEX order book. By combining large language models (LLMs), Prototype Verification System (PVS), and SeaHorn, we are able to prove core properties of the production codebase. Our approach also identified an inconsistency in documentation related to the reachability of an exception location. Most importantly, however, we produce artifacts that make it easy for code changes to be checked against established invariants. This work demonstrates how the strategic combination of theorem proving and model checking provides a path for delivering robust assurance to legacy systems.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-19T03:23:22Z
Lucky Verma
arXiv categories: cs.LG, cs.AI, cs.LO

LLM constraint reasoners are often evaluated near the random-SAT phase transition, confounding density and solver hardness. We test instance-level transfer while near-matching clause density. At aligned size bins, with near-matched density and matched maximum clause width, we compare proof-hard expander-Tseitin and proof-easy ladder-Tseitin formulas, pigeonhole anchors, and density-mismatched controls. Theory separates their resolution hardness; a solver-specific Glucose mean-conflict proxy differs by up to $51\times$, and five other solvers preserve the direction. Across three included models (243 instances each; a fourth is excluded for abstention), the near-matched-density accuracy gaps range from $-32$ to $+20$ points, with a pooled gap of $+1.7$ points ($p=0.74$) and a wrong-signed correctness-versus-conflict association ($r=+0.15$). A proof-preserving relabeling lowers accuracy in all five clusters for one model (mean $-93$ points) but not another, exposing model-surface sensitivity. In a preregistered extension, provider-reported completion-token spend does not consistently increase with the proxy after accounting for formula length and censoring. At 16k, the reasoning model spends more on proof-easy matched formulas and exhausts its budget on the solver-easiest UNSAT family; the 32k C1 gap is absent. These scoped dissociations concern verdict accuracy and observed token spend, not certificate solving, exact proof length, or allocation efficiency.

arXiv abstract · PDF

LLM reasoning, grounded agents, and AI assurance · primary corpus · published 2026-07-19T19:01:06Z
Junade Ali
arXiv categories: cs.AI, cs.LG, cs.LO, cs.MA

This paper provides an experimentally verified formal law for calculating the uplift that diversity of thought provides in Large Language Model (LLM) ensembles. From first principles, we derive an exact decomposition of LLM ensemble lift into rescue and damage masses, which yields a compact heuristic for calculating uplift. From this we extract the metrics which predict ensemble performance: an accuracy-adjusted correctness correlation, $φ_{\mathrm{adj}}$, together with the accuracy gap and collective accuracy of the pair. We test the law on 767,520 inferences from ten open-weight models over two graduate-level science benchmarks, together with a novel agentic cybersecurity benchmark in which each model conducts digital-forensics investigations by multi-turn tool use in a network-isolated sandbox (23,520 graded trials including abstentions); all votes are released openly. Calibrated once on SuperGPQA at a 40:60 vote split, the heuristic predicts lift on the calibration set with Spearman's $ρ=0.84$ and, with its coefficients frozen, transfers to two datasets never used in calibration ($ρ=0.51$ on GPQA Diamond and $0.84$ on the forensic tasks), whilst the measured swap mass tracks realised lift with $R^2\ge 0.96$ throughout. Raw $φ$ has almost no predictive power ($R^2\le 0.09$ throughout); the accuracy-adjusted $φ_{\mathrm{adj}}$ is markedly superior ($R^2=0.67$ on SuperGPQA), and the heuristic combining these metrics is the most stable pre-pooling predictor across the three datasets.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-13T05:53:17Z
Duc Trung Kim Nguyen, Khanh Van To
arXiv categories: cs.LO

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.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-14T11:38:30Z
Romain Sidhoum, Simon Robillard, David Delahaye
arXiv categories: cs.LO

This paper introduces the strategy language of Pgeon, a meta-prover with a clear separation between inference rules and proof search. We give the semantics of strategies as functions over proof states, and of the operators that are used to combine them, allowing for sequential composition, choice, repetition and interleaving of strategies. This language is designed to handle the challenge of fair proof search in semi-decidable logics, where simple depth-first exploration of the proof space is not guaranteed to achieve completeness. We showcase the expressiveness and effectiveness of the approach through case studies in first-order and modal logics.

arXiv abstract · PDF

Automated reasoning, constraints, and proof search · primary corpus · published 2026-07-15T07:43:08Z
Jan Krajicek
arXiv categories: cs.CC, math.LO

Ilango (FOCS 2025) invented effectively zero-knowledge proofs, a new variant of zero-knowledge. We reformulate it in the language of logic and give simple proofs (under the same assumptions as Ilango (FOCS 2025)) of its existence and of the key property defined in Ilango (FOCS 2025) that it is "indistinguishable from true" (that property is in Ilango (FOCS 2025) a part of the definition of the prover, not its consequence). Using the theory of proof complexity generators we show that the concept can be turned it into a genuinely zero-knowledge proofs, assuming a conjecture from the theory about the existence of a hard generator and allowing the parties to share a common random string.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-15T07:29:29Z
Lukas Zenger
arXiv categories: cs.LO, math.LO

This thesis develops the mathematical theory of intuitionistic dynamic logics - extensions of intuitionistic propositional logic with modalities and fixed point operators. Such systems provide formal tools for reasoning about change, such as encountered in mathematical systems evolving over time or in the knowledge state of an agent after an information update. We investigate five intuitionistic dynamic logics: intuitionistic master modality, intuitionistic common knowledge logic, intuitionistic linear temporal logic, bi-intuitionistic modal logic and bi-intuitionistic linear temporal logic. On the proof theoretic side we develop sound and complete Hilbert-style axiomatizations as well as non-wellfounded and cyclic sequent calculi. On the semantic side we study these logics over various classes of dynamic models, which are birelational Kripke models satisfying confluence and frame conditions. We establish expressivity results, the finite model property, decidability, as well as complexity bounds. The main contributions are threefold. First, we develop analytic cyclic sequent calculi for intuitionistic master modality and common knowledge logic, where completeness is obtained by a robust proof search argument. Second, we obtain the finite model property and decidability for bi-intuitionistic modal logic via an intricate combinatorial analysis of dynamic models. Third, we develop a sound and complete axiomatization for intuitionistic linear temporal logic featuring the temporal operators next, eventually and henceforth, thereby providing a positive answer to the long-standing open question concerning the existence of a finite axiomatization.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-15T08:46:48Z
Patricia Bouyer, B Srivathsan, Vaishnavi Vishwanath
arXiv categories: cs.LO, cs.FL

Satisfiability of Metric Interval Temporal Logic (MITL) is a widely investigated subject. In this work, we present a new, and arguably simpler, approach for MITL satisfiability, based on an idea of tracking time-constrained obligations along a word. To check whether a Linear Temporal Logic (LTL) formula is true at a position of a word, it is natural to generate certain obligations that need to be satisfied at a later point. For instance, $a ~\mathcal{U}~ b$ (with strict Until semantics) is true at position $i$ if either $b$ or the set $\{a, a ~\mathcal{U}~ b\}$ is true at $i+1$. We enhance this idea in the context of MITL by introducing a notion of time inside these obligations. However, a naïve procedure could lead to more and more obligations getting generated along the word, with no bound on the number. We propose a simple mechanism to eliminate or merge redundant obligations. For MITL, this mechanism ensures that only a bounded number of obligations are maintained along the entire timed word. We develop this observation into a symbolic procedure for MITL satisfiability using regions.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-15T15:55:20Z
Andrei Sipos
arXiv categories: math.FA, math.LO, math.OC

We derive new formulas for quantities involved in the study of uniformly convex spaces, linear and nonlinear.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-17T03:06:36Z
Hossein Rastgoftar
arXiv categories: eess.SY, math.LO

Persistent aerial surveillance using multi-unmanned aerial systems (UASs) requires decentralized coordination, continuous team reconfiguration, and provable mission correctness despite limited onboard energy and communication constraints. This paper develops a distributed framework for continuous aerial surveillance under bounded Linear Temporal Logic (LTL) mission specifications. The proposed approach partitions the UAS team into stationary anchors and mobile workers operating under cyclic replacement modes, and constructs a deep neural network (DNN)-inspired communication topology that enables fully decentralized coordination through local interactions. A hierarchical bounded LTL specification formally captures mode-to-mode reference consistency, cyclic team rotation, finite-time reachability, trajectory tracking, and prescribed surveillance coverage. By proving the finite-time convergence of the worker-agent coordination dynamics, the paper guarantees the finite-time satisfaction of the mission specification. To maximize sensing effectiveness, an information-theoretic optimization framework synthesizes the reference configuration of newly deployed worker agents by minimizing the Kullback--Leibler divergence between the surveillance-node distribution and the induced coverage density. The resulting reference configuration uniquely determines a deterministic, mode-dependent communication topology, eliminating online communication-graph optimization while preserving the formal mission guarantees. Finally, a decentralized quadrotor controller realizes the distributed references using only local communication. Numerical simulations demonstrate cyclic team reconfiguration, decentralized communication-topology synthesis, finite-time formation convergence, and certified persistent surveillance coverage.

arXiv abstract · PDF

Temporal, probabilistic, and quantitative reasoning · primary corpus · published 2026-07-18T10:44:18Z
Guo Li, Zhaokai Li, Xinxin Liu, Zhiming Liu, Quan Sun, Wei Zhang
arXiv categories: cs.LO

We introduce a new branching bisimulation for probabilistic processes, which induces a more refined equivalence relation than any known equivalence that abstracts from unobservable actions, with a rooted version that is a congruence for a language of probabilistic process with the usual static as well as dynamic constructs including recursion.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-13T10:15:00Z
Nachiappan Valliappan
arXiv categories: cs.LO, cs.PL

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.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-14T11:37:41Z
Dale Miller
arXiv categories: cs.LO

This paper examines the foundational distinctions between proof theory and dependent type theory (DTT) in the design of interactive theorem provers. While several implemented systems are designed using the dependently typed λ-calculus to represent proofs, no major proof assistant is designed using modern structural proof theory, even though, as I will argue here, the sequent calculus offers a compelling alternative framework. Six specific topics are proposed where the proof-theoretic perspective is arguably superior to the DTT perspective. These topics include the separation of logic from proof structure, the strategic use of non-determinism in proof reconstruction, and the avoidance of complex typing-discipline issues such as universe levels and proof irrelevance. The final topic -- the treatment of bindings -- is further developed to demonstrate how a natural, intensional approach is achieved through the mobility of binders. This methodology is illustrated via the Abella theorem prover, which leverages lambda-tree syntax and the nabla-quantifier to provide an elegant environment for reasoning about the meta-theory of languages and logics involving complex binding.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-14T20:01:41Z
Anton Kashchenko, Andrey Kudinov
arXiv categories: math.LO

In this paper, we find the axiomatization for the topological square of S4.1. This is the first known topological square of a modal logic that differs from both the fusion and the Kripke product. We also prove the finite model property and decidability for this logic.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-14T23:21:02Z
Jérémie Marquès
arXiv categories: math.LO, math.CT

Constant domain intuitionistic logic admits a complete semantics in presheaf toposes, by interpreting sorts as constant presheaves and predicates as arbitrary sub-presheaves. The goal of this note is to point out how this fits in topos theory, replacing constant presheaves with objects that are covert and Hausdorff when considered as discrete locales. We call these objects "CD" and we show that they form a Boolean pretopos in any topos.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-15T14:01:53Z
Joaquim T. Waddington, Alexander V. Gheorghiu, David J. Pym
arXiv categories: math.LO, cs.LO

Game semantics is an elegant approach to the formal semantics of reasoning and computation that grounds model-theoretic concepts of truth and validity in game-theoretic concepts that emphasize the dynamic and interactive aspects of logical reasoning. In Hyland-Ong games, plays are traces of interactions between a player and an environment and such games provide a naturally appealing semantics for computation that is derived from proof-search in logical systems. Such a semantics can be seen as providing an intensional theory of meaning for systems of logic in terms of (the computation of) proofs. In logic, an intensional theory of meaning for systems of logic is offered by proof-theoretic semantics; in particular, by base-extension semantics (B-eS), in which the model-theoretic interpretation of atomic propositions in a satisfaction relation is replaced by a validity relation which uses provability in `bases' of atomic rules. We establish a fully abstract correlation between B-eS and Hyland-Ong game semantics, employing techniques similar to those used by Sandqvist to give a sound and complete B-eS for intuitionistic propositional logic. We illustrate our semantics through the example of 4x4 Sudoku.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-16T23:04:36Z
Linh Anh Nguyen
arXiv categories: cs.LO

We introduce the notion of fuzzy directed simulation between fuzzy Kripke models over any linear and complete residuated lattice and investigate its fundamental properties. In particular, we prove that all positive formulas of the fuzzy modal logic $\mathit{fPDL}$ are preserved under fuzzy directed simulations and establish a Hennessy-Milner theorem for this notion. Furthermore, we present a method for computing the greatest fuzzy directed simulation between two finite fuzzy Kripke models and implement it for the case where the underlying residuated lattice is the Gödel, product, or Lukasiewicz structure. Finally, we experimentally evaluate the performance of the implementation and present the obtained results.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-17T06:19:06Z
Igor Gorbunov, Mikhail Rybakov
arXiv categories: math.LO

The minimal well-determined logic in the language with conjunction and implication is investigated. A calculus for this logic, in which the modus ponens rule is not postulated, is proposed. The main result consists in constructing a semantics for this logic: it is formed by the class of lower semilattices with a greatest element, where the implication is interpreted using a partial function defined via the partial order of the semilattice. This extension of the notion of interpreting logical connectives in a matrix allows for the correct determination of the truth of formulas in the language with conjunction and implication. Soundness and completeness theorems are proved. The proposed semantics creates an opportunity to investigate questions of finite model property for such systems and can also serve as a basis for studying other properties of both the minimal well-determined logic itself and its extensions. As an application of the obtained results, we prove that the set of tautologies of the minimal well-determined logic is decidable in polynomial time and present a corresponding decision algorithm.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-17T07:56:46Z
Anggha Nugraha
arXiv categories: math.LO

The Levi-Civita field $\mathcal{R}$ of formal Laurent series is a constructive, non-Archimedean ordered field that supports a full Lebesgue measure and integration theory, including a Dominated Convergence Theorem. This paper embeds that integration theory into the paraconsistent Chunk and Permeate framework, extending it from elementary calculus to genuine measure theory. The source chunk is modelled by $\mathcal{R}$ with its measure and integral, while the target chunk is the classical real line $\mathbb{R}$. A permeability relation exports the standard part of the internal integral, and it is shown that the Dominated Convergence Theorem permeates from the source chunk to the target chunk, yielding the classical Lebesgue Dominated Convergence Theorem without any choice principles and without the ultrafilters required by nonstandard measure theory. The construction is entirely explicit and demonstrates that paraconsistent logic can provide a rigorous foundation for deep analytical tools while keeping inconsistencies safely confined.

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-17T13:46:47Z
Ulrich Kohlenbach, Morenikeji Neri, Jin Wei
arXiv categories: math.LO

We extend the proof-theoretic treatment of uniform bound extraction from normed structures axiomatized in positive bounded logic [Advances in Mathematics, 290:503-551, 2016] (as developed for the model theory of Banach spaces) to the more general setting of abstract metric structures, including discrete structures viewed as classical first-order models. In particular, we establish uniform bound extraction theorems for our generalized framework for $\forall\exists$-sentences whose matrix is the negation of (an embedding of) a formula in positive bounded logic, whose proofs use saturation. In this way, we provide a formal explanation for the successes in the extraction of uniform bounds from nonstandard proofs given in [Advances in Mathematics, 343:567-623, 2019], which had informally followed the perspective of the monotone functional interpretation. As an application of the formal framework we develop, we provide novel explicit bounds for a structural theorem for stable subsets of groups given in [Mathematical Proceedings of the Cambridge Philosophical Society, 168(2):405-413, 2020].

arXiv abstract · PDF

Modal, intuitionistic, and proof-theoretic logic · primary corpus · published 2026-07-19T16:38:27Z
Sophie Nagler
arXiv categories: cs.LO, math.LO

Inference-behaviour semantics (I-bS) is a new approach to proof-theoretic semantics, grounded in two inferentialist principles: (1) the use of an expression in reasoning determines its meaning, and (2) a connective is defined by its operational rules. I-bS operationalises these ideas by measuring the syntactic use of a connective in the proof of its definability, against a substructurally minimal derivability relation. I-bS thereby gives the meaning of a connective in terms of its semantic clause, i.e. minimal substructural rule pair. This paper validates and verifies I-bS by applying it to all $10,816$ connective rule pairs that can be formulated in two-dimensional sequent calculi using at most two premiss sequents and at most two active formulae. As a result, we find semantic clauses for exactly $21$ meaningful connectives, namely bottom, top, two negations (intuitionistic and dual-intuitionistic), group and lattice conjunction, disjunction and implication, as well as their converses and inverses. We use these results to precisely map the semantic interrelations among the connectives, across linear, classical, intuitionistic, dual-intuitionistic, minimal, and lattice logic. Most notably, we find that intuitionistic negation, disjunction and implication each capture half of the meaning of their classical counterparts.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-13T02:58:37Z
Mostafa Mirabi, Saharon Shelah
arXiv categories: math.LO, math.CO, math.PR

We prove an $\mathrm{MSO}_2$ zero-one law for a very sparse Erdős-Rényi graph after pruning by component order. Let $p_n=c_n/n$, where $c_n\to0$, and delete every component of order less than $f(n)$, where $f(n)\to\infty$. If \[ f(n)\bigl(\log f(n)+\log(1/c_n)\bigr)=o(\log n), \] then the resulting graph satisfies a zero-one law for $\mathrm{MSO}_2$, with quantification over sets of vertices and sets of edges. The proof combines uniform component counts, an MSO Feferman-Vaught decomposition for disjoint unions, and semilinearity of the order spectra of MSO-definable classes of finite trees. We also show that the term $f(n)\log f(n)$ cannot simply be omitted: star components can occur at first-order-visible Poisson thresholds. We further establish first-order limit laws for bond percolation on the discrete torus $T_L^d$. In the two-sided subpolynomial regime, pruning below a sufficiently slow threshold yields a zero-one law. For the unpruned model in either one-sided polynomial regime, the reciprocal exponents $α=1/k$ are precisely the critical scales. At such a scale, an extended limit of $N p_N^k$ or $N q_N^k$ equal to $0$ or $\infty$ gives a zero-one law; a positive finite limit gives a convergence law but not a zero-one law; and the absence of an extended limit gives failure of convergence. Finally, $\mathrm{MSO}_1$ already detects the parity of the torus side length through bipartiteness, producing a natural obstruction to monadic convergence in a near-deterministic regime.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-13T13:10:40Z
Ziemowit Kostana
arXiv categories: math.GR, math.LO

We study Fraïssé classes of Abelian groups with pure embeddings. We characterize Abelian groups that are universal and homogeneous for: finitely co-generated groups, finite groups, groups of size less that $κ$, where $κ$ is strongly inaccessible.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-13T14:41:13Z
Alexander Berenstein, Evgueni Vassiliev
arXiv categories: math.LO

We study expansions of quasiminimal pregeometry structures with a dense codense unary predicate and their relation with the complexity properties of the pregeometry of the underlying structure. We consider beautiful pairs as well as $H$-structures. We show each of these expansions can be axiomatized with a single $L_{ω_1 ω}(Q)$-sentence and that both expansions are $ω$-stable. For $H$-structures we provide a natural notion of independence in the expansion and when the underlying structure is modular, we also provide a natural notion of independence for beautiful pairs. Then we relate the complexity of the pregeometry to properties of the expansions.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-13T21:10:08Z
Roberto Carnevale, Gianluca Paolini
arXiv categories: math.LO

We prove several new results in the theory of $μ$-AECs, focusing mainly on (almost) stability, with the primary objective of undertaking a systematic study of $μ$-AECs of $R$-modules. Our main results are the following. 1. We show that, under suitable syntactic assumptions, all tame $μ$-AECs of $R$-modules (where $R$ is a ring) are almost stable, and are stable if they additionally satisfy a strong amalgamation property. This extends the work of the second author and Shelah [49] to the setting of $μ$-AECs. 2. We then turn to applications to concrete $μ$-AECs of $R$-modules. Our main result in this direction is that $(R$-Mod$, \leq_{pp}^μ)$ has a stable independence relation and is a stable and tame $μ$-AEC, where $\leq_{pp}^μ$ denotes the $μ$-pure submodule relation. We also prove similar stability results for various classes of abelian groups, including the $\aleph_1$-AEC of torsion-free abelian groups with the balanced subgroup relation. Moreover, we prove the almost stability of all $μ$-AECs of modules of the form $(R$-Mod$, \preccurlyeq)$, where $\preccurlyeq$ refines the direct summand relation and satisfies a strong form of coherence. 3. Finally, we study $μ$-AECs of the form $(K, \leq_\oplus)$, where $K$ is a class of pure-injective $R$-modules (note that this is, in general, not an AEC), and use our results to show that, for many natural choices of $K$, the class $(K, \leq_\oplus)$ has a stable independence relation and is therefore stable and tame. We use these results to give a sufficient condition for abstract classes of modules of the form $(K, \leq_{pp})$ to be stable when $K$ is closed under pure-injective envelopes. This generalizes, by a substantially different proof, results of Mazari-Armida [45].

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-14T17:13:08Z
Yiwen Ding
arXiv categories: math.LO

The classical Los-Tarski theorem characterises first-order sentences preserved under extensions as the existentially definable ones. In [6], Purdy claimed that the analogous preservation theorem holds for the fluted fragment. We refute this claim by constructing, over an equality-free vocabulary with only one binary relation symbol, a fluted sentence of quantifier rank three which is preserved under extensions but is not equivalent, even over finite structures, to any existential fluted sentence.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-16T01:36:14Z
Benjamin Castle, Ronan O'Gorman
arXiv categories: math.AG, math.LO

Working over uncountable algebraically closed fields, we extend the theorems of Kollár-Lieblich-Olsson-Sawin on reconstructing varieties from their Zariski topological spaces. In particular, we adapt their results to arbitrary quasi-projective varieties in arbitrary characteristic, and thus we give positive answers to each of the relevant `speculations' made by the original authors in our setting. Our proofs use techniques from model theory: in particular, we employ a general model-theoretic setting for algebro-geometric reconstruction problems, known as the `Zilber trichotomy for ACF-relics'.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-18T11:14:56Z
Hongyi Gou, Mihir Mittal, Chieu-Minh Tran, Zhenyu Yang
arXiv categories: math.LO, math.CO

We establish absolute and relative almost-linear Zarankiewicz bounds for semilinear relations in valued vector spaces. For every fixed arity and description complexity, a $K_{t,\ldots,t}$-free semilinear $r$-partite hypergraph has at most \[ O\!\left(n^{r-1}(\log n)^c\right) \] edges, where $c$ depends only on the arity and the number of valuative literals. In the bipartite case a separate arbitrary-trace argument gives the explicit bound $O(n(\log n)^{2s})$ for description complexity $(ρ,s)$. We also prove a relative extension theorem: intersecting any relation with a hereditary almost-linear profile by $s$ affine moving-radius comparisons increases the logarithmic exponent by at most $2s$. For the additive affine-valuative structures on $\mathbb Q_p$ and $\mathbb C_p$, quantifier elimination converts these semilinear results into bounds for all definable relations. Finally, over every valued field with infinite value group, we construct $K_{2,2}$-free semilinear point--box graphs of description complexity $(1,4)$ with $Ω(n\log n/\log\log n)$ edges.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-18T19:37:21Z
Elliot Kaplan, Angus Matthews, Erik Walsberg
arXiv categories: math.LO

We show that large rosy fields are bounded, and substantially simplify the proofs that large stable fields are separably closed and that large simple fields are bounded. Our proofs go through in a general topological setting. We obtain instability, non-simplicity, and non-rosiness explicitly by building the appropriate trees of definable sets. We also show that orders on large rosy fields have several properties of orders on pseudo real closed fields.

arXiv abstract · PDF

Model theory, finite structures, and definability · primary corpus · published 2026-07-19T00:42:07Z
Leon Chini
arXiv categories: math.LO

This paper further studies the model companion of an endomorphism acting on a vector space, possibly with extra structure. Let $T$ be a model-complete theory that $\varnothing$-defines an infinite $K$-vector space $\mathbb{V}$. In previous work, we introduced a family $\{T^C_θ: C \in \mathcal{C}\}$ of extensions of the theory $T_θ:= T \cup \{\text{``$θ$ is an endomorphism of $\mathbb{V}$''}\}$ that parameterizes all consistent extensions of the form $$ T_θ\cup \left\{\sum\nolimits_{k}\bigcap\nolimits_{l}\operatorname{Ker}(ρ_{j, k, l}[θ]) = \sum\nolimits_{k}\bigcap\nolimits_{l} \operatorname{Ker}(η_{j, k, l}[θ]) : j \in \mathcal{J}\right\}, $$ where all sums and intersections are finite, all the $ρ[θ]$'s and $η[θ]$'s are polynomials over $K$ with $θ$ plugged in, and $\mathcal{J}$ is some possibly infinite index set. We also presented a sufficient condition that implies that every $T^C_θ$ has a model companion $Tθ^C$. We simplify our axiomatization of $Tθ^C$ and the criterion for its existence for theories ``close to the theory of $K$-vector spaces''. We apply this to the explicit case where $T$ is the pure theory of $K$-vector spaces and characterize all $\varnothing$-definable endomorphisms of $\mathbb{V}$ in this case. Given an existentially closed model $(\mathcal{M}, θ) \models T^C_θ$ and a polynomial $ρ\in K[X]$, we show that $(\mathcal{M},\operatorname{Ker}(ρ[θ]))$ is, unless $\operatorname{Ker}(ρ[θ]) = \{0\}$ or $\operatorname{Ker}(ρ[θ]) = \mathbb{V}$, an existentially closed model of $T_V := T \cup \{\text{``$V$ is a vector subspace of $\mathbb{V}$''}\}$. In the same vein, we present a criterion for when $(\mathcal{M}, ρ[θ])$ is again an existentially closed model of $T^{C'}_θ$ for some $C' \in \mathcal{C}$.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-13T10:31:52Z
Platon Sifnaios
arXiv categories: math.LO

We introduce two first-order theories of hereditarily finite multisets: a schematic theory WF^- and a finitely axiomatized theory F^-, in the language with the empty multiset, singleton formation, multiset union, and a containment relation. We prove that WF^- is mutually interpretable with Robinson's theory R, and F^- with Robinson arithmetic Q; in particular, F^- is essentially undecidable. Multisets thereby join numbers, strings, trees, sets, and sequences in the mutual-interpretability classes of R and Q. The distinctive obstacle of the multiset case is the simultaneous failure of the standard devices for recovering ordered pairs: positional order, local order on immediate constituents, and idempotence-based Kuratowski pairing. We show that order is recoverable from bare multiplicity: the term pi(x,y) = <x> u <x> u <y> is provably injective in F^-, yielding a direct interpretation of the Kristiansen-Murwanashyaka tree theory T; conversely, F^- is interpreted in Q by arithmetizing a normal-form calculus for multiset terms within bounded arithmetic. Each structural axiom of F^- is shown independent of the others, with finite or Presburger-definable decidable witnesses, and the containment axiom is conservative. As an application, we identify Spencer-Brown's forms modulo commutative juxtaposition with hereditarily finite multisets and locate the boundary of essential undecidability within the calculus of indications.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-13T11:10:27Z
Léo Gayral, Mathieu Hoyrup
arXiv categories: math.DS, cs.CC, cs.LO, math-ph

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.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-13T15:22:34Z
Junhong Chen
arXiv categories: math.LO

We propose the Coding Conception of ordinals and sets, which takes Cantor's three generating principles as its sole foundation. Bounded sets of ordinals are generated synchronously with the ordinals themselves through a bijective encoding function that, at each stage, selects only the finitely many bounded sets actually required by the successor, limit, and restriction principles. This selective coding yields the first-order theory $SC^{reg}$, which we establish is the metamathematically correct theory of the ordinals: it is bi-interpretable with $ZFGC^+$, yet makes no claim about the general concept of set. Extending the conception to full set theory via a monadic second-order ordinal theory with arithmetic and class comprehension produces two mutually inconsistent first-order set theories according to distinct maximality intuitions: a Type-A universe $MC_A$, in which the power set of every ordinal is a set and the universe satisfies $ZFC$; and a Type-B universe $MC_B^+$, in which sets are strictly more than ordinals and a ``largeness cardinal'' exists, beyond which power sets remain unencodable. We prove that this Power Set Dichotomy is unavoidable, even under potentialism, and conclude that $ZFC^-+$``every cardinal has a successor'' is the only philosophically uncontroversial common fragment of any true set theory; the status of the full power-set axiom remains the sole open philosophical choice point.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-13T17:08:03Z
Pingshi Yu, Chengsong Tan, Nicolas Wu, Alastair Donaldson
arXiv categories: cs.PL, cs.CC, cs.SE

Randomised testing is a widely-used approach to software validation, yet its theoretical foundations remain thin. In particular, the fundamental question of what it means for a set of inputs to be \emph{generable} has gone unanswered in both the literature and folklore. We present the first complexity-theoretic foundations for random generators in software testing. We model generators as Turing transducers that consume random bits and produce string-encoded outputs, and show that the theoretically generable languages coincide exactly with the recursively enumerable languages. This has direct implications for testing at the boundaries of decidability, such as compiler testing. For \emph{efficient} generation, we show that the polynomial-time generable languages lie within \textit{NP}, that certain \textit{NP}-complete languages admit efficient generators, and that -- under standard cryptographic assumptions -- there are languages in \textit{P} for which no efficient generator exists: the complexity of efficienct generation and of efficient decision are not the same. We show space-bounded complexity is the natural framework for generators producing \emph{correlated} samples, capturing methodologies such as coverage-guided fuzzing and symbolic execution. Beyond classification, we characterise efficient generability: a language has a polynomial-time generator iff it admits a \emph{certificate scheme} over a verifier -- so witness planting, the folklore technique behind generators to test SAT solvers, is in a sense the only route to efficient generation. On the design of property-based testing libraries, we prove no library can compositionally derive efficient generators from logical predicates involving conjunction or negation, under standard assumptions. However, restricted classes like \textit{NL} (equivalently, linear Datalog predicates) would admit such a compilation.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-13T19:17:27Z
José de Jesús Pelayo Gómez
arXiv categories: math.LO

An ideal $\mathcal{I}$ on $ω$ has the Ramsey property if $\mathcal{I}^{+}\to(\mathcal{I}^{+})^2_2$: every $2$-colouring of the pairs of an $\mathcal{I}$-positive set has an $\mathcal{I}$-positive homogeneous subset. Whether a tall Borel ideal can have the Ramsey property is an open question of Hrušák, Meza-Alcántara, Thümmel and Uzcátegui; a coanalytic example exists in ZFC, so a negative answer must use definability essentially. Our main theorem, a synthesis of the results of the paper, states that a tall Borel Ramsey ideal admits no countable local reading. Below every positive set, such an ideal is not a countable intersection of topologically represented (or tall analytic $P$-) ideals, and its quotient has no countable dense subset. Moreover, every quotient name for a new real has uncountable width, the colouring witnessing non-selectivity of the generic ultrafilter is never read continuously on a positive condition, and hereditary tall subfamilies saturate every finite window of barrier dimensions coherently but never all dimensions at once. We prove separately that a weakly selective $q^+$ ideal admits no positive $\mathcal{ED}_{\mathrm{fin}}$-carrier. The converse question -- must Borelness force a properness-like countable reading on some positive condition? -- is stated in three precise forms with proved consequences: two of them would refute tall Borel Ramsey ideals outright, the third the strictly weaker Nash--Williams class. The main question remains open.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-14T16:09:33Z
Tatsuya Goto
arXiv categories: math.LO

We investigate the cardinal invariants on universally null sets. In particular, we prove $\mathfrak{b} < \operatorname{cof}(\mathcal{UN})$ and $\operatorname{non}(\mathcal{N}) = \operatorname{non}(\mathcal{UN}) < \operatorname{cof}(\mathcal{UN})$ in $\mathsf{ZFC}$. Also, assuming $\operatorname{add}(\mathcal{N}) = \mathfrak{c}$, we prove $\operatorname{cof}(\mathcal{UN}) = \mathfrak{d}_\mathfrak{c}$ by adapting Yorioka's technique. Moreover, we prove the consistency of $\operatorname{add}(\mathcal{UN}) < \operatorname{cov}(\mathcal{UN}) < \operatorname{non}(\mathcal{UN}) < \operatorname{cof}(\mathcal{UN})$.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-15T12:59:32Z
Romie Banerjee
arXiv categories: cs.IT, cs.AI, math.CT, math.GR

This paper establishes a direct analogue of the classical Coding Theorem in the setting of symmetry groups. We consider computable bijections on the set of binary strings, called symmetries and define the symmetry prior of a string as the probability that a randomly chosen symmetry from a given group has the string as its unique fixed point. We show that for any fix-retractable symmetry group, a group admitting a computable section that selects an isolating symmetry for every string, the symmetry prior is a universal lower semi-computable semi-measure. In this case, the Geometric Coding Theorem holds. We also develop a Galois connection between subgroups of G and subsets of binary strings, characterizing closed points and maximal closed subgroups, and explore the join-semilattice of dense subgroups. Our results unify algorithmic information theory with group theory and provide a framework for studying symmetry-induced complexity measures. This paper is the first in a series on Computational Algorithmic Statistics (CAS).

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-16T12:25:38Z
Tobias Boege, Geva Yashfe
arXiv categories: math.CO, math.LO

We prove that the recognition problem for algebraic matroids is undecidable. Explicitly, this means that there is no algorithm that takes as input a finite set $S$ and a function $r\colon\mathcal{P}(S) \to \mathbb{Z}_{\ge 0}$ (where $\mathcal{P}(S)$ is the power set) and decides whether there exists a pair of fields $F \subset K$, and a function $f\colon S \to K$, such that for all $A \subseteq S$: $\mathrm{trdeg}_F f(A) = r(A)$. This problem is known to be decidable if the characteristic of the fields involved is constrained to be zero. We prove that it is undecidable if the characteristic is either left unspecified (in which case a realization over any characteristic is accepted) or fixed to be a prime $p$. The proof relies on Hrushovski--Zilber's Group Configuration Theorem and on the work of Evans and Hrushovski on "Projective Planes in Algebraically Closed Fields". We relate two different such projective planes, and eventually construct a reduction from the solvability of Diophantine equations over $\mathbb{F}_p(x)$ ($p$ prime) to algebraicity of matroids. Solvability of Diophantine equations over $\mathbb{F}_p(x)$ was proved to be undecidable by Pheidas for all $p > 2$, and later by Videla for $p=2$. A central part of our proof is a variant of the so-called Field Configuration Theorem.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-18T00:23:22Z
Hiroshi Sakai, M. Catalina Torres
arXiv categories: math.LO

The notion of $n$-stationary subsets of $\mathcal{P}_κλ$ for $n < ω$ were introduced and studied by Cody, Lambie-Hanson \& Zhang \cite{CLHZ} and Torres \cite{T}. They proved that if $κ$ is supercompact, then $\mathcal{P}_κλ$ is $n$-stationary in itself for all cardinals $λ\geq κ$ and all $n < ω$. In this paper we prove that strong compactness of $κ$ does not imply the $2$-stationarity of $\mathcal{P}_κλ$ for cardinals $λ> κ$. We also discuss Menas' Theorem for $1$-stationary and $2$-stationary subsets of $\mathcal{P}_κλ$.

arXiv abstract · PDF

Set theory, computability, and mathematical foundations · primary corpus · published 2026-07-18T01:11:23Z
José de Jesús Pelayo Gómez
arXiv categories: math.LO

We develop a machinery for deriving ideals on a countable set from a partition of $ω$ indexed by $ω^{<ω}$. A derivative operator on trace trees, parametrized by an auxiliary ideal $\mathcal J$, yields a strict transfinite hierarchy $\mathcal H^{\mathcal J}_α$ of proper ideals, tall from level one onward and independent of the chosen partition. Its finite levels are exactly the Fubini powers, $\mathcal H_n\cong\mathrm{Fin}^{\otimes(n+1)}$, while $\mathcal H_ω=\bigcup_n\mathcal H_n$ amalgamates all finite powers. We establish presentation independence, local homogeneity, Fubini recursion, and $Π^1_1$-completeness of the full hierarchy. Let $\mathcal F_ω$ be Kwela's canonical inductive limit and $\mathcal F'_ω$ his independent-partitions limit. We prove $\mathcal F_ω\not\leq_K\mathcal H_ω$, although $\mathcal F'_ω\sqsubseteq\mathcal H_ω$ and every finite coherent fragment of a putative reduction is realizable over $\mathcal H_ω$. The proof introduces essential depth, an invariant monotone along Katetov reductions of $\mathrm{Fin}\otimes\mathrm{Fin}$, and gives the sharp non-extension bound $N(m)=m+2$. Thus $\mathcal H_ω$ contains no isomorphic copy of $\mathcal F_ω$, and $\mathcal F_ω\not\leq_K\mathcal F'_ω$. Applications include chromatic ideals $\mathcal G_k\in\mathcal H_2\setminus\mathcal H_1$ whose inclusion order records divisibility and whose Katetov order records arithmetic. We also prove the orthogonality of Cantor--Bendixson and derivative ranks. Finally, $\mathcal P(ω)/\mathcal H$ is a $σ$-closed reduced power $\mathbb B\cong\mathbb B^ω/\mathrm{Fin}$, contains $\mathcal P(ω)/\mathrm{Fin}$ regularly, and under CH is forcing-equivalent to $(\mathcal P(ω)/\mathrm{Fin})^+$.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-13T14:56:35Z
Philippe Gaucher
arXiv categories: math.CO, math.AT, math.CT

We introduce the chain replacement of a poset flow: it is obtained by considering the simplicial nerves of the posets of strictly increasing chains in the given poset, ordered by refinement. It maps finite posets to q-cofibrant flows and inclusions of finite posets to q-cofibrations. Using the combinatorial properties of the chain replacement, we prove that pushouts along the chain replacement of an order-reflecting inclusion of finite posets preserve spaces of execution paths. By introducing the Hurewicz model structure on flows (or H-model structure), we deduce the same property for any q-cofibrant replacement of an order-reflecting inclusion of finite posets.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-13T17:00:45Z
Stefano Ronchi
arXiv categories: math.DG, math.AT, math.CT, math.SG

In this thesis we define $n$-duals of VB $n$-groupoids over Lie $n$-groupoids and study their properties. For $n = 0$ this returns the dual vector bundle construction, while for $n = 1$ this returns Pradines's construction of the dual of a VB groupoid over a Lie groupoid, which includes the cotangent symplectic groupoid of Coste, Dazord and Weinstein. For $n = 2$, we propose a new construction that shows that VB 2-duals exist for VB 2-groupoids and they are VB 2-groupoids themselves. Their canonical dual pairings are nondegenerate up to homotopy in the same sense as shifted symplectic structures. In particular, we can apply this construction to the tangent of a Lie 2-groupoid and obtain a cotangent VB 2-groupoid (the 2-cotangent) which is canonically 2-shifted symplectic. We apply this in two ways: First, to characterize 2-shifted symplectic structures on a Lie 2-groupoid as Morita equivalences between its tangent and 2-cotangent groupoid. Second, to compute the 2-cotangent of a Lie 1-groupoid and show it is symplectic Morita equivalent to the bar construction of the 1-cotangent. Along the way, we develop the theory of $n$-duals for simplicial vector spaces, which covers the case where the base is a point. In this case, $n$-duals always exist, as they are defined by a mapping space construction. By a reformulation of the Eilenberg-Zilber theorem in terms of mapping spaces, we obtain that the canonical $n$-dual pairing is nondegenerate up to homotopy for all $n$-types.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-14T04:16:19Z
Julia E. Bergner, Brandon T. Shapiro, Inna Zakharevich
arXiv categories: math.AT, math.CT, math.KT

In this paper, we establish a precise relationship between CGW categories and pointed stable double Segal spaces, both of which were developed as general input for algebraic K-theory. In particular, we show that any CGW category can be regarded as a pointed stable double Segal space, and they can be identified using a classifying diagram construction for double categories with shared isomorphisms.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-14T15:16:48Z
Alberto Canonaco, Amnon Neeman, Paolo Stellari
arXiv categories: math.AG, math.CT

In this paper we investigate the uniqueness of enhancements of the natural subcategories of weakly approximable triangulated categories. The main idea is to enhance at the level of $\infty$-categories the recently developed theory of excellent metrics. The applications of our results include a vast generalization of the known results about the (strong) uniqueness of enhancements in the linear and nonlinear setting, providing positive answers to some open questions. In addition we prove that, under some natural assumptions, the equivalences between such subcategories can be lifted through their natural inclusions. This completes the picture started in our previous paper arXiv:2505.10374 and extends the known results about Margolis Uniqueness Conjecture for the homotopy category of spectra.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-15T16:48:12Z
Virgile Constantin
arXiv categories: math.CT, math.AT

We formulate and prove internal versions of the Yoneda lemma and of the Yoneda embedding theorem in a finitely complete, locally Cartesian closed $\infty$-category $\mathscr{C}$: for every object $X\in \mathscr{C}$ and every universe $\mathscr{U}$ classifying the diagonal of $X$, the Yoneda map $\mathscr{Y}_X\colon X \to \mathscr{U}^X$ is a monomorphism. The proof uses only finite limits, dependent products and universes, and does not rely on the external Yoneda lemma. The result applies notably to every elementary $\infty$-topos, where it recovers a theorem of Rasekh [Ras18].

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-16T09:54:50Z
Virgile Constantin
arXiv categories: math.AT, math.CT

We develop a systematic theory of $(n-1)$-truncated maps, called $n$-covering maps, in a fixed $\infty$-topos $\mathscr{E}$, guided by the analogy with classical covering spaces. We prove an equivalence of $n$-categories between $n$-coverings over a pointed connected object $(X,x)$ and $\infty$-actions of the fundamental $n$-group $Π_n(X,x)$ on $(n-1)$-truncated objects, which restricts to a classification of pointed connected $n$-coverings in terms of sub-$n$-groups of $Π_n(X,x)$. We study the $n$-group of deck transformations $\mathscr{D}\mathrm{eck}(p)$, identifying it with $Π_n(X,x)$-equivariant autoequivalences of the fiber $F$. For normal $n$-coverings, it is further described as a quotient of $Π_n(X,x)$, yielding a classification of such coverings in terms of normal subgroups of $π_n(X,x)$. For an arbitrary $n$-covering, the deck $n$-group arises as a quotient of a suitable normalizer. Our approach relies on a careful study of $n$-groups and their $\infty$-actions, on the use of univalent universes, and on an internal Yoneda embedding. When $n=1$ and $\mathscr{E}$ is the $\infty$-category of homotopy types, our results recover the classical theory of covering spaces. We further illustrate the theory in sheaf and étale $\infty$-topoi, where the external deck group recovers cohomology of the base, and in cohesive $\infty$-topoi, where it recovers the $1$-covering theory of manifolds.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-18T20:07:27Z
Claudia Scheimbauer, Pelle Steffens, William Stewart
arXiv categories: math.CT, math.AT, math.QA

We prove a conjecture of Lurie characterizing $(n+1)$-dualizability in higher Morita categories of $\mathbb{E}_n$-algebras in terms of dualizability over certain factorization homologies. A key ingredient is a higher Morita category based on the recently developed framework of pointless factorization algebras of Karlsson and the first author. We also verify an invertibility conjecture of Brochier--Jordan--Safranov--Snyder as an immediate corollary of our main result. Moreover, we prove a relative version of the dualizability conjecture, yielding a new criterion for relative/twisted field theories. We give some examples, including Dirichlet and Neumann relative theories.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-19T15:24:54Z
Runze Xue
arXiv categories: cs.LO, cs.PL, math.CT, math.LO

This project investigates the Phoa principle in synthetic domain theory (SDT), and provides a generalisation to the transfinite cases. The Phoa principle plays a pivotal role in SDT by illustrating how the paths give the information order on the interval type and other algebraic structures in SDT. The project defines the dual simplices and spines and introduces the concept of sobriomorphisms, which contributes to a new interpretation of the Phoa principle and its generalisations. Finally, the project proposes a hypothetical completeness theorem that may unify the Segal completeness and the chain completeness in SDT based on investigations on the Phoa principle in the project. The project also includes axiomatisation of the interval type in Cubical Agda and the formalised proof for the main theorems.

arXiv abstract · PDF

Higher categories, homotopy, and categorical topology · primary corpus · published 2026-07-19T18:04:25Z
Miquel Cueca, Florian Dorsch, Reyer Sjamaar, Chenchang Zhu
arXiv categories: math.SG, math.CT, math.DG

The main goal of this work is to introduce derived Lie n-groupoids and their shifted symplectic structures. We further define shifted lagrangian structures and prove that their composition is well defined under suitable conditions. As an application, we show that our framework incorporates several reduction procedures at critical values, including: classical Hamiltonian reduction, group valued moment maps, Poisson Lie group valued moment maps and Mikami-Weinstein for proper symplectic groupoids.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-13T07:05:31Z
Lory Aintablian, Christian Blohmann
arXiv categories: math.CT, math.DG

We determine the structure needed in a tangent category in the sense of Rosický and Cockett-Cruttwell to construct the Cartan calculus on all objects. The missing ingredient is a scalar multiplication by a commutative ring object $R$, playing the role of the smooth real line, which equips the tangent bundle of every object with the structure of an $R$-module compatible with the tangent structure. We show that under these axioms the Lie algebra of vector fields acts by derivations on the ring of $R$-valued functions and satisfies the Leibniz rule. In other words, the tangent bundle is an abstract Lie algebroid, so that the Lie algebra of vector fields is a Lie-Rinehart algebra over the ring of functions. Consequently, every object carries a Cartan calculus of Lie-Rinehart forms, given by the Chevalley-Eilenberg complex together with its differential, inner derivative, and Lie derivative. Examples include the tangent categories of smooth manifolds, $G$-manifolds, Lie groupoids, log manifolds, pro-manifolds, elastic diffeological spaces, affine and general schemes, graded manifolds, and affine $C^\infty$-schemes.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-13T10:25:07Z
Lennert De Baecke
arXiv categories: math.CT

We study Schreier extensions of monoids and establish a Kaluzhnin--Krasner embedding theorem for Schreier extensions. First, we prove that the category of monoids is not locally algebraically cartesian closed (LACC) and that a monoid is algebraically exponentiable in the category of monoids if and only if it is a Dedekind-finite monoid. Second, we recall that the category of extensions of monoids is $S$-LACC with $S$ the class of Schreier extensions, which defines a wreath product $A \wr B$ for any two monoids. Finally, we prove a Kaluzhnin-Krasner embedding theorem for Schreier extensions that are not necessarily split, i.e. given any Schreier extension $A \hookrightarrow G \twoheadrightarrow B$ of monoids, there is a monomorphism $φ_G \colon G \hookrightarrow A \wr B$, which is part of a morphism of extensions. The proof adapts the classical group-theoretic argument by replacing conjugation, which requires inverses, with a substitute made available by the Schreier property, namely, the unique factorization of elements in the fibers of the projection $p \colon G \twoheadrightarrow B$.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-13T16:26:24Z
Paul Balmer, Hatice Mutlu
arXiv categories: math.RT, math.CT

Colloquially speaking, `equivariant categories' refer to families of additive categories $\mathcal{A}(G)$ depending 2-functorially on a finite group $G$. We construct approximations of equivariant categories by Mackey 2-functors, both on the left and on the right. The idea is to enlarge $\mathcal{A}$ in a minimal way to make induction appear. These `mackeyfications' are inspired by Boltje's work with ordinary Mackey 1-functors. We also relate our left and right mackeyfications via a mark transformation. Finally we discuss examples.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-13T20:10:08Z
William Fisher
arXiv categories: math.CT, math.AG, math.AT

We define the notion of an exchange theorem and show that any two functors satisfying an exchange theorem are canonically related via twisted norm maps. This is done by identifying the universal category receiving a pair of functors satisfying an exchange theorem. Additionally, we show that the twists occurring are $K$-theoretic in nature, parametrized by a categorified analogue of virtual vector bundles. As an application, we show that every 3-functor formalism has a canonical extension which encodes Poincaré duality and Thom twists internal to the formalism. This gives a 1-categorical realization of the "coherent six operations" outlined by Hoyois. In the process of proving universality, techniques for computing categories associated to bi- and $n$-simplicial spaces are developed. Many of the results in this direction may be viewed as model-independent rederivations of work of Liu--Zheng.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-14T12:10:28Z
Mathieu Anel, Marcelo Fiore, Nicola Gambino
arXiv categories: math.CT

We study coexponentiability in the context of the cocartesian 2-category RIG of symmetric 2-rigs, symmetric strong monoidal cocontinuous functors, and symmetric monoidal natural transformations. Our results characterize the coexponentiable symmetric 2-rigs as those that are deformation retracts of presheaf categories over small categories. As an application, we give an account of the cartesian closure of two full sub-2-categories of the dual of RIG arising from the theory of combinatorial species and the theory of symmetric operads.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-14T12:28:24Z
M. Anel, M. Fiore, N. Gambino
arXiv categories: math.CT, math.AT, math.QA

We show that the bicategory of operads and bimodules can be embedded into the bicategory of symmetric 2-rigs, a categorification of commutative rings. In order to do this, we introduce the notion of an operadic 2-rig and show that the full sub-bicategory of symmetric 2-rigs spanned by operadic 2-rigs has the universal property of being a completion under Eilenberg-Moore-Kleisli objects.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-14T16:24:14Z
Elena Caviglia, Peter F. Faul, Graham Manuell, Luca Mesiti
arXiv categories: math.CT, math.RA

Clifford semigroups are known to correspond to functors from a semilattice into the category of groups. We show that this correspondence is an instance of the monoidal Grothendieck construction. Moreover, applying the Grothendieck construction to the functor sending a semilattice L to the functor category [L, Grp] yields the category of all Clifford semigroups. We use this to construct a number of factorisation systems on the category of Clifford monoids. Finally, we prove a general result on taking monoids in a monoidal fibration and apply it to give a correspondence between inverse semirings and lax monoidal functors from idempotent semirings into the category of abelian groups.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-14T23:22:19Z
Jiacheng Liang, Changhan Zou
arXiv categories: math.AT, math.AG, math.CT

We introduce the Zariski frame of any presentably symmetric monoidal $\infty$-category. This allows us to unify several spectral theories arising in higher algebra. The Zariski frame is coherent whenever the category is compactly generated, and the associated spectral space recovers both the classical Zariski spectrum of a commutative ring and the Hochster dual of the Balmer spectrum of a commutative $2$-ring. Moreover, the smashing frame of any stable presentably symmetric monoidal $\infty$-category can be identified with the Zariski frame of its category of dualizable modules. This construction is based on the principle that ideals in a symmetric monoidal $\infty$-category should be understood as monomorphisms into the unit object. In suitable contexts, this notion recovers the kinds of ideals appearing in the preceding examples, including thick ideals and smashing ideals, and it also accommodates the smashing ideals of non-stable $\infty$-categories. We also study the problem of forming quotients by ideals, which is subtle in the setting of higher algebra. To address this, we introduce two properties of pointed $\infty$-categories, called $Σ$-triviality and $Σ$-exactness. These conditions ensure that quotienting by ideals behaves well. As an application, we construct quotients of $\mathbb{E}_\infty$-semirings.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-15T14:53:14Z
Jiasen Liu, J. P. May, Kyle I. Roke, Hongyi Zhang, Keming Zhou
arXiv categories: math.CT, math.AG, math.AT

Symmetric monoidal categories have been understood since the 1960's and are central to many branches of mathematics. In particular, the construction of spectra from symmetric monoidal categories is at the heart of algebraic $K$-theory. This construction starts from either categories with an action by a suitable operad $\sP$ or with suitable functors from the category $\sF$ of finite sets to the category $\mathbf{Cat}$ of categories. Infinite loop space theory, which codifies these constructions, led to the invention of $\infty$-categories. So why the title? We shall prove that the $2$-category of symmetric monoidal categories is equivalent (in fact very nearly isomorphic) both to a $2$-category of $\sP$-pseudoalgebras and to an isomorphic $2$-category of strictly special $\sF$-pseudoalgebras. This equivalence underlies a streamlined equivariant and multiplicative enhancement of infinite loop space theory, but it should be of independent interest.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-15T19:02:05Z
A. M. Bouhada
arXiv categories: math.AG, math.CT, math.RT

We establish a bounded derived Koszul duality for infinite-dimensional Koszul algebras, and we obtain the corresponding singular Koszul duality. We then apply this framework to two classes of Koszul algebras, namely quadratic monomial algebras and absolutely Koszul algebras satisfying an additional homological condition. For these classes, the general duality specializes to particularly well-behaved forms. As an application to algebraic geometry, let \(Λ\) be a commutative noetherian Koszul algebra generated in degree \(1\), and let \(X=\operatorname{Proj}(Λ)\). We obtain a Koszul-dual description of the bounded derived category \(\mathsf{D}^{b}\!\bigl(\operatorname{coh}(X)\bigr)\). This gives a BGG-type correspondence for projective schemes defined by commutative noetherian Koszul algebras.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-16T15:00:38Z
Aaron David Fairbanks, Kevin Carlson, David I. Spivak
arXiv categories: math.CT

Comonads on Set generalize both categories and topological spaces. Expanding upon Garner's work on ionads, we develop aspects of the theory of topological spaces for arbitrary comonads on arbitrary categories. Our approach is centered around density comonads, which provide an abstraction of subbases. We study subbases as well as bases in terms of density comonads, and we study continuous maps of comonads in terms of functors between coalgebra categories, with definitions that recover the usual notions for topological spaces. Whereas Ahman and Uustalu characterized categories as precisely the polynomial comonads on Set, we characterize topological spaces as precisely the density comonads of diagrams of subsets of a set, which are familiar as topological subbases. We show that every comonad on Set has an underlying topological space, and that this construction is a reflection with respect to continuous maps; similarly, every comonad on Set has an underlying small category, and this construction is a coreflection. We also show that the category of all comonads on Set with continuous maps is complete, and that its full subcategory of accessible comonads is cocomplete. Continuous maps and ordinary comonad morphisms form a double category, which, in the case of the polynomial comonads on Set, recovers the double category of functors and retrofunctors of Clarke and Di Meglio. We find topological intuition for these concepts in terms of "halos", an abstraction of infinitesimal neighborhoods of points, defined as formal limits of neighborhood systems. We include a long appendix of counterexamples, many applicable to general (co)monad theory rather than the particular concerns of this text.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-17T03:11:15Z
Peng Xu
arXiv categories: math.CT, math.RT

In this paper, we classify the localizing ideals of the derived category D(U) of global representations over a field k of characteristic zero, for various infinite families U of finite groups. These families include elementary abelian p-groups, cyclic p-groups, and cyclic groups of prime order together with the trivial group. We deduce that the telescope conjecture holds for these D(U). In particular, via Pontryagin duality, our results for elementary abelian p-groups also establish the telescope conjecture and the corresponding classification for derived VI-modules. We also prove that the telescope conjecture holds for the derived category of FI-modules.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-17T14:28:11Z
Francesco Sentieri
arXiv categories: math.RT, math.CT

We extend to abelian length categories of finite rank a characterisation of brick-finiteness known for finite-dimensional algebras. We prove that such a category is brick-finite if and only if every torsion class is generated by a wide subcategory and every torsionfree class is cogenerated by a wide subcategory. The proof is based on an exchange relation for brick labels across wide intervals which is a shadow of the mutation of simple minded collections. As a corollary,we extend the validity of the first Brick Brauer-Thrall conjecture to this setting.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-18T18:06:54Z
Pavel Etingof
arXiv categories: math.RT, math.CT, math.QA, math.RA

Let $\mathcal C$ be a symmetric tensor category over an algebraically closed field $\mathbf k$ of characteristic $\ne 2$. We study Clifford and Weyl algebras of objects of $\mathcal C$ with a (skew-)symmetric bilinear form. When the form is non-degenerate, we establish simplicity and the Azumaya property for such algebras under suitable assumptions. We also compute Clifford and Weyl algebras in the Verlinde category ${\rm Ver}_p$ and use them to prove that if $\mathcal C$ is Frobenius exact then the Weyl algebra of a symplectic object of $\mathcal C$ with finite symmetric algebra is Azumaya. Using this, we introduce the symplectic Witt group $\mathcal S\mathcal W(\mathcal C)$, the subgroup of the Brauer group ${\rm Br}(\mathcal C)$ consisting of Morita classes of such Azumaya algebras, and when $\mathcal C={\rm Rep}(G)\boxtimes{\rm sVec}$ for a finite group $G$ of order coprime to ${\rm char}(\mathbf k)$, express $\mathcal S\mathcal W(\mathcal C)$ in terms of second Stiefel-Whitney classes of orthogonal representations of $G$.

arXiv abstract · PDF

Category theory and higher algebra · primary corpus · published 2026-07-19T20:58:11Z
Ivan Zelich
arXiv categories: math.AG, math.AC, math.CT

This thesis studies various aspects of flatness in algebraic geometry. We first study flatness in the context of semi-rings. We prove some discreteness results for a derived groupification functor with respect to the homotopy theoretic model structure on simplicial semirings, compare the Zariski and fppf topology, and study fppf algebras over the positive reals. We then study descendibility properties of faithfully flat ring maps; we in particular construct a non-descendable faithfully flat ring map, and then construct examples demonstrating the precise the relationship between the exponent of descendibility and cardinality by developing a rather general method to convert module-theoretic non-vanishing "cup-products" to descendable faithfully flat ring maps with sufficiently high exponent. Finally, we prove the affineness of the maximal etale locus of morphism $X \to Y$ of schemes with $X$ and $Y$ locally Noetherian schemes, $X$ normal and $Y$ regular in fully generality. Some notable aspects of this chapter is a variant of Artin-Rees' lemma that holds for non-Noetherian rings, a characterization of $D$-modules over unramified regular local rings (similar to those obtained by O. Gabber and W. Zhang), and Tor-independence result for global sections of étale schemes which we prove by a variant of the tilting correspondence which doesn't require completion.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-07-13T08:09:12Z
Jun Inoue
arXiv categories: quant-ph, cs.PL

We present a quantum process calculus that can split the system state along process boundaries and follow the evolution of each process in isolation, without losing information about the joint state-a property we call spatial compositionality. Compositionality is the key to reasoning about any complex system, yet quantum process calculi have struggled to provide its spatial kind, which would enable analyzing a system one process at a time. Many a quantum process calculi have been proposed, but they invariably rely on a global state representation based on state vectors or density matrices, with no known way to split them without losing information about entanglement. We propose to model quantum states with Deutsch-Hayden descriptors instead, which provide a modular representation of qubit states and their evolution. We adapt these descriptors to allow arbitrary splitting and merging of the store of qubits, leading to an unusual process calculus in which qubit transfer messages carry the actual state of the qubit, where existing calculi transfer only a reference. The calculus gives localized views of system state visible to each process, which can be assembled back together into the joint state. We define a notion of process equivalence with extensive justification grounded in physics and show a bisimulation whose soundness proof is simplified by spatial compositionality. The calculus can model open systems entangled with external processes, and we demonstrate this capability on a fragment of the BB84 key distribution protocol. This exercise shows that Deutsch-Hayden descriptors can successfully track qubit movements across process and system boundaries, though it needs help from density matrices to reason about information flow.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-07-13T20:21:14Z
Naihong Hu, Ruining Li, Futao Wang
arXiv categories: quant-ph, math-ph, math.CT

This paper systematically investigates quantum computing protocols from the intuitive perspective of categorical tensor-graph semantics within the category FHilb. While conventional Hilbert-space formalisms conceal the structural nature of quantum algorithms behind high-dimensional matrix operations, the topological framework developed herein directly encodes algorithmic functionalities to their graphical skeletons. We provide a comprehensive topological reinterpretation of the Bernstein-Vazirani and the Simon algorithms, demonstrating how topological transformations distill their core mathematical essence and clarify the operational mechanism of oracles. Going beyond standard qubit models, we formalize the qutrit-adapted generalized Deutsch-Jozsa algorithm as well as the generalized single-shot Grover algorithm, explicitly laying out their graphical representations. We further implement CNOT gates via complementary Frobenius structures, trace the diagrammatic genesis of quantum entanglement including Bell and GHZ states, and present a diagrammatic simplification for W-state preparation protocol. By bridging tensor category theory with practical quantum algorithmic design, this work furnishes composable, scalable diagrammatic toolkit essential for automated circuit optimization across the evolving quantum hardware ecosystem.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-07-14T15:14:38Z
Jean-Pierre Magnot
arXiv categories: cs.LO

We introduce a graded graph-series semantics for recursive hybrid quantum programs interpreted in the quantum orchestra monad. Finite terminating executions are represented by directed paths whose edges carry normal completely positive subunital maps and whose terminal vertices carry classical results. Path concatenation defines a graded execution category, while continuation grafting models outcome-dependent sequential composition. We construct a semantic evaluation from admissible execution-graph series to quantum orchestras and prove that it is compatible with both channel composition and Kleisli composition. For finitary recursive programs, the truncation of the execution series at degree $n$ is shown to coincide with the $n$-th Kleene approximant of the associated Scott-continuous recursion functional. Consequently, evaluation of the complete graph series recovers the ordinary least-fixed-point denotation. Weighting a graph of degree $n$ by $q^n$, with $0<q<1$, yields an Abel-regularised semantics whose Scott limit as $q\to 1^{-}$ is the unregularised recursive denotation. Equivalently, the parametrisation $q=e^{-t}$ exponentially suppresses long executions and reconstructs the denotation as $t\to 0^{+}$. In a supplementary linear feedback sector, repeated recursion is represented by the execution resolvent $(I-qST)^{-1}$. We identify $I-qST$ with an algebraic cross-ratio of graph subspaces. Under Hilbert--Schmidt assumptions, the associated return operator is trace class and defines the Fredholm feedback determinant \( \operatorname{det}_{F}(I-qST), \) whose zeros detect singular feedback configurations and whose logarithmic expansion records closed loop traversals.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-07-16T01:01:04Z
Fernando Lucatelli Nunes, Diogo Simm, Matthijs Vákár
arXiv categories: cs.PL, math.CT

Reverse-mode automatic differentiation is commonly given a denotational account in which each source type has a single cotangent type. Variant types obstruct this simply typed representation because the valid cotangent space depends on the branch selected at run time. Existing correctness results therefore use primal-indexed families of cotangent spaces, whose natural internal language is dependently typed. We show that the same dependency can be represented in an ordinary nondependent target. The cotangent fibres of each source type are embedded in a common ambient type, and a primal-indexed idempotent selects the valid fibre. Semantically, this amounts to passing from the constant-family model to its Karoubi completion. For a category $\mathcal C$ and a regular infinite cardinal $κ$, we prove that the constant-family inclusion extends to an equivalence $\mathrm{Kar}(\mathrm{Copow}*κ(\mathcal C)) \simeq \mathrm{Fam}*κ(\mathcal C)$ precisely when $\mathcal C$ is Cauchy complete and every $κ$-small family admits a common retract host. We also construct the resulting coproducts explicitly. Applying this theorem, we obtain a bicartesian closed semantics for reverse-mode automatic differentiation with variants using only ordinary target types, projectors, and backpropagators. Splitting the generated idempotents recovers the established dependent semantics. Thus dependent cotangent families and simply typed ambient cotangents equipped with projectors are equivalent presentations of the same denotational transformation.

arXiv abstract · PDF

Categorical, quantum, and computational semantics · primary corpus · published 2026-07-17T16:46:18Z
Neil J. Ross, Scott Wesley
arXiv categories: quant-ph, cs.LO, math.CT

It is well-known that combinatorial circuits are modeled mathematically by string diagrams in monoidal categories. Given a gate set $Σ$, the circuits over $Σ$ can be thought of as string diagrams in the free monoidal category generated by $Σ$. In this model, circuit semantics are then given by monoidal functors out of this free category. For quantum circuits, this functor is often valued in the category of unitary matrices. This model suffices for concrete quantum circuits, but fails to describe parameterized families of quantum circuits, such as those which arise in the analysis of ansatz circuits. In this paper, we introduce an approach to parameterized circuit semantics, which is based on enriched category theory. We first introduce an abstract categorical construction, and use this to gain new insights on controlled operations and quantum communication. We then study the special cases of Cartesian monoidal parameters and monoidal closed parameters, both endowing the parameterized semantics with useful constructions. We conclude by showing that the monoidal closed case can be used to unify two perspectives on quantum control.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-13T13:42:52Z
Matheus Duzi, Gabriel Fernandes, Paulo Magalhães Júnior
arXiv categories: math.GN, math.CO, math.LO

We provide a combinatorial characterization for pairs of order-theoretic trees with homeomorphic ray spaces, answering an open problem proposed by Kurkofka ad Pitz. This solution is inspired by the introduction of a transfinite topological game, which allows us to characterize not only ray spaces through the existence of winning strategies for one of the players, but also their homeomorphic classes. As applications of these results, we obtain a new topological characterization for graph-theoretic end spaces (thus obtaining yet another solution to a recently solved problem of Diestel), as well as for edge-end spaces and completely ultrametrizable spaces. We also introduce a generalization of the class of ray spaces (which is strict, as witnessed by the Sorgenfrey line). Furthermore, we establish that, for subspaces with cardinality less than continuum of end spaces, the scattered property is equivalent to the property of being, itself, an end space. At last, we determine that ray spaces in a couple of classes fail to have their product with any non-discrete space as a ray space.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-14T09:03:45Z
Yoshito Ishiki
arXiv categories: math.MG, math.GN, math.LO, math.RA

We investigate valued-field structures on Urysohn universal ultrametric spaces. We introduce $p$-adic Levi--Civita fields as subfields of $p$-adic Hahn fields and treat them together with ordinary Levi--Civita fields. For a subgroup $G$ of $\mathbb{R}$ containing $\mathbb{Z}$ and a countably infinite perfect field $k$, the corresponding Levi--Civita valued field is isometric to the $R$-Urysohn universal ultrametric space, where $R=\{0\}\cup\{η^{-g}\mid g\in G\}$. Thus these spaces admit field structures extending prescribed prime valued fields, including $\mathbb{Q}$ with the trivial valuation and the $p$-adic fields $\mathbb{Q}_{p}$. We also prove that complete valued fields with infinite residue fields are haloed, and hence universal for separable ultrametric spaces with corresponding distance sets. In the separable case, such a valued field is itself isometric to the corresponding Urysohn space. Examples include $\mathbb{C}_{p}$, the completion of the maximal unramified extension of $\mathbb{Q}_{p}$, Laurent series fields, and completions of their algebraic closures. Finally, for a countably infinite perfect residue field, the corresponding full Hahn-type valued field is a Urysohn universal ultrametric space exactly when its value group is order-isomorphic to $\mathbb{Z}$.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-15T11:41:07Z
Max Carroll, Anil Madhavapeddy, Patrick Ferris
arXiv categories: cs.PL

We explore how to provide programmers with an interactive interface for explaining the process by which static types and dynamic casts are derived, with the goal of improving the debugging of static and dynamic type errors. To this end, we define mathematical foundations for a decomposable highlighting system within a bidirectional system and show how these can be propagated through dynamic types in a cast system. Our prototype implementation in the gradually typed Hazel language includes a web-based user interface, through which we highlight the importance of type-level debugging.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-16T13:05:19Z
Jan Friso Groote, Erik P. de Vink
arXiv categories: cs.LO

This article gives a historical overview of the background, motivation and development of μCRL and its successor mCRL2, from the inception to the present. Both mCRL2 and μCRL are similar, compact, but very expressive formalisms based on process algebra, term rewriting, and the modal mu-calculus. They are developed to model and analyse the behaviour of interacting systems, i.e., systems that communicate by exchange of messages, among each other and with the outside world. Every contemporary computer system can be viewed as such an interacting system and their communication schemes are difficult to design correctly. By sticking to the mathematical foundations, but being led by the desire to be practically relevant, the formalism has grown to become very versatile. In particular, mCRL2 does not only foster the development of theory and the formulation of correctness proofs, but it is also the basis of a large set of automatic tools that help to provide insight in the behaviour of complex computer controlled systems.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-16T13:35:56Z
Weijun Chen, Bo Fu, Yuxi Fu, Huan Long, Chengfeng Xue, Qizhe Yang, Yangluo Zheng
arXiv categories: cs.FL, cs.LO

A VASS can be viewed as a finite-state automaton manipulating a fixed number (called its dimension) of counters holding non-negative values. The reachability problem, asking whether there is a run from one configuration, defined by a state and values of the counters, to another configuration, has been a long-standing algorithmic challenge in theoretical computer science. When the dimension is part of the input, the problem has been shown to be ACKERMANN-complete in 2021. For fixed dimension greater than 2, and in particular for dimension 3, the exact complexity of the reachability problem remains unclear. For a long time the known algorithms for the 3-dimensional VASS reachability problem had been non-elementary, while the best known lower bound is merely PSPACE hardness inherited from dimension 2. A recent breakthrough in (Czerwiński, Jecker, Lasota, Orlikowski, ICALP 2025) gave the first elementary upper bound for the problem, namely 2-EXPSPACE. In this paper it is shown that the reachability problem in 3-VASS belongs to EXPSPACE. The proof is based on a hierarchical pumpability analysis, yielding a doubly-exponential length bound on the shortest runs between two configurations.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-17T01:57:57Z
Douglas S Bridges
arXiv categories: math.CA, math.LO

We give an improved, detailed presentation of the constructive proof of the following corrected version of Theorem 2 of Locatedness, Convexity, and Lebesgue measurability: Let $\mathbf{S}$ be a Lebesgue integrable complemented set in $\mathbb{R}^N$ such that $μ(\mathbf{S})>0$ and $S^1$ is both bounded and convex. Then $S^1$ is totally bounded and hence located in $\mathbb{R}^N$.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-17T10:04:24Z
Zalán Gyenis
arXiv categories: math.LO

That the inclusion $Q(F_3(X))\subseteq \mathsf{Pa}^-_3$ is proper and Mod$(\mathbf{qb}_3)$ is not generated by free $p$-algebras is proved, answering two open questions from Kowalski-Słomczyńska \cite{KowSlom}.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-18T00:48:24Z
Abdallah Khemais
arXiv categories: cs.AI, cs.LG, cs.PL

Function-preserving network growth techniques such as Net2Net and progressive stacking expand a model's capacity without destroying its learned function, but existing formulations either tolerate numerical perturbations or require a full rebuild of the training program. We formalize Exact Network Surgery: the in-place insertion of a residual block into a live computational graph such that (i) the network function is preserved -- bit-exactly under explicit floating-point hypotheses -- and (ii) inserted parameters remain trainable immediately after insertion. We prove an identity-morphism theorem for gated residual blocks, a structural-locality theorem showing that a reactive invalidation engine recomputes exactly the downstream cone of the insertion point, leaving every other node's value and optimizer state untouched, and an escape-from-initialization proposition showing that the Gradient Shadowing gate alpha, initialized at zero over a randomly initialized branch, receives a generically non-zero gradient at insertion time. We identify a degenerate configuration -- zero-initialized output projections combined with a zero gate -- that is an exact saddle point gradient descent cannot escape. Every claim is validated on the reference implementation in NeuroDSL, a reactive graph engine in Julia: grafting is bit-exact on every logit tested (0 mismatches out of 1600); the gate escapes zero at the first optimizer step and unlocks branch gradients at the second, exactly as predicted; the degenerate configuration exhibits gradients identically zero for the entire 600-step run; surgery cost tracks downstream cone size with r = 0.9992 while graft-plus-invalidation bookkeeping is constant (about 0.75 ms) across insertion depths; and training resumes bit-identically across a real process restart. A flagged preliminary appendix reports first single-seed observations on post-insertion gate dynamics.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-18T02:33:53Z
Sebastián Buss, Diego Castaño, José Patricio Díaz Varela
arXiv categories: math.LO

A conucleus $δ$ on a partially ordered monoid $\mathbf{A}$ is an interior operator that satisfies $δ(a) \cdot δ(b) \leq δ(a \cdot b)$ and $δ(a) \cdot δ(1) = δ(a)$ for all $a,b \in A$. A conucleus is multiplicative if the equality $δ(a \cdot b) = δ(a) \cdot δ(b)$ holds for all $a,b \in A$. In this article we focus on the study of conuclei on hoops, structures which generalize well-known classes of algebras, such as the class of MV-algebras and BL-algebras. Among several results, we provide a Glivenko-type theorem for conuclei. Special emphasis is given to term definable conuclei. The main result of this article is an explicit description of all terms that define a multiplicative conucleus on every structure of an arbitrary proper variety of Wajsberg hoops. We also show that the problem of finding terms that define (multiplicative) conuclei on a variety of basic hoops or BL-algebras is equivalent to finding such terms on some variety or some pair of varieties of Wajsberg hoops. We provide nontrivial interesting examples.

arXiv abstract · PDF

Other logic and mathematical structures · primary corpus · published 2026-07-18T16:58:59Z
Roberto Borelli, Davide Bresolin, Luca Geatti, Angelo Montanari, Matteo Zavatteri
arXiv categories: cs.FL, cs.LO

The cascade product is a fundamental construction in automata theory, enabling hierarchical composition of automata and playing a central role in decomposition results such as the Krohn-Rhodes theorem. However, its use is limited by the exponential size required to represent cascades, which stems from the fact that each component may depend on all preceding ones, leading to exponentially large alphabets. To address this issue, we introduce the $Σ$-chain product, a restricted variant in which each component depends only on the input alphabet and the component immediately preceding it. We show that $Σ$-chains achieve linear-size representations and can be exponentially more succinct than cascades. We prove that $Σ$-chains and cascades are expressively equivalent to specific classes of automata, such as permutation-reset automata. As a consequence, we derive that a language is regular if and only if it is recognized by a $Σ$-chain of permutation-reset automata. Finally, we analyze structural properties of $Σ$-chains of reset automata, including a relation with well-known subclasses of star-free languages.

arXiv abstract · PDF