Exploring modal types for the Intel Quantum SDK (Extended Abstract)
summary
Defines a modal type system for the Intel Quantum SDK that enforces the SDK rule that every quantum kernel compiles to at most one quantum basic block, using three modes (compile-time, classical runtime, quantum runtime) to forbid compile-time-resolvable qubit indices from being indexed at runtime and to forbid classical gate parameters from depending on measurements in the same kernel. Provides a type-directed compilation to a runtime language that emits (pre-processing, qbb, post-processing) triples; implementation and soundness proofs remain work in progress.
AI-written summary · about
chapters (12)
- 0:00Modal types in Quantum SDK
- 1:09Quantum programming challenges
- 3:42Quantum circuits and models
- 5:25Intel SDK and hybrid algorithms
- 7:10Compile-time qubit constraints
- 8:14Classical parameters and measurements
- 10:26Modal types for enforcement
- 11:30Typing rules for Quantum ops
- 14:42Compilation to runtime language
- 17:38Type system correctness
- 18:22Trade-offs in Quantum programming
- 19:04Q&A on modal types
related talks
24mSemantics for Variational Quantum Programming
18mType-safe (Variational) Quantum Programming in Idris
15mToward A Quantum Programming Language for Higher Level Formal Verification
21mQuantum and Classical Control (work-in-progress)
40mQ# - going beyond quantum circuits
21mExtending Modern C++ for Heterogeneous Quantum-Classical Computing
17mToward a Type Theoretic Interpretation of Q# and Statically Enforcing the No Cloning Theorem
30mDependently Typed Quantum Programming in Proto-Quipper