https://arxiv.org/api/C7F5ysXTeylZFJmYEg3NK9haxe0 2026-09-11T19:05:51Z 10292 15 15 http://arxiv.org/abs/2608.27180v2 2026-09-06T11:15:06Z

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.

2026-08-27T14:28:11Z Vincent Wang-Maścianica http://arxiv.org/abs/2609.06443v1 2026-09-06T07:35:08Z

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. This is the extended version of a paper presented at APLAS 2025.

2026-09-06T07:35:08Z 82 pages, 17 figures. Extended version of a paper presented at APLAS 2025 (LNCS 16201, pp. 88-106, https://doi.org/10.1007/978-981-95-3585-9_5, full version: arXiv:2509.11901) Kentaro Kobayashi Yukiyoshi Kameyama http://arxiv.org/abs/2609.06328v1 2026-09-06T01:25:41Z

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.

2026-09-06T01:25:41Z 25 pages, 18 figures, 2 tables Adhitha Dias Kirshanthan Sundararajah Artem Pelenitsyn Milind Kulkarni http://arxiv.org/abs/2609.06301v1 2026-09-05T23:22:25Z

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.

2026-09-05T23:22:25Z Amir Shaikhha Anna Herlihy Hung Ngo http://arxiv.org/abs/2601.15294v2 2026-09-05T22:18:48Z

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.

2025-12-16T18:24:28Z Elif Uskuplu Lawrence S. Moss Valeria de Paiva http://arxiv.org/abs/2609.06231v1 2026-09-05T19:09:44Z

Two centuries ago Pierre-Joseph Proudhon envisioned a social contract that is (1) an agreement of man with man; (2) reciprocal; (3) imposing no obligation upon the parties except that which results from their personal promise; (4) subject to no external authority; (5) freely accepted and signed by all the participants; (6) of the nature of a contract of exchange. He also envisioned a property of social contracts, analogous to a property of digital platforms we term grassroots: that one could "make a contract with all, as ... with some"; digitally, that a grassroots platform can have multiple instances, which may coalesce by mutual consent. We define grassroots social contracts as social contracts meeting these conditions and that (7) people are free to deal with each other; and (8) there is no external register of people. We show that a grassroots social contract can be transformed into a working grassroots platform through an abstraction cascade, from the contract text to formal act schemas, verified syntactically to be grassroots, and then to volition-guarded multiagent atomic transactions. Act schemas are a formal language for the acts the contract describes, each naming the parties' roles, which of them must will the act, and its precondition and effect at each role. Any contract written in this language meets the eight conditions, provided it is syntactically grassroots, satisfying three decidable conditions, Introduction, Provenance and Volition. We prove that the protocol realising a syntactically grassroots contract is grassroots, and volitionally so. Clauses of a grassroots social contract are of three legal types: a breach of an enforced clause is impossible with a correct implementation; a breach of an attested or undertaken clause can be taken to court, with signed evidence for an attested clause. We illustrate them with a grassroots social graph and grassroots currencies.

2026-09-05T19:09:44Z James Golike Andy Lewis-Pye Ehud Shapiro http://arxiv.org/abs/2609.05364v1 2026-09-04T17:08:51Z

Machine-learning performance modeling is a uniquely hostile terrain for long-lived software: the assumptions baked into today's abstractions are invalidated by tomorrow's models and systems, forcing perpetual refactoring of performance-modeling frameworks. Meanwhile, AI coding agents have become fast and capable enough that regenerating an entire library is cheaper than paying down the tech debt of incrementally patching it. We describe SMART, a rigorous symbolic performance-modeling library for ML systems whose main branch contains almost no code: the repository is a DAG of self-contained natural-language design docs, coding sub-agents regenerate the implementation from only the docs on new version updates, and every human change is a natural-language edit to a doc--self-documenting by construction. Two ingredients make regeneration reliable: (i) a design-doc style built around step-by-step worked examples that act as in-context demonstrations for the generating agents, and (ii) a minimal, recursively defined operator IR with symbolic (SymPy) cost expressions, a fast analytical roll-up mode for large sweeps, and a slow modulo-scheduling mode for fine-grained schedule studies. Regenerated implementations reproduce hand-audited reference models--including DeepSeek-V3 serving on a TPU pod slice--to round-off precision, suggesting that design docs--not code--can be the durable artifact for ML-systems co-design tools.

2026-09-04T17:08:51Z Samuel Kushnir Kimia Noorbakhsh Kavya Sreedhar Liqun Cheng Ming Liu Parthasarathy Ranganathan Mohammad Alizadeh Fred Kjolstad Suvinay Subramanian http://arxiv.org/abs/2609.05288v1 2026-09-04T15:42:57Z

Data stores are widely used because they provide persistence, scalability, and fault tolerance with a simple interface. However, most data store applications configure the data store to use weak isolation to achieve scalable performance, resulting in sporadic unserializable executions that are incorrect or fail. Prior work uses dynamic predictive analysis to infer violations from execution traces, but it cannot handle relational (i.e., SQL) queries with complex predicates, and it predicts executions that do not violate View Serializability. This paper introduces Augur, the first dynamic predictive program analysis that (1) supports data store applications with complex relational queries and (2) reports only executions that violate View Serializability. The evaluation demonstrates that Augur finds feasible, unserializable executions in the widely used OLTP-Bench programs and in the widely used e-commerce application Spree.

2026-09-04T15:42:57Z Chujun Geng Noah Charlton Spyros Blanas Michael D. Bond Yang Wang 10.1145/3839480 http://arxiv.org/abs/2608.18084v2 2026-09-04T09:09:56Z

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

2026-06-04T11:21:04Z 18 pages; accepted to Findings of EMNLP 2026 Zhuo Liu Ding Yu Hangfeng He http://arxiv.org/abs/2609.04904v1 2026-09-04T09:07:15Z

This paper presents Cordell Programming Language (CPL), a compact C-like systems language that retains C's direct access to memory, layout, and machine interfaces while experimenting with a smaller grammar and selected conveniences from newer languages. Also this paper studies whether C-like are more convenient to use for compiler experiments than modern approaches and paradigms. While the language and compiler provide primitive values, pointers, arrays, containers with methods, unions, generic functions, overloads, entry-point and section control, system calls, and inline assembly, they do not provide high-level constructs such as classes, built-in methods, a standard library, or memory protection. The article describes the language design, compiler pipeline, target backends, static-analysis architecture, and OS-facing use cases, then evaluates the prototype backend with reproducible x86_64 and i386 microbenchmarks against C compiler baselines. The obtained results suggest that the compiler can produce code comparable to that produced by production compilers such as GCC and Clang, as well as by small compilers such as TinyC and SmallerC.

2026-09-04T09:07:15Z Nikolay Fot Alexander Vinarsky http://arxiv.org/abs/2605.23358v2 2026-09-04T08:18:37Z

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.

2026-05-22T08:22:31Z 35 pages, 15 figures Qifan Huang Minbo Gao Li Zhou Mingsheng Ying http://arxiv.org/abs/2609.04585v1 2026-09-04T00:35:54Z

The Multi-Level Intermediate Representation (MLIR) has made reusable compiler infrastructure practical for domain-specific computation. However, MLIR's strong compile-time type requirements and low-level (C++) extension model can be a poor match for high-level, dynamically specialized languages such as Julia. MLIR has several drawbacks for dynamic programming languages in terms of the type system and level of abstraction. It is thus extremely challenging for non-compiler or scientific computing users to introduce new programming abstractions and express algorithm implementations in a form that remains both natural and optimizable. As a result, library interfaces for linear algebra, mesh processing, partial differential equations, and related domains often sit outside the compiler optimization path. We present JLIR (Julia-native Level Intermediate Representation), a Julia-native intermediate representation framework that brings the main benefits of MLIR-style multi-level, dialect-oriented compilation into the Julia ecosystem while remaining usable as ordinary Julia code. JLIR represents Julia programs before low-level lowering, supports extensible operations and transformation passes through Julia's language mechanisms, and allows partially typed programs to remain transformable until concrete types are known. The framework includes built-in dialects for arithmetic, control flow, functions, structured loops, and memory operations, and it also includes a lightweight mechanism for adding new domain operations without modifying the core system. To demonstrate JLIR's capabilities, we applied it to automatic Julia for Accelerators (JACC) kernel generation.

2026-09-04T00:35:54Z Narasinga Rao Miniskar Seyong Lee Keita Teranishi Jeffrey S Vetter http://arxiv.org/abs/2609.04535v1 2026-09-03T22:48:21Z

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.

2026-09-03T22:48:21Z Amirali Sajadi Saikat Dutta Preetha Chatterjee http://arxiv.org/abs/2609.04528v1 2026-09-03T22:37:04Z

Humans can learn and generalize novel concepts from sparse data because they express knowledge in rich structural formats. In this paper, we propose that programs are a strong candidate for universal representation of concepts. We review computational models of concept learning that use programs as their concept representation and evaluate their contribution toward a universal representational language.

2026-09-03T22:37:04Z Originally completed as an M.S. capstone project at UCLA in 2022 Aishni Parab http://arxiv.org/abs/2609.04523v1 2026-09-03T22:22:37Z

Designing and authoring high-performance custom kernels for accelerators is a complex task that requires deep hardware-level expertise. Large Language Models (LLM) can be leveraged together with real-time compiler feedback to build agentic systems for kernel generation. In this work, we present MaxKernel, a multi-agent system that implements three distinct paradigms for TPU kernel development: (1) a Human-in-the-Loop (HITL) agent for collaborative, step-by-step design; (2) an Autonomous (Auto) agent that executes a fully automated, metric/trace-driven optimization loop; and (3) a Graph-Based Autonomous Search that scales the Auto agent for global exploration of the design space. All three paradigms leverage a shared pool of specialized sub-agents to handle planning, implementation, self-debugging, testing, and hardware profiling. We evaluate MaxKernel on JaxBench, a comprehensive suite of 50 diverse kernel tasks for TPUs, alongside complex, real-world workloads from state-of-the-art open-source models. We demonstrate that MaxKernel consistently generates highly optimized implementations, matching expert hand-tuned baselines and delivering significant performance across the benchmark. Our agent is open-sourced and available https://github.com/AI-Hypercomputer/accelerator-agents/tree/main/MaxKernel.

2026-09-03T22:22:37Z 14 pages, 6 figures, 4 tables Shangkun Wang Nina Cai Charles Hoong Julian Walker Gerson Kroiz George Vanica Deepak Patil Andi Gavrilescu Hassan Sipra Sethu Sankaran