An Algebraic Language for Specifying Quantum Networks
summary
Defines BellKAT — a Kleene-algebra based language whose semantics live in a new algebra BellSKA and whose basic primitives are create/transmit/swap/weight/fail; expresses protocols as compositions of atomic guarded actions and models three-round executions that produce two end-to-end Bell pairs in the example. Proves normal forms and soundness/completeness for single-round semantics, proves soundness (but not completeness) for multi-round traces, and gives a decidability result for semantic equivalence under bounded qubit resources; provides a GitHub/artifact-backed prototype for verification and optimization.
AI-written summary · about
chapters (11)
- 0:00Quantum network protocols intro
- 1:53Quantum networks and Bell pairs
- 3:20Classical vs quantum execution
- 5:48Formal verification needs
- 6:30Bellat language design
- 7:13Bellat language basics
- 9:00Combining actions in Bellat
- 10:26Quantum network particularities
- 11:53Bellat formal results
- 13:16Summary and demo
- 13:38Q&A on axioms
related talks
14mA Language for Quantifying Quantum Network Behavior
16mqKleene: Verification of Quantum RAM Made Easy
18mFormalization of a Programming Language for Quantum Circuits with Measurement and Classical Control
22mIntroducing BRAT
14mDenotational semantics for stabiliser quantum programs
15mToward A Quantum Programming Language for Higher Level Formal Verification
21mQuantum and Classical Control (work-in-progress)
27mParameterized Verification of Quantum Circuits