Proto-Quipper with Reversing and Control

Explore a conference talk from PLanQC 2025 that presents a formal semantics for reversible and controllable quantum circuits in the Proto-Quipper language. Learn how researchers Peng Fu, Kohei Kishida, Neil Julien Ross, and Peter Selinger extend Proto-Quipper with reversing, control, and the with-computed operation, which enables efficient implementation of circuits in the form g;f;g†. Discover how they use a dagger symmetric monoidal category to interpret reversible circuits and introduce a new "controllable category" concept to handle controllable circuits. The presentation explains how their type system with modalities tracks reversibility and controllability, provides an abstract categorical semantics for these operations, and demonstrates soundness with respect to this semantics. The talk concludes with a concrete model using a generalization of biset enrichment, advancing the theoretical foundations of quantum programming languages.