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)- \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq
- Healthiness conditions for predicate transformers
- A proof system for disjoint parallel quantum programs
- Natural Quantum Operational Semantics with Predicates
- Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
- Distributed measurement-based quantum computation
- The monoidal structure of Turing machines
- Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs
- Reachability analysis of quantum Markov decision processes
- A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls
- Commutativity of quantum weakest preconditions
- Generalised quantum weakest preconditions
- Programming with quantum communication
- Termination of nondeterministic quantum programs
- Complete positivity and natural representation of quantum computations
- Commutativity of quantum weakest liberal precondition and its properties
- The expectation monad in quantum foundations
- Infinite-Dimensionality in Quantum Foundations: W*-algebras as Presheaves over Matrix Algebras
- Dijkstra and Hoare monads in monadic computation
- Quantum temporal logic and reachability problems of matrix semigroups
- Quantum relational Hoare logic with expectations
- Semantics for a quantum programming language by operator algebras
- Checking continuous stochastic logic against quantum continuous-time Markov chains
- Dagger compact closed categories and completely positive maps (extended abstract)
- Quantum Hoare type theory: extended abstract
- Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
- Eigenlogic in the spirit of George Boole
- Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
- Toward automatic verification of quantum programs
- Quantum loop programs
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)
