Silq: a high-level quantum language with safe uncomputation and intuitive semantics
Benjamin Bichsel, Maximilian Baader, Timon Gehr, Martin T. Vechev
Abstract
Existing quantum languages force the programmer to work at a low level of abstraction leading to unintuitive and cluttered code. A fundamental reason is that dropping temporary values from the program state requires explicitly applying quantum operations that safely uncompute these values.
We present Silq, the first quantum language that addresses this challenge by supporting safe, automatic uncomputation. This enables an intuitive semantics that implicitly drops temporary values, as in classical computation. To ensure physicality of Silq's semantics, its type system leverages novel annotations to reject unphysical programs.
Our experimental evaluation demonstrates that Silq programs are not only easier to read and write, but also significantly shorter than equivalent programs in other quantum languages (on average -46% for Q#, -38% for Quipper), while using only half the number of quantum primitives.
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.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 9365d335-4bcb-4e62-bc22-1bd55dbccdd7Cited by top-tier papers35
- A verified optimizer for Quantum circuitsKesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu et al.POPL 2021 · 111 citations
- Bugs in Quantum computing platforms: an empirical studyMatteo Paltenghi, Michael PradelOOPSLA 2022 · 70 citations
- Distributed quantum computing with QMPIThomas Häner, Damian S. Steiger, Torsten Hoefler, Matthias TroyerSC 2021 · 48 citations
- Qunity: A Unified Language for Quantum and Classical ComputingFinn Voichick, Liyi Li, Robert Rand, Michael HicksPOPL 2023 · 35 citations
- Unqomp: synthesizing uncomputation in Quantum circuitsAnouk Paradis, Benjamin Bichsel, Samuel Steffen, Martin T. VechevPLDI 2021 · 34 citations
Related papers
- Modular Synthesis of Efficient Quantum UncomputationHristo Venev, Timon Gehr, Dimitar Dimitrov, Martin T. VechevOOPSLA 2024 · 5 citations
- Borrowing Dirty Qubits in Quantum ProgramsBonan Su, Li Zhou, Yuan Feng, Mingsheng YingASPLOS 2026 · 1 citation
- Qurts: Automatic Quantum Uncomputation by Affine Types with LifetimeKengo Hirata, Chris HeunenPOPL 2025 · 4 citations
- Proto-Quipper with Dynamic LiftingPeng Fu, Kohei Kishida, Neil J. Ross, Peter SelingerPOPL 2023 · 17 citations
- Optimizing Ancilla-Based Quantum Circuits with SPARERitvik Sharma, Sara AchourPLDI 2025
