Algebraic and denotational semantics for Classically Controlled Quantum Communication
summary
Claims a parameterised algebraic theory for classically controlled quantum I/O and gives two sound models: a quantum stream operational semantics (streams as in/out state machines that record IO traces) and a monadic denotational semantics. Shows the denotation is adequate and fully abstract for the operational behavior, characterises denotations as a weighted sum over traces, and models them as the free IO monad on CP maps (DCPO-completed). Works only for finite programs (no loops); proofs and constructions are explicit.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:08Motivation and applications
- 2:14Algebraic theories for quantum computing
- 3:59Classical branching in quantum semantics
- 7:53Operational semantics derivation
- 10:21Extending to classically controlled quantum
- 12:07Operational semantics with streams
- 14:11Program equivalence via traces
- 16:00Denotational semantics construction
- 18:49Full abstraction and future work
- 20:22Q&A
related talks
21mQuantum and Classical Control (work-in-progress)
18mFormalization of a Programming Language for Quantum Circuits with Measurement and Classical Control
22mQuantum Controlled Measurements via Program Transformation
15mStable Relations and Abstract Interpretation of Higher-Order Programs
14mAdequacy for Algebraic Effects Revisited
22mQuantum Coherence Spaces Revisited: A von Neumann (Co)Algebraic Approach
12mA Unified View of Modalities in Type Systems
49mSemantic Foundations for Probabilistic Programming