Enriched Presheaf Model of Quantum FPC
summary
Extends Selinger’s superoperator model to higher-order programs by building modules over superoperators (equivalently enriched presheaves) and carving a classical linear-logic model via bi-orthogonality; morphisms reduce to simple matrix of completely positive maps. Model is ωCPO-enriched, interprets arbitrary recursive types, forbids impossible states (no state with true and false each having probability 2/3), and is fully abstract for Quantum FPC, inheriting definability properties from the first-order superoperator semantics.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:05Quantum systems and superoperators
- 3:57Limitations of CPM
- 6:08Entanglement challenges
- 8:00Linear algebra and logic
- 10:10Extending to probabilistic quantum
- 12:18Sigma monoids and enrichment
- 13:43Enriched presheaves in FPC
- 14:46Recursive types interpretation
- 15:28Comparison with Q Prime
- 16:10Q&A
related talks
49mSemantic Foundations for Probabilistic Programming
22mQuantum Coherence Spaces Revisited: A von Neumann (Co)Algebraic Approach
24mProgramming with Projective Cliffords
24mConcurrent Quantum Separation Logic for Fine-Grained Parallelism
01h 07mAn introduction to synthetic guarded domain theory with applications to probabilistic(…)
27mFunctorial Semantics for Partial Theories
18mQualifying System F-sub
14mOn Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs