A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL
From MaRDI portal
Publication:6190081
DOI10.1007/S10817-023-09689-9arXiv2306.12535OpenAlexW4389978614MaRDI QIDQ6190081
Publication date: 6 February 2024
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2306.12535
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A reversible theory of entanglement and its relation to the second law
- A generalization of quantum Stein's lemma
- From types to sets by local type definition in higher-order logic
- An automated deductive verification framework for circuit-building quantum programs
- Locales: a module system for mathematical theories
- Certified quantum computation in Isabelle/HOL
- Three-Player Entangled XOR Games are NP-Hard to Approximate
- Concrete Semantics
- Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types
- Bell Nonlocality
- Proposed Experiment to Test Local Hidden-Variable Theories
- Mathematics of Quantum Computing
- Can Quantum-Mechanical Description of Physical Reality Be Considered Complete?
- MIP* = RE
- Formal verification of quantum algorithms using quantum Hoare logic
This page was built for publication: A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL
