Proto-Quipper with Reversing and Control
summary
Formalizes reversible and controllable circuits with a dagger symmetric monoidal category R and a new controllable category N, adds a Proto-Quipper extension with reversing, control and a with-computed optimization that ensures controlling g; f; g† only controls f, and uses three modalities 0/1/2 to track non‑reversible, reversible but non‑controllable, and reversible+controllable code. Gives categorical semantics, proves operational/type soundness, builds a concrete model via generalized biset enrichment, and ships a prototype that typechecks examples like CCZ and QFT-based adders.
AI-written summary · about
chapters (6)
- 0:00Proto-Quipper intro
- 1:11Reverse and control ops
- 4:24Modality for safe reverse
- 8:44Typing rules for modalities
- 13:43Modality usage examples
- 15:31Q&A
related talks
24mA Computational Interpretation of Compact Closed Categories
20mTowards a Hierarchical Quantum Circuit Language
21mQuantum and Classical Control (work-in-progress)
22mSymmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible
30mContinuations and Coexponentials
45mA categorical view of computational effects
22mQuantum Controlled Measurements via Program Transformation
24mAddressable quantum gates