On Circuit Description Languages, Indexed Monads, and Resource Analysis
summary
Presents a monad-based denotational semantics for Proto-Quipper variants that cleanly separates returned values from the circuits a term generates, using a closure types tweak plus an indexed (parameterized) monad / category-action monad to model circuit generation. Extends to resource analysis by replacing index monads with category-graded monads so effects encode width, depth and gate counts; shows soundness and adequacy and proves: if evaluation yields a value then some generated circuit E exists with size ≤ the effect annotation. Leaves combining grading with dependent types open.
AI-written summary · about
chapters (6)
- 0:00Circuit description languages
- 3:11Indexed monads in semantics
- 9:54Closure types and monads
- 14:54Resource analysis with effects
- 21:14Correctness and future work
- 23:29Q&A
related talks
19mFlexible Type-Based Resource Estimation in Quantum Circuit Description Languages
30mDependently Typed Quantum Programming in Proto-Quipper
26mCircuit Width Estimation via Effect Typing and Linear Dependency (Extended Abs...
20mProto-Quipper with Dynamic Lifting
01h 02mThe quantum monad: structuring quantum advantage
17mEncoding High-level Quantum Programs as SZX-diagrams
17mQGAT: A Generate-and-Test Paradigm for Quantum Circuits
20mGraphical Primitive Recursion For String Diagrams