SEARCH · Searcharxiv

Search Searcharxiv

Search indexed arXiv papers on artificial intelligence, large language models, computer vision and robotics. Read source abstracts and follow links to arXiv.

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

At least 19 recordsLinked to original sources

arXiv2026

Support Local Variables

Ruby is a dynamically typed and object-oriented programming language. Its primary implementation, CRuby, contains a bytecode virtual machine and a mature lazy basic block versioning (LBBV) just-in-time (JIT) compiler called YJIT. In order to both implement more advanced optimizations than YJIT supports and also encourage more outside contributions, we present a new method-based JIT called ZJIT. Like YJIT, ZJIT compiles from bytecode to machine code. Unlike YJIT, ZJIT has multiple global and local optimization passes. ZJIT's high-level intermediate representation is in static single assignment (SSA) form. In order to optimize Ruby's local variables, ZJIT lifts local variables into SSA values. This is a departure from how other Ruby compilers handle locals: other JIT compilers either leave local variables as memory loads and stores or do advanced partial evaluation to recover SSA values from memory. While implementing locals, we (re-)discovered what features make local variables in Ruby especially challenging to compile correctly and efficiently. We demonstrate these features and illustrate how we solved these problems in ZJIT.

cs.PL↗

arXiv2026

KnowTeX: Visualizing Mathematical Dependencies

Dependency graphs that show how definitions, theorems, and proofs relate to each other are valuable for understanding the structure of mathematical texts. Existing tools such as Lean Blueprint and plasTeXdepgraph generate such graphs within formal proof ecosystems, but they require familiarity with proof assistants or specific compilation pipelines. We present KnowTeX, a standalone Python tool that extracts dependency graphs directly from LaTeX sources without requiring any external framework. KnowTeX supports two complementary modes: a manual mode where authors annotate their source with lightweight commands compatible with Lean Blueprint, and an infer mode that automatically discovers dependencies through a layered system of deterministic and heuristic rules. The tool handles multi-file projects, detects cycles, applies transitive reduction, and exports graphs in DOT, TikZ, and PNG formats with an interactive preview. We evaluate KnowTeX on several mathematical texts and discuss how it complements recent tools such as LeanArchitect, which operates from the Lean side, while KnowTeX works entirely on the LaTeX side without requiring any formalization.

cs.HC↗

arXiv2026

Confluence of conditional rewriting modulo

Sets of equations E play an important computational role in rewriting-based systems R. The equivalence relation =E induced by E introduces a partition of terms into E-equivalence classes on which rewriting computations, denoted ->R/E and called rewriting modulo E, are issued. This paper investigates confluence of ->R/E, usually called E-confluence, for conditional rewriting-based systems, where rewriting steps are determined by conditional rules. We rely on Jouannaud and Kirchner's framework to investigate confluence of an abstract relation R modulo an abstract equivalence relation E on a set A. We show how to particularize such a framework to be used with conditional systems. Then, we show how to define appropriate finite sets of conditional pairs to prove and disprove E-confluence. We introduce (i) Logic-based Conditional Critical Pairs, which do not require the use of (often infinitely many) E-unifiers to provide a finite representation of the local peaks considered in the abstract framework. We also introduce (ii) parametric Conditional Variable Pairs which are essential to deal with conditional rules in the analysis of E-confluence. Finally, we introduce (iii) Down Conditional Pairs which are often necessary to disprove E-confluence. Our results apply to well-known classes of rewriting-based systems, improving on previous results. As for unconditional systems, our results apply to Equational Term Rewriting Systems, first investigated by Huet and then by Jouannaud, and Jouannaud and Kirchner, among others. As for conditional systems, our results also apply to conditional rewrite theories and Maude.

cs.LO↗

arXiv2026

Typed Flexible-Arity Slotted E-Graphs: A Soundness Construction and an Alloy Case Study

Slotted e-graphs represent open terms modulo consistent renaming, while algebraic operators benefit from canonical sequence, bag, or set children. We compose the two at a specification level: typed slot-mapped invocations inhabit operator-declared ports whose sibling quotient and recursive flattening licenses are certified separately. A generic finite quotient presentation proves exactness of its least-orbit normal form, while certified records specify effective-support kernel extraction and collision. For abstract obligation traces carrying local endpoint certificates, we prove finite-unfolding equational soundness. An Alloy case study compares seven related pipeline arms on a frozen corpus and a controlled transformation suite.

