Quantum projective measurements and the CHSH inequality in Isabelle/HOL. Echenim, M. & Mhalla, M. March, 2021. abstract bibtex We present a formalization in Isabelle/HOL of quantum projective measurements, a class of measurements involving orthogonal projectors that is frequently used in quantum computing. We also formalize the CHSH inequality, a result that holds on arbitrary probability spaces, which can used to disprove the existence of a local hidden-variable theory for quantum mechanics.
@misc{Echenim2021,
title = {Quantum projective measurements and the {CHSH} inequality in Isabelle/HOL},
author = {Echenim, Mnacho and Mhalla, Mehdi},
year = {2021},
month = mar,
archiveprefix = {arXiv},
eprint = {2103.08535},
abstract = {We present a formalization in Isabelle/HOL of quantum projective measurements, a class of measurements involving orthogonal projectors that is frequently used in quantum computing. We also formalize the CHSH inequality, a result that holds on arbitrary probability spaces, which can used to disprove the existence of a local hidden-variable theory for quantum mechanics.},
webnote = {See also: Isabelle AFP entry \cite{Echenim2021a}},
bibsource = qplbib
}
Downloads: 0
{"_id":"quBjQJ6jhzsgf38qD","bibbaseid":"echenim-mhalla-quantumprojectivemeasurementsandthechshinequalityinisabellehol-2021","author_short":["Echenim, M.","Mhalla, M."],"bibdata":{"bibtype":"misc","type":"misc","title":"Quantum projective measurements and the CHSH inequality in Isabelle/HOL","author":[{"propositions":[],"lastnames":["Echenim"],"firstnames":["Mnacho"],"suffixes":[]},{"propositions":[],"lastnames":["Mhalla"],"firstnames":["Mehdi"],"suffixes":[]}],"year":"2021","month":"March","archiveprefix":"arXiv","eprint":"2103.08535","abstract":"We present a formalization in Isabelle/HOL of quantum projective measurements, a class of measurements involving orthogonal projectors that is frequently used in quantum computing. We also formalize the CHSH inequality, a result that holds on arbitrary probability spaces, which can used to disprove the existence of a local hidden-variable theory for quantum mechanics.","webnote":"See also: Isabelle AFP entry i̧teEchenim2021a","bibsource":"Quantum Programming Languages & Verification Bibliography, https://git.io/qpl-bib","bibtex":"@misc{Echenim2021,\n title = {Quantum projective measurements and the {CHSH} inequality in Isabelle/HOL},\n author = {Echenim, Mnacho and Mhalla, Mehdi},\n year = {2021},\n month = mar,\n archiveprefix = {arXiv},\n eprint = {2103.08535},\n abstract = {We present a formalization in Isabelle/HOL of quantum projective measurements, a class of measurements involving orthogonal projectors that is frequently used in quantum computing. We also formalize the CHSH inequality, a result that holds on arbitrary probability spaces, which can used to disprove the existence of a local hidden-variable theory for quantum mechanics.},\n webnote = {See also: Isabelle AFP entry \\cite{Echenim2021a}},\n bibsource = qplbib\n}\n\n","author_short":["Echenim, M.","Mhalla, M."],"key":"Echenim2021","id":"Echenim2021","bibbaseid":"echenim-mhalla-quantumprojectivemeasurementsandthechshinequalityinisabellehol-2021","role":"author","urls":{},"metadata":{"authorlinks":{}}},"bibtype":"misc","biburl":"https://raw.githubusercontent.com/QuantumPL/bib/main/bbt.bib","dataSources":["JG9W34HAXfSxsC6ML"],"keywords":[],"search_terms":["quantum","projective","measurements","chsh","inequality","isabelle","hol","echenim","mhalla"],"title":"Quantum projective measurements and the CHSH inequality in Isabelle/HOL","year":2021}