Toward Certified Quantum Programming
summary
A core language called Cubics encodes circuits with a denotational path-sum semantics and lifted constructors whose specifications compose isomorphically with the algebraic circuit constructors. The work embeds the framework in Why3/SMT (Alt-Ergo) and produces a certified phase-estimation implementation: 237 lines (specs included), generating 190 proof obligations, of which 24 fail automatic discharge and require 163 manual proof commands. A flat/diagonal fragment yields simpler semantics and measurable automation gains.
AI-written summary · about
chapters (10)
- 0:00Intro
- 7:53Quantum Circuits
- 8:47Passive Semantics
- 10:15Lifted constructors
- 11:05Building a Quantum Circuit
- 11:59Mapping isomorphism
- 12:22Automation
- 13:54Implementation
- 15:45Conclusion
- 16:50Questions
related talks
40mDemocratizing quantum formal verification: the path-sum way
15mToward A Quantum Programming Language for Higher Level Formal Verification
22mProgramming Abstractions for Quantum Linear Algebra
27mQuantum Circuits Are Just a Phase
29mEfficiently Verifying Quantum Programs with Few T Gates
21mCobble: Compiling Block Encodings for Quantum Computational Linear Algebra
22mCoqQ: Foundational Verification of Quantum Programs
23mA feasible and unitary programming language with quantum control