cs.PL↗

arXiv2026

Expressive power of one-shot control operators and coroutines

Control operators, such as exceptions and effect handlers, provide a means of representing computational effects in programs abstractly and modularly. While most theoretical studies have focused on multi-shot control operators, one-shot control operators---which restrict the use of captured continuations to at most once---are gaining attention for their balance between expressiveness and efficiency. This study aims to fill the gap. We present a mathematically rigorous comparison of the expressive power among one-shot control operators, including effect handlers, delimited continuations, and even asymmetric coroutines. Following previous studies on multi-shot control operators, we adopt Felleisen's macro-expressiveness as our measure of expressiveness. We verify the folklore that one-shot effect handlers and one-shot delimited-control operators can be macro-expressed by asymmetric coroutines, but not vice versa. We explain why a previous informal argument fails, and how to revise it to make a valid macro-translation.

cs.PL↗

arXiv2026

An Empirical Analysis of CodeQL False Positives and Query Refinements for Java Vulnerabilities

Static application security testing (SAST) tools help developers find vulnerabilities before deployment, but false positives create substantial triage effort. We study whether CodeQL false positives in Java security analysis form recurring, explainable patterns that can be reduced by refining the analysis. We run CodeQL's Java security query suite on 167 CVE instances from 110 projects, focusing on the ten queries with the highest false positive rates. We manually review 500 sampled false positive paths and locations and construct a source-level taxonomy. The five categories are Missed Path Constraint or Sanitization (36.6%), Benign Execution Context (29.4%), Missing Trust Boundary Modeling (27.6%), Imprecise Concurrency Modeling (5%), and Imprecise Sink Modeling (1.4%). Guided by these findings, we implement CodeQL refinements that detect and filter recurring false positive patterns at the query level. The refinements remove 81.8% of reviewed false positives. Across the full selected-query dataset, they remove 15.8% of reported paths and locations while retaining 7 of 8 true positives. This shows that many false positives can be reduced in the analysis, although fixed refinements often depend on project-specific context. To address this generalization gap, we evaluate whether agentic coding tools can adapt refinement patterns to new projects. Given our patterns as templates, the two tools succeed on 56% and 62% of tasks, with query compile-pass rates above 90%. Without this guidance, both succeed on only 28%, while compile rates fall to 30-36%. These results support a refinement-oriented SAST workflow in which recurring false positives are modeled in CodeQL queries and automatically adapted to different project contexts, reducing repeated triage.

cs.SE↗

arXiv2026

Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code

Symbolic execution is a powerful program analysis technique, but its effectiveness is fundamentally limited by solver-hostile program fragments, complex numerical reasoning, and unbounded heap structures. Recent work proposed replacing constraint solvers with large language models (LLMs) to bypass these limitations, but such approaches struggle to analyze real-world codebases, where deep execution paths require globally consistent reasoning across many interacting constraints. We present Gordian, a hybrid symbolic execution framework that uses LLMs selectively to generate lightweight ghost code that aids an SMT solver in handling solver-hostile code fragments, while preserving its precise, global reasoning capability. In particular, we propose three types of ghost code: (1) inversion of difficult code fragments with iterative bidirectional constraint propagation, (2) modeling via solver-friendly surrogates while preserving relevant behavior, and (3) semantic partitioning of unbounded heap spaces. We implemented Gordian on top of the KLEE symbolic execution engine and evaluated it on synthetic "logic bombs" capturing distinct symbolic reasoning challenges, a popular mathematical library FDLibM, and four structured-input programs (libexpat, jq, bc and libyaml). Across benchmarks, Gordian improves coverage by 28.5-115.2% over traditional symbolic execution baseline and by 74.1-189.8% over LLM-based symbolic execution baselines, while reducing LLM token usage by an average of 91-96%. This highlights the practicality and effectiveness of this approach in real-world settings.

cs.PL↗

arXiv2026

Granthi: Higher-Order Quantum Programming via Unitary Wiring

