{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T18:55:05Z","timestamp":1784314505486,"version":"3.55.0"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2023,12,19]],"date-time":"2023-12-19T00:00:00Z","timestamp":1702944000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,19]],"date-time":"2023-12-19T00:00:00Z","timestamp":1702944000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-22-PETQ-0007"],"award-info":[{"award-number":["ANR-22-PETQ-0007"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,3]]},"DOI":"10.1007\/s10817-023-09689-9","type":"journal-article","created":{"date-parts":[[2023,12,19]],"date-time":"2023-12-19T13:01:56Z","timestamp":1702990916000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Formalization of the CHSH Inequality and Tsirelson\u2019s Upper-bound in Isabelle\/HOL"],"prefix":"10.1007","volume":"68","author":[{"given":"Mnacho","family":"Echenim","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mehdi","family":"Mhalla","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,12,19]]},"reference":[{"key":"9689_CR1","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-1-4684-4550-3_8","volume-title":"Atomic Physics 8","author":"A Aspect","year":"1983","unstructured":"Aspect, A.: Experimental tests of Bell\u2019s inequalities in atomic physics. In: Lindgren, I., Ros\u00e9n, A., Svanberg, S. (eds.) Atomic Physics 8, pp. 103\u2013128. Springer, Boston (1983)"},{"issue":"2","key":"9689_CR2","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9689_CR3","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1103\/PhysicsPhysiqueFizika.1.195","volume":"1","author":"JS Bell","year":"1964","unstructured":"Bell, J.S.: On the Einstein Podolsky Rosen paradox. Physics 1(3), 195\u2013200 (1964)","journal-title":"Physics"},{"key":"9689_CR4","doi-asserted-by":"crossref","unstructured":"Berta, M., Brand\u00e3o, F.G., Gour, G., Lami, L., Plenio, M.B., Regula, B., Tomamichel, M.: On a gap in the proof of the generalised quantum Stein\u2019s lemma and its consequences for the reversibility of quantum resources. arXiv preprint arXiv:2205.02813 (2022)","DOI":"10.22331\/q-2023-09-07-1103"},{"key":"9689_CR5","doi-asserted-by":"publisher","first-page":"71","DOI":"10.4204\/EPTCS.195.6","volume":"195","author":"J Boender","year":"2015","unstructured":"Boender, J., Kamm\u00fcller, F., Nagarajan, R.: Formalization of quantum protocols using Coq. Electron. Proc. Theoret. Comput. Sci. 195, 71\u201383 (2015)","journal-title":"Electron. Proc. Theoret. Comput. Sci."},{"key":"9689_CR6","unstructured":"Bordg, A., Lachnitt, H., He, Y.: Isabelle marries Dirac: a library for quantum computation and quantum information. Archive of Formal Proofs (2020). https:\/\/isa-afp.org\/entries\/Isabelle_Marries_Dirac.html, Formal proof development"},{"issue":"5","key":"9689_CR7","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1007\/s10817-020-09584-7","volume":"65","author":"A Bordg","year":"2021","unstructured":"Bordg, A., Lachnitt, H., He, Y.: Certified quantum computation in Isabelle\/HOL. J. Autom. Reason. 65(5), 691\u2013709 (2021)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9689_CR8","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1080\/10586458.2022.2062073","volume":"31","author":"A Bordg","year":"2022","unstructured":"Bordg, A., Paulson, L.C., Li, W.: Simple type theory is not too simple: Grothendieck\u2019s schemes without dependent types. Exp. Math. 31(2), 364\u2013382 (2022)","journal-title":"Exp. Math."},{"issue":"7","key":"9689_CR9","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.115.070503","volume":"115","author":"FG Brandao","year":"2015","unstructured":"Brandao, F.G., Gour, G.: Reversible framework for quantum resource theories. Phys. Rev. Lett. 115(7), 070503 (2015)","journal-title":"Phys. Rev. Lett."},{"issue":"11","key":"9689_CR10","doi-asserted-by":"publisher","first-page":"873","DOI":"10.1038\/nphys1100","volume":"4","author":"FG Brandao","year":"2008","unstructured":"Brandao, F.G., Plenio, M.B.: Entanglement theory and the second law of thermodynamics. Nat. Phys. 4(11), 873\u2013877 (2008)","journal-title":"Nat. Phys."},{"key":"9689_CR11","doi-asserted-by":"publisher","first-page":"791","DOI":"10.1007\/s00220-010-1005-z","volume":"295","author":"FG Brandao","year":"2010","unstructured":"Brandao, F.G., Plenio, M.B.: A generalization of quantum Stein\u2019s lemma. Commun. Math. Phys. 295, 791\u2013828 (2010)","journal-title":"Commun. Math. Phys."},{"key":"9689_CR12","doi-asserted-by":"publisher","first-page":"829","DOI":"10.1007\/s00220-010-1003-1","volume":"295","author":"FG Brandao","year":"2010","unstructured":"Brandao, F.G., Plenio, M.B.: A reversible theory of entanglement and its relation to the second law. Commun. Math. Phys. 295, 829\u2013851 (2010)","journal-title":"Commun. Math. Phys."},{"key":"9689_CR13","doi-asserted-by":"crossref","unstructured":"Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An automated deductive verification framework for circuit-building quantum programs. In: Yoshida, N. (ed.) Programming Languages and Systems\u201430th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27\u2013April 1, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12648, pp. 148\u2013177. Springer, Luxembourg (2021)","DOI":"10.1007\/978-3-030-72019-3_6"},{"issue":"2","key":"9689_CR14","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/BF00417500","volume":"4","author":"BS Cirel\u2019son","year":"1980","unstructured":"Cirel\u2019son, B.S.: Quantum generalizations of Bell\u2019s inequality. Lett. Math. Phys. 4(2), 93\u2013100 (1980)","journal-title":"Lett. Math. Phys."},{"issue":"15","key":"9689_CR15","doi-asserted-by":"publisher","first-page":"880","DOI":"10.1103\/PhysRevLett.23.880","volume":"23","author":"JF Clauser","year":"1969","unstructured":"Clauser, J.F., Horne, M.A., Shimony, A., Holt, R.A.: Proposed experiment to test local hidden-variable theories. Phys. Rev. Lett. 23(15), 880\u2013884 (1969)","journal-title":"Phys. Rev. Lett."},{"key":"9689_CR16","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.101.012117","volume":"101","author":"BJ Dalton","year":"2020","unstructured":"Dalton, B.J., Garraway, B.M., Reid, M.D.: Tests for Einstein-Podolsky-Rosen steering in two-mode systems of identical massive bosons. Phys. Rev. A 101, 012117 (2020)","journal-title":"Phys. Rev. A"},{"key":"9689_CR17","volume-title":"Probability? Theory and Examples. The Wadsworth & Brooks\/Cole Statistics\/Probability Series","author":"R Durrett","year":"1991","unstructured":"Durrett, R.: Probability? Theory and Examples. The Wadsworth & Brooks\/Cole Statistics\/Probability Series. Wadsworth Inc. Duxbury Press, Belmont (1991)"},{"key":"9689_CR18","unstructured":"Echenim, M., Mhalla, M., Mori, C.: The CHSH inequality: Tsirelson\u2019s upper-bound and other results. Archive of Formal Proofs (2023). https:\/\/isa-afp.org\/entries\/TsirelsonBound.html, Formal proof development"},{"key":"9689_CR19","unstructured":"Echenim, M.: Quantum projective measurements and the CHSH inequality. Archive of Formal Proofs (2021). https:\/\/isa-afp.org\/entries\/Projective_Measurements.html, Formal proof development"},{"key":"9689_CR20","unstructured":"Echenim, M.: Simultaneous diagonalization of pairwise commuting Hermitian matrices. Archive of Formal Proofs (2022). https:\/\/isa-afp.org\/entries\/Commuting_Hermitian.html, Formal proof development"},{"issue":"10","key":"9689_CR21","doi-asserted-by":"publisher","first-page":"777","DOI":"10.1103\/PhysRev.47.777","volume":"47","author":"A Einstein","year":"1935","unstructured":"Einstein, A., Podolsky, B., Rosen, N.: Can quantum-mechanical description of physical reality be considered complete? Phys. Rev. 47(10), 777\u2013780 (1935). https:\/\/doi.org\/10.1103\/PhysRev.47.777","journal-title":"Phys. Rev."},{"issue":"1","key":"9689_CR22","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1017\/S0013091500028145","volume":"26","author":"PA Fuhrmann","year":"1983","unstructured":"Fuhrmann, P.A.: Linear systems and operators in Hilbert space. Proc. Edinb. Math. Soc. 26(1), 113\u2013114 (1983). https:\/\/doi.org\/10.1017\/S0013091500028145","journal-title":"Proc. Edinb. Math. Soc."},{"issue":"2","key":"9689_CR23","first-page":"197","volume":"54","author":"IM Gelfand","year":"1943","unstructured":"Gelfand, I.M., Naimark, M.A.: On the imbedding of normed rings into the ring of operators in Hilbert space. Matematiceskij sbornik 54(2), 197\u2013217 (1943)","journal-title":"Matematiceskij sbornik"},{"issue":"7575","key":"9689_CR24","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1038\/nature15759","volume":"526","author":"B Hensen","year":"2015","unstructured":"Hensen, B., Bernien, H., Dr\u00e9au, A.E., Reiserer, A., Kalb, N., Blok, M.S., Ruitenberg, J., Vermeulen, R.F., Schouten, R.N., Abell\u00e1n, C.: Loophole-free Bell inequality violation using electron spins separated by 1.3 kilometres. Nature 526(7575), 682\u2013686 (2015)","journal-title":"Nature"},{"key":"9689_CR25","unstructured":"H\u00f6lzl, J.: Construction and stochastic applications of measure spaces in higher-order logic. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2012)"},{"issue":"11","key":"9689_CR26","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/3485628","volume":"64","author":"Z Ji","year":"2021","unstructured":"Ji, Z., Natarajan, A., Vidick, T., Wright, J., Yuen, H.: MIP*= RE. Commun. ACM 64(11), 131\u2013138 (2021)","journal-title":"Commun. ACM"},{"key":"9689_CR27","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2019.101572","volume":"87","author":"F Kamm\u00fcller","year":"2019","unstructured":"Kamm\u00fcller, F.: Attack trees in Isabelle extended with probabilities for quantum cryptography. Comput. Secur. 87, 101572 (2019)","journal-title":"Comput. Secur."},{"key":"9689_CR28","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales: a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) Theorem Proving in Higher Order Logics, pp. 149\u2013165. Springer, Berlin (1999)"},{"issue":"2","key":"9689_CR29","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s10817-018-9464-6","volume":"62","author":"O Kuncar","year":"2019","unstructured":"Kuncar, O., Popescu, A.: From types to sets by local type definition in higher-order logic. J. Autom. Reason. 62(2), 237\u2013260 (2019)","journal-title":"J. Autom. Reason."},{"key":"9689_CR30","unstructured":"Liu, J., Zhan, B., Wang, S., Ying, S., Liu, T., Li, Y., Ying, M., Zhan, N.: Quantum Hoare logic. Archive of Formal Proofs (2019). https:\/\/isa-afp.org\/entries\/QHLProver.html, Formal proof development"},{"key":"9689_CR31","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-030-25543-5_12","volume-title":"Computer Aided Verification","author":"J Liu","year":"2019","unstructured":"Liu, J., Zhan, B., Wang, S., Ying, S., Liu, T., Li, Y., Ying, M., Zhan, N.: Formal verification of quantum algorithms using Quantum Hoare Logic. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification, pp. 187\u2013207. Springer, New York (2019)"},{"key":"9689_CR32","doi-asserted-by":"publisher","first-page":"803","DOI":"10.1103\/RevModPhys.65.803","volume":"65","author":"ND Mermin","year":"1993","unstructured":"Mermin, N.D.: Hidden variables and the two theorems of John Bell. Rev. Mod. Phys. 65, 803\u2013815 (1993)","journal-title":"Rev. Mod. Phys."},{"key":"9689_CR33","volume-title":"Quantum Computation and Quantum Information: 10th Anniversary Edition","author":"MA Nielsen","year":"2011","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition, 10th edn. Cambridge University Press, Cambridge (2011)","edition":"10"},{"key":"9689_CR34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics: With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle\/HOL. Springer, New York (2014)"},{"key":"9689_CR35","doi-asserted-by":"publisher","first-page":"119","DOI":"10.4204\/EPTCS.266.8","volume":"266","author":"R Rand","year":"2018","unstructured":"Rand, R., Paykin, J., Zdancewic, S.: Qwire practice: formal verification of quantum circuits in Coq. Electron. Proc. Theoret. Comput. Sci. 266, 119\u2013132 (2018). https:\/\/doi.org\/10.4204\/EPTCS.266.8","journal-title":"Electron. Proc. Theoret. Comput. Sci."},{"key":"9689_CR36","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.70.052113","volume":"70","author":"MQ Ruan","year":"2004","unstructured":"Ruan, M.Q., Zeng, J.Y.: Complete sets of commuting observables of Greenberger-Horne-Zeilinger states. Phys. Rev. A 70, 052113 (2004). https:\/\/doi.org\/10.1103\/PhysRevA.70.052113","journal-title":"Phys. Rev. A"},{"key":"9689_CR37","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198788416.001.0001","volume-title":"Bell Nonlocality","author":"V Scarani","year":"2019","unstructured":"Scarani, V.: Bell Nonlocality. Oxford Graduate Texts. Oxford University Press, Oxford (2019)"},{"key":"9689_CR38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-12358-1","volume-title":"Mathematics of Quantum Computing: An Introduction","author":"W Scherer","year":"2019","unstructured":"Scherer, W.: Mathematics of Quantum Computing: An Introduction. Springer, Switzerland (2019). https:\/\/doi.org\/10.1007\/978-3-030-12358-1"},{"key":"9689_CR39","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1038\/s41586-023-05885-0","volume":"617","author":"S Storz","year":"2023","unstructured":"Storz, S., Sch\u00e4r, J., Kulikov, A., Magnard, P., Kurpiers, P., L\u00fctolf, J., Walter, T., Copetudo, A., Reuer, K., Akin, A.: Loophole-free Bell inequality violation with superconducting circuits. Nature 617, 265\u2013270 (2023)","journal-title":"Nature"},{"key":"9689_CR40","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle\/HOL. In: Avigad, J., Chlipala, A. (eds.) Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20\u201322, 2016, pp. 88\u201399. ACM, USA (2016)","DOI":"10.1145\/2854065.2854073"},{"key":"9689_CR41","unstructured":"Thiemann, R., Yamada, A.: Matrices, Jordan normal forms, and spectral radius theory. Archive of Formal Proofs (2015). https:\/\/isa-afp.org\/entries\/Jordan_Normal_Form.html, Formal proof development"},{"key":"9689_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3290346","volume":"3","author":"D Unruh","year":"2019","unstructured":"Unruh, D.: Quantum relational Hoare logic. Proc. ACM Programm. Lang. 3, 1\u201331 (2019). https:\/\/doi.org\/10.1145\/3290346","journal-title":"Proc. ACM Programm. Lang."},{"issue":"3","key":"9689_CR43","doi-asserted-by":"publisher","first-page":"1007","DOI":"10.1137\/140956622","volume":"45","author":"T Vidick","year":"2016","unstructured":"Vidick, T.: Three-player entangled XOR games are NP-hard to approximate. SIAM J. Comput. 45(3), 1007\u20131063 (2016)","journal-title":"SIAM J. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09689-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09689-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09689-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,18]],"date-time":"2024-03-18T13:13:19Z","timestamp":1710767599000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09689-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,19]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3]]}},"alternative-id":["9689"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09689-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,12,19]]},"assertion":[{"value":"21 June 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 November 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 December 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"2"}}