Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2611.08503

pfoqcompiler: Efficient Compilation of Quantum Control in Recursive First-Order Quantum Programs

Mário Silva·Alexandre Guernut·Marco Lewis
View original source ↗Read source document ↗Export metadata ↓

Abstract

Recursive quantum control allows for simple and concise descriptions of algorithms. However, a naive circuit compilation sequentializes the different branches of the quantum if-statement and results in an exponential increase in circuit depth. Existing techniques can parallelize these branches, but do so at the cost of an exponential number of ancillary qubits. We present pfoqcompiler, a compiler targeting Qiskit for the first-order quantum programming language FOQ that exploits program structure to merge compatible recursive procedure calls across quantum branches. We introduce weaker syntactically-checkable conditions for well-foundedness, recursive halving, and uniformity, while preserving previously demonstrated complexity characterizations. For weakly well-founded bounded-width programs, the compiler produces polynomial-size circuits; weakly recursively halving programs additionally yield polylogarithmic depth, while weak uniformity removes the asymptotic overhead of branch sequentialization.

Explore related subjects

cs.PLcs.LOquant-ph

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Mário Silva, Alexandre Guernut, Marco Lewis. 2026-09-08. pfoqcompiler: Efficient Compilation of Quantum Control in Recursive First-Order Quantum Programs. https://arxiv.org/abs/2611.08503

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A Physically-Realisable Quantum Programming Language with Quantum-Controlled Quantum Channels

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, and it is then tempting to superpose programs as well. Indeed, a particular superposition of programs, known as the quantum SWITCH, has attracted considerable attention. A natural way to superpose programs is conditional branching on quantum data, and several studies have pursued this idea. However, there is a well-known semantic difficulty with this approach, and the fundamental question of whether the languages proposed in prior work can be physically realised remains open. This paper proposes a physically realisable quantum programming language with quantum branching over quantum channels. We first analyse the semantic difficulty from an implementation perspective and show that the difficulty is caused by arbitrariness in the implementation. We then design a language that is free from this arbitrariness. As expected from its implementation-oriented design, our language is physically realisable. We argue for this from two directions: first, we give a method for compiling programs into quantum circuits; and second, we show that our programs stay within the physically admissible range, namely, that they neither yield probabilities greater than one nor violate causal inequalities. The absence of such violations is established through the inclusion of our language in QC-QC, a notion of realisability studied in physics.

cs.PL↗
arXiv2026

Nothing Is Shared Until You Synchronise: Reinterpreting Java for Data-Race Freedom

In mainstream shared-memory languages, programmers use synchronisation mechanisms such as locks to isolate shared data accesses across threads to avoid data races. Yet synchronisation enforces only a temporal ordering, while shared memory still communicates updates between threads at every ordinary read and write. To achieve isolation, programmers therefore need to understand the connection between ordering and communication, and to apply synchronisation correctly and consistently, while compilers and hardware optimise assuming they have. When programmers synchronise incorrectly, they lose isolation, and the semantics of their programs change without notice. We propose Sync-as-Share, a memory model built on isolation and communication rather than on the ordering of accesses to shared memory. We start from thread isolation, where each thread reads and writes a private view of memory, and reinterpret programs' existing synchronisation actions to also communicate updates explicitly. As nothing is communicated outside synchronisation actions, data races become impossible by construction. Instead, conflicting updates are detected at synchronisation points. Viewing synchronisation as explicit communication exposes the design decisions of what should be communicated, to whom, and what counts as a conflict. We propose two communication topologies with different trade-offs. We instantiate Sync-as-Share for Java by making the synchronisation actions already defined by its memory model the only points at which threads communicate, so Java programs can adopt Sync-as-Share unmodified. We formalise this instantiation as version-controlled memory, in which synchronisation actions push and pull updates between private views, and mechanise it in Rocq. We show that Java programs that are correctly synchronised under the Java memory model behave identically under shared memory and Sync-as-Share.

cs.PL↗
arXiv2026

GUARDTs: Decentralized Access Control for Replicated Data Types

Replicated data types providing strong eventual consistency offer a principled foundation for developing decentralized software. Yet existing approaches to programming such data types leave access control unresolved: they either provide none at all, delegate it to a trusted coordinator, reintroducing the centralization they were designed to avoid, or tie it to specific data-type constructions, while typically assuming non-Byzantine replicas and static policies. We present GUARDTs: Guarded Unforgeable Algebraic Replicated Data Types, which embed fine-grained permissions directly into the application data model, operate without a central authority, support dynamic policy evolution, and tolerate Byzantine replicas. We formally prove that GUARDTs guarantee confidentiality, integrity, and availability and show empirically that their access control adds negligible overhead on top of the cost of Byzantine-resilient replication itself.

cs.PL↗