https://arxiv.org/api/tLochFBLEQ+DtrtyD8oOVRZPD9A 2026-06-28T07:27:00Z 9951 1500 15 http://arxiv.org/abs/2408.10054v3 2025-06-14T05:21:49Z

Quantum recursive programming has been recently introduced for describing sophisticated and complicated quantum algorithms in a compact and elegant way. However, implementation of quantum recursion involves intricate interplay between quantum control flow and recursive procedure calls. In this paper, we aim at resolving this fundamental challenge and develop a series of techniques to efficiently implement quantum recursive programs. Our main contributions include: 1. We propose a notion of quantum register machine, the first quantum architecture (including an instruction set) that provides instruction-level support for quantum control flow and recursive procedure calls at the same time. 2. Based on quantum register machine, we describe the first comprehensive implementation process of quantum recursive programs, including the compilation, the partial evaluation of quantum control flow, and the execution on the quantum register machine. 3. As a bonus, our efficient implementation of quantum recursive programs also offers automatic parallelisation of quantum algorithms. For implementing certain quantum algorithmic subroutine, like the widely used quantum multiplexor, we can even obtain exponential parallel speed-up (over the straightforward implementation) from this automatic parallelisation. This demonstrates that quantum recursive programming can be win-win for both modularity of programs and efficiency of their implementation.

2024-08-19T14:48:41Z 63 pages, 25 figures. Extended version of PLDI 2025 publication Zhicheng Zhang Mingsheng Ying 10.1145/3729283 http://arxiv.org/abs/2506.12212v1 2025-06-13T20:30:25Z

Freer monads are a useful structure commonly used in various domains due to their expressiveness. However, a known issue with freer monads is that they are not amenable to static analysis. This paper explores freer arrows, a relatively expressive structure that is amenable to static analysis. We propose several variants of freer arrows. We conduct a case study on choreographic programming to demonstrate the usefulness of freer arrows in Haskell.

2025-06-13T20:30:25Z In submission to the Haskell Symposium 2025 Grant VanDomelen Gan Shen Lindsey Kuper Yao Li http://arxiv.org/abs/2506.12202v1 2025-06-13T20:11:22Z

Modern large language models (LLMs) are often deployed as agents, calling external tools adaptively to solve tasks. Rather than directly calling tools, it can be more effective for LLMs to write code to perform the tool calls, enabling them to automatically generate complex control flow such as conditionals and loops. Such code actions are typically provided as Python code, since LLMs are quite proficient at it; however, Python may not be the ideal language due to limited built-in support for performance, security, and reliability. We propose a novel programming language for code actions, called Quasar, which has several benefits: (1) automated parallelization to improve performance, (2) uncertainty quantification to improve reliability and mitigate hallucinations, and (3) security features enabling the user to validate actions. LLMs can write code in a subset of Python, which is automatically transpiled to Quasar. We evaluate our approach on the ViperGPT visual question answering agent, applied to the GQA dataset, demonstrating that LLMs with Quasar actions instead of Python actions retain strong performance, while reducing execution time when possible by 42%, improving security by reducing user approval interactions when possible by 52%, and improving reliability by applying conformal prediction to achieve a desired target coverage level.

2025-06-13T20:11:22Z Stephen Mell Botong Zhang David Mell Shuo Li Ramya Ramalingam Nathan Yu Steve Zdancewic Osbert Bastani http://arxiv.org/abs/2408.02509v2 2025-06-13T15:36:41Z

Modern code completion engines, powered by large language models (LLMs), assist millions of developers with their strong capabilities to generate functionally correct code. Due to this popularity, it is crucial to investigate the security implications of relying on LLM-based code completion. In this work, we demonstrate that state-of-the-art black-box LLM-based code completion engines can be stealthily biased by adversaries to significantly increase their rate of insecure code generation. We present the first attack, named INSEC, that achieves this goal. INSEC works by injecting an attack string as a short comment in the completion input. The attack string is crafted through a query-based optimization procedure starting from a set of carefully designed initialization schemes. We demonstrate INSEC's broad applicability and effectiveness by evaluating it on various state-of-the-art open-source models and black-box commercial services (e.g., OpenAI API and GitHub Copilot). On a diverse set of security-critical test cases, covering 16 CWEs across 5 programming languages, INSEC increases the rate of generated insecure code by more than 50%, while maintaining the functional correctness of generated code. We consider INSEC practical -- it requires low resources and costs less than 10 US dollars to develop on commodity hardware. Moreover, we showcase the attack's real-world deployability, by developing an IDE plug-in that stealthily injects INSEC into the GitHub Copilot extension.