Many mainstream quantum programming languages confine higher-order structure to a classical host while restricting the quantum layer to first-order operations on qubits. This paper presents Granthi, a purely unitary higher-order quantum programming language built on three design commitments: quantum programs are first-class values that may be passed, returned, and coherently composed; additive structure is tag-preserving routing rather than observational branching, so control may remain in superposition; and programmer-facing finite label types with staged reversible-operation bindings provide domain-level control spaces without exposing tag management. These bindings are eliminated by elaboration before Source typing. Granthi deterministically normalizes each Source program to a canonical wiring form. Every well-typed Source program, including a term of function type, has a unitary boundary interpretation. Under backend correctness (BC), the reference compiler produces a unitary circuit realizing that interpretation. Granthi's currently supported executable fragment is implemented end-to-end: an OCaml DSL elaborates surface programs through a higher-order Core IR to executable quantum circuits via pytket. The language directly supports the pure-unitary quantum switch for explicitly supplied operations; closed instances compile to static circuits. It also supports interference on control-flow history and structured finite control, all within the purely unitary fragment

quant-ph↗

arXiv2026

Mapping Dynamic, Hierarchical Quantum Circuits

Qubit mapping is a critical pass in quantum compilation. Despite various advances, dynamic circuits, those exhibiting data dependent control-flow, often resulting from qubit measurements, are not yet supported by the vast majority of available qubit mappers. The crucial limitation to overcome is the dependence on flat, one-dimensional representations of circuits. Further, qubit mappers currently lack compiler abstractions that capture the hierarchical nature of circuits, hindering the qubit mapping process. In this paper, 1 we introduce a new qubit mapping method and analyses to tackle hierarchical dynamic circuits. Our novelty resides in four key aspects: modeling (statically) sub-circuits in disjoint control-flow paths, introducing a novel Qubit Reconciliation pass to maintain consistency between sub-circuit and control-flow boundaries, a loop-entry remapping pass, and a refined cost function enhanced for SWAP count, circuit depth, circuit latency and error. We demonstrate the efficiency of our approach on a wide range of dynamic circuits on two monolithic Quantum Processing Units of 127 and 156 qubits, and on chiplet hexagon-based QPUs. On monolithic QPUs, our qubit mapper improves the SWAP count by up to 52%, depth by up to 18%, latency by up to 18.6%, and error by up to 40%. On chiplet architectures, we achieve improvements of up to 36% on SWAP count, 8.7% on depth, 15% on latency, and 15% of error.

cs.PL↗

arXiv2026

Erased Postulates, Identity Types and Quotients

This text is concerned with the question of whether, in type theory with erasure annotations, one can postulate that some type is inhabited and still have a guarantee that a program will not get stuck. Previous work has provided such guarantees for consistent erased postulates, i.e. postulates that are restricted to be used in erased contexts. Here those guarantees are extended to type theory with identity types. Similar ideas provide a simple way to support quotient types: it is shown that one can let things like "the equivalence classes for two related values are equal" be erased postulates and have an eliminator that only computes for the equivalence class constructor, and still get a guarantee that programs will compute correctly. Another question is whether programs compute correctly if one is allowed to transport (cast) using erased identity proofs. It is shown that this is safe in the absence of quotients and postulates, and in the presence of quotients and erased postulates that can be implemented using equality reflection. However, unrestricted transports of this kind are not compatible with erased, postulated univalence. For that reason the text includes a study of the function []-cong, which encapsulates a limited form of transport for erased identity proofs. The text is accompanied by machine-checked Agda proofs.

cs.PL↗

arXiv2026

Python in the front, party in the Backline: compiling quantum workloads across CPUs, GPUs, and FPGAs

