01921nas a2200205 4500008004100000245009400041210006900135260001500204520125300219653004301472653002701515653003401542653003101576100001301607700001701620700001201637700001401649700001501663856003701678 2022 eng d00aQuantum Natural Proof: A New Perspective of Hybrid Quantum-Classical Program Verification0 aQuantum Natural Proof A New Perspective of Hybrid QuantumClassic c11/11/20223 a

Many quantum programs are assured by formal verification, but such verification is usually laborious and time-consuming. This paper proposes quantum natural proof (QNP), an automated proof system for verifying hybrid quantum-classical algorithms. Natural proofs are a subclass of proofs that are amenable to completely automated reasoning, provide sound but incomplete procedures, and capture common reasoning tactics in program verification. The core of QNP is a type-guided quantum proof system, named Qafny, which views quantum operations as some classical array operations that can be modeled as proof rules in a classical separation logic framework, suitable for automated reasoning. We proved the soundness and completeness of the Qafny proof system as well as the soundness of the proof system compilation from Qafny to Dafny. By using the QNP implementation in Dafny, automated verification can be efficiently perform for many hybrid quantum-classical algorithms, including GHZ, Shor's, Grover's, and quantum walk algorithms, which saves a great amount of human efforts. In addition, quantum programs written in Qafny can be compiled to quantum circuits so that every verified quantum program can be run on a quantum machine.

10aFOS: Computer and information sciences10aFOS: Physical sciences10aProgramming Languages (cs.PL)10aQuantum Physics (quant-ph)1 aLi, Liyi1 aZhu, Mingwei1 aLee, Yi1 aChang, Le1 aWu, Xiaodi uhttps://arxiv.org/abs/2211.0641101906nas a2200205 4500008004100000245008600041210006900127260001400196520121200210653004301422653002701465653003801492653003401530653003101564100001901595700001301614700001701627700001901644856003701663 2022 eng d00aQunity: A Unified Language for Quantum and Classical Computing (Extended Version)0 aQunity A Unified Language for Quantum and Classical Computing Ex c4/26/20223 a

We introduce Qunity, a new quantum programming language designed to treat quantum computing as a natural generalization of classical computing. Qunity presents a unified syntax where familiar programming constructs can have both quantum and classical effects. For example, one can use sum types to implement the direct sum of linear operators, exception-handling syntax to implement projective measurements, and aliasing to induce entanglement. Further, Qunity takes advantage of the overlooked BQP subroutine theorem, allowing one to construct reversible subroutines from irreversible quantum algorithms through the uncomputation of "garbage" outputs. Unlike existing languages that enable quantum aspects with separate add-ons (like a classical language with quantum gates bolted on), Qunity provides a unified syntax and a novel denotational semantics that guarantees that programs are quantum mechanically valid. We present Qunity's syntax, type system, and denotational semantics, showing how it can cleanly express several quantum algorithms. We also detail how Qunity can be compiled into a low-level qubit circuit language like OpenQASM, proving the realizability of our design.

10aFOS: Computer and information sciences10aFOS: Physical sciences10aLogic in Computer Science (cs.LO)10aProgramming Languages (cs.PL)10aQuantum Physics (quant-ph)1 aVoichick, Finn1 aLi, Liyi1 aRand, Robert1 aHicks, Michael uhttps://arxiv.org/abs/2204.1238401360nas a2200229 4500008004100000020002200041022001400063245003700077210003700114260001200151300001700163490000800180520076100188100001900949700001700968700001900985700001301004700001901017700001701036700002101053856005601074 2021 eng d a978-3-95977-188-7 a1868-896900aProving Quantum Programs Correct0 aProving Quantum Programs Correct c06/2021 a21:1–21:190 v1933 a

As quantum computing progresses steadily from theory into practice, programmers will face
a common problem: How can they be sure that their code does what they intend it to do? This
paper presents encouraging results in the application of mechanized proof to the domain of quantum
programming in the context of the sqir development. It verifies the correctness of a range of a
quantum algorithms including Grover’s algorithm and quantum phase estimation, a key component
of Shor’s algorithm. In doing so, it aims to highlight both the successes and challenges of formal
verification in the quantum context and motivate the theorem proving community to target quantum
computing as an application domain.

1 aHietala, Kesha1 aRand, Robert1 aHung, Shih-Han1 aLi, Liyi1 aHicks, Michael1 aCohen, Liron1 aKaliszyk, Cezary uhttps://drops.dagstuhl.de/opus/volltexte/2021/13916