Quantum weakest preconditions
From MaRDI portal
Publication:5482269
Abstract: We develop a notion of predicate transformer and, in particular, the weakest precondition, appropriate for quantum computation. We show that there is a Stone-type duality between the usual state-transformer semantics and the weakest precondition semantics. Rather than trying to reduce quantum computation to probabilistic programming we develop a notion that is directly taken from concepts used in quantum computation. The proof that weakest preconditions exist for completely positive maps follows immediately from the Kraus representation theorem. As an example we give the semantics of Selinger's language in terms of our weakest preconditions. We also cover some specific situations and exhibit an interesting link with stabilizers.
Recommendations
- Generalised quantum weakest preconditions
- Commutativity of quantum weakest preconditions
- Commutativity of quantum weakest liberal precondition and its properties
- Weakly intuitionistic quantum logic
- Weak sufficiency of quantum statistics
- Contextuality under weak assumptions
- Kochen-Specker theorem as a precondition for quantum computing
- scientific article; zbMATH DE number 764483
- Quantum lower bounds by quantum arguments
- Quantum lower bounds by quantum arguments
Cited in
(30)- Reachability analysis of quantum Markov decision processes
- Semantics for a quantum programming language by operator algebras
- Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs
- A proof system for disjoint parallel quantum programs
- Eigenlogic in the spirit of George Boole
- Commutativity of quantum weakest preconditions
- Termination of nondeterministic quantum programs
- Complete positivity and natural representation of quantum computations
- Distributed measurement-based quantum computation
- Dagger compact closed categories and completely positive maps (extended abstract)
- The expectation monad in quantum foundations
- \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq
- The monoidal structure of Turing machines
- Infinite-Dimensionality in Quantum Foundations: W*-algebras as Presheaves over Matrix Algebras
- A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls
- Natural Quantum Operational Semantics with Predicates
- Commutativity of quantum weakest liberal precondition and its properties
- Healthiness conditions for predicate transformers
- Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
- Quantum temporal logic and reachability problems of matrix semigroups
- Quantum Hoare type theory: extended abstract
- Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
- Toward automatic verification of quantum programs
- Checking continuous stochastic logic against quantum continuous-time Markov chains
- Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
- Programming with quantum communication
- Quantum relational Hoare logic with expectations
- Dijkstra and Hoare monads in monadic computation
- Quantum loop programs
- Generalised quantum weakest preconditions
This page was built for publication: Quantum weakest preconditions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5482269)
