Refinement orders for quantum programs

• URL: http://arxiv.org/abs/2504.14158v1
• Date: Sat, 19 Apr 2025 03:09:36 GMT
• Title: Refinement orders for quantum programs
• Authors: Yuan Feng, Li Zhou,
• Abstract summary: Refinement is an influential technique used in the verification and development of computer programs.<n>Different orders can be defined with respect to partial and total correctness, as well as for deterministic and nondeterministic programs.<n>This paper thoroughly explores different refinement orders for quantum programs and examines the relationships between them.
• Score: 4.6914963480854155
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Refinement is an influential technique used in the verification and development of computer programs. It provides a systematic and rigorous approach to software development through stepwise refinement, where a high-level abstract specification is progressively transformed into an implementation that meets the desired requirements. Central to this technique is the notion of a refinement order, which ensures that each refinement step preserves program correctness. Different orders can be defined with respect to partial and total correctness, as well as for deterministic and nondeterministic programs. In the realm of quantum programs, the theory becomes even more intricate due to the existence of various quantum state predicates, leading to different notions of specifications. This paper thoroughly explores different refinement orders for quantum programs and examines the relationships between them.

Related papers

• Design and synthesis of scalable quantum programs [0.8007726207322294]
  We present a scalable, robust approach to creating quantum programs of arbitrary size and complexity.<n>The quantum program is expressed in terms of a high-level model together with constraints and objectives on the final program.<n>The technology adapts electronic design automation methods to quantum computing, finding feasible implementations in a virtually unlimited functional space.
  arXiv  Detail & Related papers  (2024-12-10T10:12:03Z)
• An Abstraction Hierarchy Toward Productive Quantum Programming [0.3640881838485995]
  We propose an abstraction hierarchy to support quantum software engineering. We discuss the consequences of overlaps across the programming, execution, and hardware models found in current technologies. While our work points to concrete conceptual challenges and gaps in quantum programming, our primary thesis is that progress hinges on thinking about the abstraction hierarchy holistically.
  arXiv  Detail & Related papers  (2024-05-22T18:48:36Z)
• Refinement calculus of quantum programs with projective assertions [5.151896714190243]
  This paper introduces a refinement calculus tailored for quantum programs. We first study the partial correctness of nondeterministic programs within a quantum. We also present their semantics in transforming a postcondition to the weakest liberal postconditions.
  arXiv  Detail & Related papers  (2023-11-23T22:12:57Z)
• Quantum algorithms: A survey of applications and end-to-end complexities [90.05272647148196]
  The anticipated applications of quantum computers span across science and industry. We present a survey of several potential application areas of quantum algorithms. We outline the challenges and opportunities in each area in an "end-to-end" fashion.
  arXiv  Detail & Related papers  (2023-10-04T17:53:55Z)
• Near-Term Distributed Quantum Computation using Mean-Field Corrections and Auxiliary Qubits [77.04894470683776]
  We propose near-term distributed quantum computing that involve limited information transfer and conservative entanglement production. We build upon these concepts to produce an approximate circuit-cutting technique for the fragmented pre-training of variational quantum algorithms.
  arXiv  Detail & Related papers  (2023-09-11T18:00:00Z)
• QbC: Quantum Correctness by Construction [4.572433350229651]
  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 find that the approach naturally suggests how to derive program details, highlighting key design choices along the way.
  arXiv  Detail & Related papers  (2023-07-28T16:00:57Z)
• Verification of Nondeterministic Quantum Programs [1.9302781323430196]
  Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the details of possible implementations. Nondeterminism has also been introduced in quantum programming, and the termination of nondeterministic quantum programs has been extensively analysed.
  arXiv  Detail & Related papers  (2023-02-15T22:37:23Z)
• Assessing requirements to scale to practical quantum advantage [56.22441723982983]
  We develop a framework for quantum resource estimation, abstracting the layers of the stack, to estimate resources required for large-scale quantum applications. We assess three scaled quantum applications and find that hundreds of thousands to millions of physical qubits are needed to achieve practical quantum advantage. A goal of our work is to accelerate progress towards practical quantum advantage by enabling the broader community to explore design choices across the stack.
  arXiv  Detail & Related papers  (2022-11-14T18:50:27Z)
• Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
  We propose circuit-oriented symmetry verification that are capable of verifying the commutativity of quantum circuits without the knowledge of the quantum state. In particular, we propose the Fourier-temporal stabilizer (STS) technique, which generalizes the conventional quantum-domain formalism to circuit-oriented stabilizers.
  arXiv  Detail & Related papers  (2021-12-27T21:15:35Z)
• Realization of arbitrary doubly-controlled quantum phase gates [62.997667081978825]
  We introduce a high-fidelity gate set inspired by a proposal for near-term quantum advantage in optimization problems. By orchestrating coherent, multi-level control over three transmon qutrits, we synthesize a family of deterministic, continuous-angle quantum phase gates acting in the natural three-qubit computational basis.
  arXiv  Detail & Related papers  (2021-08-03T17:49:09Z)
• Detailed Account of Complexity for Implementation of Some Gate-Based Quantum Algorithms [55.41644538483948]
  In particular, some steps of the implementation, as state preparation and readout processes, can surpass the complexity aspects of the algorithm itself. We present the complexity involved in the full implementation of quantum algorithms for solving linear systems of equations and linear system of differential equations.
  arXiv  Detail & Related papers  (2021-06-23T16:33:33Z)
• On the Principles of Differentiable Quantum Programming Languages [13.070557640180004]
  Variational Quantum Circuits (VQCs) are predicted to be one of the most important near-term quantum applications. We propose the first formalization of auto-differentiation techniques for quantum circuits.
  arXiv  Detail & Related papers  (2020-04-02T16:46:13Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.