Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages
summary
Introduces a type-and-effect system for Quipper that produces parametric upper bounds on circuit size (width, gate count, and wire-level depth) by combining refinement indices, abstract resource operators, and localized wire annotations; correctness is proved by logical predicates when a chosen resource metric interpretation (RMI) is coherent with a recursive circuit metric. Implementation (the QuRA tool) uses SMT solving to infer often-tight bounds automatically, handles QFT-level examples exactly, and requires some user annotations for local metrics; depth needs per-wire indices rather than global composition.
AI-written summary · about
chapters (9)
- 0:00Quantum resource estimation motivation
- 3:55Circuit families and limits
- 6:03Proto Quipper basics
- 7:30Extending Proto Quipper
- 10:44Handling local metrics
- 13:15Resource metric interpretations
- 15:03Kura tool results
- 16:51Future work challenges
- 17:14Conclusion
related talks
26mCircuit Width Estimation via Effect Typing and Linear Dependency (Extended Abs...
25mOn Circuit Description Languages, Indexed Monads, and Resource Analysis
30mDependently Typed Quantum Programming in Proto-Quipper
18mType-safe (Variational) Quantum Programming in Idris
27mParameterized Verification of Quantum Circuits
18mSAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum(…)
17mQGAT: A Generate-and-Test Paradigm for Quantum Circuits
17mEncoding High-level Quantum Programs as SZX-diagrams