Quantum and Classical Control (work-in-progress)
summary
Language defines a typed calculus that stitches a quantum control fragment (pure quantum types interpreted as Hilbert spaces, formation rules ensuring normalized superpositions and a separate class of unitary types U(q1,q2)) into a simply‑typed linear lambda calculus for classical control, using quantum configurations to link a Hilbert‑space state with program terms. Denotational semantics map to von Neumann algebras (NMIU and NCPSU categories) with a strong monoidal functor B embedding isometries, and the team states small‑step and big‑step soundness plus adequacy as conjectured work‑in‑progress results.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:45Classical and quantum control
- 3:14Combining control paradigms
- 4:17Quantum subsystem and types
- 7:14Unitary construction via pattern matching
- 8:42Main calculus syntax
- 11:37Von Neumann algebras in semantics
- 13:28Categories for model
- 15:15Denotational interpretation of types
- 17:07Soundness and adequacy
- 17:51Future work and summary
- 18:59Q&A
related talks
22mAlgebraic and denotational semantics for Classically Controlled Quantum Communication
18mFormalization of a Programming Language for Quantum Circuits with Measurement and Classical Control
14mDenotational semantics for stabiliser quantum programs
24mSemantics for Variational Quantum Programming
22mA Semantics for Quantum Loops
28mA type-theoretic account of quantum computation (Extended Abstract)
30mQuantum Computing for Programming Languages Researchers
24mQunity: A Unified Language for Quantum and Classical Computing