Q*: Implementing Quantum Separation Logic in F*
summary
Prototype implements quantum separation logic inside F using the Steel library and Z3 for automation, ports Quantum Lib, and adds four quantum actions: allocate, discard, measure, apply. Tensor is handled by a commutative workaround that keeps qubit order. A machine-checked proof shows teleportation preserves an arbitrary entangled context; proof needs one nontrivial manual lemma and a few admitted facts. Code and separation-logic branch are available, and basic properties like discard-safety and no-cloning are already encoded.
AI-written summary · about
chapters (7)
- 0:00Intro
- 0:31Background: Separation Logic
- 1:39Quantum Separation Logic?
- 6:39Example: Quantum Teleportation
- 9:46Prototype Implementation
- 11:18Additional Applications
- 12:22Future Directions
related talks
18mConcurrent Quantum Separation Logic for Fine-Grained Parallelism
20mA Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantu
42mQuantum program analysis: Verification and Testing
15mToward A Quantum Programming Language for Higher Level Formal Verification
39mHigh-fidelity and Fault-tolerant Teleportation of a Logical Qubit on a Trapped-ion Quantum Computer
22mCoqQ: Foundational Verification of Quantum Programs
31mDemonstrating an Unconditional Separation Between Quantum and Classical Information Resources
01h 01mInvited Talk: Welcome to Quantum 3.0!