Quantum Hoare Type Theory: Extended Abstract

• URL: http://arxiv.org/abs/2109.02198v1
• Date: Mon, 6 Sep 2021 01:02:20 GMT
• Title: Quantum Hoare Type Theory: Extended Abstract
• Authors: Kartik Singhal (University of Chicago), John Reppy (University of Chicago)
• Abstract summary: 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.
• 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. In classical computing, formal verification and sound static type systems prevent several classes of bugs from being introduced. There is a need for similar techniques in the quantum regime. Inspired by Hoare Type Theory in the classical paradigm, we propose Quantum Hoare Types by extending the Quantum IO Monad by indexing it with pre- and post-conditions that serve as program specifications. In this paper, we introduce Quantum Hoare Type Theory (QHTT), present its syntax and typing rules, and demonstrate its effectiveness with the help of examples. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs. This is a work in progress.

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)
• Quantum types: going beyond qubits and quantum gates [0.0]
  This article outlines the need for higher-level abstractions and proposes some of them in a developer-friendly programming language called Rhyme. The new quantum types are extensions of classical types, including bits, integers, floats, characters, arrays, and strings.
  arXiv  Detail & Related papers  (2024-01-26T18:54:35Z)
• 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)
• Quantum data learning for quantum simulations in high-energy physics [55.41644538483948]
  We explore the applicability of quantum-data learning to practical problems in high-energy physics. We make use of ansatz based on quantum convolutional neural networks and numerically show that it is capable of recognizing quantum phases of ground states. The observation of non-trivial learning properties demonstrated in these benchmarks will motivate further exploration of the quantum-data learning architecture in high-energy physics.
  arXiv  Detail & Related papers  (2023-06-29T18:00:01Z)
• Simple Tests of Quantumness Also Certify Qubits [69.96668065491183]
  A test of quantumness is a protocol that allows a classical verifier to certify (only) that a prover is not classical. We show that tests of quantumness that follow a certain template, which captures recent proposals such as (Kalai et al., 2022) can in fact do much more. Namely, the same protocols can be used for certifying a qubit, a building-block that stands at the heart of applications such as certifiable randomness and classical delegation of quantum computation.
  arXiv  Detail & Related papers  (2023-03-02T14:18:17Z)
• Quantum Machine Learning: from physics to software engineering [58.720142291102135]
  We show how classical machine learning approach can help improve the facilities of quantum computers. We discuss how quantum algorithms and quantum computers may be useful for solving classical machine learning tasks.
  arXiv  Detail & Related papers  (2023-01-04T23:37:45Z)
• 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)
• LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
  This paper introduces a dynamic logic formalism for reasoning about information flow in composite quantum systems. We present a finitary syntax, a relational semantics and a sound proof system for this logic. As applications, we use our system to give formal correctness for the Teleportation protocol and for a standard Quantum Secret Sharing protocol.
  arXiv  Detail & Related papers  (2021-10-04T12:20:23Z)
• Imaginary Time Propagation on a Quantum Chip [50.591267188664666]
  Evolution in imaginary time is a prominent technique for finding the ground state of quantum many-body systems. We propose an algorithm to implement imaginary time propagation on a quantum computer.
  arXiv  Detail & Related papers  (2021-02-24T12:48:00Z)
• Quantum Hoare Type Theory [0.0]
  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.
  arXiv  Detail & Related papers  (2020-12-03T18:41:08Z)
• Compiling quantamorphisms for the IBM Q Experience [0.0]
  This paper contributes to extending the laws of classical program algebra to quantum programming. It aims at building correct-by-construction quantum circuits to be deployed on quantum devices such as those available at the IBM Q Experience.
  arXiv  Detail & Related papers  (2020-10-21T13:32:24Z)
• Quantum Gram-Schmidt Processes and Their Application to Efficient State Read-out for Quantum Algorithms [87.04438831673063]
  We present an efficient read-out protocol that yields the classical vector form of the generated state. Our protocol suits the case that the output state lies in the row space of the input matrix. One of our technical tools is an efficient quantum algorithm for performing the Gram-Schmidt orthonormal procedure.
  arXiv  Detail & Related papers  (2020-04-14T11:05:26Z)

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.