Quantum and classical registers
summary
Defines a register as a linear map that lifts any operator on a register Hilbert space to an operator on the whole memory, and requires it to be linear, multiplicative and preserves adjoints, avoiding index arithmetic and swap plumbing. Builds a register category, instantiates it for quantum and classical cases, formalizes the finite‑dimensional theory in Isabelle/HOL, and uses it to specify and verify quantum teleportation with a tiny language and logic; approach scales to infinite dimensions with extra care.
AI-written summary · about
chapters (7)
- 0:00Overview
- 0:29A tiny quantum program
- 4:35More "easy" things
- 8:03Semantics of quantum registers?
- 10:50What is a quantum register?
- 12:59Properties of registers
- 15:32Teleporting Isabelle
related talks
20mQuantum Register Machine: Efficient Implementation of Quantum Recursive Programs
23mA Unified Assertion-Based Framework for Classical-Quantum Program Verification
35mQuantum relational Hoare logic, towards a formalization
22mA Semantics for Quantum Loops
28mA type-theoretic account of quantum computation (Extended Abstract)
18mFormalization of a Programming Language for Quantum Circuits with Measurement and Classical Control
27mQuantum Circuits Are Just a Phase
30mQuantum Computing for Programming Languages Researchers