Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control
summary
Formalizes a circuit description language that records measurement-dependent control as a branching tree of channels rather than flat gate lists, introduces a quantum channel algebra QC-arc, and extends quantum lambda calculus with boxing/unboxing and channel constants. Gives two operational semantics (circuit-buffering and QM-based) where measurement yields probabilistic reductions, enforces linear typing to ensure single-use of wires, and proves safety theorems for both semantics. Examples show dynamic lifting can produce multiple circuit branches with no single linear circuit representation.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:10Outline
- 0:33Model
- 1:20Motivation
- 3:07Circuit Description Languages
- 4:25Dynamic Lifting
- 5:40Summary
- 7:06Work
- 10:07Syntax
- 11:34Operational Semantics
- 13:07Measurement
- 13:42More complicated examples
- 14:38Conclusion
- 15:26Questions
related talks
22mQuantum Controlled Measurements via Program Transformation
21mQuantum and Classical Control (work-in-progress)
22mAlgebraic and denotational semantics for Classically Controlled Quantum Communication
15mToward A Quantum Programming Language for Higher Level Formal Verification
20mTowards a Hierarchical Quantum Circuit Language
22mA Semantics for Quantum Loops
23mA Unified Assertion-Based Framework for Classical-Quantum Program Verification
19mThe Quantum Abstract Machine