@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
}

{"_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}