Semantics for Variational Quantum Programming
summary
A type-safe language combines a higher-order probabilistic classical core (PFPC) with a first-order linear quantum core and a new first-order quantum-function type Q(A,B), plus primitives for state preparation and measurement. Denotational semantics uses a commutative probabilistic monad on DCPO for the classical side and models quantum effects in von Neumann algebras enriched over domains, and proves the crucial barycenter map exists so the mixed semantics is sound and computationally adequate.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:18Motivation
- 1:42Overview
- 2:58Classical Subsystem
- 5:37Quantum Subsystem
- 9:12New Additions
- 14:57Categorical Model
- 15:22Quantum Model
- 15:59Quantum Semantics
- 16:40Lambda Semantics
- 17:26Quantum Function Application
- 19:25Kegelspitzen
- 21:12Conclusion
related talks
14mDenotational semantics for stabiliser quantum programs
15mToward A Quantum Programming Language for Higher Level Formal Verification
30mQuantum Computing for Programming Languages Researchers
21mQuantum and Classical Control (work-in-progress)
22mA Semantics for Quantum Loops
22mLocal Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
13mQbC: Quantum Correctness by Construction
18mFormalization of a Programming Language for Quantum Circuits with Measurement and Classical Control