Proto-Quipper with Dynamic Lifting
summary
Extends Proto-Quipper-M with dynamic lifting to let measurement bits become compile-time parameters, implements a new language Proto-Quipper-Dyn, and gives a modality system (values 0/1) that forbids boxing when lifting is used. Provides an operational semantics for the two runtimes (deterministic circuit generation, probabilistic execution), an enriched-categorical semantics, and machine-checked soundness proofs; demo shows Bell-pair measurement lifted to Booleans and executed successfully.
AI-written summary · about
chapters (8)
- 0:00Proto-Quipper with Dynamic Lifting
- 1:28Two runtimes in compilation
- 3:36Dynamic Lifting in quantum programming
- 6:29Categorical model for lifting
- 8:13Type system with lifting modality
- 10:00Demo: Boxing in Proto-Quipper
- 15:45Demo: Dynamic Lifting
- 17:11Summary and Q&A
related talks
30mDependently Typed Quantum Programming in Proto-Quipper
25mOn Circuit Description Languages, Indexed Monads, and Resource Analysis
19mFlexible Type-Based Resource Estimation in Quantum Circuit Description Languages
17mEncoding High-level Quantum Programs as SZX-diagrams
15mToward A Quantum Programming Language for Higher Level Formal Verification
17mToward a Type Theoretic Interpretation of Q# and Statically Enforcing the No Cloning Theorem
21mQurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
26mQudit Quantum Programming with Projective Cliffords