2024-08-05T14:31:26Z Slobodan Jenko Niels Mündler Jingxuan He Mark Vero Martin Vechev http://arxiv.org/abs/2506.11701v1 2025-06-13T12:06:56Z

Permission systems which restrict access to system resources are a well-established technology in operating systems, especially for smartphones. However, as such systems are implemented in the operating system they can at most manage access on the process-level. Since moderns software often (re)uses code from third-parties libraries, a permission system for libraries can be desirable to enhance security. In this short-paper, we adapt concepts from capability systems building a novel theoretical foundation for permission system at the level of the programming language. This leads to PermRust, a token-based permission system for the Rust programming language as a zero cost abstraction on top of its type-system. With it access to system resources can be managed per library.

2025-06-13T12:06:56Z 11 pages Lukas Gehring Sebastian Rehms Florian Tschorsch http://arxiv.org/abs/2504.02455v2 2025-06-13T08:22:40Z

In emerging quantum-classical integration applications, the classical time cost-especially from compilation and protocol-level communication often exceeds the execution time of quantum circuits themselves, posing a severe bottleneck to practical deployment. To overcome these limitations, QPanda3 has been extensively optimized as a high-performance quantum programming framework tailored for the demands of the NISQ era and quantum-classical hybrid workflows. It features optimized circuit compilation, a custom binary instruction stream (OriginBIS), and hardware-aware execution strategies to significantly reduce latency and communication overhead. OriginBIS achieves up to 86.9$\times$ faster encoding and 35.6$\times$ faster decoding than OpenQASM 2.0, addressing critical bottlenecks in hybrid quantum systems. Benchmarks show 10.7$\times$ compilation speedup and up to 597$\times$ acceleration in compiling large-scale circuits (e.g., a 118-qubit W-state) compared to Qiskit. n high-performance simulation, QPanda3 excels in variational quantum algorithms, achieving up to 26$\times$ faster gradient computation than Qiskit, with minimal time-complexity growth across circuit depths. These capabilities make QPanda3 well-suited for scalable quantum algorithm development in finance, materials science, and combinatorial optimization, while supporting industrial deployment and cloud-based execution in quantum-classical hybrid computing scenarios.

2025-04-03T10:20:16Z Tianrui Zou Yuan Fang Jing Wang Menghan Dou Jun Fu ZiQiang Zhao ShuBin Zhao Lei Yu Dongyi Zhao Zhaoyun Chen Guoping Guo http://arxiv.org/abs/2506.06227v2 2025-06-12T18:56:51Z

Current compiler optimization reports often present complex, technical information that is difficult for programmers to interpret and act upon effectively. This paper assesses the capability of large language models (LLM) to understand compiler optimization reports and automatically rewrite the code accordingly. To this end, the paper introduces CompilerGPT, a novel framework that automates the interaction between compilers, LLMs, and user defined test and evaluation harness. CompilerGPT's workflow runs several iterations and reports on the obtained results. Experiments with two leading LLM models (GPT-4o and Claude Sonnet), optimization reports from two compilers (Clang and GCC), and five benchmark codes demonstrate the potential of this approach. Speedups of up to 6.5x were obtained, though not consistently in every test. This method holds promise for improving compiler usability and streamlining the software optimization process.

2025-06-06T16:42:14Z C3PO at ISC HPC 2025 Peter Pirkelbauer Chunhua Liao http://arxiv.org/abs/2506.10803v1 2025-06-12T15:18:30Z

Package managers are everywhere, with seemingly every language and operating system implementing their own solution. The lack of interoperability between these systems means that multi-lingual projects are unable to express precise dependencies across language ecosystems, and external system and hardware dependencies are typically implicit and unversioned. We define HyperRes, a formal system for describing versioned dependency resolution using a hypergraph that is expressive enough to model many ecosystems and solve dependency constraints across them. We define translations from dozens of existing package managers to HyperRes and comprehensively demonstrate that dependency resolution can work across ecosystems that are currently distinct. This does not require users to shift their choice of package managers; instead, HyperRes allows for the translation of packaging metadata between ecosystems, and for solving to be precisely specialised to a particular deployment environment.