Moving from quantum research and development to production-grade, fault-tolerant quantum workload execution remains one of the most significant challenges facing quantum platform builders. While Python frameworks have enabled an easy entry point for quantum algorithm design, the low-latency requirements for real-time quantum error correction (QEC) demand performance that traditional interpreted environments cannot provide. FPGAs and ASICs play a central role at these layers, but their specialized programming models make development rigid and time-consuming. CPUs, GPUs, and other accelerators introduce a different challenge: as infrastructure becomes increasingly heterogeneous, programming across different devices and their associated abstractions becomes more complex. Allowing researchers to write workloads in high-level languages that map to low-latency execution across diverse distributed target platforms will enable the development of key infrastructure for utility-scale quantum systems. For this, we introduce $\textit{Backline}$, a heterogeneous compilation and runtime framework built within PennyLane and Catalyst. Backline allows us to design and build quantum-classical workloads for high-performance and low-latency devices, with compilation directly from a Python interface through MLIR. We demonstrate the compilation and execution of several quantum workloads with low-latency data movement across a mix of CPUs, GPUs, and FPGAs, for both local and distributed remote hardware targets, all from a vendor-agnostic Python frontend. With an AMD VPK120 FPGA board as the controller, issuing each round from its hardware-handshake engine, we measured median steady-state round-trip latencies over RoCE v2 of $2.305~μ$s to an AMD Ryzen Threadripper PRO CPU and $4.5~μ$s to an AMD Instinct MI210 GPU across $10^6-1$ rounds per path, demonstrating microsecond-scale synchronous co-processing.

quant-ph↗

arXiv2026

A monadic interpreter and type-and-effect checker

We present a concrete implementation in Haskell of a monadic framework that includes both a small-step interpreter and a type-and-effect checker for the corresponding language. Our approach separates the language syntax from the semantics of its effects. This design allows the interpreter to remain parametric over the underlying monad, while the static checker approximates effects independently of their concrete implementation. The theoretical foundation of this framework-applied to a call-by-value lambda calculus with generic effects represented by operations that produce monadic values and are managed through handlers-was introduced in previous work, where the focus was on proving the soundness of the approach. In contrast, the present work leverages Haskell's support for modular programming and monads to demonstrate that the framework is practically implementable and usable. We illustrate the approach with examples using the monad of exceptions and the one of nondeterminism and expressions both with and without handlers.

cs.PL↗

arXiv2026

You may implement this later: Cofunctors as partial implementations

A functor is a familiar model of an implementation, where every operation in a specification is assigned a concrete instantiation at the outset. But some tasks are less eager: we often want to assemble systems while leaving backend choices such as data representations and algorithms for later. We observe that cofunctors admit a direct reading as such partial implementations, which are implementations whose extra argument is a state-dependent family of deferred choices. While cofunctors (also called retrofunctors) are not novel, their conceptual and purposive reading in this manner appears to be.

cs.PL↗

arXiv2026

SparseConflicts: Handling Conflicting Data Layouts in Sparse Tensor Contractions

Optimizing sparse tensor computations is challenging due to the use of compressed storage formats, which leads to non-affine loop nests and a vast, complex schedule space. The performance of a given schedule is sensitive to the sparsity pattern of the input tensors, making it difficult to find a single optimal solution. When input tensors in the same tensor contraction have conflicting data layouts in relation to the iteration order, it requires costly-both in time and memory-layout transformation, such as transposition. A promising but under-explored alternative is to generate a schedule that avoids explicit transposition, but this has not been systematically supported in existing compilers. This paper presents a new code generation strategy that generalizes the intermediate representation of the TACO sparse tensor compiler to generate a single loop nest, circumventing explicit transposition of tensors when the tensors have conflicting data layout iteration orders. We extend TACOś iteration graph to express a search-based strategy for locating elements in tensors with conflicting layouts, and we introduce new intermediate representation nodes to lower these schedules to efficient code. This enables the systematic generation of loops that do not require explicit transposition, thus avoiding the overhead of materializing temporary tensors. We evaluate our approach on a set of sparse tensor contractions using both real-world and synthetic datasets. Our results demonstrate that for computations with misaligned data layouts, our fused approach achieves up to 2x speedup for some sparsity patterns over the traditional approach of explicitly creating a transposed temporary. We also provide guidelines for when this new scheduling strategy is likely to be beneficial.

cs.PL↗

arXiv2026

Staged Hybrid Quantum-Classical Programming

