Tower: data structures in Quantum superposition
Charles Yuan, Michael Carbin
Abstract
Emerging quantum algorithms for problems such as element distinctness, subset sum, and closest pair demonstrate computational advantages by relying on abstract data structures. Practically realizing such an algorithm as a program for a quantum computer requires an efficient implementation of the data structure whose operations correspond to unitary operators that manipulate quantum superpositions of data. To correctly operate in superposition, an implementation must satisfy three properties --- reversibility, history independence, and bounded-time execution. Standard implementations, such as the representation of an abstract set as a hash table, fail these properties, calling for tools to develop specialized implementations. In this work, we present Core Tower, the first language for quantum programming with random-access memory. Core Tower enables the developer to implement data structures as pointer-based, linked data. It features a reversible semantics enabling every valid program to be translated to a unitary quantum circuit. We present Boson, the first memory allocator that supports reversible, history-independent, and constant-time dynamic memory allocation in quantum superposition. We also present Tower, a language for quantum programming with recursively defined data structures. Tower features a type system that bounds all recursion using classical parameters as is necessary for a program to execute on a quantum computer. Using Tower, we implement Ground, the first quantum library of data structures, including lists, stacks, queues, strings, and sets. We provide the first executable implementation of sets that satisfies all three mandated properties of reversibility, history independence, and bounded-time execution.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Cited by top-tier papers11
- CoqQ: Foundational Verification of Quantum ProgramsLi Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu et al.POPL 2023 · 33 citations
- Modular Component-Based Quantum Circuit SynthesisChan Gu Kang, Hakjoo OhOOPSLA 2023 · 11 citations
- The T-Complexity Costs of Error Correction for Control Flow in Quantum ComputationCharles Yuan, Michael CarbinPLDI 2024 · 10 citations
- Quantum Control Machine: The Limits of Control Flow in Quantum ProgrammingCharles Yuan, Agnes Villanyi, Michael CarbinOOPSLA 2024 · 9 citations
- Optimizing Quantum Circuits, Fast and SlowAmanda Xu, Abtin Molavi, Swamit Tannu, Aws AlbarghouthiASPLOS 2025 · 8 citations
Builds on4
- Silq: a high-level quantum language with safe uncomputation and intuitive semanticsBenjamin Bichsel, Maximilian Baader, Timon Gehr, Martin T. VechevPLDI 2020 · 145 citations
- Projection-based runtime assertions for testing and debugging Quantum programsGushu Li, Li Zhou, Nengkun Yu, Yufei Ding et al.OOPSLA 2020 · 120 citations
- Unqomp: synthesizing uncomputation in Quantum circuitsAnouk Paradis, Benjamin Bichsel, Samuel Steffen, Martin T. VechevPLDI 2021 · 34 citations
- SQUARE: Strategic Quantum Ancilla Reuse for Modular Quantum Programs via Cost-Effective UncomputationYongshan Ding, Xin-Chuan Wu, Adam Holmes, Ash Wiseth et al.ISCA 2020 · 33 citations
Related papers
- Quantum Circuits Are Just a PhaseChris Heunen, Louis Lemonnier, Christopher McNally, Alex RicePOPL 2026
- Hadamard-Pi: Equational Quantum ProgrammingWang Fang, Chris Heunen, Robin KaarsgaardPOPL 2026
- Verification of Nondeterministic Quantum ProgramsYuan Feng, Yingte XuASPLOS 2023 · 7 citations
- Quantum Control and General Recursion Beyond the Unitary CaseKathleen Barsse, Romain Péchoux, Simon PerdrixLICS 2026
- Qunity: A Unified Language for Quantum and Classical ComputingFinn Voichick, Liyi Li, Robert Rand, Michael HicksPOPL 2023 · 35 citations
