Quantum Information Effects
summary
A type-and-effect system (languages: yuppie, yuppie-a, yuppie-chi-a) models two quantum information effects — allocation and hiding — and proves the system is fully expressive for irreversible quantum computing including measurement and decoherence. Categorical constructions start from any rig groupoid and semantically transform unitaries → CPTP maps and bijections → functions with chosen garbage, recovering Toffoli and Stinespring results; the language is approximately universal for unitaries and artifacts are available.
AI-written summary · about
chapters (10)
- 0:00Start
- 0:16Cost of Computation
- 1:28Information Cost
- 2:39Classical Reversible Computation and Information Effects
- 3:02Information Effects
- 4:24Quantum Pure State Formalism
- 4:43Mixed States
- 4:57Probabilistic Mixed States
- 6:40Quantum Information Costs
- 17:48Conclusion
related talks
20mEffect Semantics for Quantum Protocols
28mA type-theoretic account of quantum computation (Extended Abstract)
21mInteractive Proofs for Synthesizing Quantum States and Unitaries
23mA feasible and unitary programming language with quantum control
22mQbC: Quantum Correctness by Construction
25mTower: Data Structures in Quantum Superposition
27mQuantum Circuits Are Just a Phase
30mQuantum Computing for Programming Languages Researchers