Quantum Hoare Type Theory

• URL: http://arxiv.org/abs/2012.02154v2
• Date: Mon, 15 Nov 2021 17:57:45 GMT
• Title: Quantum Hoare Type Theory
• Authors: Kartik Singhal
• Abstract summary: Quantum Hoare Type Theory (QHTT) is inspired by Hoare Type Theory in classical computing. QHTT provides precise specifications about the modification to the quantum state can be provided within the type of computation.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. Inspired by Hoare Type Theory in classical computing, we propose Quantum Hoare Type Theory (QHTT), in which precise specifications about the modification to the quantum state can be provided within the type of computation. These specifications within a Hoare type are given in the form of Hoare-logic style pre- and postconditions following the propositions-as-types principle. The type-checking process verifies that the implementation conforms to the provided specification. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs.

Related papers

• A Practical Quantum Hoare Logic with Classical Variables, I [2.789440475527173]
  We present a Hoare-style logic for reasoning about quantum programs with classical variables. Our approach offers several improvements over previous work. It applies to quantum programs with classical variables that incorporate quantum arrays and parameterised quantum gates.
  arXiv  Detail & Related papers  (2024-12-13T05:28:19Z)
• Formal verification of higher dimensional quantum protocols [0.0]
  We present our preliminary results in extending the theory of behavioural equivalence in CQP to verify higher dimensional quantum protocols using qudits. This is a work-in-progress and we present our preliminary results in extending the theory of behavioural equivalence in CQP to verify higher dimensional quantum protocols using qudits.
  arXiv  Detail & Related papers  (2024-09-26T15:53:14Z)
• Efficient Learning for Linear Properties of Bounded-Gate Quantum Circuits [63.733312560668274]
  Given a quantum circuit containing d tunable RZ gates and G-d Clifford gates, can a learner perform purely classical inference to efficiently predict its linear properties? We prove that the sample complexity scaling linearly in d is necessary and sufficient to achieve a small prediction error, while the corresponding computational complexity may scale exponentially in d. We devise a kernel-based learning model capable of trading off prediction error and computational complexity, transitioning from exponential to scaling in many practical settings.
  arXiv  Detail & Related papers  (2024-08-22T08:21:28Z)
• Non-unitary Coupled Cluster Enabled by Mid-circuit Measurements on Quantum Computers [37.69303106863453]
  We propose a state preparation method based on coupled cluster (CC) theory, which is a pillar of quantum chemistry on classical computers. Our approach leads to a reduction of the classical computation overhead, and the number of CNOT and T gates by 28% and 57% on average.
  arXiv  Detail & Related papers  (2024-06-17T14:10:10Z)
• 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)
• TeD-Q: a tensor network enhanced distributed hybrid quantum machine learning framework [59.07246314484875]
  TeD-Q is an open-source software framework for quantum machine learning. It seamlessly integrates classical machine learning libraries with quantum simulators. It provides a graphical mode in which the quantum circuit and the training progress can be visualized in real-time.
  arXiv  Detail & Related papers  (2023-01-13T09:35:05Z)
• Qafny: A Quantum-Program Verifier [39.47005122712576]
  We present Qafny, an automated proof system for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations. We show how Qafny can efficiently verify important quantum algorithms, including quantum-walk algorithms, Grover's algorithm, and Shor's algorithm.
  arXiv  Detail & Related papers  (2022-11-11T18:50:52Z)
• An Introduction to Quantum Machine Learning for Engineers [36.18344598412261]
  Quantum machine learning is emerging as a dominant paradigm to program gate-based quantum computers. This book provides a self-contained introduction to quantum machine learning for an audience of engineers with a background in probability and linear algebra.
  arXiv  Detail & Related papers  (2022-05-11T12:10:52Z)
• Quantum Neuron with Separable-State Encoding [0.0]
  It is not yet possible to test advanced quantum neuron models on a large scale in currently available quantum processors. We propose a quantum perceptron (QP) model that uses a reduced number of multi-qubit gates. We demonstrate the performance of the proposed model by implementing a few qubits version of the QP in a simulated quantum computer.
  arXiv  Detail & Related papers  (2022-02-16T19:26:23Z)
• 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)
• Quantum Hoare Type Theory: Extended Abstract [0.0]
  In quantum computing, formal verification and sound static type systems prevent several classes of bugs from being introduced. We propose Quantum Hoare Types by extending the Quantum IO Monad by indexing it with pre- and post-conditions that serve as program specifications. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs.
  arXiv  Detail & Related papers  (2021-09-06T01:02:20Z)
• The Hintons in your Neural Network: a Quantum Field Theory View of Deep Learning [84.33745072274942]
  We show how to represent linear and non-linear layers as unitary quantum gates, and interpret the fundamental excitations of the quantum model as particles. On top of opening a new perspective and techniques for studying neural networks, the quantum formulation is well suited for optical quantum computing.
  arXiv  Detail & Related papers  (2021-03-08T17:24:29Z)
• Facial Expression Recognition on a Quantum Computer [68.8204255655161]
  We show a possible solution to facial expression recognition using a quantum machine learning approach. We define a quantum circuit that manipulates the graphs adjacency matrices encoded into the amplitudes of some appropriately defined quantum states.
  arXiv  Detail & Related papers  (2021-02-09T13:48:00Z)

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.