diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 00000000..c9f51000 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,14 @@ +name: pre-commit + +on: + pull_request: + push: + branches: [main] + +jobs: + pre-commit: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v5 + - uses: actions/setup-python@v5 + - uses: pre-commit/action@v3.0.1 diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml new file mode 100644 index 00000000..f8723cf7 --- /dev/null +++ b/.pre-commit-config.yaml @@ -0,0 +1,21 @@ +# See https://pre-commit.com for more information +# See https://pre-commit.com/hooks.html for more hooks +repos: + - repo: https://github.com/pre-commit/pre-commit-hooks + rev: v6.0.0 + hooks: + - id: check-added-large-files + - id: check-merge-conflict + - id: check-toml + - id: check-vcs-permalinks + - id: check-yaml + - id: end-of-file-fixer + - id: fix-byte-order-marker + - id: mixed-line-ending + - id: trailing-whitespace + + - repo: https://github.com/crate-ci/typos + rev: v1.35.5 + hooks: + - id: typos + args: [] diff --git a/_typos.toml b/_typos.toml new file mode 100644 index 00000000..eedfc396 --- /dev/null +++ b/_typos.toml @@ -0,0 +1,12 @@ +[default.extend-words] +# Don't correct the surname "Ono" +Ono = "Ono" +Ond = "Ond" +ois = "ois" +Fo = "Fo" +ket = "ket" +Certi = "Certi" + +[type.conf] +extend-glob = ["*.conf"] +check-file = false diff --git a/bbt.bib b/bbt.bib index 6d02e997..f1e88db2 100644 --- a/bbt.bib +++ b/bbt.bib @@ -53,6 +53,26 @@ @string{toplas % bibsource @string{qplbib = "Quantum Programming Languages \& Verification Bibliography, https://git.io/qpl-bib"} +@article{Abdulla2025, + author = {Abdulla, Parosh Aziz and Chen, Yo-Ga and Chen, Yu-Fang and Hol\'{\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej and Lin, Jyun-Ao and Lo, Fang-Yi and Tsai, Wei-Lun}, + title = {Verifying Quantum Circuits with Level-Synchronized Tree Automata}, + year = {2025}, + publisher = acm, + address = {New York, NY, USA}, + volume = {9}, + number = {POPL}, + doi = {10.1145/3704868}, + abstract = {We present a new method for the verification of quantum circuits based on a novel symbolic representation of sets of quantum states using level-synchronized tree automata (LSTAs). LSTAs extend classical tree automata by labeling each transition with a set of choices, which are then used to synchronize subtrees of an accepted tree. Compared to the traditional tree automata, LSTAs have an incomparable expressive power while maintaining important properties, such as closure under union and intersection, and decidable language emptiness and inclusion. We have developed an efficient and fully automated symbolic verification algorithm for quantum circuits based on LSTAs. The complexity of supported gate operations is at most quadratic, dramatically improving the exponential worst-case complexity of an earlier tree automata-based approach. Furthermore, we show that LSTAs are a promising model for parameterized verification, i.e., verifying the correctness of families of circuits with the same structure for any number of qubits involved, which principally lies beyond the capabilities of previous automated approaches. We implemented this method as a C++ tool and compared it with three symbolic quantum circuit verifiers and two simulators on several benchmark examples. The results show that our approach can solve problems with sizes orders of magnitude larger than the state of the art.}, + journal = pacmpl, + month = jan, + eid = {32}, + pages = {32}, + numpages = {31}, + keywords = {quantum circuits, tree automata, verification}, + webnote = {POPL '25}, + bibsource = qplbib +} + @inproceedings{Abramsky2004, title = {A Categorical Semantics of Quantum Protocols}, author = {Abramsky, Samson and Coecke, Bob}, @@ -199,6 +219,26 @@ @article{Amy2020 bibsource = qplbib } +@article{Amy2025, + author = {Amy, Matthew and Lunderville, Joseph}, + title = {Linear and Non-linear Relational Analyses for Quantum Program Optimization}, + year = {2025}, + publisher = acm, + address = {New York, NY, USA}, + volume = {9}, + number = {POPL}, + doi = {10.1145/3704873}, + abstract = {The phase folding optimization is a circuit optimization used in many quantum compilers as a fast and effective way of reducing the number of high-cost gates in a quantum circuit. However, existing formulations of the optimization rely on an exact, linear algebraic representation of the circuit, restricting the optimization to being performed on straightline quantum circuits or basic blocks in a larger quantum program. We show that the phase folding optimization can be re-cast as an affine relation analysis, which allows the direct application of classical techniques for affine relations to extend phase folding to quantum programs with arbitrarily complicated classical control flow including nested loops and procedure calls. Through the lens of relational analysis, we show that the optimization can be powered-up by substituting other classical relational domains, particularly ones for non-linear relations which are useful in analyzing circuits involving classical arithmetic. To increase the precision of our analysis and infer non-linear relations from gate sets involving only linear operations — such as Clifford+t — we show that the sum-over-paths technique can be used to extract precise symbolic transition relations for straightline circuits. Our experiments show that our methods are able to generate and use non-trivial loop invariants for quantum program optimization, as well as achieve some optimizations of common circuits which were previously attainable only by hand.}, + journal = pacmpl, + month = jan, + eid = {37}, + pages = {37}, + numpages = {32}, + keywords = {Quantum software, compiler optimization, data flow analysis, invariant generation, relational program analysis}, + webnote = {POPL '25}, + bibsource = qplbib +} + @article{ArdeshirLarijani2018, title = {Automated Equivalence Checking of Concurrent Quantum Systems}, author = {{Ardeshir-Larijani}, Ebrahim and Gay, Simon J. and Nagarajan, Rajagopal}, @@ -366,6 +406,66 @@ @article{Briegel2009 bibsource = qplbib } +@article{Buckley2024, + author = {Buckley, Anita and Chuprikov, Pavel and Otoni, Rodrigo and Soul\'{e}, Robert and Rand, Robert and Eugster, Patrick}, + title = {An Algebraic Language for Specifying Quantum Networks}, + year = {2024}, + publisher = acm, + address = {New York, NY, USA}, + volume = {8}, + number = {PLDI}, + doi = {10.1145/3656430}, + abstract = {Quantum networks connect quantum capable nodes in order to achieve capabilities that are impossible only using classical information. Their fundamental unit of communication is the Bell pair, which consists of two entangled quantum bits. Unfortunately, Bell pairs are fragile and difficult to transmit directly, necessitating a network of repeaters, along with software and hardware that can ensure the desired results. Challenging intrinsic features of quantum networks, such as dealing with resource competition, motivate formal reasoning about quantum network protocols. To this end, we developed BellKAT, a novel specification language for quantum networks based upon Kleene algebra. To cater to the specific needs of quantum networks, we designed an algebraic structure, called BellSKA, which we use as the basis of BellKAT's denotational semantics. BellKAT's constructs describe entanglement distribution rules that allow for modular specification. We give BellKAT a sound and complete equational theory, allowing us to verify network protocols. We provide a prototype tool to showcase the expressiveness of BellKAT and how to optimize and verify networks in practice.}, + journal = pacmpl, + month = jun, + eid = {200}, + pages = {200}, + numpages = {23}, + keywords = {Kleene algebra, quantum networks, entanglement}, + webnote = {PLDI '24}, + bibsource = qplbib +} + +@article{Cao2025, + author = {Cao, Xiuqi and Zhou, Junyu and Liu, Yuhao and Shi, Yunong and Li, Gushu}, + title = {MarQSim: Reconciling Determinism and Randomness in Compiler Optimization for Quantum Simulation}, + year = {2025}, + publisher = acm, + address = {New York, NY, USA}, + volume = {9}, + number = {PLDI}, + doi = {10.1145/3729269}, + abstract = {Quantum Hamiltonian simulation, fundamental in quantum algorithm design, extends far beyond its foundational roots, powering diverse quantum computing applications. However, optimizing the compilation of quantum Hamiltonian simulation poses significant challenges. Existing approaches fall short in reconciling deterministic and randomized compilation, lack appropriate intermediate representations, and struggle to guarantee correctness. Addressing these challenges, we present MarQSim, a novel compilation framework. MarQSim leverages a Markov chain-based approach, encapsulated in the Hamiltonian Term Transition Graph, adeptly reconciling deterministic and randomized compilation benefits. Furthermore, we formulate a Minimum-Cost Flow model that can tune transition matrices to enforce correctness while accommodating various optimization objectives. Experimental results demonstrate MarQSim's superiority in generating more efficient quantum circuits for simulating various quantum Hamiltonians while maintaining precision.}, + journal = pacmpl, + month = jun, + eid = {170}, + pages = {170}, + numpages = {25}, + keywords = {Hamiltonian Simulation, Markov Chain, Minimum-Cost Flow Model, Quantum Computing}, + webnote = {PLDI '25}, + bibsource = qplbib +} + +@article{Carette2025, + author = {Carette, Jacques and Heunen, Chris and Kaarsgaard, Robin and Sabry, Amr}, + title = {How to Bake a Quantum Π}, + year = {2024}, + publisher = acm, + address = {New York, NY, USA}, + volume = {8}, + number = {ICFP}, + doi = {10.1145/3674625}, + abstract = {We construct a computationally universal quantum programming language QuantumΠ from two copies of Π, the internal language of rig groupoids. The first step constructs a pure (measurement-free) term language by interpreting each copy of Π in a generalisation of the category Unitary in which every morphism is "rotated" by a particular angle, and the two copies are amalgamated using a free categorical construction expressed as a computational effect. The amalgamated language only exhibits quantum behaviour for specific values of the rotation angles, a property which is enforced by imposing a small number of equations on the resulting category. The second step in the construction introduces measurements by layering an additional computational effect.}, + journal = pacmpl, + month = aug, + eid = {236}, + pages = {236}, + numpages = {29}, + keywords = {quantum programming language, reversible computing, rig category, unitary quantum computing}, + webnote = {ICFP '24}, + bibsource = qplbib +} + @inproceedings{Chardonnet2021, title = {{Geometry of Interaction for ZX-Diagrams}}, author = {Chardonnet, Kostia and Valiron, Beno{\^i}t and Vilmart, Renaud}, @@ -461,7 +561,7 @@ @article{Choudhury2022 volume = {6}, number = {POPL}, eid = {6}, - page = {6}, + pages = {6}, doi = {10.1145/3498667}, url = {https://github.com/vikraman/popl22-symmetries-artifact}, abstract = {The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic data types. In this paper, we give a denotational semantics for this language, using weak groupoids {\`a} la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of type isomorphisms. We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, which is shown to be sound and complete for both levels, forming an equivalence of groupoids. We use this to establish a Curry-Howard-Lambek correspondence between Reversible Logic, Reversible Programming Languages, and Symmetric Rig Groupoids, by showing that the syntax of Pi is presented by the free symmetric rig groupoid, given by finite sets and bijections. Using the formalisation of our results, we perform normalisation-by-evaluation, verification and synthesis of reversible logic gates, motivated by examples from quantum computing. We also show how to reason about and transfer theorems between different representations of reversible circuits.}, @@ -536,6 +636,26 @@ @misc{Colledan2022 bibsource = qplbib } +@article{Colledan2025, + author = {Colledan, Andrea and Dal Lago, Ugo}, + title = {Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages}, + year = {2025}, + publisher = acm, + address = {New York, NY, USA}, + volume = {9}, + number = {POPL}, + doi = {10.1145/3704883}, + abstract = {We introduce a type system for the Quipper language designed to derive upper bounds on the size of the circuits produced by the typed program. This size can be measured according to various metrics, including width, depth and gate count, but also variations thereof obtained by considering only some wire types or some gate kinds. The key ingredients for achieving this level of flexibility are effects and refinement types, both relying on indices, that is, generic arithmetic expressions whose operators are interpreted differently depending on the target metric. The approach is shown to be correct through logical predicates, under reasonable assumptions about the chosen resource metric. This approach is empirically evaluated through the QuRA tool, showing that, in many cases, inferring tight bounds is possible in a fully automatic way.}, + journal = pacmpl, + month = jan, + eid = {47}, + pages = {47}, + numpages = {31}, + keywords = {Effects, Lambda Calculus, Quantum Computing, Quipper, Refinement Types}, + webnote = {POPL '25}, + bibsource = qplbib +} + @misc{Cross2017, title = {Open {{Quantum Assembly Language}}}, author = {Cross, Andrew W. and Bishop, Lev S. and Smolin, John A. and Gambetta, Jay M.}, @@ -816,6 +936,26 @@ @article{Echenim2021a bibsource = qplbib } +@article{Fang2024, + author = {Fang, Wang and Ying, Mingsheng}, + title = {Symbolic Execution for Quantum Error Correction Programs}, + year = {2024}, + publisher = acm, + address = {New York, NY, USA}, + volume = {8}, + number = {PLDI}, + doi = {10.1145/3656419}, + abstract = {We define QSE, a symbolic execution framework for quantum programs by integrating symbolic variables into quantum states and the outcomes of quantum measurements. The soundness of QSE is established through a theorem that ensures the correctness of symbolic execution within operational semantics. We further introduce symbolic stabilizer states, which symbolize the phases of stabilizer generators, for the efficient analysis of quantum error correction (QEC) programs. Within the QSE framework, we can use symbolic expressions to characterize the possible discrete Pauli errors in QEC, providing a significant improvement over existing methods that rely on sampling with simulators. We implement QSE with the support of symbolic stabilizer states in a prototype tool named QuantumSE.jl. Our experiments on representative QEC codes, including quantum repetition codes, Kitaev's toric codes, and quantum Tanner codes, demonstrate the efficiency of QuantumSE.jl for debugging QEC programs with over 1000 qubits. In addition, by substituting concrete values in symbolic expressions of measurement results, QuantumSE.jl is also equipped with a sampling feature for stabilizer circuits. Despite a longer initialization time than the state-of-the-art stabilizer simulator, Google's Stim, QuantumSE.jl offers a quicker sampling rate in the experiments.}, + journal = pacmpl, + month = jun, + eid = {189}, + pages = {189}, + numpages = {26}, + keywords = {symbolic execution, stabilizer formalism}, + webnote = {PLDI '24}, + bibsource = qplbib +} + @article{Feng2021, title = {Quantum Hoare Logic with Classical Variables}, author = {Feng, Yuan and Ying, Mingsheng}, @@ -1248,6 +1388,26 @@ @phdthesis{Hietala2022 bibsource = qplbib } +@article{Hirata2025, + author = {Hirata, Kengo and Heunen, Chris}, + title = {Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime}, + year = {2025}, + publisher = acm, + address = {New York, NY, USA}, + volume = {9}, + number = {POPL}, + doi = {10.1145/3704842}, + abstract = {Uncomputation is a feature in quantum programming that allows the programmer to discard a value without losing quantum information, and that allows the compiler to reuse resources. Whereas quantum information has to be treated linearly by the type system, automatic uncomputation enables the programmer to treat it affinely to some extent. Automatic uncomputation requires a substructural type system between linear and affine, a subtlety that has only been captured by existing languages in an ad hoc way. We extend the Rust type system to the quantum setting to give a uniform framework for automatic uncomputation called Qurts (pronounced quartz). Specifically, we parameterise types by lifetimes, permitting them to be affine during their lifetime, while being restricted to linear use outside their lifetime. We also provide two operational semantics: one based on classical simulation, and one that does not depend on any specific uncomputation strategy.}, + journal = pacmpl, + month = jan, + eid = {6}, + pages = {6}, + numpages = {28}, + keywords = {Affine Type, Lifetime, Linear Type, Quantum Programming, Rust, Uncomputation}, + webnote = {POPL '25}, + bibsource = qplbib +} + @inproceedings{Honda2015, title = {Analysis of Quantum Entanglement in Quantum Programs using Stabilizer Formalism}, author = {Honda, Kentaro}, @@ -1284,6 +1444,26 @@ @inproceedings{Huang2019 bibsource = qplbib } +@article{Huang2025, + author = {Huang, Qifan and Zhou, Li and Fang, Wang and Zhao, Mengyu and Ying, Mingsheng}, + title = {Efficient Formal Verification of Quantum Error Correcting Programs}, + year = {2025}, + publisher = acm, + address = {New York, NY, USA}, + volume = {9}, + number = {PLDI}, + doi = {10.1145/3729293}, + abstract = {Quantum error correction (QEC) is fundamental for suppressing noise in quantum hardware and enabling fault-tolerant quantum computation. In this paper, we propose an efficient verification framework for QEC programs. We define an assertion logic and a program logic specifically crafted for QEC programs and establish a sound proof system. We then develop an efficient method for handling verification conditions (VCs) of QEC programs: for Pauli errors, the VCs are reduced to classical assertions that can be solved by SMT solvers, and for non-Pauli errors, we provide a heuristic algorithm. We formalize the proposed program logic in Coq proof assistant, making it a verified QEC verifier. Additionally, we implement an automated QEC verifier, Veri-QEC, for verifying various fault-tolerant scenarios. We demonstrate the efficiency and broad functionality of the framework by performing different verification tasks across various scenarios. Finally, we present a benchmark of 14 verified stabilizer codes.}, + journal = pacmpl, + month = jun, + eid = {190}, + pages = {190}, + numpages = {26}, + keywords = {Formal verification, Hoare logic, Quantum error correction, Quantum programming language}, + webnote = {PLDI '25}, + bibsource = qplbib +} + @inproceedings{Huot2019, title = {Universal Properties in Quantum Theory}, author = {Huot, Mathieu and Staton, Sam}, @@ -1371,6 +1551,26 @@ @article{JavadiAbhari2015 bibsource = qplbib } +@article{Jeon2024, + author = {Jeon, Seungmin and Cho, Kyeongmin and Kang, Chan Gu and Lee, Janggun and Oh, Hakjoo and Kang, Jeehoon}, + title = {Quantum Probabilistic Model Checking for Time-Bounded Properties}, + year = {2024}, + publisher = acm, + address = {New York, NY, USA}, + volume = {8}, + number = {OOPSLA2}, + doi = {10.1145/3689731}, + abstract = {Probabilistic model checking (PMC) is a verification technique for analyzing the properties of probabilistic systems. However, existing techniques face challenges in verifying large systems with high accuracy. PMC struggles with state explosion, where the number of states grows exponentially with the size of the system, making large system verification infeasible. While statistical model checking (SMC) avoids PMC's state explosion problem by using a simulation approach, it suffers from runtime explosion, requiring numerous samples for high accuracy. To address these limitations in verifying large systems with high accuracy, we present quantum probabilistic model checking (QPMC), the first method leveraging quantum computing for PMC with respect to time-bounded properties. QPMC addresses state explosion by encoding PMC problems into quantum circuits that superpose states within qubits. Additionally, QPMC resolves runtime explosion through Quantum Amplitude Estimation, efficiently estimating the probabilities of specified properties. We prove that QPMC correctly solves PMC problems and achieves a quadratic speedup in time complexity compared to SMC.}, + journal = pacmpl, + month = oct, + eid = {291}, + pages = {291}, + numpages = {31}, + keywords = {bounded reachability, probabilistic model checking, quantum computing}, + webnote = {OOPSLA '24}, + bibsource = qplbib +} + @article{Jia2022, title = {Semantics for Variational Quantum Programming}, author = {Jia, Xiaodong and Kornell, Andre and Lindenhovius, Bert and Mislove, Michael and Zamdzhiev, Vladimir}, @@ -1424,6 +1624,26 @@ @article{Kang2023 bibsource = qplbib } +@article{Kang2024, + author = {Kang, Chan Gu and Lee, Joonghoon and Oh, Hakjoo}, + title = {Statistical Testing of Quantum Programs via Fixed-Point Amplitude Amplification}, + year = {2024}, + publisher = acm, + address = {New York, NY, USA}, + volume = {8}, + number = {OOPSLA2}, + doi = {10.1145/3689716}, + abstract = {We present a new technique for accelerating quantum program testing. Given a quantum circuit with an input/output specification, our goal is to check whether executing the program on the input state produces the expected output. In quantum computing, however, it is impossible to directly check the equivalence of the two quantum states. Instead, we rely on statistical testing, which involves repeated program executions, state measurements, and subsequent comparisons with the specified output. To guarantee a high level of assurance, however, this method requires an extensive number of measurements. In this paper, we propose a solution to alleviate this challenge by adapting Fixed-Point Amplitude Amplification (FPAA) for quantum program testing. We formally present our technique, demonstrate its ability to reduce the required number of measurements as well as runtime cost without sacrificing the original statistical guarantee, and showcase its runtime effectiveness through case studies.}, + journal = pacmpl, + month = oct, + eid = {276}, + pages = {276}, + numpages = {25}, + keywords = {Quantum Computing, Quantum Programming, Testing, Verification}, + webnote = {OOPSLA '24}, + bibsource = qplbib +} + @techreport{Knill1996, title = {Conventions for Quantum Pseudocode}, author = {Knill, Emanuel}, @@ -1618,6 +1838,26 @@ @article{Li2022 bibsource = qplbib } +@article{Li2025, + author = {Li, Liyi and Young, David and Graves, James Bryan and Dissanayake, Chandeepa and Sabry, Amr}, + title = {A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware}, + year = {2025}, + publisher = acm, + address = {New York, NY, USA}, + volume = {9}, + number = {ICFP}, + doi = {10.1145/3747521}, + abstract = {In physics and chemistry, quantum systems are typically modeled using energy constraints formulated as Hamiltonians. Investigations into such systems often focus on the evolution of the Hamiltonians under various initial conditions, an approach summarized as Adiabatic Quantum Computing (AQC). Although this perspective may initially seem foreign to functional programmers, we demonstrate that conventional functional programming abstractions—specifically, the Traversable and Monad type classes—naturally capture the essence of AQC. To illustrate this connection, we introduce EnQ, a functional programming library designed to express diverse optimization problems as energy constraint computations (ECC). The library comprises three core components: generating the solution space, associating energy costs with potential solutions, and searching for optimal or near-optimal solutions. Because EnQ is implemented using standard Haskell, it can be executed directly through conventional classical Haskell compilers. More interestingly, we develop and implement a process to compile EnQ programs into circuits executable on quantum hardware. We validate EnQ's effectiveness through a number of case studies, demonstrating its capacity to express and solve classical optimization problems on quantum hardware, including search problems, type inference, number partitioning, clique finding, and graph coloring.}, + journal = pacmpl, + month = aug, + eid = {252}, + pages = {252}, + numpages = {31}, + keywords = {Adiabatic Quantum Computation, Energy Constraint Computation, Functional Programming}, + webnote = {ICFP '25}, + bibsource = qplbib +} + @inproceedings{Lindenhovius2018, title = {Enriching a {{Linear}}/{{Non}}-Linear {{Lambda Calculus}}: {{A Programming Language}} for {{String Diagrams}}}, shorttitle = {Enriching a {{Linear}}/{{Non}}-Linear {{Lambda Calculus}}}, @@ -1740,6 +1980,26 @@ @article{Meuli2020 bibsource = qplbib } +@article{Molavi2025, + author = {Molavi, Abtin and Xu, Amanda and Tannu, Swamit and Albarghouthi, Aws}, + title = {Dependency-Aware Compilation for Surface Code Quantum Architectures}, + year = {2025}, + publisher = acm, + address = {New York, NY, USA}, + volume = {9}, + number = {OOPSLA1}, + doi = {10.1145/3720416}, + abstract = {Practical applications of quantum computing depend on fault-tolerant devices with error correction. We study the problem of compiling quantum circuits for quantum computers implementing surface codes. Optimal or near-optimal compilation is critical for both efficiency and correctness. The compilation problem requires (1) mapping circuit qubits to the device qubits and (2) routing execution paths between interacting qubits. We solve this problem efficiently and near-optimally with a novel algorithm that exploits the dependency structure of circuit operations to formulate discrete optimization problems that can be approximated via simulated annealing, a classic and simple algorithm. Our extensive evaluation shows that our approach is powerful and flexible for compiling realistic workloads.}, + journal = pacmpl, + month = apr, + eid = {82}, + pages = {82}, + numpages = {28}, + keywords = {quantum error-correction, simulated annealing}, + webnote = {OOPSLA '25}, + bibsource = qplbib +} + @article{Mosca2019, title = {{Quantum Programming Languages (Dagstuhl Seminar 18381)}}, author = {Mosca, Michele and Roetteler, Martin and Selinger, Peter}, @@ -1902,6 +2162,26 @@ @inproceedings{Paradis2021 bibsource = qplbib } +@article{Paradis2024, + author = {Paradis, Anouk and Dekoninck, Jasper and Bichsel, Benjamin and Vechev, Martin}, + title = {Synthetiq: Fast and Versatile Quantum Circuit Synthesis}, + year = {2024}, + publisher = acm, + address = {New York, NY, USA}, + volume = {8}, + number = {OOPSLA1}, + doi = {10.1145/3649813}, + abstract = {To implement quantum algorithms on quantum computers it is crucial to decompose their operators into the limited gate set supported by those computers. Unfortunately, existing works automating this essential task are generally slow and only applicable to narrow use cases. We present Synthetiq, a method to synthesize quantum circuits implementing a given specification over arbitrary finite gate sets, which is faster and more versatile than existing works. Synthetiq utilizes Simulated Annealing instantiated with a novel, domain-specific energy function that allows developers to leverage partial specifications for better efficiency. Synthetiq further couples this synthesis method with a custom simplification pass, to ensure efficiency of the found circuits.We experimentally demonstrate that Synthetiq can generate better implementations than were previously known for multiple relevant quantum operators including RCCCX, CCT, CCiSWAP, C SWAP, and CiSWAP Our extensive evaluation also demonstrates Synthetiq frequently outperforms a wide variety of more specialized tools in their own domains, including (i) the well-studied task of synthesizing fully specified operators in the Clifford+T gate set, (ii) ϵ-approximate synthesis of multi-qubit operators in the same gate set, and (iii) synthesis tasks with custom gate sets. On all those tasks, Synthetiq is typically one to two orders of magnitude faster than previous state-of-the-art and can tackle problems that were previously out of the reach of any synthesis tool.}, + journal = pacmpl, + month = apr, + eid = {96}, + pages = {96}, + numpages = {28}, + keywords = {Quantum Circuits, Synthesis, Clifford+T}, + webnote = {OOPSLA '24}, + bibsource = qplbib +} + @inproceedings{Paykin2017, title = {{{QWIRE}}: A Core Language for Quantum Circuits}, author = {Paykin, Jennifer and Rand, Robert and Zdancewic, Steve}, @@ -1988,6 +2268,26 @@ @inproceedings{Peduri2022 bibsource = qplbib } +@article{Peduri2025, + author = {Peduri, Anurudh and Schaefer, Ina and Walter, Michael}, + title = {QbC: Quantum Correctness by Construction}, + year = {2025}, + publisher = acm, + address = {New York, NY, USA}, + volume = {9}, + number = {OOPSLA1}, + doi = {10.1145/3720433}, + abstract = {Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC): an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.}, + journal = pacmpl, + month = apr, + eid = {99}, + pages = {99}, + numpages = {29}, + keywords = {correctness by construction, quantum Hoare logic, quantum while language}, + webnote = {OOSPLA '25}, + bibsource = qplbib +} + @inproceedings{Peng2022, title = {Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra}, author = {Peng, Yuxiang and Ying, Mingsheng and Wu, Xiaodi}, @@ -2395,6 +2695,26 @@ @incollection{Selinger2009 bibsource = qplbib } +@article{Sharma2025, + author = {Sharma, Ritvik and Achour, Sara}, + title = {Optimizing Ancilla-Based Quantum Circuits with SPARE}, + year = {2025}, + publisher = acm, + address = {New York, NY, USA}, + volume = {9}, + number = {PLDI}, + doi = {10.1145/3729253}, + abstract = {Many quantum algorithms instantiate and use ancillas, spare qubits that serve as temporary storage in a quantum circuit. In particular, many recently developed high-level and modular quantum programming languages (QPLs) use ancilla qubits to implement various programming constructs. These are lowered to circuits with nested/cascading compute-uncompute gate sequences that use ancilla qubits to track internal state. We present SPARE, a rewrite-based quantum circuit optimizer that restructures these compute-uncompute gate sequences, leveraging the ancilla qubit state information to optimize the circuit. In this work, we prove the correctness of SPARE's rewrites and link SPARE's gate-level transforms to language-level program rewrites, which may be performed on the input language. We evaluate SPARE on QPL-generated quantum circuits against Unqomp and Spire, two optimizing compilers for QPLs. SPARE achieves a reduction of up to 27.3\% in qubit count, 56.7\% in 2-qubit gates, 68.2\% in 1-qubit gates and 73.9\% in depth against Unqomp, and up to 17.8\% in qubits, 67.3\% in 2-qubit gates, 61.4\% in 1-qubit gates and 59.9\% in depth against Spire. We also evaluate SPARE against the Quartz, Feynman, and PyZX circuit optimizers: SPARE achieves up to a 70.0\% reduction in two-qubit gates, up to a 53.6\% reduction in 1-qubit gates, and up to a 56.7\% reduction in depth compared to the best result from all the gate-level optimizers.}, + journal = pacmpl, + month = jun, + eid = {154}, + pages = {154}, + numpages = {25}, + keywords = {quantum optimizing compilers, quantum programming languages}, + webnote = {PLDI '25}, + bibsource = qplbib +} + @inproceedings{Singhal2020, title = {Verified translation between low-level quantum languages}, author = {Singhal, Kartik and Rand, Robert and Hicks, Michael}, @@ -2648,6 +2968,26 @@ @inproceedings{Tao2022 bibsource = qplbib } +@article{Tornow2025, + author = {Tornow, Nathaniel and Giortamis, Emmanouil and Bhatotia, Pramod}, + title = {QVM: Quantum Gate Virtualization Machine}, + year = {2025}, + publisher = acm, + address = {New York, NY, USA}, + volume = {9}, + number = {PLDI}, + doi = {10.1145/3729290}, + abstract = {We present the Quantum Gate Virtualization Machine (QVM), an end-to-end generic system for scalable execution of large quantum circuits with high fidelity on noisy and small quantum processors (QPUs) by leveraging gate virtualization. QVM exposes a virtual circuit intermediate representation (IR) that extends the notion of quantum circuits to incorporate gate virtualization. Based on the virtual circuit as our IR, we propose the QVM compiler—an extensible compiler infrastructure to transpile a virtual circuit through a series of modular optimization passes to produce a set of optimized circuit fragments. Lastly, these transpiled circuit fragments are executed on QPUs using our QVM runtime—a scalable and parallel infrastructure to virtualize and execute circuit fragments on a set of QPUs. We evaluate QVM on IBM's 7- and 27-qubit QPUs. Our evaluation shows that our approach allows for the execution of circuits with up to double the number of qubits compared to the qubit-count of a QPU, while improving fidelity by 4.7\texttimes{} on average compared to larger QPUs and that we can effectively reduce circuit depths to only 40\% of the original circuit depths.}, + journal = pacmpl, + month = jun, + eid = {187}, + pages = {187}, + numpages = {26}, + keywords = {Circuit Cutting, Quantum Circuit Optimization and Compilation}, + webnote = {PLDI '25}, + bibsource = qplbib +} + @article{Unruh2019, title = {Quantum Relational {{Hoare}} Logic}, author = {Unruh, Dominique}, @@ -2741,6 +3081,26 @@ @misc{Vandewetering2020 bibsource = qplbib } +@article{Venev2024, + author = {Venev, Hristo and Gehr, Timon and Dimitrov, Dimitar and Vechev, Martin}, + title = {Modular Synthesis of Efficient Quantum Uncomputation}, + year = {2024}, + publisher = acm, + address = {New York, NY, USA}, + volume = {8}, + number = {OOPSLA2}, + doi = {10.1145/3689785}, + abstract = {A key challenge of quantum programming is uncomputation: the reversible deallocation of qubits. And while there has been much recent progress on automating uncomputation, state-of-the-art methods are insufficient for handling today's expressive quantum programming languages. A core reason is that they operate on primitive quantum circuits, while quantum programs express computations beyond circuits, for instance, they can capture families of circuits defined recursively in terms of uncomputation and adjoints. In this paper, we introduce the first modular automatic approach to synthesize correct and efficient uncomputation for expressive quantum programs. Our method is based on two core technical contributions: (i) an intermediate representation (IR) that can capture expressive quantum programs and comes with support for uncomputation, and (ii) modular algorithms over that IR for synthesizing uncomputation and adjoints. We have built a complete end-to-end implementation of our method, including an implementation of the IR and the synthesis algorithms, as well as a translation from an expressive fragment of the Silq programming language to our IR and circuit generation from the IR. Our experimental evaluation demonstrates that we can handle programs beyond the capabilities of existing uncomputation approaches, while being competitive on the benchmarks they can handle. More broadly, we show that it is possible to benefit from the greater expressivity and safety offered by high-level quantum languages without sacrificing efficiency.}, + journal = pacmpl, + month = oct, + eid = {345}, + pages = {345}, + numpages = {28}, + keywords = {intermediate representations, quantum programming languages}, + webnote = {OOPSLA '24}, + bibsource = qplbib +} + @article{Vizzotto2006, title = {Structuring quantum effects: superoperators as arrows}, author = {Vizzotto, Juliana Kaizer and Altenkirch, Thorsten and Sabry, Amr}, @@ -2883,6 +3243,7 @@ @article{Yan2022 bibsource = qplbib } + @incollection{Ying2009, title = {Predicate {{Transformer Semantics}} of {{Quantum Programs}}}, author = {Ying, Mingsheng and Duan, Runyao and Feng, Yuan and Ji, Zhengfeng}, @@ -3121,6 +3482,46 @@ @article{Yuan2022a bibsource = qplbib } +@article{Yuan2025, + author = {Yuan, Charles and Villanyi, Agnes and Carbin, Michael}, + title = {Quantum Control Machine: The Limits of Control Flow in Quantum Programming}, + year = {2024}, + publisher = acm, + address = {New York, NY, USA}, + volume = {8}, + number = {OOPSLA1}, + doi = {10.1145/3649811}, + abstract = {Quantum algorithms for tasks such as factorization, search, and simulation rely on control flow such as branching and iteration that depends on the value of data in superposition. High-level programming abstractions for control flow, such as switches, loops, higher-order functions, and continuations, are ubiquitous in classical languages. By contrast, many quantum languages do not provide high-level abstractions for control flow in superposition, and instead require the use of hardware-level logic gates to implement such control flow.The reason for this gap is that whereas a classical computer supports control flow abstractions using a program counter that can depend on data, the typical architecture of a quantum computer does not analogously provide a program counter that can depend on data in superposition. As a result, the complete set of control flow abstractions that can be correctly realized on a quantum computer has not yet been established.In this work, we provide a complete characterization of the properties of control flow abstractions that are correctly realizable on a quantum computer. First, we prove that even on a quantum computer whose program counter exists in superposition, one cannot correctly realize control flow in quantum algorithms by lifting the classical conditional jump instruction to work in superposition. This theorem denies the ability to directly lift general abstractions for control flow such as the λ-calculus from classical to quantum programming.In response, we present the necessary and sufficient conditions for control flow to be correctly realizable on a quantum computer. We introduce the quantum control machine, an instruction set architecture featuring a conditional jump that is restricted to satisfy these conditions. We show how this design enables a developer to correctly express control flow in quantum algorithms using a program counter in place of logic gates.}, + journal = pacmpl, + month = apr, + eid = {94}, + pages = {94}, + numpages = {28}, + keywords = {quantum programming languages, quantum instruction set architectures}, + webnote = {OOPSLA '24}, + bibsource = qplbib +} + +@article{Zhang2025, + author = {Zhang, Zhicheng and Ying, Mingsheng}, + title = {Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs}, + year = {2025}, + publisher = acm, + address = {New York, NY, USA}, + volume = {9}, + number = {PLDI}, + doi = {10.1145/3729283}, + abstract = {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.}, + journal = pacmpl, + month = jun, + eid = {180}, + pages = {180}, + numpages = {26}, + keywords = {automatic parallelisation, compilation, partial evaluation, quantum architectures, quantum programming languages, recursive definition}, + webnote = {PLDI '25}, + bibsource = qplbib +} + @misc{Zhao2020, title = {{Quantum Software Engineering}: {Landscapes and Horizons}}, author = {Zhao, Jianjun}, diff --git a/biblatex.bib b/biblatex.bib index eabcf34a..2d43fb82 100644 --- a/biblatex.bib +++ b/biblatex.bib @@ -57,6 +57,22 @@ @string{pc % bibsource @string{qplbib = "Quantum Programming Languages \& Verification Bibliography, https://git.io/qpl-bib"} +@article{Abdulla2025, + author = {Abdulla, Parosh Aziz and Chen, Yo-Ga and Chen, Yu-Fang and Hol\'{\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej and Lin, Jyun-Ao and Lo, Fang-Yi and Tsai, Wei-Lun}, + title = {Verifying Quantum Circuits with Level-Synchronized Tree Automata}, + year = {2025}, + volume = {9}, + number = {POPL}, + doi = {10.1145/3704868}, + abstract = {We present a new method for the verification of quantum circuits based on a novel symbolic representation of sets of quantum states using level-synchronized tree automata (LSTAs). LSTAs extend classical tree automata by labeling each transition with a set of choices, which are then used to synchronize subtrees of an accepted tree. Compared to the traditional tree automata, LSTAs have an incomparable expressive power while maintaining important properties, such as closure under union and intersection, and decidable language emptiness and inclusion. We have developed an efficient and fully automated symbolic verification algorithm for quantum circuits based on LSTAs. The complexity of supported gate operations is at most quadratic, dramatically improving the exponential worst-case complexity of an earlier tree automata-based approach. Furthermore, we show that LSTAs are a promising model for parameterized verification, i.e., verifying the correctness of families of circuits with the same structure for any number of qubits involved, which principally lies beyond the capabilities of previous automated approaches. We implemented this method as a C++ tool and compared it with three symbolic quantum circuit verifiers and two simulators on several benchmark examples. The results show that our approach can solve problems with sizes orders of magnitude larger than the state of the art.}, + journaltitle = pacmpl, + month = jan, + eid = {32}, + keywords = {quantum circuits, tree automata, verification}, + webnote = {POPL '25}, + bibsource = qplbib +} + @inproceedings{Abramsky2004, title = {A Categorical Semantics of Quantum Protocols}, author = {Abramsky, Samson and Coecke, Bob}, @@ -193,6 +209,22 @@ @article{Amy2020 bibsource = qplbib } +@article{Amy2025, + author = {Amy, Matthew and Lunderville, Joseph}, + title = {Linear and Non-linear Relational Analyses for Quantum Program Optimization}, + year = {2025}, + volume = {9}, + number = {POPL}, + doi = {10.1145/3704873}, + abstract = {The phase folding optimization is a circuit optimization used in many quantum compilers as a fast and effective way of reducing the number of high-cost gates in a quantum circuit. However, existing formulations of the optimization rely on an exact, linear algebraic representation of the circuit, restricting the optimization to being performed on straightline quantum circuits or basic blocks in a larger quantum program. We show that the phase folding optimization can be re-cast as an affine relation analysis, which allows the direct application of classical techniques for affine relations to extend phase folding to quantum programs with arbitrarily complicated classical control flow including nested loops and procedure calls. Through the lens of relational analysis, we show that the optimization can be powered-up by substituting other classical relational domains, particularly ones for non-linear relations which are useful in analyzing circuits involving classical arithmetic. To increase the precision of our analysis and infer non-linear relations from gate sets involving only linear operations — such as Clifford+t — we show that the sum-over-paths technique can be used to extract precise symbolic transition relations for straightline circuits. Our experiments show that our methods are able to generate and use non-trivial loop invariants for quantum program optimization, as well as achieve some optimizations of common circuits which were previously attainable only by hand.}, + journaltitle = pacmpl, + month = jan, + eid = {37}, + keywords = {Quantum software, compiler optimization, data flow analysis, invariant generation, relational program analysis}, + webnote = {POPL '25}, + bibsource = qplbib +} + @article{ArdeshirLarijani2018, title = {Automated Equivalence Checking of Concurrent Quantum Systems}, author = {{Ardeshir-Larijani}, Ebrahim and Gay, Simon J. and Nagarajan, Rajagopal}, @@ -276,8 +308,6 @@ @inproceedings{Bichsel2020 author = {Bichsel, Benjamin and Baader, Maximilian and Gehr, Timon and Vechev, Martin}, date = {2020-06}, booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation}, - publisher = acm, - location = {New York, NY, USA}, series = {{{PLDI}} '20}, pages = {286--300}, doi = {10.1145/3385412.3386007}, @@ -346,6 +376,54 @@ @article{Briegel2009 bibsource = qplbib } +@article{Buckley2024, + author = {Buckley, Anita and Chuprikov, Pavel and Otoni, Rodrigo and Soul\'{e}, Robert and Rand, Robert and Eugster, Patrick}, + title = {An Algebraic Language for Specifying Quantum Networks}, + year = {2024}, + volume = {8}, + number = {PLDI}, + doi = {10.1145/3656430}, + abstract = {Quantum networks connect quantum capable nodes in order to achieve capabilities that are impossible only using classical information. Their fundamental unit of communication is the Bell pair, which consists of two entangled quantum bits. Unfortunately, Bell pairs are fragile and difficult to transmit directly, necessitating a network of repeaters, along with software and hardware that can ensure the desired results. Challenging intrinsic features of quantum networks, such as dealing with resource competition, motivate formal reasoning about quantum network protocols. To this end, we developed BellKAT, a novel specification language for quantum networks based upon Kleene algebra. To cater to the specific needs of quantum networks, we designed an algebraic structure, called BellSKA, which we use as the basis of BellKAT's denotational semantics. BellKAT's constructs describe entanglement distribution rules that allow for modular specification. We give BellKAT a sound and complete equational theory, allowing us to verify network protocols. We provide a prototype tool to showcase the expressiveness of BellKAT and how to optimize and verify networks in practice.}, + journaltitle = pacmpl, + month = jun, + eid = {200}, + keywords = {Kleene algebra, quantum networks, entanglement}, + webnote = {PLDI '24}, + bibsource = qplbib +} + +@article{Cao2025, + author = {Cao, Xiuqi and Zhou, Junyu and Liu, Yuhao and Shi, Yunong and Li, Gushu}, + title = {MarQSim: Reconciling Determinism and Randomness in Compiler Optimization for Quantum Simulation}, + year = {2025}, + volume = {9}, + number = {PLDI}, + doi = {10.1145/3729269}, + abstract = {Quantum Hamiltonian simulation, fundamental in quantum algorithm design, extends far beyond its foundational roots, powering diverse quantum computing applications. However, optimizing the compilation of quantum Hamiltonian simulation poses significant challenges. Existing approaches fall short in reconciling deterministic and randomized compilation, lack appropriate intermediate representations, and struggle to guarantee correctness. Addressing these challenges, we present MarQSim, a novel compilation framework. MarQSim leverages a Markov chain-based approach, encapsulated in the Hamiltonian Term Transition Graph, adeptly reconciling deterministic and randomized compilation benefits. Furthermore, we formulate a Minimum-Cost Flow model that can tune transition matrices to enforce correctness while accommodating various optimization objectives. Experimental results demonstrate MarQSim's superiority in generating more efficient quantum circuits for simulating various quantum Hamiltonians while maintaining precision.}, + journaltitle = pacmpl, + month = jun, + eid = {170}, + keywords = {Hamiltonian Simulation, Markov Chain, Minimum-Cost Flow Model, Quantum Computing}, + webnote = {PLDI '25}, + bibsource = qplbib +} + +@article{Carette2025, + author = {Carette, Jacques and Heunen, Chris and Kaarsgaard, Robin and Sabry, Amr}, + title = {How to Bake a Quantum Π}, + year = {2024}, + volume = {8}, + number = {ICFP}, + doi = {10.1145/3674625}, + abstract = {We construct a computationally universal quantum programming language QuantumΠ from two copies of Π, the internal language of rig groupoids. The first step constructs a pure (measurement-free) term language by interpreting each copy of Π in a generalisation of the category Unitary in which every morphism is "rotated" by a particular angle, and the two copies are amalgamated using a free categorical construction expressed as a computational effect. The amalgamated language only exhibits quantum behaviour for specific values of the rotation angles, a property which is enforced by imposing a small number of equations on the resulting category. The second step in the construction introduces measurements by layering an additional computational effect.}, + journaltitle = pacmpl, + month = aug, + eid = {236}, + keywords = {quantum programming language, reversible computing, rig category, unitary quantum computing}, + webnote = {ICFP '24}, + bibsource = qplbib +} + @inproceedings{Chardonnet2021, title = {{Geometry of Interaction for ZX-Diagrams}}, author = {Chardonnet, Kostia and Valiron, Beno{\^i}t and Vilmart, Renaud}, @@ -500,6 +578,22 @@ @misc{Colledan2022 bibsource = qplbib } +@article{Colledan2025, + author = {Colledan, Andrea and Dal Lago, Ugo}, + title = {Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages}, + year = {2025}, + volume = {9}, + number = {POPL}, + doi = {10.1145/3704883}, + abstract = {We introduce a type system for the Quipper language designed to derive upper bounds on the size of the circuits produced by the typed program. This size can be measured according to various metrics, including width, depth and gate count, but also variations thereof obtained by considering only some wire types or some gate kinds. The key ingredients for achieving this level of flexibility are effects and refinement types, both relying on indices, that is, generic arithmetic expressions whose operators are interpreted differently depending on the target metric. The approach is shown to be correct through logical predicates, under reasonable assumptions about the chosen resource metric. This approach is empirically evaluated through the QuRA tool, showing that, in many cases, inferring tight bounds is possible in a fully automatic way.}, + journaltitle = pacmpl, + month = jan, + eid = {47}, + keywords = {Effects, Lambda Calculus, Quantum Computing, Quipper, Refinement Types}, + webnote = {POPL '25}, + bibsource = qplbib +} + @misc{Cross2017, title = {Open {{Quantum Assembly Language}}}, author = {Cross, Andrew W. and Bishop, Lev S. and Smolin, John A. and Gambetta, Jay M.}, @@ -757,6 +851,22 @@ @article{Echenim2021a bibsource = qplbib } +@article{Fang2024, + author = {Fang, Wang and Ying, Mingsheng}, + title = {Symbolic Execution for Quantum Error Correction Programs}, + year = {2024}, + volume = {8}, + number = {PLDI}, + doi = {10.1145/3656419}, + abstract = {We define QSE, a symbolic execution framework for quantum programs by integrating symbolic variables into quantum states and the outcomes of quantum measurements. The soundness of QSE is established through a theorem that ensures the correctness of symbolic execution within operational semantics. We further introduce symbolic stabilizer states, which symbolize the phases of stabilizer generators, for the efficient analysis of quantum error correction (QEC) programs. Within the QSE framework, we can use symbolic expressions to characterize the possible discrete Pauli errors in QEC, providing a significant improvement over existing methods that rely on sampling with simulators. We implement QSE with the support of symbolic stabilizer states in a prototype tool named QuantumSE.jl. Our experiments on representative QEC codes, including quantum repetition codes, Kitaev's toric codes, and quantum Tanner codes, demonstrate the efficiency of QuantumSE.jl for debugging QEC programs with over 1000 qubits. In addition, by substituting concrete values in symbolic expressions of measurement results, QuantumSE.jl is also equipped with a sampling feature for stabilizer circuits. Despite a longer initialization time than the state-of-the-art stabilizer simulator, Google's Stim, QuantumSE.jl offers a quicker sampling rate in the experiments.}, + journaltitle = pacmpl, + month = jun, + eid = {189}, + keywords = {symbolic execution, stabilizer formalism}, + webnote = {PLDI '24}, + bibsource = qplbib +} + @article{Feng2021, title = {Quantum Hoare Logic with Classical Variables}, author = {Feng, Yuan and Ying, Mingsheng}, @@ -1153,6 +1263,22 @@ @thesis{Hietala2022 bibsource = qplbib } +@article{Hirata2025, + author = {Hirata, Kengo and Heunen, Chris}, + title = {Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime}, + year = {2025}, + volume = {9}, + number = {POPL}, + doi = {10.1145/3704842}, + abstract = {Uncomputation is a feature in quantum programming that allows the programmer to discard a value without losing quantum information, and that allows the compiler to reuse resources. Whereas quantum information has to be treated linearly by the type system, automatic uncomputation enables the programmer to treat it affinely to some extent. Automatic uncomputation requires a substructural type system between linear and affine, a subtlety that has only been captured by existing languages in an ad hoc way. We extend the Rust type system to the quantum setting to give a uniform framework for automatic uncomputation called Qurts (pronounced quartz). Specifically, we parameterise types by lifetimes, permitting them to be affine during their lifetime, while being restricted to linear use outside their lifetime. We also provide two operational semantics: one based on classical simulation, and one that does not depend on any specific uncomputation strategy.}, + journaltitle = pacmpl, + month = jan, + eid = {6}, + keywords = {Affine Type, Lifetime, Linear Type, Quantum Programming, Rust, Uncomputation}, + webnote = {POPL '25}, + bibsource = qplbib +} + @inproceedings{Honda2015, title = {Analysis of Quantum Entanglement in Quantum Programs using Stabilizer Formalism}, author = {Honda, Kentaro}, @@ -1186,6 +1312,22 @@ @inproceedings{Huang2019 bibsource = qplbib } +@article{Huang2025, + author = {Huang, Qifan and Zhou, Li and Fang, Wang and Zhao, Mengyu and Ying, Mingsheng}, + title = {Efficient Formal Verification of Quantum Error Correcting Programs}, + year = {2025}, + volume = {9}, + number = {PLDI}, + doi = {10.1145/3729293}, + abstract = {Quantum error correction (QEC) is fundamental for suppressing noise in quantum hardware and enabling fault-tolerant quantum computation. In this paper, we propose an efficient verification framework for QEC programs. We define an assertion logic and a program logic specifically crafted for QEC programs and establish a sound proof system. We then develop an efficient method for handling verification conditions (VCs) of QEC programs: for Pauli errors, the VCs are reduced to classical assertions that can be solved by SMT solvers, and for non-Pauli errors, we provide a heuristic algorithm. We formalize the proposed program logic in Coq proof assistant, making it a verified QEC verifier. Additionally, we implement an automated QEC verifier, Veri-QEC, for verifying various fault-tolerant scenarios. We demonstrate the efficiency and broad functionality of the framework by performing different verification tasks across various scenarios. Finally, we present a benchmark of 14 verified stabilizer codes.}, + journaltitle = pacmpl, + month = jun, + eid = {190}, + keywords = {Formal verification, Hoare logic, Quantum error correction, Quantum programming language}, + webnote = {PLDI '25}, + bibsource = qplbib +} + @inproceedings{Huot2019, title = {Universal Properties in Quantum Theory}, author = {Huot, Mathieu and Staton, Sam}, @@ -1265,6 +1407,22 @@ @article{JavadiAbhari2015 bibsource = qplbib } +@article{Jeon2024, + author = {Jeon, Seungmin and Cho, Kyeongmin and Kang, Chan Gu and Lee, Janggun and Oh, Hakjoo and Kang, Jeehoon}, + title = {Quantum Probabilistic Model Checking for Time-Bounded Properties}, + year = {2024}, + volume = {8}, + number = {OOPSLA2}, + doi = {10.1145/3689731}, + abstract = {Probabilistic model checking (PMC) is a verification technique for analyzing the properties of probabilistic systems. However, existing techniques face challenges in verifying large systems with high accuracy. PMC struggles with state explosion, where the number of states grows exponentially with the size of the system, making large system verification infeasible. While statistical model checking (SMC) avoids PMC's state explosion problem by using a simulation approach, it suffers from runtime explosion, requiring numerous samples for high accuracy. To address these limitations in verifying large systems with high accuracy, we present quantum probabilistic model checking (QPMC), the first method leveraging quantum computing for PMC with respect to time-bounded properties. QPMC addresses state explosion by encoding PMC problems into quantum circuits that superpose states within qubits. Additionally, QPMC resolves runtime explosion through Quantum Amplitude Estimation, efficiently estimating the probabilities of specified properties. We prove that QPMC correctly solves PMC problems and achieves a quadratic speedup in time complexity compared to SMC.}, + journaltitle = pacmpl, + month = oct, + eid = {291}, + keywords = {bounded reachability, probabilistic model checking, quantum computing}, + webnote = {OOPSLA '24}, + bibsource = qplbib +} + @article{Jia2022, title = {Semantics for Variational Quantum Programming}, author = {Jia, Xiaodong and Kornell, Andre and Lindenhovius, Bert and Mislove, Michael and Zamdzhiev, Vladimir}, @@ -1313,6 +1471,22 @@ @article{Kang2023 bibsource = qplbib } +@article{Kang2024, + author = {Kang, Chan Gu and Lee, Joonghoon and Oh, Hakjoo}, + title = {Statistical Testing of Quantum Programs via Fixed-Point Amplitude Amplification}, + year = {2024}, + volume = {8}, + number = {OOPSLA2}, + doi = {10.1145/3689716}, + abstract = {We present a new technique for accelerating quantum program testing. Given a quantum circuit with an input/output specification, our goal is to check whether executing the program on the input state produces the expected output. In quantum computing, however, it is impossible to directly check the equivalence of the two quantum states. Instead, we rely on statistical testing, which involves repeated program executions, state measurements, and subsequent comparisons with the specified output. To guarantee a high level of assurance, however, this method requires an extensive number of measurements. In this paper, we propose a solution to alleviate this challenge by adapting Fixed-Point Amplitude Amplification (FPAA) for quantum program testing. We formally present our technique, demonstrate its ability to reduce the required number of measurements as well as runtime cost without sacrificing the original statistical guarantee, and showcase its runtime effectiveness through case studies.}, + journaltitle = pacmpl, + month = oct, + eid = {276}, + keywords = {Quantum Computing, Quantum Programming, Testing, Verification}, + webnote = {OOPSLA '24}, + bibsource = qplbib +} + @techreport{Knill1996, title = {Conventions for Quantum Pseudocode}, author = {Knill, Emanuel}, @@ -1486,6 +1660,22 @@ @article{Li2022 bibsource = qplbib } +@article{Li2025, + author = {Li, Liyi and Young, David and Graves, James Bryan and Dissanayake, Chandeepa and Sabry, Amr}, + title = {A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware}, + year = {2025}, + volume = {9}, + number = {ICFP}, + doi = {10.1145/3747521}, + abstract = {In physics and chemistry, quantum systems are typically modeled using energy constraints formulated as Hamiltonians. Investigations into such systems often focus on the evolution of the Hamiltonians under various initial conditions, an approach summarized as Adiabatic Quantum Computing (AQC). Although this perspective may initially seem foreign to functional programmers, we demonstrate that conventional functional programming abstractions—specifically, the Traversable and Monad type classes—naturally capture the essence of AQC. To illustrate this connection, we introduce EnQ, a functional programming library designed to express diverse optimization problems as energy constraint computations (ECC). The library comprises three core components: generating the solution space, associating energy costs with potential solutions, and searching for optimal or near-optimal solutions. Because EnQ is implemented using standard Haskell, it can be executed directly through conventional classical Haskell compilers. More interestingly, we develop and implement a process to compile EnQ programs into circuits executable on quantum hardware. We validate EnQ's effectiveness through a number of case studies, demonstrating its capacity to express and solve classical optimization problems on quantum hardware, including search problems, type inference, number partitioning, clique finding, and graph coloring.}, + journaltitle = pacmpl, + month = aug, + eid = {252}, + keywords = {Adiabatic Quantum Computation, Energy Constraint Computation, Functional Programming}, + webnote = {ICFP '25}, + bibsource = qplbib +} + @inproceedings{Lindenhovius2018, title = {Enriching a {{Linear}}/{{Non}}-Linear {{Lambda Calculus}}: {{A Programming Language}} for {{String Diagrams}}}, shorttitle = {Enriching a {{Linear}}/{{Non}}-Linear {{Lambda Calculus}}}, @@ -1597,6 +1787,22 @@ @article{Meuli2020 bibsource = qplbib } +@article{Molavi2025, + author = {Molavi, Abtin and Xu, Amanda and Tannu, Swamit and Albarghouthi, Aws}, + title = {Dependency-Aware Compilation for Surface Code Quantum Architectures}, + year = {2025}, + volume = {9}, + number = {OOPSLA1}, + doi = {10.1145/3720416}, + abstract = {Practical applications of quantum computing depend on fault-tolerant devices with error correction. We study the problem of compiling quantum circuits for quantum computers implementing surface codes. Optimal or near-optimal compilation is critical for both efficiency and correctness. The compilation problem requires (1) mapping circuit qubits to the device qubits and (2) routing execution paths between interacting qubits. We solve this problem efficiently and near-optimally with a novel algorithm that exploits the dependency structure of circuit operations to formulate discrete optimization problems that can be approximated via simulated annealing, a classic and simple algorithm. Our extensive evaluation shows that our approach is powerful and flexible for compiling realistic workloads.}, + journaltitle = pacmpl, + month = apr, + eid = {82}, + keywords = {quantum error-correction, simulated annealing}, + webnote = {OOPSLA '25}, + bibsource = qplbib +} + @article{Mosca2019, title = {{Quantum Programming Languages (Dagstuhl Seminar 18381)}}, author = {Mosca, Michele and Roetteler, Martin and Selinger, Peter}, @@ -1747,6 +1953,22 @@ @inproceedings{Paradis2021 bibsource = qplbib } +@article{Paradis2024, + author = {Paradis, Anouk and Dekoninck, Jasper and Bichsel, Benjamin and Vechev, Martin}, + title = {Synthetiq: Fast and Versatile Quantum Circuit Synthesis}, + year = {2024}, + volume = {8}, + number = {OOPSLA1}, + doi = {10.1145/3649813}, + abstract = {To implement quantum algorithms on quantum computers it is crucial to decompose their operators into the limited gate set supported by those computers. Unfortunately, existing works automating this essential task are generally slow and only applicable to narrow use cases. We present Synthetiq, a method to synthesize quantum circuits implementing a given specification over arbitrary finite gate sets, which is faster and more versatile than existing works. Synthetiq utilizes Simulated Annealing instantiated with a novel, domain-specific energy function that allows developers to leverage partial specifications for better efficiency. Synthetiq further couples this synthesis method with a custom simplification pass, to ensure efficiency of the found circuits.We experimentally demonstrate that Synthetiq can generate better implementations than were previously known for multiple relevant quantum operators including RCCCX, CCT, CCiSWAP, C SWAP, and CiSWAP Our extensive evaluation also demonstrates Synthetiq frequently outperforms a wide variety of more specialized tools in their own domains, including (i) the well-studied task of synthesizing fully specified operators in the Clifford+T gate set, (ii) ϵ-approximate synthesis of multi-qubit operators in the same gate set, and (iii) synthesis tasks with custom gate sets. On all those tasks, Synthetiq is typically one to two orders of magnitude faster than previous state-of-the-art and can tackle problems that were previously out of the reach of any synthesis tool.}, + journaltitle = pacmpl, + month = apr, + eid = {96}, + keywords = {Quantum Circuits, Synthesis, Clifford+T}, + webnote = {OOPSLA '24}, + bibsource = qplbib +} + @inproceedings{Paykin2017, title = {{{QWIRE}}: A Core Language for Quantum Circuits}, author = {Paykin, Jennifer and Rand, Robert and Zdancewic, Steve}, @@ -1829,6 +2051,22 @@ @inproceedings{Peduri2022 bibsource = qplbib } +@article{Peduri2025, + author = {Peduri, Anurudh and Schaefer, Ina and Walter, Michael}, + title = {QbC: Quantum Correctness by Construction}, + year = {2025}, + volume = {9}, + number = {OOPSLA1}, + doi = {10.1145/3720433}, + abstract = {Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC): an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.}, + journaltitle = pacmpl, + month = apr, + eid = {99}, + keywords = {correctness by construction, quantum Hoare logic, quantum while language}, + webnote = {OOSPLA '25}, + bibsource = qplbib +} + @inproceedings{Peng2022, title = {Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra}, author = {Peng, Yuxiang and Ying, Mingsheng and Wu, Xiaodi}, @@ -2207,6 +2445,22 @@ @inbook{Selinger2009 bibsource = qplbib } +@article{Sharma2025, + author = {Sharma, Ritvik and Achour, Sara}, + title = {Optimizing Ancilla-Based Quantum Circuits with SPARE}, + year = {2025}, + volume = {9}, + number = {PLDI}, + doi = {10.1145/3729253}, + abstract = {Many quantum algorithms instantiate and use ancillas, spare qubits that serve as temporary storage in a quantum circuit. In particular, many recently developed high-level and modular quantum programming languages (QPLs) use ancilla qubits to implement various programming constructs. These are lowered to circuits with nested/cascading compute-uncompute gate sequences that use ancilla qubits to track internal state. We present SPARE, a rewrite-based quantum circuit optimizer that restructures these compute-uncompute gate sequences, leveraging the ancilla qubit state information to optimize the circuit. In this work, we prove the correctness of SPARE's rewrites and link SPARE's gate-level transforms to language-level program rewrites, which may be performed on the input language. We evaluate SPARE on QPL-generated quantum circuits against Unqomp and Spire, two optimizing compilers for QPLs. SPARE achieves a reduction of up to 27.3\% in qubit count, 56.7\% in 2-qubit gates, 68.2\% in 1-qubit gates and 73.9\% in depth against Unqomp, and up to 17.8\% in qubits, 67.3\% in 2-qubit gates, 61.4\% in 1-qubit gates and 59.9\% in depth against Spire. We also evaluate SPARE against the Quartz, Feynman, and PyZX circuit optimizers: SPARE achieves up to a 70.0\% reduction in two-qubit gates, up to a 53.6\% reduction in 1-qubit gates, and up to a 56.7\% reduction in depth compared to the best result from all the gate-level optimizers.}, + journaltitle = pacmpl, + month = jun, + eid = {154}, + keywords = {quantum optimizing compilers, quantum programming languages}, + webnote = {PLDI '25}, + bibsource = qplbib +} + @inproceedings{Singhal2020, title = {Verified translation between low-level quantum languages}, author = {Singhal, Kartik and Rand, Robert and Hicks, Michael}, @@ -2437,6 +2691,22 @@ @inproceedings{Tao2022 bibsource = qplbib } +@article{Tornow2025, + author = {Tornow, Nathaniel and Giortamis, Emmanouil and Bhatotia, Pramod}, + title = {QVM: Quantum Gate Virtualization Machine}, + year = {2025}, + volume = {9}, + number = {PLDI}, + doi = {10.1145/3729290}, + abstract = {We present the Quantum Gate Virtualization Machine (QVM), an end-to-end generic system for scalable execution of large quantum circuits with high fidelity on noisy and small quantum processors (QPUs) by leveraging gate virtualization. QVM exposes a virtual circuit intermediate representation (IR) that extends the notion of quantum circuits to incorporate gate virtualization. Based on the virtual circuit as our IR, we propose the QVM compiler—an extensible compiler infrastructure to transpile a virtual circuit through a series of modular optimization passes to produce a set of optimized circuit fragments. Lastly, these transpiled circuit fragments are executed on QPUs using our QVM runtime—a scalable and parallel infrastructure to virtualize and execute circuit fragments on a set of QPUs. We evaluate QVM on IBM's 7- and 27-qubit QPUs. Our evaluation shows that our approach allows for the execution of circuits with up to double the number of qubits compared to the qubit-count of a QPU, while improving fidelity by 4.7\texttimes{} on average compared to larger QPUs and that we can effectively reduce circuit depths to only 40\% of the original circuit depths.}, + journaltitle = pacmpl, + month = jun, + eid = {187}, + keywords = {Circuit Cutting, Quantum Circuit Optimization and Compilation}, + webnote = {PLDI '25}, + bibsource = qplbib +} + @article{Unruh2019, title = {Quantum Relational {{Hoare}} Logic}, author = {Unruh, Dominique}, @@ -2521,6 +2791,22 @@ @misc{Vandewetering2020 bibsource = qplbib } +@article{Venev2024, + author = {Venev, Hristo and Gehr, Timon and Dimitrov, Dimitar and Vechev, Martin}, + title = {Modular Synthesis of Efficient Quantum Uncomputation}, + year = {2024}, + volume = {8}, + number = {OOPSLA2}, + doi = {10.1145/3689785}, + abstract = {A key challenge of quantum programming is uncomputation: the reversible deallocation of qubits. And while there has been much recent progress on automating uncomputation, state-of-the-art methods are insufficient for handling today's expressive quantum programming languages. A core reason is that they operate on primitive quantum circuits, while quantum programs express computations beyond circuits, for instance, they can capture families of circuits defined recursively in terms of uncomputation and adjoints. In this paper, we introduce the first modular automatic approach to synthesize correct and efficient uncomputation for expressive quantum programs. Our method is based on two core technical contributions: (i) an intermediate representation (IR) that can capture expressive quantum programs and comes with support for uncomputation, and (ii) modular algorithms over that IR for synthesizing uncomputation and adjoints. We have built a complete end-to-end implementation of our method, including an implementation of the IR and the synthesis algorithms, as well as a translation from an expressive fragment of the Silq programming language to our IR and circuit generation from the IR. Our experimental evaluation demonstrates that we can handle programs beyond the capabilities of existing uncomputation approaches, while being competitive on the benchmarks they can handle. More broadly, we show that it is possible to benefit from the greater expressivity and safety offered by high-level quantum languages without sacrificing efficiency.}, + journaltitle = pacmpl, + month = oct, + eid = {345}, + keywords = {intermediate representations, quantum programming languages}, + webnote = {OOPSLA '24}, + bibsource = qplbib +} + @article{Vizzotto2006, title = {Structuring quantum effects: superoperators as arrows}, author = {Vizzotto, Juliana Kaizer and Altenkirch, Thorsten and Sabry, Amr}, @@ -2866,6 +3152,38 @@ @article{Yuan2022a bibsource = qplbib } +@article{Yuan2025, + author = {Yuan, Charles and Villanyi, Agnes and Carbin, Michael}, + title = {Quantum Control Machine: The Limits of Control Flow in Quantum Programming}, + year = {2024}, + volume = {8}, + number = {OOPSLA1}, + doi = {10.1145/3649811}, + abstract = {Quantum algorithms for tasks such as factorization, search, and simulation rely on control flow such as branching and iteration that depends on the value of data in superposition. High-level programming abstractions for control flow, such as switches, loops, higher-order functions, and continuations, are ubiquitous in classical languages. By contrast, many quantum languages do not provide high-level abstractions for control flow in superposition, and instead require the use of hardware-level logic gates to implement such control flow.The reason for this gap is that whereas a classical computer supports control flow abstractions using a program counter that can depend on data, the typical architecture of a quantum computer does not analogously provide a program counter that can depend on data in superposition. As a result, the complete set of control flow abstractions that can be correctly realized on a quantum computer has not yet been established.In this work, we provide a complete characterization of the properties of control flow abstractions that are correctly realizable on a quantum computer. First, we prove that even on a quantum computer whose program counter exists in superposition, one cannot correctly realize control flow in quantum algorithms by lifting the classical conditional jump instruction to work in superposition. This theorem denies the ability to directly lift general abstractions for control flow such as the λ-calculus from classical to quantum programming.In response, we present the necessary and sufficient conditions for control flow to be correctly realizable on a quantum computer. We introduce the quantum control machine, an instruction set architecture featuring a conditional jump that is restricted to satisfy these conditions. We show how this design enables a developer to correctly express control flow in quantum algorithms using a program counter in place of logic gates.}, + journaltitle = pacmpl, + month = apr, + eid = {94}, + keywords = {quantum programming languages, quantum instruction set architectures}, + webnote = {OOPSLA '24}, + bibsource = qplbib +} + +@article{Zhang2025, + author = {Zhang, Zhicheng and Ying, Mingsheng}, + title = {Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs}, + year = {2025}, + volume = {9}, + number = {PLDI}, + doi = {10.1145/3729283}, + abstract = {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.}, + journaltitle = pacmpl, + month = jun, + eid = {180}, + keywords = {automatic parallelisation, compilation, partial evaluation, quantum architectures, quantum programming languages, recursive definition}, + webnote = {PLDI '25}, + bibsource = qplbib +} + @misc{Zhao2020, title = {{Quantum Software Engineering}: {Landscapes and Horizons}}, author = {Zhao, Jianjun},