Hybrid quantum-classical computing systems consist of a classical control system that sends quantum circuits and receives measurement results from a quantum co-processor. Such systems allow us to model algorithms that require the classical control system to generate quantum circuits on the fly, potentially based on prior measurement results. This is challenging, as the classical control system must generate quantum circuits that manipulate live quantum states. In this setting, the classical control system is generating further quantum circuits while the quantum co-processor is internally maintaining the state of the live qubits; this is not ideal, since this not only is costly but also introduces additional sources of noise to the live qubits. Thus, we want to minimize the latency between receiving measurement results and sending the next quantum circuit to be executed by pre-computing quantum circuits. We introduce HyQ (pronounced haiku), a multi-modal language based on adjoint logic that pre-generates quantum circuits before executing a hybrid quantum-classical program. We achieve this by separating our semantics into two distinct stages: 1) compile-time generation of quantum circuits and classical runtime code and 2) execution of the classical runtime code that instruments the quantum co-processor. This separation between stages allows us to formally guarantee that all circuit-generation logic occurs before the instrumentation logic, i.e., the actual runtime, and minimizes the idling of the quantum co-processor at runtime. We give a type system, a circuit-normalization semantics for the compile-time stage, which eagerly performs all circuit-generation logic, and a runtime semantics for HyQ that corresponds to the second stage. We prove type preservation and progress for both semantics.

cs.PL↗

arXiv2026

Compiling Linear Datalog to SQL for Program Analysis

Datalog is a declarative query language that has proven highly effective for expressing static program analyses. Although Datalog has deep roots in database theory, most recent advances have largely emerged from the programming languages and compiler communities, with systems such as Soufflé. In contrast, modern relational engines have made significant progress in optimizing recursive SQL. This paper revisits the connection between Datalog and relational databases, advocating recursive SQL as a backend for Datalog evaluation. We present a compilation framework that translates Datalog programs, particularly those in the Linear Datalog fragment, into equivalent recursive SQL queries. To bridge the gap between Datalog and SQL, the compiler routes every program through an intermediate language called Midlog. The compiler additionally recovers functional dependencies from the program and exposes them as schema keys, unlocking the engine's standard query optimizations. This approach enables existing database engines to execute a broad class of program analyses, outperforming the Soufflé engine by up to an order of magnitude on the Umbra backend. Umbra achieves a geometric-mean speedup of 5.46$\times$ at 8 threads, whereas DuckDB is competitive with Soufflé single-threaded and is slower at 8 threads (geometric-mean speedup of 0.68$\times$). Furthermore, the generated SQL is portable; it runs on seven database systems without any engine modification. Our results highlight what the relational engines require to fully support Datalog for large-scale program analysis.

cs.DB↗

arXiv2026

A Compilation Framework for Quantum Simulation of Non-unitary Dynamics

Most quantum compilers assume programs are reversible unitary circuits. This fits closed-system algorithms, but not open-system simulation, where the natural program objects are quantum channels describing non-unitary dynamics. We present a channel-first compilation framework that treats channels as first-class compilation objects. Our core IR, ChannelIR, represents channels explicitly in Kraus form, a standard channel representation, with Pauli-sum structure, enabling algebraic rewrites before circuit synthesis. We instantiate the framework with LindFront, a frontend that lowers continuous-time Lindbladian generators to short-time channels, and a backend that compiles these channels to executable circuits with structure-aware optimizations. On Lindbladian and channel-simulation benchmarks, the optimized pipeline reduces gate count by up to 99% over an unoptimized channel-first baseline and scales better than circuit-first Stinespring compilation.

quant-ph↗

arXiv2026

Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Proving

Theorem proving in real-world Lean 4 projects is challenging because proofs often depend on project-specific context. While iterative refinement can use compiler errors to repair failed proofs, reusing failed attempts requires careful search control: some proofs provide better starting points than others, and later revisions may degrade a partially correct proof. We propose a compiler-guided proof search framework that balances exploration and exploitation. It explores diverse starting points through dual-model generation and stagnation-triggered resampling, while exploiting promising proof states through current-best refinement guided by compiler-grounded pairwise comparison. Experiments on seven real-world Lean 4 projects from miniCTX-v2 show that our method achieves a better effectiveness--efficiency tradeoff than pass@k baselines. Within the pass@32 budget, our method improves average pass rate by 12.8 percentage points while reducing LLM calls by 21.9%.

cs.CL↗