2025-06-12T15:18:30Z Submitted to SPLASH 2025 Ryan Gibb Patrick Ferris David Allsopp Michael Winston Dales Mark Elvers Thomas Gazagnaire Sadiq Jaffer Thomas Leonard Jon Ludlam Anil Madhavapeddy http://arxiv.org/abs/2506.10781v1 2025-06-12T14:54:44Z

Students in programming languages and formal logic courses often struggle with constructing rule-based derivation trees due to the complexity of applying inference rules, the lack of immediate feedback, and the manual effort required for handwritten proofs. We present Hazel Deriver, a live, web-based editor designed to scaffold derivation construction through multiple layers of support. Built on the Hazel live programming environment, it provides a structured, interactive experience that encourages iterative exploration and real-time feedback. A preliminary user study with former students suggests that Hazel Deriver reduces the perceived difficulty of derivation tasks while improving conceptual understanding and engagement. We discuss the design of its layered scaffolding features and raise questions about balancing system guidance with learner autonomy.

2025-06-12T14:54:44Z 5 pages, 2 figures, includes a preliminary user study; intended for computer science education and PL/HCI conference audiences Zhiyao Zhong Cyrus Omar http://arxiv.org/abs/2409.07870v2 2025-06-12T07:48:51Z

While the prominent quantum computing architectures are based on superconducting technology, new quantum hardware technologies are emerging, such as Trapped Ions, Neutral Atoms (or FPQAs), Silicon Spin Qubits, etc. This diverse set of technologies presents fundamental trade-offs in terms of scalability, performance, manufacturing, and operating expenses. To manage these diverse quantum technologies, there is a growing need for a retargetable compiler that can efficiently adapt existing code to these emerging hardware platforms. Such a retargetable compiler must be extensible to support new and rapidly evolving technologies, performant with fast compilation times and high-fidelity execution, and verifiable through rigorous equivalence checking to ensure the functional equivalence of the retargeted code. To this end, we present $Weaver$, the first extensible, performant, and verifiable retargetable quantum compiler framework with a focus on FPQAs due to their unique, promising features. $Weaver$ introduces WQASM, the first formal extension of the standard OpenQASM quantum assembly with FPQA-specific instructions to support their distinct capabilities. Next, $Weaver$ implements the WOptimizer, an extensible set of FPQA-specific optimization passes to improve execution quality. Last, the WChecker automatically checks for equivalence between the original and the retargeted code. Our evaluation shows that $Weaver$ improves compilation times by $10^3\times$, execution times by $4.4\times$, and execution fidelity by $10\%$, on average, compared to superconducting and state-of-the-art (non-retargetable) FPQA compilers.

2024-09-12T09:28:30Z 11 pages, 12 figures Oğuzcan Kırmemiş Francisco Romão Emmanouil Giortamis Pramod Bhatotia http://arxiv.org/abs/2502.18917v2 2025-06-10T22:11:53Z

Formal program specifications in the form of preconditions, postconditions, and class invariants have several benefits for the construction and maintenance of programs. They not only aid in program understanding due to their unambiguous semantics but can also be enforced dynamically (or even statically when the language supports a formal verifier). However, synthesizing high-quality specifications in an underlying programming language is limited by the expressivity of the specifications or the need to express them in a declarative manner. Prior work has demonstrated the potential of large language models (LLMs) for synthesizing high-quality method pre/postconditions for Python and Java, but does not consider class invariants. In this work, we describe ClassInvGen, a method for co-generating executable class invariants and test inputs to produce high-quality class invariants for a mainstream language such as C++, leveraging LLMs' ability to synthesize pure functions. We show that ClassInvGen outperforms a pure LLM-based technique to generate specifications (from code) as well as prior data-driven invariant inference techniques such as Daikon. We contribute a benchmark of standard C++ data structures along with a harness that can help measure both the correctness and completeness of generated specifications using tests and mutants. We also demonstrate its applicability to real-world code by performing a case study on several classes within a widely used and high-integrity C++ codebase.

2025-02-26T08:10:57Z Chuyue Sun Viraj Agashe Saikat Chakraborty Jubi Taneja Clark Barrett David Dill Xiaokang Qiu Shuvendu K. Lahiri http://arxiv.org/abs/2504.14480v3 2025-06-10T14:21:28Z

