A logical analysis of entanglement and separability in quantum higher-order functions
arXiv:0801.0649 · doi:10.1007/978-3-642-03745-0_25
Abstract
We present a logical separability analysis for a functional quantum computation language. This logic is inspired by previous works on logical analysis of aliasing for imperative functional programs. Both analyses share similarities notably because they are highly non-compositional. Quantum setting is harder to deal with since it introduces non determinism and thus considerably modifies semantics and validity of logical assertions. This logic is the first proposal of entanglement/separability analysis dealing with a functional quantum programming language with higher-order functions.
19 pages
References in corpus (6)
- Efficient classical simulation of slightly entangled quantum computations
- A Lambda Calculus for Quantum Computation
- A functional quantum programming language
- Quantum entanglement analysis based on abstract interpretation
- A lambda calculus for quantum computation with classical control
- A logical analysis of entanglement and separability in quantum higher-order functions
Cited by in corpus (7)
- ScaffCC: Scalable Compilation and Analysis of Quantum Programs
- Quantum entanglement analysis based on abstract interpretation
- Lineal: A linear-algebraic Lambda-calculus
- Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
- A logical analysis of entanglement and separability in quantum higher-order functions
- Analysis of Quantum Entanglement in Quantum Programs using Stabilizer Formalism
- Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs