Type-safe (Variational) Quantum Programming in Idris
summary
Qimaera implements variational quantum programming as Idris 2 libraries that use dependent types and linearity to guarantee at compile time that circuits respect wire counts and the no-cloning law via a linear IO monad R and qubit identifiers. It defines a parameterized unitary type, tensor/compose primitives, and a quantum state transformer for effects. It encodes QAOA and VQE as concrete, parameterized circuits and runs them with a simulator based on linear algebra (no hardware yet); the optimizer is a stub that returns random parameters. Qimaera library first type-safe QAOA and VQE implementations
AI-written summary · about
chapters (14)
- 0:00Introduction
- 2:04Dependent Types
- 3:22Linearity
- 4:23Unitary Gates in Qimaera
- 6:14Example: A Small Circuit
- 6:47Compose and Control Unitary Gates
- 7:12Example: The Quantum Fourier Transform
- 9:18Effectful Quantum Computation
- 9:38The Quantum State Transformer
- 10:30The QuantumOp Interface
- 11:55Quantum Approximation Optimization Algorithm
- 13:16Trial state
- 14:25QAOA: Classical Optimization
- 16:49Conclusion
related talks
30mDependently Typed Quantum Programming in Proto-Quipper
15mToward A Quantum Programming Language for Higher Level Formal Verification
40mQ# - going beyond quantum circuits
19mFlexible Type-Based Resource Estimation in Quantum Circuit Description Languages
23mExploring modal types for the Intel Quantum SDK (Extended Abstract)
24mSemantics for Variational Quantum Programming
17mQVM: Quantum Gate Virtualization Machine
29mA Verified Optimizer for Quantum Circuits