We present the first technique to synthesize programs that compose side-effecting functions, pure functions, and control flow, from partial traces containing records of only the side-effecting functions. This technique can be applied to synthesize API composing scripts from logs of calls made to those APIs, or a script from traces of system calls made by a workload, for example. All of the provided traces are positive examples, meaning that they describe desired behavior. Our approach does not require negative examples. Instead, it generalizes over the examples and uses cost metrics to prevent over-generalization. Because the problem is too complex for traditional monolithic program synthesis techniques, we propose a new combination of optimizing rewrites and syntax-guided program synthesis. The resulting program is correct by construction, so its output will always be able to reproduce the input traces. We evaluate the quality of the programs synthesized when considering various optimization metrics and the synthesizer's efficiency on real-world benchmarks. The results show that our approach can generate useful real-world programs.

2025-04-20T04:09:09Z To appear at PLDI 2025 (46th ACM SIGPLAN Conference on Programming Language Design and Implementation) Margarida Ferreira Victor Nicolet Joey Dodds Daniel Kroening 10.1145/3729316 http://arxiv.org/abs/2401.04594v3 2025-06-10T12:50:34Z

Starting with Hoare Logic over 50 years ago, numerous program logics have been devised to reason about the diverse programs encountered in the real world. This includes reasoning about computational effects, particularly those effects that cause the program execution to branch into multiple paths due to, e.g., nondeterministic or probabilistic choice. The recently introduced Outcome Logic reimagines Hoare Logic with branching at its core, using an algebraic representation of choice to capture programs that branch into many outcomes. In this article, we expand on prior Outcome Logic papers in order to give a more authoritative and comprehensive account of the metatheory. This includes a relatively complete proof system for Outcome Logic with the ability to reason about general purpose looping. We also show that this proof system applies to programs with various types of branching and that it facilitates the reuse of proof fragments across different kinds of specifications.

2024-01-09T14:55:54Z ACM Transactions on Programming Languages and Systems (TOPLAS), June 2025 Noam Zilberstein 10.1145/3743131 http://arxiv.org/abs/2506.08396v1 2025-06-10T03:08:51Z

Linguine is a natural-language-inspired programming language that enables users to write programs in a fluent, controlled subset of English while preserving formal semantics. The language introduces anaphoric constructs, such as pronoun variables (e.g., "it", "them"), that are statically resolved through referent-tracking analysis combined with a Hindley-Milner-style type system. Each pronoun is guaranteed to be unambiguous and well-typed at compile time. The Linguine compiler pipeline includes lexing, parsing, clause graph construction, desugaring into a typed intermediate representation, type inference, and abstract interpretation. This enables the early detection of semantic errors, such as undefined or type-inconsistent references. A lightweight backend currently generates Python code. This paper formalizes the core language, defines its typing and operational semantics, and proves the soundness of its pronoun resolution mechanism. An initial evaluation shows that Linguine allows the expression of concise and readable programs while supporting static verification. Linguine represents a step toward programming systems that prioritize human linguistic intuition while remaining grounded in formal methods and type-theoretic rigor.

2025-06-10T03:08:51Z Lifan Hu http://arxiv.org/abs/2506.10026v1 2025-06-10T00:50:08Z

Today's computing landscape has been gradually shifting to applications targeting distributed and *heterogeneous* systems, such as cloud computing and Internet of Things (IoT) applications. These applications are predominantly *concurrent*, employ *message-passing*, and interface with *foreign objects*, ranging from externally implemented code to actual physical devices such as sensors. Verifying that the resulting systems adhere to the intended protocol of interaction is challenging -- the usual assumption of a common implementation language, let alone a type system, no longer applies, ruling out any verification method based on them. This paper develops a framework for certifying *protocol compliance* of heterogeneous message-passing systems. It contributes the first mechanization of a *language-agnostic logical relation*, asserting that its inhabitants comply with the protocol specified. This definition relies entirely on a labelled transition-based semantics, accommodating arbitrary inhabitants, typed and untyped alike, including foreign objects. As a case study, the paper considers two scenarios: (1) *per-instance verification* of a specific application or hardware device, and (2) *once-and-for-all verification* of well-typed applications for a given type system. The logical relation and both scenarios are mechanized in the Coq theorem prover.

2025-06-10T00:50:08Z 19 pages, 8 figures Tesla Zhang Sonya Simkin Rui Li Yue Yao Stephanie Balzer