Circuit Width Estimation via Effect Typing and Linear Dependency (Extended Abs...
summary
Proto-Quipper-R implements a linear dependent type-and-effect system that produces parametric upper bounds on circuit width (indices are arithmetic expressions over input sizes), tracks captured wires by giving functions two indices (produced width and closure wire count), and proves type safety plus soundness against a big‑step circuit-building semantics. The system models recycling via the let/max composition of effects, supports limited recursion, has a prototype implementation underway, and successfully types the QFT family with an exact bound while planning extensions to gate count and depth analysis.
AI-written summary · about
chapters (8)
- 0:00Quantum circuit languages intro
- 3:04Resource estimation motivation
- 7:38Width estimation challenges
- 10:31Effect typing type system
- 14:38Typing rules for circuits
- 16:49Well-typed semantics
- 18:59Future work plans
- 19:20Q&A
related talks
19mFlexible Type-Based Resource Estimation in Quantum Circuit Description Languages
25mOn Circuit Description Languages, Indexed Monads, and Resource Analysis
30mDependently Typed Quantum Programming in Proto-Quipper
19mPanel: Compilation Frameworks
17mThe Bounded Pathwidth of Control-Flow Graphs
20mProto-Quipper with Dynamic Lifting
27mParameterized Verification of Quantum Circuits
17mEncoding High-level Quantum Programs as SZX-diagrams