pith. sign in

arxiv: 1904.06319 · v4 · pith:UNQLXVUTnew · submitted 2019-04-12 · 💻 cs.LO · cs.ET· cs.PL· quant-ph

Verified Optimization in a Quantum Intermediate Representation

Kesha Hietala , Robert Rand , Shih-Han Hung , Xiaodi Wu , Michael Hicks This is my paper
classification 💻 cs.LO cs.ETcs.PLquant-ph
keywords quantumsqireverificationdemonstrateintermediateprogramsrepresentationallowing
0
0 comments X
read the original abstract

We present sqire, a low-level language for quantum computing and verification. sqire uses a global register of quantum bits, allowing easy compilation to and from existing `quantum assembly' languages and simplifying the verification process. We demonstrate the power of sqire as an intermediate representation of quantum programs by verifying a number of useful optimizations, and we demonstrate sqire's use as a tool for general verification by proving several quantum programs correct.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs (Technical Report)

    cs.LO 2024-11 unverdicted novelty 6.0

    AutoQ 2.0 verifies quantum programs with classical control flow and successfully checks RUS algorithms instantly plus weak-measurement Grover search on 100 qubits in about 20 minutes.