Verified Compilation of Quantum Oracles
summary
Verified compilation proves an imperative oracle language OQIMP compiles to OQASM and then to SQIR via Coq, preserving semantics and keeping simulation cost O(n) instead of O(2^n). The toolchain uses QuickChick for 10,000 randomized tests, finds subtle QFT bugs, and yields concrete resource wins: QFT-based oracles use far fewer qubits and the sine oracle uses 94 fewer gates while partial evaluation cuts an x*y/n subroutine by ~95% of gates compared to prior implementations.
AI-written summary · about
chapters (21)
- 0:00Intro
- 1:45How? Qubits Allow Superposition
- 3:08Operators on Qubits
- 3:33Quantum Algorithms (Shor's)
- 4:21Quantum Programming is Hard!
- 6:23Verified Quantum Computing
- 8:26Quantum Oracles
- 8:51Shor's Oracle: Modular Exp
- 9:26Grover's Oracle: Predicate Fun
- 9:54Verification and Testing
- 12:13QVM: High-assurance Stack
- 15:23Rest of Talk
- 16:58OQASM Syntax
- 19:03Quantum Fourier Transform
- 20:38OQASM Type System
- 22:13QFT Adder Example
- 23:50OQASM Metatheory
- 26:02Sine Function
- 26:48Evaluation: OQASM arithmetic
- 28:41Evaluation: OQIMP
- 29:50Summary: Contributions
related talks
29mA Verified Optimizer for Quantum Circuits
24mA Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages
22mCoqQ: Foundational Verification of Quantum Programs
15mToward A Quantum Programming Language for Higher Level Formal Verification
22mEfficient Formal Verification of Quantum Error Correcting Programs
18mSAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum(…)
17mQGAT: A Generate-and-Test Paradigm for Quantum Circuits
01h 31mLightning Talks