A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL

Mnacho Echenim, Mehdi Mhalla. A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL. Journal of Automated Reasoning, 68(1):2, March 2024. [doi]

Authors

Mnacho Echenim

This author has not been identified. Look up 'Mnacho Echenim' in Google

Mehdi Mhalla

This author has not been identified. Look up 'Mehdi Mhalla' in Google