Towards Quantum Multiparty Session Types
summary
Proposes Quantum MPSTs that extend multiparty session types with linearity and quantum primitives, implements an operational semantics as a labeled transition system over a quantum register with probabilistic measurement transitions, and proves subject reduction, progress, session fidelity and a qubit ownership theorem ensuring each qubit reference is owned by one process (preventing no-cloning/no-deleting violations). The framework types and successfully verifies Quantum Teleportation and other protocols (secret sharing, bit commitment, QKD) but currently supports only classical channels and omits delegation.
AI-written summary · about
chapters (15)
- 0:00Quantum multiparty session types
- 1:45Session types guarantees
- 3:10Binary session types example
- 6:01Binary session types limits
- 7:04Quantum protocols adaptation
- 8:29Untyped Quantum calculi
- 8:49Quantum teleportation overview
- 10:38Global type teleportation
- 12:04Local types composition
- 13:05Term calculus Quantum
- 14:47Syntax typing Quantum
- 16:53Extensions to classical types
- 17:33Semantics Quantum systems
- 17:57Meta-theoretic results
- 19:21Conclusion future
related talks
18mFormalization of a Programming Language for Quantum Circuits with Measurement and Classical Control
21mQuantum and Classical Control (work-in-progress)
22mProbabilistic Refinement Session Types
22mQuantum Controlled Measurements via Program Transformation
18mQuantum Probabilistic Model Checking for Time-Bounded Properties
21mPolymorphic Typestate for Session Types
15mAssertion-Based Optimization of Quantum Programs
20mMessage-Observing Sessions